Fix issue in clingo propagator.

* Clingo propagator must never backtrack during addClause() from client code. Previously, when a static asserting clause was added, the propagator immediately tried to backtrack to the assertion level. Instead, it should return false from addClause() and then only add the clause once control returned from the client code.
potassco · Dec 4, 2024 · 2207c3a · 2207c3a
1 parent 8661297
commit 2207c3a
Show file tree

Hide file tree

Showing 5 changed files with 123 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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;