From 88a200cdd7575481ffdd92677f1ff78b6f38694e Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Wed, 23 Oct 2024 10:26:10 +0200 Subject: [PATCH 1/3] Update clasp. --- clasp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clasp b/clasp index bf2d3d05e..031323a79 160000 --- a/clasp +++ b/clasp @@ -1 +1 @@ -Subproject commit bf2d3d05ed4b420ab3a954f52cdc435060a0a544 +Subproject commit 031323a790f9af4e73b94ae1e29fe33fcce15b4b From 8c70fe3596f3872441f1b88d893e2bf365234159 Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Wed, 23 Oct 2024 11:22:30 +0200 Subject: [PATCH 2/3] Fix some typos and drop some dead test code. --- libclingo/clingo.h | 28 ++++++++++++++-------------- libclingo/tests/clingo.cc | 31 ------------------------------- libpyclingo/clingo/control.py | 10 +++++----- 3 files changed, 19 insertions(+), 50 deletions(-) diff --git a/libclingo/clingo.h b/libclingo/clingo.h index 23ccd76de..c3a08daa4 100644 --- a/libclingo/clingo.h +++ b/libclingo/clingo.h @@ -611,7 +611,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_is_fact(clingo_symbolic_ato //! //! @param[in] atoms the target //! @param[in] iterator iterator to the atom -//! @param[out] external whether the atom is a external +//! @param[out] external whether the atom is an external //! @return whether the call was successful CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_is_external(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, bool *external); //! Returns the (numeric) aspif literal corresponding to the given symbolic atom. @@ -910,14 +910,14 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_to_string(clingo_theory_ // {{{1 propagator //! @example propagator.c -//! The example shows how to write a simple propagator for the pigeon hole problem. For +//! The example shows how to write a simple propagator for the pigeonhole problem. For //! a detailed description of what is implemented here and some background, take a look at the following paper: //! //! https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/GebserKKOSW16x //! //! ## Output ## //! -//! The output is empty because the pigeon hole problem is unsatisfiable. +//! The output is empty because the pigeonhole problem is unsatisfiable. //! //! ## Code ## @@ -1026,7 +1026,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_at(clingo_assignment_t const *a //! Check if the assignment is total, i.e. there are no free literal. //! //! @param[in] assignment the target -//! @return wheather the assignment is total +//! @return whether the assignment is total CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total(clingo_assignment_t const *assignment); //! Returns the number of literals in the trail, i.e., the number of assigned literals. //! @@ -1050,7 +1050,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_size(clingo_assignment_t CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_begin(clingo_assignment_t const *assignment, uint32_t level, uint32_t *offset); //! Returns the offset following the last literal with the given decision level. //! -//! @note This function is the counter part to clingo_assignment_trail_begin(). +//! @note This function is the counterpart to clingo_assignment_trail_begin(). //! //! @param[in] assignment the target //! @param[in] level the decision level @@ -1464,7 +1464,7 @@ typedef struct clingo_propagator { //! //! @param[in] thread_id the solver's thread id //! @param[in] assignment the assignment of the solver - //! @param[in] fallback the literal choosen by the solver's heuristic + //! @param[in] fallback the literal chosen by the solver's heuristic //! @param[out] decision the literal to make true //! @return whether the call was successful bool (*decide) (clingo_id_t thread_id, clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, clingo_literal_t *decision); @@ -1475,7 +1475,7 @@ typedef struct clingo_propagator { // {{{1 backend //! @example backend.c -//! The example shows how to used the backend to extend a grounded program. +//! The example shows how to use the backend to extend a grounded program. //! //! ## Output ## //! @@ -1617,7 +1617,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_backend_external(clingo_backend_t *backend //! @return whether the call was successful; might set one of the following error codes: //! - ::clingo_error_bad_alloc CLINGO_VISIBILITY_DEFAULT bool clingo_backend_assume(clingo_backend_t *backend, clingo_literal_t const *literals, size_t size); -//! Add an heuristic directive. +//! Add a heuristic directive. //! //! @param[in] backend the target backend //! @param[in] atom the target atom @@ -1841,7 +1841,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_size(clingo_configuratio //! @note Multiple levels can be looked up by concatenating keys with a period. //! @param[in] configuration the target configuration //! @param[in] key the key -//! @param[in] name the name to lookup the subkey +//! @param[in] name the name to look up the subkey //! @param[out] result whether the key is in the map //! @return whether the call was successful CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_has_subkey(clingo_configuration_t const *configuration, clingo_id_t key, char const *name, bool *result); @@ -1860,7 +1860,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_subkey_name(clingo_confi //! @note Multiple levels can be looked up by concatenating keys with a period. //! @param[in] configuration the target configuration //! @param[in] key the key -//! @param[in] name the name to lookup the subkey +//! @param[in] name the name to look up the subkey //! @param[out] subkey the resulting subkey //! @return whether the call was successful CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_at(clingo_configuration_t const *configuration, clingo_id_t key, char const *name, clingo_id_t* subkey); @@ -1869,7 +1869,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_at(clingo_configuration_ //! @name Functions to access values //! @{ -//! Check whether a entry has a value. +//! Check whether an entry has a value. //! //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_value. //! @param[in] configuration the target configuration @@ -2042,7 +2042,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_subkey_name(clingo_statisti //! @note Multiple levels can be looked up by concatenating keys with a period. //! @param[in] statistics the target statistics //! @param[in] key the key -//! @param[in] name the name to lookup the subkey +//! @param[in] name the name to look up the subkey //! @param[out] subkey the resulting subkey //! @return whether the call was successful CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_at(clingo_statistics_t const *statistics, uint64_t key, char const *name, uint64_t *subkey); @@ -2862,7 +2862,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_control_solve(clingo_control_t *control, c //! //! This function removes atoms from domains that are false and marks atoms as //! facts that are true. With multi-shot solving, this can result in smaller -//! groundings because less rules have to be instantiated and more +//! groundings because fewer rules have to be instantiated and more //! simplifications can be applied. //! //! @note It is typically not necessary to call this function manually because @@ -3838,7 +3838,7 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_ast_unpool(clingo_ast_t *ast, clingo_ast_u //! @example application.c //! The example shows how to extend the clingo application. //! -//! It behaves like a normal normal clingo but adds one option to override the default program part to ground. +//! It behaves like a normal clingo but adds one option to override the default program part to ground. //! ## Example calls ## //! //! ~~~~~~~~~~~~ diff --git a/libclingo/tests/clingo.cc b/libclingo/tests/clingo.cc index 1d607d3ef..e6fb50fee 100644 --- a/libclingo/tests/clingo.cc +++ b/libclingo/tests/clingo.cc @@ -359,16 +359,6 @@ TEST_CASE("solving", "[clingo]") { REQUIRE(priorities == (std::vector{2, 1})); REQUIRE(messages.empty()); } -#if defined(CLASP_HAS_THREADS) && CLASP_HAS_THREADS == 1 - SECTION("async") { - ctl.add("base", {}, "{a}."); - ctl.ground({{"base", {}}}); - auto async = ctl.solve_async(MCB(models)); - REQUIRE(async.get().is_satisfiable()); - REQUIRE(models == ModelVec({{},{Id("a")}})); - REQUIRE(messages.empty()); - } -#endif SECTION("model") { ctl.add("base", {}, "a. #show b."); ctl.ground({{"base", {}}}); @@ -642,27 +632,6 @@ TEST_CASE("solving", "[clingo]") { REQUIRE(ctl.get_const("a") == Number(10)); REQUIRE(ctl.get_const("b") == Id("b")); } -#if defined(CLASP_HAS_THREADS) && CLASP_HAS_THREADS == 1 - SECTION("async and cancel") { - static int n = 0; - if (++n < 3) { // workaround for some bug with catch - ctl.add("pigeon", {"p", "h"}, "1 {p(P,H) : P=1..p}1 :- H=1..h." - "1 {p(P,H) : H=1..h}1 :- P=1..p."); - ctl.ground({{"pigeon", {Number(21), Number(20)}}}); - int fcalled = 0; - SolveResult fret; - FinishCallback fh = [&fret, &fcalled](SolveResult ret) { ++fcalled; fret = ret; }; - auto async = ctl.solve_async(nullptr, fh); - REQUIRE(!async.wait(0.01)); - SECTION("interrupt") { ctl.interrupt(); } - SECTION("cancel") { async.cancel(); } - auto ret = async.get(); - REQUIRE((ret.is_unknown() && ret.is_interrupted())); - REQUIRE(fcalled == 1); - REQUIRE(fret == ret); - } - } -#endif SECTION("ground callback") { ctl.add("base", {}, "a(@f(X)):- X=1..2. b(@f())."); ctl.ground({{"base", {}}}, [&messages](Location loc, char const *name, SymbolSpan args, SymbolSpanCallback report) { diff --git a/libpyclingo/clingo/control.py b/libpyclingo/clingo/control.py index e3d1782be..5a5f36688 100644 --- a/libpyclingo/clingo/control.py +++ b/libpyclingo/clingo/control.py @@ -509,10 +509,10 @@ def register_observer(self, observer: Observer, replace: bool = False) -> None: Parameters ---------- observer - The observer to register. See below for a description of the requirede + The observer to register. See below for a description of the required interface. replace - If set to true, the output is just passed to the observer and nolonger to + If set to true, the output is just passed to the observer and no longer to the underlying solver (or any previously registered observers). See Also @@ -767,7 +767,7 @@ def solve( on_model Optional callback for intercepting models. A `clingo.solving.Model` object is passed to the callback. The - search can be interruped from the model callback by returning + search can be interrupted from the model callback by returning False. on_unsat Optional callback to intercept lower bounds during optimization. @@ -777,7 +777,7 @@ def solve( on_finish Optional callback called once search has finished. A `clingo.solving.SolveResult` also indicating whether the solve - call has been intrrupted is passed to the callback. + call has been interrupted is passed to the callback. on_core Optional callback called with the assumptions that made a problem unsatisfiable. @@ -892,7 +892,7 @@ def enable_cleanup(self, value: bool) -> None: @property def enable_enumeration_assumption(self) -> bool: """ - Whether do discard or keep learnt information from enumeration modes. + Whether to discard or keep learnt information from enumeration modes. If the enumeration assumption is enabled, then all information learnt from clasp's various enumeration modes is removed after a solve call. This includes From 68e9664526197e753b78ac971f36bafc98d94472 Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Wed, 23 Oct 2024 15:53:56 +0200 Subject: [PATCH 3/3] Add support for getting last computed model. * Add clingo_solve_handle_last() for querying the last computed model after search has finished and make this function available to python code via Control.solve.SolveHandle. * Add new optional `on_last` callback to callback based python solve API for getting the last computed model. NOTE: The callback is only invoked for the solve overloads that return a SolveResult instead of a SolveHandle. --- app/pyclingo/_clingo.c | 56 +++++++++++++++++++++++- libclingo/clingo.h | 10 +++++ libclingo/clingo.hh | 7 +++ libclingo/clingo/clingocontrol.hh | 1 + libclingo/clingo/control.hh | 4 ++ libclingo/src/clingocontrol.cc | 8 ++++ libclingo/src/control.cc | 6 +++ libclingo/tests/clingo.cc | 15 ++++++- libpyclingo/_clingo.c | 56 +++++++++++++++++++++++- libpyclingo/clingo/control.py | 10 +++++ libpyclingo/clingo/solving.py | 14 ++++++ libpyclingo/clingo/tests/test_solving.py | 27 +++++++++--- libpyclingo/clingo/tests/util.py | 5 +++ 13 files changed, 208 insertions(+), 11 deletions(-) diff --git a/app/pyclingo/_clingo.c b/app/pyclingo/_clingo.c index 59f26b159..34c092ab0 100644 --- a/app/pyclingo/_clingo.c +++ b/app/pyclingo/_clingo.c @@ -14254,6 +14254,59 @@ _cffi_f_clingo_solve_handle_get(PyObject *self, PyObject *args) # define _cffi_f_clingo_solve_handle_get _cffi_d_clingo_solve_handle_get #endif +static _Bool _cffi_d_clingo_solve_handle_last(clingo_solve_handle_t * x0, clingo_model_t const * * x1) +{ + return clingo_solve_handle_last(x0, x1); +} +#ifndef PYPY_VERSION +static PyObject * +_cffi_f_clingo_solve_handle_last(PyObject *self, PyObject *args) +{ + clingo_solve_handle_t * x0; + clingo_model_t const * * x1; + Py_ssize_t datasize; + struct _cffi_freeme_s *large_args_free = NULL; + _Bool result; + PyObject *pyresult; + PyObject *arg0; + PyObject *arg1; + + if (!PyArg_UnpackTuple(args, "clingo_solve_handle_last", 2, 2, &arg0, &arg1)) + return NULL; + + datasize = _cffi_prepare_pointer_call_argument( + _cffi_type(778), arg0, (char **)&x0); + if (datasize != 0) { + x0 = ((size_t)datasize) <= 640 ? (clingo_solve_handle_t *)alloca((size_t)datasize) : NULL; + if (_cffi_convert_array_argument(_cffi_type(778), arg0, (char **)&x0, + datasize, &large_args_free) < 0) + return NULL; + } + + datasize = _cffi_prepare_pointer_call_argument( + _cffi_type(782), arg1, (char **)&x1); + if (datasize != 0) { + x1 = ((size_t)datasize) <= 640 ? (clingo_model_t const * *)alloca((size_t)datasize) : NULL; + if (_cffi_convert_array_argument(_cffi_type(782), arg1, (char **)&x1, + datasize, &large_args_free) < 0) + return NULL; + } + + Py_BEGIN_ALLOW_THREADS + _cffi_restore_errno(); + { result = clingo_solve_handle_last(x0, x1); } + _cffi_save_errno(); + Py_END_ALLOW_THREADS + + (void)self; /* unused */ + pyresult = _cffi_from_c__Bool(result); + if (large_args_free != NULL) _cffi_free_array_arguments(large_args_free); + return pyresult; +} +#else +# define _cffi_f_clingo_solve_handle_last _cffi_d_clingo_solve_handle_last +#endif + static _Bool _cffi_d_clingo_solve_handle_model(clingo_solve_handle_t * x0, clingo_model_t const * * x1) { return clingo_solve_handle_model(x0, x1); @@ -18566,6 +18619,7 @@ static const struct _cffi_global_s _cffi_globals[] = { { "clingo_solve_handle_close", (void *)_cffi_f_clingo_solve_handle_close, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_O, 777), (void *)_cffi_d_clingo_solve_handle_close }, { "clingo_solve_handle_core", (void *)_cffi_f_clingo_solve_handle_core, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 784), (void *)_cffi_d_clingo_solve_handle_core }, { "clingo_solve_handle_get", (void *)_cffi_f_clingo_solve_handle_get, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 789), (void *)_cffi_d_clingo_solve_handle_get }, + { "clingo_solve_handle_last", (void *)_cffi_f_clingo_solve_handle_last, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 780), (void *)_cffi_d_clingo_solve_handle_last }, { "clingo_solve_handle_model", (void *)_cffi_f_clingo_solve_handle_model, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 780), (void *)_cffi_d_clingo_solve_handle_model }, { "clingo_solve_handle_resume", (void *)_cffi_f_clingo_solve_handle_resume, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_O, 777), (void *)_cffi_d_clingo_solve_handle_resume }, { "clingo_solve_handle_wait", (void *)_cffi_f_clingo_solve_handle_wait, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 1186), (void *)_cffi_d_clingo_solve_handle_wait }, @@ -19108,7 +19162,7 @@ static const struct _cffi_type_context_s _cffi_type_context = { _cffi_struct_unions, _cffi_enums, _cffi_typenames, - 517, /* num_globals */ + 518, /* num_globals */ 26, /* num_struct_unions */ 33, /* num_enums */ 78, /* num_typenames */ diff --git a/libclingo/clingo.h b/libclingo/clingo.h index c3a08daa4..9d58ff913 100644 --- a/libclingo/clingo.h +++ b/libclingo/clingo.h @@ -2431,6 +2431,16 @@ CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_model(clingo_solve_handle_t * //! @return whether the call was successful; might set one of the following error codes: //! - ::clingo_error_bad_alloc CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core(clingo_solve_handle_t *handle, clingo_literal_t const **core, size_t *size); +//! When a problem is satisfiable and the search is finished, get the last computed model. +//! +//! If the program is unsatisfiable or the search is not finished, model is set to NULL. +//! +//! @param[in] handle the target +//! @param[out] model the last computed model (or NULL if the program is unsatisfiable or the search is still ongoing) +//! @return whether the call was successful; might set one of the following error codes: +//! - ::clingo_error_bad_alloc +//! - ::clingo_error_runtime if solving fails +CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_last(clingo_solve_handle_t *handle, clingo_model_t const **model); //! Discards the last model and starts the search for the next one. //! //! If the search has been started asynchronously, this function continues the search in the background. diff --git a/libclingo/clingo.hh b/libclingo/clingo.hh index 655206ed4..73b6314b8 100644 --- a/libclingo/clingo.hh +++ b/libclingo/clingo.hh @@ -1664,6 +1664,7 @@ public: Model const &next(); LiteralSpan core(); SolveResult get(); + Model const *last(); void cancel(); clingo_solve_handle_t *to_c() const { return iter_; } private: @@ -3088,6 +3089,12 @@ inline Model const &SolveHandle::model() { new (&model_) Model{const_cast(m)}; // NOLINT return model_; } + inline Model const *SolveHandle::last() { + clingo_model_t const *m = nullptr; + Detail::handle_error(clingo_solve_handle_last(iter_, &m), *exception_); + new (&model_) Model{const_cast(m)}; // NOLINT + return m ? &model_ : nullptr; +} inline LiteralSpan SolveHandle::core() { literal_t const *core = nullptr; diff --git a/libclingo/clingo/clingocontrol.hh b/libclingo/clingo/clingocontrol.hh index 6b13fe67e..9376e8ce5 100644 --- a/libclingo/clingo/clingocontrol.hh +++ b/libclingo/clingo/clingocontrol.hh @@ -447,6 +447,7 @@ public: SolveResult get() override; Model const *model() override; Potassco::LitSpan unsatCore() override; + Model const *lastModel() override; bool wait(double timeout) override; void resume() override; void cancel() override; diff --git a/libclingo/clingo/control.hh b/libclingo/clingo/control.hh index 859589933..ef5e242b3 100644 --- a/libclingo/clingo/control.hh +++ b/libclingo/clingo/control.hh @@ -137,6 +137,7 @@ struct SolveFuture { virtual SolveResult get() = 0; virtual Model const *model() = 0; virtual Potassco::LitSpan unsatCore() = 0; + virtual Model const *lastModel() = 0; virtual bool wait(double timeout) = 0; virtual void cancel() = 0; virtual void resume() = 0; @@ -151,6 +152,9 @@ struct DefaultSolveFuture : SolveFuture { Potassco::LitSpan unsatCore() override { throw std::runtime_error("no core available"); } + Model const *lastModel() override { + throw std::runtime_error("no model available"); + } bool wait(double) override { resume(); return true; } void cancel() override { resume(); } void resume() override { diff --git a/libclingo/src/clingocontrol.cc b/libclingo/src/clingocontrol.cc index 5679e4bfe..cc98c2c7c 100644 --- a/libclingo/src/clingocontrol.cc +++ b/libclingo/src/clingocontrol.cc @@ -865,6 +865,14 @@ Model const *ClingoSolveFuture::model() { } else { return nullptr; } } +Model const *ClingoSolveFuture::lastModel() { + auto &facade = *model_.context().clasp_; + if (!facade.solved() || !facade.summary().sat() || !facade.summary().model()) { + return nullptr; + } + model_.reset(*facade.summary().model()); + return &model_; +} Potassco::LitSpan ClingoSolveFuture::unsatCore() { auto &facade = *model_.context().clasp_; auto &summary = facade.summary(); diff --git a/libclingo/src/control.cc b/libclingo/src/control.cc index 46d3f1d9b..ab2b02b0c 100644 --- a/libclingo/src/control.cc +++ b/libclingo/src/control.cc @@ -1261,6 +1261,12 @@ extern "C" bool clingo_solve_handle_core(clingo_solve_handle_t *handle, clingo_l } GRINGO_CLINGO_CATCH; } +extern "C" bool clingo_solve_handle_last(clingo_solve_handle_t *handle, clingo_model_t const **model) { + GRINGO_CLINGO_TRY { + *model = handle->lastModel(); + } + GRINGO_CLINGO_CATCH; +} extern "C" bool clingo_solve_handle_resume(clingo_solve_handle_t *handle) { GRINGO_CLINGO_TRY { handle->resume(); } GRINGO_CLINGO_CATCH; diff --git a/libclingo/tests/clingo.cc b/libclingo/tests/clingo.cc index e6fb50fee..d0bfe0f88 100644 --- a/libclingo/tests/clingo.cc +++ b/libclingo/tests/clingo.cc @@ -554,11 +554,22 @@ TEST_CASE("solving", "[clingo]") { auto iter = ctl.solve(); { MCB mcb(models); - SECTION("c++") { for (auto &m : iter) { mcb(m); }; } - SECTION("java") { while (auto &m = iter.next()) { mcb(m); }; } + SECTION("c++") { for (auto &m : iter) { mcb(m); } } + SECTION("java") { + while (auto &m = iter.next()) { + mcb(m); + REQUIRE(iter.last() == nullptr); + } + } } REQUIRE(models == ModelVec{{Id("a")}}); REQUIRE(iter.get().is_satisfiable()); + const auto* m = iter.last(); + REQUIRE(m != nullptr); + models.clear(); + MCB mcb(models); + mcb(*m); + REQUIRE(models == ModelVec{{Id("a")}}); } REQUIRE(test_solve(ctl.solve(), models).is_satisfiable()); REQUIRE(models == ModelVec{{Id("a")}}); diff --git a/libpyclingo/_clingo.c b/libpyclingo/_clingo.c index 2d6e4cca0..2f019d3be 100644 --- a/libpyclingo/_clingo.c +++ b/libpyclingo/_clingo.c @@ -14991,6 +14991,59 @@ _cffi_f_clingo_solve_handle_get(PyObject *self, PyObject *args) # define _cffi_f_clingo_solve_handle_get _cffi_d_clingo_solve_handle_get #endif +static _Bool _cffi_d_clingo_solve_handle_last(clingo_solve_handle_t * x0, clingo_model_t const * * x1) +{ + return clingo_solve_handle_last(x0, x1); +} +#ifndef PYPY_VERSION +static PyObject * +_cffi_f_clingo_solve_handle_last(PyObject *self, PyObject *args) +{ + clingo_solve_handle_t * x0; + clingo_model_t const * * x1; + Py_ssize_t datasize; + struct _cffi_freeme_s *large_args_free = NULL; + _Bool result; + PyObject *pyresult; + PyObject *arg0; + PyObject *arg1; + + if (!PyArg_UnpackTuple(args, "clingo_solve_handle_last", 2, 2, &arg0, &arg1)) + return NULL; + + datasize = _cffi_prepare_pointer_call_argument( + _cffi_type(778), arg0, (char **)&x0); + if (datasize != 0) { + x0 = ((size_t)datasize) <= 640 ? (clingo_solve_handle_t *)alloca((size_t)datasize) : NULL; + if (_cffi_convert_array_argument(_cffi_type(778), arg0, (char **)&x0, + datasize, &large_args_free) < 0) + return NULL; + } + + datasize = _cffi_prepare_pointer_call_argument( + _cffi_type(782), arg1, (char **)&x1); + if (datasize != 0) { + x1 = ((size_t)datasize) <= 640 ? (clingo_model_t const * *)alloca((size_t)datasize) : NULL; + if (_cffi_convert_array_argument(_cffi_type(782), arg1, (char **)&x1, + datasize, &large_args_free) < 0) + return NULL; + } + + Py_BEGIN_ALLOW_THREADS + _cffi_restore_errno(); + { result = clingo_solve_handle_last(x0, x1); } + _cffi_save_errno(); + Py_END_ALLOW_THREADS + + (void)self; /* unused */ + pyresult = _cffi_from_c__Bool(result); + if (large_args_free != NULL) _cffi_free_array_arguments(large_args_free); + return pyresult; +} +#else +# define _cffi_f_clingo_solve_handle_last _cffi_d_clingo_solve_handle_last +#endif + static _Bool _cffi_d_clingo_solve_handle_model(clingo_solve_handle_t * x0, clingo_model_t const * * x1) { return clingo_solve_handle_model(x0, x1); @@ -19303,6 +19356,7 @@ static const struct _cffi_global_s _cffi_globals[] = { { "clingo_solve_handle_close", (void *)_cffi_f_clingo_solve_handle_close, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_O, 777), (void *)_cffi_d_clingo_solve_handle_close }, { "clingo_solve_handle_core", (void *)_cffi_f_clingo_solve_handle_core, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 784), (void *)_cffi_d_clingo_solve_handle_core }, { "clingo_solve_handle_get", (void *)_cffi_f_clingo_solve_handle_get, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 789), (void *)_cffi_d_clingo_solve_handle_get }, + { "clingo_solve_handle_last", (void *)_cffi_f_clingo_solve_handle_last, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 780), (void *)_cffi_d_clingo_solve_handle_last }, { "clingo_solve_handle_model", (void *)_cffi_f_clingo_solve_handle_model, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 780), (void *)_cffi_d_clingo_solve_handle_model }, { "clingo_solve_handle_resume", (void *)_cffi_f_clingo_solve_handle_resume, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_O, 777), (void *)_cffi_d_clingo_solve_handle_resume }, { "clingo_solve_handle_wait", (void *)_cffi_f_clingo_solve_handle_wait, _CFFI_OP(_CFFI_OP_CPYTHON_BLTN_V, 1186), (void *)_cffi_d_clingo_solve_handle_wait }, @@ -19845,7 +19899,7 @@ static const struct _cffi_type_context_s _cffi_type_context = { _cffi_struct_unions, _cffi_enums, _cffi_typenames, - 517, /* num_globals */ + 518, /* num_globals */ 26, /* num_struct_unions */ 33, /* num_enums */ 78, /* num_typenames */ diff --git a/libpyclingo/clingo/control.py b/libpyclingo/clingo/control.py index 5a5f36688..adb8c3cb4 100644 --- a/libpyclingo/clingo/control.py +++ b/libpyclingo/clingo/control.py @@ -688,6 +688,7 @@ def solve( on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None, on_finish: Optional[Callable[[SolveResult], None]] = None, on_core: Optional[Callable[[Sequence[int]], None]] = None, + on_last: Optional[Callable[[Model], None]] = None, *, yield_: Literal[False] = False, async_: Literal[False] = False, @@ -728,6 +729,7 @@ def solve( on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None, on_finish: Optional[Callable[[SolveResult], None]] = None, on_core: Optional[Callable[[Sequence[int]], None]] = None, + on_last: Optional[Callable[[Model], None]] = None, ) -> SolveResult: ... @overload @@ -739,6 +741,7 @@ def solve( on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None, on_finish: Optional[Callable[[SolveResult], None]] = None, on_core: Optional[Callable[[Sequence[int]], None]] = None, + on_last: Optional[Callable[[Model], None]] = None, yield_: bool = False, async_: bool = False, ) -> Union[SolveHandle, SolveResult]: ... @@ -751,6 +754,7 @@ def solve( on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None, on_finish: Optional[Callable[[SolveResult], None]] = None, on_core: Optional[Callable[[Sequence[int]], None]] = None, + on_last: Optional[Callable[[Model], None]] = None, yield_: bool = False, async_: bool = False, ) -> Union[SolveHandle, SolveResult]: @@ -781,6 +785,9 @@ def solve( on_core Optional callback called with the assumptions that made a problem unsatisfiable. + on_last + Optional callback for getting the last model computed for a satisfiable problem. + A `clingo.solving.Model` object is passed to the callback. yield_ The resulting `clingo.solving.SolveHandle` is iterable yielding `clingo.solving.Model` objects. @@ -864,6 +871,9 @@ def solve( ret = handle.get() if on_core is not None and ret.unsatisfiable: on_core(handle.core()) + if on_last is not None: + m = handle.last() + if m is not None: on_last(m) return ret return handle diff --git a/libpyclingo/clingo/solving.py b/libpyclingo/clingo/solving.py index 341690f0c..ad1b4b33d 100644 --- a/libpyclingo/clingo/solving.py +++ b/libpyclingo/clingo/solving.py @@ -559,6 +559,20 @@ def core(self) -> List[int]: ) return [core[i] for i in range(size)] + def last(self) -> Optional[Model]: + """ + The last computed model if there is any. + + Notes + ----- + If the search is not completed yet or the problem is unsatisfiable, the function returns None. + """ + p_model = _ffi.new("clingo_model_t**") + _handle_error(_lib.clingo_solve_handle_last(self._rep, p_model), self._handler) + if p_model[0] == _ffi.NULL: + return None + return Model(p_model[0]) + def get(self) -> SolveResult: """ Get the result of a solve call. diff --git a/libpyclingo/clingo/tests/test_solving.py b/libpyclingo/clingo/tests/test_solving.py index bbdf3e4d7..0785fdeac 100644 --- a/libpyclingo/clingo/tests/test_solving.py +++ b/libpyclingo/clingo/tests/test_solving.py @@ -60,11 +60,12 @@ def test_solve_cb(self): self, cast( SolveResult, - self.ctl.solve(on_model=self.mcb.on_model, yield_=False, async_=False), + self.ctl.solve(on_model=self.mcb.on_model, on_last=self.mcb.on_last, yield_=False, async_=False), ), ) self.assertEqual(self.mcb.models, _p(["a", "c"], ["b", "c"])) self.assertEqual(self.mcb.last[0], ModelType.StableModel) + self.assertEqual(self.mcb.last, self.mcb.final) def test_solve_async(self): """ @@ -78,6 +79,8 @@ def test_solve_async(self): ) as hnd: _check_sat(self, hnd.get()) self.assertEqual(self.mcb.models, _p(["a", "c"], ["b", "c"])) + self.mit.on_last(hnd.last()) + self.assertEqual(self.mcb.last, self.mit.final) def test_solve_yield(self): """ @@ -91,7 +94,10 @@ def test_solve_yield(self): ) as hnd: for m in hnd: self.mit.on_model(m) + self.assertEqual(hnd.last(), None) # Not yet finished _check_sat(self, hnd.get()) + self.mit.on_last(hnd.last()) + self.assertEqual(self.mcb.last, self.mit.final) self.assertEqual(self.mcb.models, _p(["a", "c"], ["b", "c"])) self.assertEqual(self.mit.models, _p(["a", "c"], ["b", "c"])) @@ -112,7 +118,10 @@ def test_solve_async_yield(self): if m is None: break self.mit.on_model(m) + self.assertEqual(hnd.last(), None) # Not yet finished _check_sat(self, hnd.get()) + self.mit.on_last(hnd.last()) + self.assertEqual(self.mcb.last, self.mit.final) self.assertEqual(self.mcb.models, _p(["a", "c"], ["b", "c"])) self.assertEqual(self.mit.models, _p(["a", "c"], ["b", "c"])) @@ -160,23 +169,26 @@ def test_enum(self): self.ctl = Control(["0", "-e", "cautious"]) self.ctl.add("base", [], "1 {a; b} 1. c.") self.ctl.ground([("base", [])]) - self.ctl.solve(on_model=self.mcb.on_model) + self.ctl.solve(on_model=self.mcb.on_model, on_last=self.mcb.on_last) self.assertEqual(self.mcb.last[0], ModelType.CautiousConsequences) self.assertEqual([self.mcb.last[1]], _p(["c"])) + self.assertEqual(self.mcb.last, self.mcb.final) + self.mcb.final = None self.ctl = Control(["0", "-e", "brave"]) self.ctl.add("base", [], "1 {a; b} 1. c.") self.ctl.ground([("base", [])]) - self.ctl.solve(on_model=self.mcb.on_model) + self.ctl.solve(on_model=self.mcb.on_model, on_last=self.mcb.on_last) self.assertEqual(self.mcb.last[0], ModelType.BraveConsequences) self.assertEqual([self.mcb.last[1]], _p(["a", "b", "c"])) + self.assertEqual(self.mcb.last, self.mcb.final) def test_model(self): """ Test functions of model. """ - def on_model(m: Model): + def on_model(m: Model, last: bool): self.assertTrue(m.contains(Function("a"))) self.assertTrue( m.is_true( @@ -186,15 +198,16 @@ def on_model(m: Model): self.assertFalse(m.is_true(1000)) self.assertEqual(m.thread_id, 0) self.assertEqual(m.number, 1) - self.assertFalse(m.optimality_proven) + self.assertEqual(m.optimality_proven, last) self.assertEqual(m.cost, [3]) self.assertEqual(m.priority, [5]) - m.extend([Function("e")]) + if not last: + m.extend([Function("e")]) self.assertSequenceEqual(m.symbols(theory=True), [Function("e")]) self.ctl.add("base", [], "a. b. c. #minimize { 1@5,a:a; 1@5,b:b; 1@5,c:c }.") self.ctl.ground([("base", [])]) - self.ctl.solve(on_model=on_model) + self.ctl.solve(on_model=lambda m:on_model(m, False), on_last=lambda m:on_model(m, True)) def test_cautious_consequences(self): """ diff --git a/libpyclingo/clingo/tests/util.py b/libpyclingo/clingo/tests/util.py index e36105935..f75d6165f 100644 --- a/libpyclingo/clingo/tests/util.py +++ b/libpyclingo/clingo/tests/util.py @@ -20,6 +20,7 @@ def __init__(self): self._models = [] self._core = None self.last = None + self.final = None def on_core(self, c): self._core = c @@ -28,6 +29,10 @@ def on_model(self, m): self.last = (m.type, sorted(m.symbols(shown=True))) self._models.append(self.last[1]) + def on_last(self, m): + assert self.final is None + self.final = (m.type, sorted(m.symbols(shown=True))) + @property def core(self): return sorted(self._core)