From 7e3f909c8f882f890a64d4147524b88ddddfbe92 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Sun, 20 Apr 2025 11:49:38 +0100 Subject: [PATCH 1/2] add is_expanding boolean in cpp --- src/graph/htps.cpp | 6 +++++- src/graph/htps.h | 2 ++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/graph/htps.cpp b/src/graph/htps.cpp index 2c96c13..9440cd8 100644 --- a/src/graph/htps.cpp +++ b/src/graph/htps.cpp @@ -1374,8 +1374,12 @@ void HTPS::expand_and_backup(std::vector> &expans // HTPS_move(); } +bool HTPS::is_expanding() const { + return !currently_expanding.empty(); +} + void HTPS::theorems_to_expand(std::vector &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); diff --git a/src/graph/htps.h b/src/graph/htps.h index d908304..4a178a6 100644 --- a/src/graph/htps.h +++ b/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 &terminal, std::vector> &to_expand); void expand_and_backup(std::vector> &expansions); From 608a975b63595985828143e25888b3aec6f1f527 Mon Sep 17 00:00:00 2001 From: Simon Sorg Date: Sun, 20 Apr 2025 11:56:26 +0100 Subject: [PATCH 2/2] add is_expanding() to Python --- python/htps.cpp | 7 +++++++ tests/test_cpython.py | 2 ++ 2 files changed, 9 insertions(+) diff --git a/python/htps.cpp b/python/htps.cpp index 10b778d..d520078 100644 --- a/python/htps.cpp +++ b/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"}, diff --git a/tests/test_cpython.py b/tests/test_cpython.py index f4943b7..e218655 100644 --- a/tests/test_cpython.py +++ b/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