refine interface to initialize propagators

- There is a new method to add literals while initializing the propagator. - Clauses are now added after propagator initialization. This also means that the Boolean return value of add_clause can now be ignored.
potassco · Sep 8, 2019 · 45327d5 · 45327d5
1 parent e572887
commit 45327d5
Show file tree

Hide file tree

Showing 12 changed files with 159 additions and 89 deletions.
diff --git a/app/clingo/tests/lua/add-clause-lua.lp b/app/clingo/tests/lua/add-clause-lua.lp
@@ -15,22 +15,28 @@ end
 function Propagator:init(init)
  local a = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("a")).literal)
  local b = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("b")).literal)
+ local c = init:solver_literal(init.symbolic_atoms:lookup(clingo.Function("c")).literal)
  if self.step == 0 then
- assert(init:add_clause({-a, -b}))
- assert(init:add_clause({-a, b}))
- assert(init:add_clause({-a, -a, -b}))
- assert(init:add_clause({-a, a}))
+ l = init:add_literal()
+ init:add_clause({-b, l})
+ init:add_clause({-l, b})
+ init:add_clause({-c, l})
+ init:add_clause({-l, c})
+ init:add_clause({-a, -b})
+ init:add_clause({-a, b})
+ init:add_clause({-a, -a, -b})
+ init:add_clause({-a, a})
  end
  if self.step == 1 then
- assert(init:add_clause({b}))
- assert(init:add_clause({b}))
+ init:add_clause({b})
+ init:add_clause({b})
  end
  if self.step == 2 then
- assert(not init:add_clause({}))
- assert(not init:add_clause({a}))
- assert(not init:add_clause({b}))
- assert(not init:add_clause({-a}))
- assert(not init:add_clause({-b}))
+ init:add_clause({})
+ init:add_clause({a})
+ init:add_clause({b})
+ init:add_clause({-a})
+ init:add_clause({-b})
  end
  self.step = self.step + 1
 end
@@ -46,4 +52,4 @@ end
 
 #end.
 
-{ a; b }.
+{ a; b; c }.
diff --git a/app/clingo/tests/lua/add-clause-lua.sol b/app/clingo/tests/lua/add-clause-lua.sol
@@ -1,7 +1,7 @@
 Step: 1
 
-b
+b c
 Step: 2
-b
+b c
 Step: 3
 UNSAT
diff --git a/app/clingo/tests/python/add-clause-py.lp b/app/clingo/tests/python/add-clause-py.lp
@@ -9,20 +9,26 @@ class Propagator:
  def init(self, init):
  a = init.solver_literal(init.symbolic_atoms[clingo.Function("a")].literal)
  b = init.solver_literal(init.symbolic_atoms[clingo.Function("b")].literal)
+ c = init.solver_literal(init.symbolic_atoms[clingo.Function("c")].literal)
  if self.step == 0:
- assert(init.add_clause([-a, -b]))
- assert(init.add_clause([-a, b]))
- assert(init.add_clause([-a, -a, -b]))
- assert(init.add_clause([-a, a]))
+ l = init.add_literal()
+ init.add_clause([-b, l])
+ init.add_clause([-l, b])
+ init.add_clause([-c, l])
+ init.add_clause([-l, c])
+ init.add_clause([-a, -b])
+ init.add_clause([-a, b])
+ init.add_clause([-a, -a, -b])
+ init.add_clause([-a, a])
  if self.step == 1:
- assert(init.add_clause([b]))
- assert(init.add_clause([b]))
+ init.add_clause([b])
+ init.add_clause([b])
  if self.step == 2:
- assert(not init.add_clause([]))
- assert(not init.add_clause([a]))
- assert(not init.add_clause([b]))
- assert(not init.add_clause([-a]))
- assert(not init.add_clause([-b]))
+ init.add_clause([])
+ init.add_clause([a])
+ init.add_clause([b])
+ init.add_clause([-a])
+ init.add_clause([-b])
  self.step += 1
 
 def main(prg):
