Acquire problem vars in ClauseCreator.

* Call SharedContext::startAddConstraints() from ClauseCreator if necessary, i.e. if the clause to be created contains problem vars not yet added to the solver.
potassco · Sep 21, 2019 · 1c7246a · 1c7246a
1 parent 4ed33ff
commit 1c7246a
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 1 deletion.
diff --git a/clasp/solver.h b/clasp/solver.h
@@ -782,6 +782,7 @@ class Solver {
 	SolverStrategies&  strategies() { return strategy_; }
 	bool resolveToFlagged(const LitVec& conflictClause, uint8 vflag, LitVec& out, uint32& lbd) const;
 	void resolveToCore(LitVec& out);
+	void acquireProblemVars();
 	//@}
 private:
 	struct DLevel {

diff --git a/src/clause.cpp b/src/clause.cpp
@@ -131,7 +131,10 @@ ClauseRep ClauseCreator::prepare(Solver& s, const Literal* in, uint32 inSize, co
 	uint32 abst_w1 = 0, abst_w2 = 0;
 	bool simplify  = ((flags & clause_force_simplify) != 0) && inSize > 2 && outMax >= inSize;
 	Literal tag    = ~s.tagLiteral();
-	Var     vMax   = 0;
+	Var     vMax   = s.numProblemVars() > s.numVars() ? std::max_element(in, in + inSize)->var() : 0;
+	if (!s.validVar(vMax)) { // Handle any uncommitted vars
+		s.acquireProblemVars();
+	}
 	for (uint32 i = 0, j = 0, MAX_OUT = outMax - 1; i != inSize; ++i) {
 		Literal p     = in[i];
 		uint32 abst_p = watchOrder(s, p);

diff --git a/src/solver.cpp b/src/solver.cpp
@@ -378,6 +378,12 @@ Var Solver::pushAuxVar() {
 	heuristic_->updateVar(*this, aux, 1);
 	return aux;
 }
+
+void Solver::acquireProblemVars() {
+	if (!shared_->frozen() && numProblemVars() > numVars())
+		shared_->startAddConstraints();
+}
+
 void Solver::popAuxVar(uint32 num, ConstraintDB* auxCons) {
 	num = numVars() >= shared_->numVars() ? std::min(numVars() - shared_->numVars(), num) : 0;
 	if (!num) { return; }

diff --git a/tests/clause_creator_test.cpp b/tests/clause_creator_test.cpp
@@ -72,6 +72,19 @@ TEST_CASE("ClauseCreator create", "[constraint][core]") {
 		REQUIRE((bool)creator.start().add(a).add(b).add(c).add(d).end());
 		REQUIRE(1u == ctx.numConstraints());
 	}
+	SECTION("test creator acquires missing vars") {
+		Literal f = posLit(ctx.addVar(Var_t::Atom));
+		Literal g = posLit(ctx.addVar(Var_t::Atom));
+		Literal h = posLit(ctx.addVar(Var_t::Atom));
+		REQUIRE(!s.validVar(f.var()));
+		REQUIRE(!s.validVar(g.var()));
+		REQUIRE(!s.validVar(h.var()));
+		REQUIRE((bool)creator.start().add(a).add(b).add(g).add(f).end());
+		REQUIRE(1u == ctx.numConstraints());
+		REQUIRE(s.validVar(f.var()));
+		REQUIRE(s.validVar(g.var()));
+		REQUIRE(s.validVar(h.var()));
+	}
 	SECTION("test creator asserts first literal") {
 		ctx.endInit();
 		s.assume(~b);