From 732231d316aac26f2759555291f2aa527f32c7b4 Mon Sep 17 00:00:00 2001 From: Roland Kaminski Date: Fri, 6 Dec 2019 14:31:44 +0100 Subject: [PATCH] restore old add_clause semantics This commit restores the previously implemented add clause semantics. Furthemore, it adds a propagate method to the PropagateInit class. --- app/clingo/tests/lua/add-clause-lua.lp | 16 ++++ app/clingo/tests/python/add-clause-py.lp | 15 ++++ libclingo/clingo.h | 18 ++++- libclingo/clingo.hh | 7 ++ libclingo/clingo/control.hh | 3 +- libclingo/src/clingocontrol.cc | 45 +++++------ libclingo/src/control.cc | 9 ++- libclingo/tests/propagator.cc | 95 ++++++++++++++++++++++++ libluaclingo/luaclingo.cc | 7 ++ libpyclingo/pyclingo.cc | 34 ++++++++- 10 files changed, 213 insertions(+), 36 deletions(-) diff --git a/app/clingo/tests/lua/add-clause-lua.lp b/app/clingo/tests/lua/add-clause-lua.lp index af7b8a404..ba9c599fc 100644 --- a/app/clingo/tests/lua/add-clause-lua.lp +++ b/app/clingo/tests/lua/add-clause-lua.lp @@ -19,24 +19,40 @@ function Propagator:init(init) if self.step == 0 then l = init:add_literal() init:add_clause({-b, l}) + init:propagate() init:add_clause({-l, b}) + init:propagate() init:add_clause({-c, l}) + init:propagate() init:add_clause({-l, c}) + init:propagate() init:add_clause({-a, -b}) + init:propagate() init:add_clause({-a, b}) + init:propagate() init:add_clause({-a, -a, -b}) + init:propagate() init:add_clause({-a, a}) + init:propagate() end if self.step == 1 then init:add_clause({b}) + init:propagate() init:add_clause({b}) + init:propagate() end if self.step == 2 then init:add_clause({}) + init:propagate() init:add_clause({a}) + init:propagate() init:add_clause({b}) + init:propagate() + init:propagate() init:add_clause({-a}) + init:propagate() init:add_clause({-b}) + init:propagate() end self.step = self.step + 1 end diff --git a/app/clingo/tests/python/add-clause-py.lp b/app/clingo/tests/python/add-clause-py.lp index d34a202f5..618730660 100644 --- a/app/clingo/tests/python/add-clause-py.lp +++ b/app/clingo/tests/python/add-clause-py.lp @@ -13,22 +13,37 @@ class Propagator: if self.step == 0: l = init.add_literal() init.add_clause([-b, l]) + init.propagate() init.add_clause([-l, b]) + init.propagate() init.add_clause([-c, l]) + init.propagate() init.add_clause([-l, c]) + init.propagate() init.add_clause([-a, -b]) + init.propagate() init.add_clause([-a, b]) + init.propagate() init.add_clause([-a, -a, -b]) + init.propagate() init.add_clause([-a, a]) + init.propagate() if self.step == 1: init.add_clause([b]) + init.propagate() init.add_clause([b]) + init.propagate() if self.step == 2: init.add_clause([]) + init.propagate() init.add_clause([a]) + init.propagate() init.add_clause([b]) + init.propagate() init.add_clause([-a]) + init.propagate() init.add_clause([-b]) + init.propagate() self.step += 1 def main(prg): diff --git a/libclingo/clingo.h b/libclingo/clingo.h index 554aed758..8b95ccb00 100644 --- a/libclingo/clingo.h +++ b/libclingo/clingo.h @@ -1088,6 +1088,9 @@ CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_g CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_init_assignment(clingo_propagate_init_t const *init); //! Add a literal to the solver. //! +//! @attention If varibales were added, subsequent calls to ::clingo_propagate_init_add_clause() and ::clingo_propagate_init_propagate() are expensive. +//! It is best to add varables in batches. +//! //! @param[in] init the target //! @param[out] result the added literal //! @return whether the call was successful; might set one of the following error codes: @@ -1095,16 +1098,25 @@ CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_init_assig CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, clingo_literal_t *result); //! Add the given clause to the solver. //! -//! @note The result is always set to true and might be removed in a future version of the API. -//! +//! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false. //! //! @param[in] init the target //! @param[in] clause the clause to add //! @param[in] size the size of the clause -//! @param[out] result always true +//! @param[out] result result indicating whether whether the problem became unsatisfiable //! @return whether the call was successful; might set one of the following error codes: //! - ::clingo_error_bad_alloc CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_clause(clingo_propagate_init_t *init, clingo_literal_t const *clause, size_t size, bool *result); +//! Propagates consequences of the underlying problem excluding registered propagators. +//! +//! @note The function has no effect if SAT-preprocessing is enabled. +//! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false. +//! +//! @param[in] init the target +//! @param[out] result result indicating whether whether the problem became unsatisfiable +//! @return whether the call was successful; might set one of the following error codes: +//! - ::clingo_error_bad_alloc +CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_propagate(clingo_propagate_init_t *init, bool *result); //! @} diff --git a/libclingo/clingo.hh b/libclingo/clingo.hh index 25e9e456e..dd2ed5c21 100644 --- a/libclingo/clingo.hh +++ b/libclingo/clingo.hh @@ -836,6 +836,7 @@ public: void set_check_mode(PropagatorCheckMode mode); literal_t add_literal(); bool add_clause(LiteralSpan clause); + bool propagate(); clingo_propagate_init_t *to_c() const { return init_; } private: clingo_propagate_init_t *init_; @@ -2762,6 +2763,12 @@ inline bool PropagateInit::add_clause(LiteralSpan clause) { return ret; } +inline bool PropagateInit::propagate() { + bool ret; + Detail::handle_error(clingo_propagate_init_propagate(init_, &ret)); + return ret; +} + // {{{2 propagate control inline id_t PropagateControl::thread_id() const { diff --git a/libclingo/clingo/control.hh b/libclingo/clingo/control.hh index afb7dcc4a..b62d442d8 100644 --- a/libclingo/clingo/control.hh +++ b/libclingo/clingo/control.hh @@ -181,7 +181,8 @@ using PropagateInit = clingo_propagate_init; struct clingo_propagate_init { virtual Potassco::Lit_t addLiteral() = 0; - virtual void addClause(Potassco::LitSpan lits) = 0; + virtual bool addClause(Potassco::LitSpan lits) = 0; + virtual bool propagate() = 0; virtual Gringo::Output::DomainData const &theory() const = 0; virtual Gringo::SymbolicAtoms const &getDomain() const = 0; virtual Gringo::Lit_t mapLit(Gringo::Lit_t lit) const = 0; diff --git a/libclingo/src/clingocontrol.cc b/libclingo/src/clingocontrol.cc index 89ef26bde..be55f5be3 100644 --- a/libclingo/src/clingocontrol.cc +++ b/libclingo/src/clingocontrol.cc @@ -377,8 +377,8 @@ namespace { class ClingoPropagateInit : public PropagateInit { public: using Lit_t = Potassco::Lit_t; - ClingoPropagateInit(Control &c, Clasp::ClingoPropagatorInit &p, size_t &literals, Potassco::LitVec &clauses) - : c_{c}, p_{p}, a_{*facade_().ctx.solver(0)}, literals_{literals}, clauses_{clauses} { + ClingoPropagateInit(Control &c, Clasp::ClingoPropagatorInit &p, size_t &literals) + : c_{c}, p_{p}, a_{*facade_().ctx.solver(0)}, literals_{literals} { p_.enableHistory(false); } Output::DomainData const &theory() const override { return c_.theory(); } @@ -395,9 +395,20 @@ class ClingoPropagateInit : public PropagateInit { ++literals_; return Clasp::encodeLit(Clasp::Literal(facade_().ctx.addVar(Clasp::Var_t::Atom), false)); } - void addClause(Potassco::LitSpan lits) override { - for (auto &lit : lits) { clauses_.push_back(lit); } - clauses_.push_back(0); + bool addClause(Potassco::LitSpan lits) override { + auto &ctx = static_cast(c_.claspFacade())->ctx; + if (ctx.master()->hasConflict()) { return false; } + Clasp::ClauseCreator cc{ctx.master()}; + cc.start(); + for (auto &lit : lits) { + cc.add(Clasp::decodeLit(lit)); + } + return cc.end(Clasp::ClauseCreator::clause_force_simplify).ok(); + } + bool propagate() override { + auto &ctx = static_cast(c_.claspFacade())->ctx; + if (ctx.master()->hasConflict()) { return false; } + return ctx.master()->propagate(); } void setCheckMode(clingo_propagator_check_mode_t checkMode) override { p_.enableClingoPropagatorCheck(static_cast(checkMode)); @@ -411,7 +422,6 @@ class ClingoPropagateInit : public PropagateInit { Clasp::ClingoPropagatorInit &p_; Clasp::ClingoAssignment a_; size_t &literals_; - Potassco::LitVec &clauses_; }; } // namespace @@ -426,33 +436,12 @@ void ClingoControl::prepare(Assumptions ass) { postGround(*prg); if (!propagators_.empty()) { size_t literals{0}; - Potassco::LitVec clauses; clasp_->program()->endProgram(); for (auto&& pp : propagators_) { - ClingoPropagateInit i(*this, *pp, literals, clauses); + ClingoPropagateInit i(*this, *pp, literals); static_cast(pp->propagator())->init(i); } propLock_.init(clasp_->ctx.concurrency()); - auto &master = literals > 0 - ? clasp_->ctx.startAddConstraints(clauses.size()) - : *clasp_->ctx.master(); - if (!master.hasConflict() && !clauses.empty()) { - Clasp::ClauseCreator cc{&master}; - bool started = false; - for (auto &lit : clauses) { - if (!started) { - cc.start(); - started = true; - } - if (lit != 0) { cc.add(Clasp::decodeLit(lit)); } - else { - if (!cc.end(Clasp::ClauseCreator::clause_force_simplify).ok()) { - break; - } - started = false; - } - } - } } prePrepare(*clasp_); clasp_->prepare(enableEnumAssupmption_ ? Clasp::ClaspFacade::enum_volatile : Clasp::ClaspFacade::enum_static); diff --git a/libclingo/src/control.cc b/libclingo/src/control.cc index 98a15e8d2..dd4eebb66 100644 --- a/libclingo/src/control.cc +++ b/libclingo/src/control.cc @@ -668,9 +668,12 @@ extern "C" bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, } extern "C" bool clingo_propagate_init_add_clause(clingo_propagate_init_t *init, clingo_literal_t const *literals, size_t size, bool *ret) { - GRINGO_CLINGO_TRY { - if (ret) { *ret = true; } - init->addClause(Potassco::LitSpan{literals, size}); } + GRINGO_CLINGO_TRY { *ret = init->addClause(Potassco::LitSpan{literals, size}); } + GRINGO_CLINGO_CATCH; +} + +extern "C" bool clingo_propagate_init_propagate(clingo_propagate_init_t *init, bool *ret) { + GRINGO_CLINGO_TRY { *ret = init->propagate(); } GRINGO_CLINGO_CATCH; } diff --git a/libclingo/tests/propagator.cc b/libclingo/tests/propagator.cc index da95971db..b51d24785 100644 --- a/libclingo/tests/propagator.cc +++ b/libclingo/tests/propagator.cc @@ -432,6 +432,27 @@ class TestAssignment : public Propagator { size_t count_ = 0; }; +literal_t get_literal(PropagateInit &init, char const *name) { + return init.solver_literal(init.symbolic_atoms().find(Id(name))->literal()); +} + +template +class TestInit : public Propagator { +public: + TestInit(T &&f) : f_{std::forward(f)} { } + void init(PropagateInit &init) override { + f_(init); + } +private: + T f_; +}; + +template +static TestInit make_init(T &&f) { + return {std::forward(f)}; +} + + class TestAddClause : public Propagator { public: void init(PropagateInit &init) override { @@ -659,6 +680,80 @@ TEST_CASE("propagator", "[clingo][propagator]") { REQUIRE(models.size() == 4); } } + SECTION("add_clause_init") { + // NOTE: the tests would fail if sat preprocessing is activated + ctl.configuration()["sat_prepro"] = "0"; + + ctl.add("base", {}, "{a; b}. c. :- a, b."); + ctl.ground({{"base", {}}}, nullptr); + SECTION("conflict") { + auto p{make_init([](Clingo::PropagateInit &init){ + REQUIRE_FALSE(init.add_clause({-get_literal(init, "c")})); + })}; + ctl.register_propagator(p, false); + test_solve(ctl.solve(), models); + REQUIRE(models.size() == 0); + } + SECTION("propagate") { + auto p{make_init([](Clingo::PropagateInit &init){ + REQUIRE(init.add_clause({get_literal(init, "a")})); + REQUIRE(init.assignment().is_true(get_literal(init, "a"))); + REQUIRE(init.propagate()); + REQUIRE(init.assignment().is_false(get_literal(init, "b"))); + })}; + ctl.register_propagator(p, false); + test_solve(ctl.solve(), models); + REQUIRE(models.size() == 1); + } + SECTION("propagate") { + auto p{make_init([](Clingo::PropagateInit &init){ + auto ass = init.assignment(); + auto lit = init.add_literal(); + auto a = get_literal(init, "a"); + REQUIRE(init.add_clause({lit})); + REQUIRE(ass.is_true(lit)); + REQUIRE(init.add_clause({-lit, a})); + REQUIRE(ass.is_true(a)); + REQUIRE(init.propagate()); + REQUIRE(init.assignment().is_false(get_literal(init, "b"))); + })}; + ctl.register_propagator(p, false); + test_solve(ctl.solve(), models); + REQUIRE(models.size() == 1); + } + SECTION("propagate") { + auto p{make_init([](Clingo::PropagateInit &init){ + auto ass = init.assignment(); + auto lit = init.add_literal(); + auto a = get_literal(init, "a"); + REQUIRE(init.add_clause({-lit, a})); + REQUIRE(init.add_clause({lit})); + REQUIRE(ass.is_true(lit)); + REQUIRE(init.propagate()); + REQUIRE(ass.is_true(a)); + REQUIRE(init.assignment().is_false(get_literal(init, "b"))); + })}; + ctl.register_propagator(p, false); + test_solve(ctl.solve(), models); + REQUIRE(models.size() == 1); + } + SECTION("propagate") { + auto p{make_init([](Clingo::PropagateInit &init){ + auto ass = init.assignment(); + auto lit = init.add_literal(); + auto a = get_literal(init, "a"); + auto b = get_literal(init, "b"); + REQUIRE(init.add_clause({lit})); + REQUIRE(ass.is_true(lit)); + REQUIRE(init.add_clause({-lit, a})); + REQUIRE(init.add_clause({-lit, b})); + REQUIRE_FALSE(init.propagate()); + })}; + ctl.register_propagator(p, false); + test_solve(ctl.solve(), models); + REQUIRE(models.size() == 0); + } + } } TEST_CASE("propgator-sequence-mining", "[clingo][propagator]") { diff --git a/libluaclingo/luaclingo.cc b/libluaclingo/luaclingo.cc index bb397cff9..eded5e5be 100644 --- a/libluaclingo/luaclingo.cc +++ b/libluaclingo/luaclingo.cc @@ -2390,6 +2390,12 @@ struct PropagateInit : Object { return 1; } + static int propagate(lua_State *L) { + auto &self = get_self(L); + lua_pushboolean(L, call_c(L, clingo_propagate_init_propagate, self.init)); + return 1; + } + static int getCheckMode(lua_State *L) { PropagatorCheckMode::new_(L, static_cast(clingo_propagate_init_get_check_mode(get_self(L).init))); return 1; @@ -2451,6 +2457,7 @@ luaL_Reg const PropagateInit::meta[] = { {"add_watch", addWatch}, {"add_literal", addLiteral}, {"add_clause", addClause}, + {"propagate", propagate}, {"set_state", setState}, {nullptr, nullptr} }; diff --git a/libpyclingo/pyclingo.cc b/libpyclingo/pyclingo.cc index ba0f353f4..aa53205c9 100644 --- a/libpyclingo/pyclingo.cc +++ b/libpyclingo/pyclingo.cc @@ -3533,6 +3533,12 @@ Control.register_propagator return cppToPy(ret); } + Object propagate() { + bool ret; + handle_c_error(clingo_propagate_init_propagate(init, &ret)); + return cppToPy(ret); + } + Object getCheckMode() { return PropagatorCheckMode::getAttr(clingo_propagate_init_get_check_mode(init)); } @@ -3585,6 +3591,11 @@ Returns ------- int Returns the added literal. + +Notes +----- +If literals are added to the solver, subsequent calls to `add_clause` and +`propagate` are expensive. It is best to add literals in batches. )"}, {"add_clause", to_function<&PropagateInit::addClause>(), METH_KEYWORDS | METH_VARARGS, R"(add_clause(self, clause: List[int]) -> bool @@ -3598,7 +3609,28 @@ clause : List[int] Returns ------- bool - The return value is always true and should be ignored. + Returns false if the program becomes unsatisfiable. + +Notes +----- +If this function returns false, initialization should be stopped and no further +functions of the `PropagateInit` and related objects should be called. +)"}, + {"propagate", to_function<&PropagateInit::propagate>(), METH_NOARGS, R"(propagate(self) -> bool + +Propagates consequences of the underlying problem excluding registered propagators. + +Returns +------- +bool + Returns false if the program becomes unsatisfiable. + +Notes +----- +This function has no effect if SAT-preprocessing is enabled. + +If this function returns false, initialization should be stopped and no further +functions of the `PropagateInit` and related objects should be called. )"}, {nullptr, nullptr, 0, nullptr} };