Add is_expanding()

python/htps.cpp

@@ -3221,6 +3221,12 @@ static PyObject *PyHTPS_from_jsonstr(PyTypeObject *type, PyObject *args) {
     }
 }
 
+static PyObject *PyHTPS_is_expanding(PyHTPS *self, PyObject *Py_UNUSED(ignored)) {
+    PyObject *res = self->graph.is_expanding() ? Py_True : Py_False;
+    Py_INCREF(res);
+    return res;
+}
+
 static PyGetSetDef HTPS_getsetters[] = {
         {"expansions", (getter) PyHTPS_expansions, NULL, "Number of expansions", NULL},
         {NULL}
@@ -3232,6 +3238,7 @@ static PyMethodDef HTPS_methods[] = {
         {"proven",             (PyCFunction) PyHTPS_is_proven,          METH_NOARGS,  "Whether the start theorem is proven or not"},
         {"get_result",         (PyCFunction) PyHTPS_get_result,         METH_NOARGS,  "Returns the result of the HTPS run"},
         {"is_done",            (PyCFunction) PyHTPS_is_done,            METH_NOARGS,  "Whether the HTPS run is done or not"},
+        {"is_expanding",       (PyCFunction) PyHTPS_is_expanding,       METH_NOARGS,  "Whether the HTPS run is still awaiting EnvExpansions or not (in which case new theorems can be requested)"},
         {"get_json_str",       (PyCFunction) PyHTPS_get_jsonstr,        METH_NOARGS,  "Returns a JSON string representation of the HTPS object"},
         {"from_json_str",      (PyCFunction) PyHTPS_from_jsonstr,       METH_VARARGS |
                                                                         METH_CLASS, "Creates a HTPS object from a JSON string"},

src/graph/htps.cpp

@@ -1374,8 +1374,12 @@ void HTPS::expand_and_backup(std::vector<std::shared_ptr<env_expansion>> &expans
 //        HTPS_move();
 }
 
+bool HTPS::is_expanding() const {
+    return !currently_expanding.empty();
+}
+
 void HTPS::theorems_to_expand(std::vector<TheoremPointer> &theorems) {
-    if (!currently_expanding.empty()) {
+    if (is_expanding()) {
         throw std::runtime_error("Currently expanding is not empty, give results first!");
     }
     return batch_to_expand(theorems);

src/graph/htps.h

@@ -608,6 +608,8 @@ namespace htps {
 
         bool is_done() const;
 
+        bool is_expanding() const;
+
         Simulation find_leaves_to_expand(std::vector<TheoremPointer> &terminal, std::vector<std::pair<TheoremPointer, size_t>> &to_expand);
 
         void expand_and_backup(std::vector<std::shared_ptr<env_expansion>> &expansions);

tests/test_cpython.py

@@ -419,6 +419,7 @@ def test_htps_expansion():
     # Will find the root
     theorems = search.theorems_to_expand()
     assert len(theorems) == 1
+    assert search.is_expanding()
     _compare_theorem(theorems[0], theorem)
     assert theorems[0].metadata == {"key": "value"}
 
@@ -434,6 +435,7 @@ def test_htps_expansion():
     effects = [effect1, effect2]
     expansion = EnvExpansion(theorems[0], 100, 200, env_durations, effects, log_critic, expansion_tactics, children_for_tactic, priors)
     search.expand_and_backup([expansion])
+    assert not search.is_expanding()
 
     theorems = search.theorems_to_expand()
     assert len(theorems) == 1