Merge pull request #523 from potassco/last-model

Add support for getting last computed model.

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 */

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);
@@ -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.
@@ -2862,7 +2872,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 +3848,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 ##
 //!
 //! ~~~~~~~~~~~~

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<clingo_model_t*>(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<clingo_model_t*>(m)}; // NOLINT
+    return m ? &model_ : nullptr;
+}
 
 inline LiteralSpan SolveHandle::core() {
     literal_t const *core = nullptr;

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;

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 {

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();

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;

libclingo/tests/clingo.cc

@@ -359,16 +359,6 @@ TEST_CASE("solving", "[clingo]") {
             REQUIRE(priorities == (std::vector<int>{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", {}}});
@@ -564,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")}});
@@ -642,27 +643,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) {