@@ -34,4 +40,4 @@ def main(prg):
 
 #end.
 
-{ a; b }.
+{ a; b; c }.
diff --git a/app/clingo/tests/python/add-clause-py.sol b/app/clingo/tests/python/add-clause-py.sol
@@ -1,7 +1,7 @@
 Step: 1
 
-b
+b c
 Step: 2
-b
+b c
 Step: 3
 UNSAT
diff --git a/libclingo/clingo.h b/libclingo/clingo.h
@@ -1086,14 +1086,22 @@ CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_g
 //! @param[in] init the target
 //! @return the assignment
 CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_init_assignment(clingo_propagate_init_t const *init);
+//! Add a literal to the solver.
+//!
+//! @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:
+//! - ::clingo_error_bad_alloc
+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.
 //!
-//! This method sets its result to false if the clause is causing a conflict.
+//! @note The result is always set to true and might be removed in a future version of the API.
+//!
 //!
 //! @param[in] init the target
 //! @param[in] clause the clause to add
 //! @param[in] size the size of the clause
-//! @param[out] result result indicating whether the clause is conflicting
+//! @param[out] result always true
 //! @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);

diff --git a/libclingo/clingo.hh b/libclingo/clingo.hh
@@ -834,6 +834,7 @@ public:
  TheoryAtoms theory_atoms() const;
  PropagatorCheckMode get_check_mode() const;
  void set_check_mode(PropagatorCheckMode mode);
+ literal_t add_literal();
  bool add_clause(LiteralSpan clause);
  clingo_propagate_init_t *to_c() const { return init_; }
 private:
@@ -2749,6 +2750,12 @@ inline void PropagateInit::set_check_mode(PropagatorCheckMode mode) {
  clingo_propagate_init_set_check_mode(init_, mode);
 }
 
