Simplify and fix QueryFinder.

* QueryFinder must close the "true" query on initial model so that
  other threads always select a new query on next update.

src/cb_enumerator.cpp

@@ -108,19 +108,19 @@ class CBConsequences::QueryFinder : public EnumerationConstraint{
 		uint32   size_;
 		SizeType refs_;
 	};
-	explicit QueryFinder(const LitVec& c, uint32 nVars) : EnumerationConstraint(), open_(c), state_(new State(nVars)), query_(lit_false()), level_(0), dirty_(false) {
-		state_->push(query_);
+	explicit QueryFinder(const LitVec& c, uint32 nVars) : EnumerationConstraint(), open_(c), state_(new State(nVars)), query_(lit_false()) {
+		state_->push(query_); // start with true as initial query
 	}
-	explicit QueryFinder(const LitVec& c, State* st) : EnumerationConstraint(), open_(c), state_(st), query_(lit_false()), level_(0), dirty_(false) {
+	explicit QueryFinder(const LitVec& c, State* st) : EnumerationConstraint(), open_(c), state_(st), query_(lit_false()) {
 	}
 	~QueryFinder() { state_->release(); }
 	ConPtr clone() { return new QueryFinder(open_, state_->share()); }
-	bool    hasQuery() const { return query_ != lit_false(); }
 	bool    doUpdate(Solver& s);
 	void    doCommitModel(Enumerator&, Solver&);
 	void    doCommitUnsat(Enumerator&, Solver&);
-	void    updateUpper(Solver& s, uint32 rl);
-	void    updateLower(Solver& s, uint32 rl);
+	void    initUpper(Solver& s);
+	void    updateUpper(Solver& s, uint32 root);
+	void    updateOpen(Solver& s);
 	bool    selectOpen(Solver& s, Literal& q);
 	void    reason(Solver& s, Literal p, LitVec& out) {
 		for (uint32 i = 1, end = s.level(p.var()); i <= end; ++i) {
@@ -129,95 +129,90 @@ class CBConsequences::QueryFinder : public EnumerationConstraint{
 		}
 	}
 	bool    popQuery(Solver& s) {
-		if (!hasQuery() || s.rootLevel() == level_ || s.value(query_.var()) == value_free) {
-			return s.popRootLevel(0);
+		if (s.isFalse(query_) && query_ != lit_false()) {
+			uint32 diff = s.rootLevel() - s.level(query_.var());
+			return s.popRootLevel(diff + 1);
 		}
-		return s.popRootLevel((s.rootLevel() - level_) + 1);
+		return s.popRootLevel(0);
 	}
 	LitVec  open_;
 	State*  state_;
 	Literal query_;
-	uint32  level_;
-	bool    dirty_;
 };
-// Reduce the overestimate by computing c = c \cap M,
-// where M is the current model stored in s.
-void CBConsequences::QueryFinder::updateUpper(Solver& s, uint32 root) {
+// Init overestimate to current model stored in s.
+void CBConsequences::QueryFinder::initUpper(Solver& s) {
 	LitVec::iterator j = open_.begin();
 	for (LitVec::iterator it = j, end = open_.end(); it != end; ++it) {
-		if      (!state_->open(*it))        { continue; }
-		else if (!s.isTrue(*it))            { state_->pop(*it); }
-		else if (s.level(it->var()) > root) { *j++ = *it; }
-		else                                { state_->fix(*it); }
+		if (s.isTrue(*it)) {
+			if (s.level(it->var())) { state_->push(*j++ = *it); }
+			else                    { state_->fix(*it); }
+		}
 	}
 	open_.erase(j, open_.end());
 }
-// Adds facts to (under) estimate.
-void CBConsequences::QueryFinder::updateLower(Solver& s, uint32 rl) {
+// Reduce the overestimate by computing c = c \cap M, where M is the current model stored in s.
+void CBConsequences::QueryFinder::updateUpper(Solver& s, uint32 root) {
 	LitVec::iterator j = open_.begin();
 	for (LitVec::iterator it = j, end = open_.end(); it != end; ++it) {
-		ValueRep val = s.value(it->var());
-		if (val != value_free && s.level(it->var()) > rl) {
-			val = value_free;
+		if (state_->open(*it)) {
+			if      (!s.isTrue(*it))            { state_->pop(*it); }
+			else if (s.level(it->var()) < root) { state_->fix(*it); }
+			else                                { *j++ = *it; }
 		}
-		if      (!state_->open(*it)) { continue; }
-		else if (val == value_free)  { *j++ = *it; }
-		else if (s.isTrue(*it))      { state_->fix(*it); }
-		else                         { state_->pop(*it); }
 	}
-	if (j != open_.end()) { dirty_ = true; }
 	open_.erase(j, open_.end());
 }
-bool CBConsequences::QueryFinder::selectOpen(Solver& s, Literal& q) {
-	for (LitVec::size_type i = 0, end = open_.size();; --end, open_.pop_back()) {
+// Removes no longer open literals from estimate.
+void CBConsequences::QueryFinder::updateOpen(Solver& s) {
+	assert(s.decisionLevel() == s.rootLevel());
+	for (LitVec::size_type i = 0, end = open_.size();;) {
 		for (; i != end && s.value(open_[i].var()) == value_free && state_->open(open_[i]); ++i) { ; }
 		if (i == end) { break; }
-		q = open_[i];
-		open_[i] = open_.back();
+		Literal q = open_[i];
 		if      (s.isTrue(q))     { state_->fix(q); }
 		else if (state_->open(q)) { state_->pop(q); }
-		else                      { continue; }
-		dirty_ = true;
+		open_[i]  = open_.back();
+		open_.pop_back();
+		--end;
+	}
+}
+bool CBConsequences::QueryFinder::selectOpen(Solver& s, Literal& q) {
+	updateOpen(s);
+	if (open_.empty()) {
+		return false;
 	}
-	if (open_.empty()) { return false; }
 	q = s.heuristic()->selectRange(s, &open_[0], &open_[0] + open_.size());
 	return true;
 }
 // solve(~query) produced a model - query is not a cautious consequence, update overestimate
 void CBConsequences::QueryFinder::doCommitModel(Enumerator&, Solver& s) {
-	bool hasQ = hasQuery();
-	if (!hasQ && state_->open(query_)) {
-		// init state to first model
-		for (LitVec::iterator it = open_.begin(), end = open_.end(); it != end; ++it) {
-			if (s.isTrue(*it)) { state_->push(*it); }
-		}
+	assert(s.isFalse(query_));
+	if (isSentinel(query_)) {
+		state_->fix(~query_);
+		initUpper(s);
+	}
+	else {
+		state_->pop(query_);
+		updateUpper(s, s.level(query_.var()));
 	}
-	if (hasQ) { state_->pop(query_); }
-	updateUpper(s, level_);
-	dirty_ = false;
 	state_->setModel(s.model);
-	query_.flag();
 }
 // solve(~query) failed - query is a cautious consequence
 void CBConsequences::QueryFinder::doCommitUnsat(Enumerator&, Solver& s) {
-	bool commit = !disjointPath() && s.hasConflict() && !s.hasStopConflict() && hasQuery();
-	popQuery(s);
-	if (commit) {
+	assert(s.isFalse(query_));
+	bool commit = !isSentinel(query_) && !disjointPath() && s.hasConflict() && !s.hasStopConflict();
+	if (popQuery(s) && commit && state_->open(query_)) {
+		assert(s.decisionLevel() == s.rootLevel());
 		state_->fix(query_);
-		query_.flag();
-	}
-	updateLower(s, level_);
-	if (dirty_) {
-		dirty_ = false;
+		updateOpen(s);
 		state_->setModel(s.model);
 	}
 }
 bool CBConsequences::QueryFinder::doUpdate(Solver& s) {
-	bool newQ = query_.flagged() || !state_->open(query_);
+	bool newQ = !state_->open(query_);
 	if (newQ || s.value(query_.var()) == value_free) { // query was SAT/UNSAT or solved by other thread
 		if (!popQuery(s)) { return false; }
 		assert(s.decisionLevel() == s.rootLevel());
-		level_ = s.rootLevel();
 		return newQ && !selectOpen(s, query_) ? s.force(query_ = lit_false(), this) : s.pushRoot(~query_);
 	}
 	return true;