Acquire problem vars when necessary.

* Ensure that all relevant problem variables are known to the master solver when creating clauses, weight-, and minimize-constraints.
potassco · Dec 7, 2019 · 13ae0ea · 13ae0ea · rkaminsk · Dec 7, 2019
1 parent fdd37e2
commit 13ae0ea
Show file tree

Hide file tree

Showing 8 changed files with 37 additions and 9 deletions.
diff --git a/clasp/solver.h b/clasp/solver.h
@@ -782,7 +782,8 @@ class Solver {
 	SolverStrategies&  strategies() { return strategy_; }
 	bool resolveToFlagged(const LitVec& conflictClause, uint8 vflag, LitVec& out, uint32& lbd) const;
 	void resolveToCore(LitVec& out);
-	void acquireProblemVars();
+	void acquireProblemVar(Var var);
+	void acquireProblemVars() { acquireProblemVar(numProblemVars());  }
 	//@}
 private:
 	struct DLevel {

diff --git a/src/clause.cpp b/src/clause.cpp
@@ -131,10 +131,8 @@ 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   = s.numProblemVars() > s.numVars() ? std::max_element(in, in + inSize)->var() : 0;
-	if (!s.validVar(vMax)) { // Handle any uncommitted vars
-		s.acquireProblemVars();
-	}
+	Var     vMax   = s.numProblemVars() > s.numVars() && inSize ? std::max_element(in, in + inSize)->var() : 0;
+	s.acquireProblemVar(vMax);
 	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/minimize_constraint.cpp b/src/minimize_constraint.cpp
@@ -717,7 +717,7 @@ MinimizeBuilder::SharedData* MinimizeBuilder::createShared(SharedContext& ctx, c
 
 MinimizeBuilder::SharedData* MinimizeBuilder::build(SharedContext& ctx) {
 	POTASSCO_REQUIRE(!ctx.frozen());
-	if ((!ctx.ok() || !ctx.master()->propagate()) || empty()) {
+	if (!ctx.ok() || (ctx.master()->acquireProblemVars(), !ctx.master()->propagate()) || empty()) {
 		clear();
 		return 0;
 	}

diff --git a/src/shared_context.cpp b/src/shared_context.cpp
@@ -956,6 +956,7 @@ Solver& SharedContext::startAddConstraints(uint32 constraintGuess) {
 }
 bool SharedContext::addUnary(Literal x) {
 	POTASSCO_REQUIRE(!frozen() || !isShared());
+	master()->acquireProblemVar(x.var());
 	return master()->force(x);
 }
 bool SharedContext::addBinary(Literal x, Literal y) {

diff --git a/src/solver.cpp b/src/solver.cpp
@@ -379,9 +379,10 @@ Var Solver::pushAuxVar() {
 	return aux;
 }
 
-void Solver::acquireProblemVars() {
-	if (!shared_->frozen() && numProblemVars() > numVars())
-		shared_->startAddConstraints();
+void Solver::acquireProblemVar(Var var) {
+	if (validVar(var) || shared_->frozen() || numProblemVars() <= numVars() || !shared_->ok())
+		return;
+	shared_->startAddConstraints();
 }
 
 void Solver::popAuxVar(uint32 num, ConstraintDB* auxCons) {

diff --git a/src/weight_constraint.cpp b/src/weight_constraint.cpp
@@ -40,6 +40,10 @@ namespace Clasp {
 // return: achievable weight
 // post  : lits is sorted by decreasing weights
 WeightLitsRep WeightLitsRep::create(Solver& s, WeightLitVec& lits, weight_t bound) {
+	// Step 0: Ensure s has all relevant problem variables
+	if (s.numProblemVars() > s.numVars() && !lits.empty()) {
+		s.acquireProblemVar(std::max_element(lits.begin(), lits.end())->first.var());
+	}
 	// Step 1: remove assigned/superfluous literals and merge duplicate/complementary ones
 	LitVec::size_type j = 0, other;
 	const weight_t MAX_W= std::numeric_limits<weight_t>::max();

diff --git a/tests/minimize_test.cpp b/tests/minimize_test.cpp
@@ -100,6 +100,21 @@ TEST_CASE("Model-guided minimize", "[constraint][asp]") {
 		REQUIRE(data->lits[0].second == 0);
 		REQUIRE(data->weights.size() == 1);
 	}
+	SECTION("testNewVariableAfterStartAddConstraints") {
+		Literal z = posLit(ctx.addVar(Var_t::Atom));
+		mb.add(0, WeightLiteral(z, 1));
+		REQUIRE_FALSE(ctx.master()->validVar(z.var()));
+		SECTION("assigned") {
+			ctx.addUnary(z);
+			REQUIRE(ctx.master()->validVar(z.var()));
+			data = mb.build(ctx);
+		}
+		SECTION("unassigned") {
+			data = mb.build(ctx);
+			REQUIRE(ctx.master()->validVar(z.var()));
+		}
+		REQUIRE(data);
+	}
 
 	SECTION("testOneLevelLits") {
 		ctx.addUnary(c);

diff --git a/tests/weight_constraint_test.cpp b/tests/weight_constraint_test.cpp
@@ -110,6 +110,14 @@ TEST_CASE("Cardinality constraints", "[constraint][pb][asp]") {
 		REQUIRE(solver.isFalse(lits[3]));
 		REQUIRE(solver.isFalse(lits[4]));
 	}
+	SECTION("testIntegrateNewVars") {
+		Literal f = posLit(ctx.addVar(Var_t::Atom));
+		lits[2] = f;
+		lits.resize(3);
+		REQUIRE_FALSE(ctx.master()->validVar(f.var()));
+		REQUIRE(newCardinalityConstraint(ctx, lits, 1));
+		REQUIRE(ctx.master()->validVar(f.var()));
+	}
 
 	SECTION("test propagate") {
 		LitVec assume, expect;