+inline literal_t PropagateInit::add_literal() {
+ literal_t ret;
+ Detail::handle_error(clingo_propagate_init_add_literal(init_, &ret));
+ return ret;
+}
+
 inline bool PropagateInit::add_clause(LiteralSpan clause) {
  bool ret;
  Detail::handle_error(clingo_propagate_init_add_clause(init_, clause.begin(), clause.size(), &ret));

diff --git a/libclingo/clingo/clingocontrol.hh b/libclingo/clingo/clingocontrol.hh
@@ -153,31 +153,6 @@ inline bool parseFoobar(const std::string& str, ClingoOptions::Foobar& foobar) {
 
 // {{{1 declaration of ClingoControl
 
-class ClingoPropagateInit : public PropagateInit {
-public:
- using Lit_t = Potassco::Lit_t;
- ClingoPropagateInit(Control &c, Clasp::ClingoPropagatorInit &p);
- Output::DomainData const &theory() const override { return c_.theory(); }
- SymbolicAtoms const &getDomain() const override { return c_.getDomain(); }
- Lit_t mapLit(Lit_t lit) const override;
- int threads() const override;
- void addWatch(Lit_t lit) override { p_.addWatch(Clasp::decodeLit(lit)); }
- void addWatch(uint32_t solverId, Lit_t lit) override { p_.addWatch(solverId, Clasp::decodeLit(lit)); }
- void enableHistory(bool b) override { p_.enableHistory(b); };
- bool addClause(Potassco::LitSpan lits) override;
- void setCheckMode(clingo_propagator_check_mode_t checkMode) override {
- p_.enableClingoPropagatorCheck(static_cast<Clasp::ClingoPropagatorCheck_t::Type>(checkMode));
- }
- Potassco::AbstractAssignment const &assignment() const override;
- clingo_propagator_check_mode_t getCheckMode() const override {
- return p_.checkMode();
- }
-private:
- Control &c_;
- Clasp::ClingoPropagatorInit &p_;
- Clasp::ClingoAssignment a_;
-};
-
 class ClingoPropagatorLock : public Clasp::ClingoPropagatorLock {
 public:
  ClingoPropagatorLock() : seq_(0) {}

diff --git a/libclingo/clingo/control.hh b/libclingo/clingo/control.hh
@@ -180,7 +180,8 @@ using PropagateInit = clingo_propagate_init;
 } // namespace Gringo
 
 struct clingo_propagate_init {
- virtual bool addClause(Potassco::LitSpan lits) = 0;
+ virtual Potassco::Lit_t addLiteral() = 0;
+ virtual void addClause(Potassco::LitSpan lits) = 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
@@ -154,35 +154,6 @@ void ClingoControl::parse() {
  }
 }
 
-ClingoPropagateInit::ClingoPropagateInit(Control &c, Clasp::ClingoPropagatorInit &p)
-: c_{c}, p_{p}, a_{*static_cast<ClingoControl&>(c).clasp_->ctx.solver(0)} {
- p_.enableHistory(false);
-}
-
-bool ClingoPropagateInit::addClause(Potassco::LitSpan lits) {
- auto &ctx = static_cast<Clasp::ClaspFacade*>(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();
-}
-
-Potassco::Lit_t ClingoPropagateInit::mapLit(Lit_t lit) const {
- const auto& prg = static_cast<Clasp::Asp::LogicProgram&>(*static_cast<ClingoControl&>(c_).clasp_->program());
- return Clasp::encodeLit(prg.getLiteral(lit, Clasp::Asp::MapLit_t::Refined));
-}
-
-int ClingoPropagateInit::threads() const {
- return static_cast<ClingoControl&>(c_).clasp_->ctx.concurrency();
-}
-
-Potassco::AbstractAssignment const &ClingoPropagateInit::assignment() const {
- return a_;
-}
-
 void ClingoControl::parse(const StringVec& files, const ClingoOptions& opts, Clasp::Asp::LogicProgram* claspOut, bool addStdIn) {
  using namespace Gringo;
  logger_.enable(Warnings::OperationUndefined, !opts.wNoOperationUndefined);
@@ -400,6 +371,51 @@ void ClingoControl::interrupt() {
 bool ClingoControl::blocked() {
  return clasp_->solving();
 }
+
+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} {
+ p_.enableHistory(false);
+ }
+ Output::DomainData const &theory() const override { return c_.theory(); }
+ SymbolicAtoms const &getDomain() const override { return c_.getDomain(); }
+ Potassco::Lit_t mapLit(Lit_t lit) const override {
+ const auto& prg = static_cast<Clasp::Asp::LogicProgram&>(*facade_().program());
+ return Clasp::encodeLit(prg.getLiteral(lit, Clasp::Asp::MapLit_t::Refined));
+ }
+ int threads() const override { return facade_().ctx.concurrency(); }
+ void addWatch(Lit_t lit) override { p_.addWatch(Clasp::decodeLit(lit)); }
+ void addWatch(uint32_t solverId, Lit_t lit) override { p_.addWatch(solverId, Clasp::decodeLit(lit)); }
+ void enableHistory(bool b) override { p_.enableHistory(b); };
+ Potassco::Lit_t addLiteral() override {
+ ++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);
+ }
+ void setCheckMode(clingo_propagator_check_mode_t checkMode) override {
+ p_.enableClingoPropagatorCheck(static_cast<Clasp::ClingoPropagatorCheck_t::Type>(checkMode));
+ }
+ Potassco::AbstractAssignment const &assignment() const override { return a_; }
+ clingo_propagator_check_mode_t getCheckMode() const override { return p_.checkMode(); }
+private:
+ Clasp::ClaspFacade &facade_() const { return *static_cast<ClingoControl&>(c_).clasp_; }
+private:
+ Control &c_;
+ Clasp::ClingoPropagatorInit &p_;
+ Clasp::ClingoAssignment a_;
+ size_t &literals_;
+ Potassco::LitVec &clauses_;
+};
+
+} // namespace
+
 void ClingoControl::prepare(Assumptions ass) {
  eventHandler_ = nullptr;
  // finalize the program
@@ -409,12 +425,34 @@ void ClingoControl::prepare(Assumptions ass) {
  Clasp::ProgramBuilder *prg = clasp_->program();
  postGround(*prg);
  if (!propagators_.empty()) {
+ size_t literals{0};
+ Potassco::LitVec clauses;
  clasp_->program()->endProgram();
  for (auto&& pp : propagators_) {
- ClingoPropagateInit i(*this, *pp);
+ ClingoPropagateInit i(*this, *pp, literals, clauses);
  static_cast<Propagator*>(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
@@ -662,8 +662,15 @@ extern "C" clingo_assignment_t const *clingo_propagate_init_assignment(clingo_pr
  return static_cast<clingo_assignment_t const *>(&init->assignment());
 }
 
+extern "C" bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, clingo_literal_t *ret) {
+ GRINGO_CLINGO_TRY { *ret = init->addLiteral(); }
+ GRINGO_CLINGO_CATCH;
+}
+
 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 { *ret = init->addClause(Potassco::LitSpan{literals, size}); }
+ GRINGO_CLINGO_TRY {
+ if (ret) { *ret = true; }
+ init->addClause(Potassco::LitSpan{literals, size}); }
  GRINGO_CLINGO_CATCH;
 }
 

diff --git a/libluaclingo/luaclingo.cc b/libluaclingo/luaclingo.cc
@@ -2349,6 +2349,12 @@ struct PropagateInit : Object<PropagateInit> {
  return 0;
  }
 
+ static int addLiteral(lua_State *L) {
+ auto &self = get_self(L);
+ lua_pushinteger(L, call_c(L, clingo_propagate_init_add_literal, self.init));
+ return 1;
+ }
+
  static int addClause(lua_State *L) {
  auto &self = get_self(L);
  luaL_checktype(L, 2, LUA_TTABLE);
@@ -2424,6 +2430,7 @@ constexpr char const *PropagateInit::typeName;
 luaL_Reg const PropagateInit::meta[] = {
  {"solver_literal", mapLit},
  {"add_watch", addWatch},
+ {"add_literal", addLiteral},
  {"add_clause", addClause},
  {"set_state", setState},
  {nullptr, nullptr}

diff --git a/libpyclingo/pyclingo.cc b/libpyclingo/pyclingo.cc
@@ -3479,6 +3479,12 @@ Control.register_propagator
  Py_RETURN_NONE;
  }
 
+ Object addLiteral() {
+ clingo_literal_t ret;
+ handle_c_error(clingo_propagate_init_add_literal(init, &ret));
+ return cppToPy(ret);
+ }
+
  Object addClause(Reference pyargs, Reference pykwds) {
  static char const *kwlist[] = {"clause", nullptr};
  Reference pyClause;
@@ -3534,7 +3540,16 @@ Returns
 int
  A solver literal.
 )"},
- {"add_clause", to_function<&PropagateInit::addClause>(), METH_KEYWORDS | METH_VARARGS, R"(add_clause(self, clause: List[int]) -> None
+ {"add_literal", to_function<&PropagateInit::addLiteral>(), METH_NOARGS, R"(add_literal(self) -> int
+
+Statically adds a literal to the solver.
+
+Returns
+-------
+int
+ Returns the added literal.
+)"},
+ {"add_clause", to_function<&PropagateInit::addClause>(), METH_KEYWORDS | METH_VARARGS, R"(add_clause(self, clause: List[int]) -> bool
 
 Statically adds the given clause to the problem.
 
@@ -3546,7 +3561,7 @@ clause : List[int]
 Returns
 -------
 bool
- Returns false if the clause is conflicting.
+ The return value is always true and should be ignored.
 )"},
  {nullptr, nullptr, 0, nullptr}
 };