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

@@ -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

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):

libclingo/clingo.h

@@ -1088,23 +1088,35 @@ 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:
 //! - ::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.
 //!
-//! @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);
 
 //! @}
 

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 {

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;

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<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();
+    }
+    bool propagate() override {
+        auto &ctx = static_cast<Clasp::ClaspFacade*>(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<Clasp::ClingoPropagatorCheck_t::Type>(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<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);

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;
 }
 

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 <typename T>
+class TestInit : public Propagator {
+public:
+    TestInit(T &&f) : f_{std::forward<T>(f)} { }
+    void init(PropagateInit &init) override {
+        f_(init);
+    }
+private:
+    T f_;
+};
+
+template <typename T>
+static TestInit<T> make_init(T &&f) {
+    return {std::forward<T>(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]") {

libluaclingo/luaclingo.cc

@@ -2390,6 +2390,12 @@ struct PropagateInit : Object<PropagateInit> {
         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_propagator_check_mode>(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}
 };