diff --git a/CHANGES b/CHANGES index bb94e5b..9793aa0 100644 --- a/CHANGES +++ b/CHANGES @@ -11,6 +11,7 @@ clasp 3.4.0: * added support for pb-constraints in [w]cnf+ format * addressed issue https://github.com/potassco/clasp/issues/107 * "tweety" asp options are now applied when using config "many" + * fixed unexpected undo calls from clingo propagator when adding "locked" clauses * fixed race condition in work splitting algorithm * fixed handling of "sticky" logic program options * fixed tests for CLASP_BUILD_WITH_THREADS=OFF diff --git a/CMakeLists.txt b/CMakeLists.txt index 53af590..06225bf 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,5 @@ cmake_minimum_required(VERSION 3.1) -project(CLASP VERSION 3.4.0.3 LANGUAGES CXX) +project(CLASP VERSION 3.4.0.4 LANGUAGES CXX) # Enable folders in IDEs like Visual Studio set_property(GLOBAL PROPERTY USE_FOLDERS ON) if (POLICY CMP0063) diff --git a/doc/output.md b/doc/output.md index d0ceee7..c57301c 100644 --- a/doc/output.md +++ b/doc/output.md @@ -250,7 +250,7 @@ ID:T Vars Constraints State Limits | learned constraints allowed (deletion is forced once this number is reached) - Event `T` is one of `D`=Lemma deletion, `G`=Database size limit update, `R`=Restart, `E`=Search exit -Verbosity **levels 4** and **5** are only relevant when solving disjunctive logic program. +Verbosity **levels 4** and **5** are only relevant when solving disjunctive logic programs. On **level 4**, progress information is restricted to stability checks, while **level 5** combines the information from levels 3 and 4. diff --git a/src/clingo.cpp b/src/clingo.cpp index e9399ae..9b42f06 100644 --- a/src/clingo.cpp +++ b/src/clingo.cpp @@ -325,15 +325,15 @@ bool ClingoPropagator::addClause(Solver& s, uint32 st) { Literal w0 = clause.size > 0 ? clause.lits[0] : lit_false(); Literal w1 = clause.size > 1 ? clause.lits[1] : lit_false(); uint32 cs = ClauseCreator::status(s, clause); + bool local = (todo_.flags & ClauseCreator::clause_no_add) != 0; if (cs & (ClauseCreator::status_unit|ClauseCreator::status_unsat)) { - uint32 dl = (cs & ClauseCreator::status_unsat) ? s.level(w0.var()) : s.level(w1.var()); + uint32 dl = (cs & ClauseCreator::status_unsat) && !local ? s.level(w0.var()) : s.level(w1.var()); if (dl < s.decisionLevel() && s.isUndoLevel()) { if ((st & state_ctrl) != 0u) { return false; } if ((st & state_prop) != 0u) { ClingoPropagator::reset(); cancelPropagation(); } s.undoUntil(dl); } } - bool local = (todo_.flags & ClauseCreator::clause_no_add) != 0; if (!s.isFalse(w0) || local || s.force(w0, this)) { ClauseCreator::Result res = ClauseCreator::create(s, clause, todo_.flags); if (res.local && local) { db_.push_back(res.local); } diff --git a/tests/facade_test.cpp b/tests/facade_test.cpp index 0048212..3e34721 100644 --- a/tests/facade_test.cpp +++ b/tests/facade_test.cpp @@ -1753,12 +1753,15 @@ TEST_CASE("Facade statistics", "[facade]") { namespace { class MyProp : public Potassco::AbstractPropagator { public: - MyProp() : fire(lit_false()), clProp(Potassco::Clause_t::Learnt) {} + MyProp() : fire(lit_false()), clProp(Potassco::Clause_t::Learnt), inProp(false) {} virtual void propagate(Potassco::AbstractSolver& s, const ChangeList& changes) { + inProp = true; map(changes); addClause(s); + inProp = false; } virtual void undo(const Potassco::AbstractSolver&, const ChangeList& changes) { + POTASSCO_REQUIRE(!inProp, "invalid call to undo from propagate"); map(changes); } virtual void check(Potassco::AbstractSolver& s) { @@ -1787,6 +1790,7 @@ class MyProp : public Potassco::AbstractPropagator { LitVec change; Potassco::LitVec clause; Potassco::Clause_t clProp; + bool inProp; }; struct PropagatorTest { @@ -1991,8 +1995,18 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") { ctx.endInit(); Solver& s = *ctx.master(); s.assume(negLit(v[2])) && s.propagate(); + uint32 learntExpected = 0; + SECTION("default") { + prop.clProp = Potassco::Clause_t::Learnt; + learntExpected = 1; + } + SECTION("static") { + prop.clProp = Potassco::Clause_t::Static; + learntExpected = 0; + } s.assume(negLit(v[3])) && s.propagate(); - REQUIRE(ctx.numLearntShort() == 1); + INFO("clause type: " << prop.clProp); + REQUIRE(ctx.numLearntShort() == learntExpected); REQUIRE(s.isTrue(posLit(v[1]))); REQUIRE((prop.change.size() == 1 && prop.change[0] == negLit(v[3]))); } @@ -2010,8 +2024,18 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") { s.assume(negLit(v[1])) && s.propagate(); s.assume(posLit(v[4])) && s.propagate(); s.assume(negLit(v[2])) && s.propagate(); + uint32 learntExpected = 0; + SECTION("default") { + prop.clProp = Potassco::Clause_t::Learnt; + learntExpected = 1; + } + SECTION("static") { + prop.clProp = Potassco::Clause_t::Static; + learntExpected = 0; + } + INFO("clause type: " << prop.clProp); s.assume(posLit(v[5])) && s.propagate(); - REQUIRE(ctx.numLearntShort() == 1); + REQUIRE(ctx.numLearntShort() == learntExpected); REQUIRE(s.decisionLevel() == 3); s.undoUntil(2); REQUIRE(std::find(prop.change.begin(), prop.change.end(), posLit(v[3])) != prop.change.end()); @@ -2028,6 +2052,13 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") { s.assume(negLit(v[1])) && s.propagate(); s.assume(negLit(v[3])); s.pushRootLevel(2); + SECTION("default") { + prop.clProp = Potassco::Clause_t::Learnt; + } + SECTION("static") { + prop.clProp = Potassco::Clause_t::Static; + } + INFO("clause type: " << prop.clProp); REQUIRE_FALSE(s.propagate()); INFO("do not add conflicting constraint"); REQUIRE(ctx.numLearntShort() == 0); @@ -2110,6 +2141,90 @@ TEST_CASE("Clingo propagator", "[facade][propagator]") { s.reduceLearnts(1.0); REQUIRE(s.numWatches(negLit(v[2])) == 1); } + SECTION("testAddStaticAsserting") { + test.addVars(2); + prop.addToClause(posLit(v[1])); + prop.addToClause(posLit(v[2])); + prop.fire = negLit(v[2]); + prop.clProp = Potassco::Clause_t::Static; + + tp.addWatch(negLit(v[2])); + tp.applyConfig(*ctx.master()); + ctx.endInit(); + + Solver& s = *ctx.master(); + s.assume(negLit(v[1])) && s.propagate(); + REQUIRE(s.assume(negLit(v[2]))); + REQUIRE(s.propagate()); + REQUIRE(s.numLearntConstraints() == 0); + REQUIRE(s.isTrue(posLit(v[2]))); + REQUIRE(s.decisionLevel() == 1); + + prop.fire = lit_false(); + s.undoUntil(0); + s.assume(negLit(v[1])) && s.propagate(); + REQUIRE(s.isTrue(posLit(v[2]))); + } + + SECTION("testAddStaticConflicting") { + ctx.setShortMode(ContextParams::short_explicit); + test.addVars(4); + ctx.addTernary(posLit(v[1]), negLit(v[2]), posLit(v[3])); + prop.addToClause(posLit(v[1])); + prop.addToClause(posLit(v[2])); + prop.addToClause(posLit(v[3])); + prop.fire = negLit(v[4]); + prop.clProp = Potassco::Clause_t::Static; + + tp.addWatch(negLit(v[4])); + tp.applyConfig(*ctx.master()); + ctx.endInit(); + + Solver& s = *ctx.master(); + s.assume(negLit(v[1])) && s.propagate(); + s.assume(negLit(v[3])) && s.propagate(); + REQUIRE(s.propagate()); + REQUIRE(s.isTrue(negLit(v[2]))); + + s.assume(negLit(4)); + REQUIRE_FALSE(s.propagate()); + REQUIRE(s.resolveConflict()); + REQUIRE(s.numLearntConstraints() == 1); + + s.undoUntil(0); + s.reduceLearnts(1.0f); + REQUIRE(s.numLearntConstraints() == 0); + + prop.fire = lit_false(); + s.assume(negLit(v[1])) && s.propagate(); + s.assume(negLit(v[3])); + REQUIRE_FALSE(s.propagate()); + } + + SECTION("testAddStaticBacktrackUnit") { + test.addVars(4); + prop.addToClause(posLit(v[1])); + prop.addToClause(posLit(v[2])); + prop.addToClause(posLit(v[3])); + prop.fire = negLit(v[4]); + prop.clProp = Potassco::Clause_t::Static; + + tp.addWatch(negLit(v[4])); + tp.applyConfig(*ctx.master()); + ctx.endInit(); + + Solver& s = *ctx.master(); + s.assume(negLit(v[1])) && s.propagate(); + s.assume(negLit(v[3])) && s.propagate(); + + s.assume(negLit(v[4])); + REQUIRE(s.decisionLevel() == 3); + REQUIRE(s.propagate()); + REQUIRE(s.decisionLevel() == 2); + REQUIRE(s.isTrue(posLit(v[2]))); + REQUIRE(s.numLearntConstraints() == 0); + } + SECTION("with facade") { ClaspConfig config; ClaspFacade libclasp;