comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
}
void CnfStream::recordTranslation(TNode node) {
- if (d_assertingLemma) {
- d_lemmas.push_back(stripNot(node));
- } else {
+ if (!d_removable) {
d_translationTrail.push_back(stripNot(node));
}
}
void CnfStream::assertClause(TNode node, SatClause& c) {
Debug("cnf") << "Inserting into stream " << c << endl;
- d_satSolver->addClause(c, d_assertingLemma);
+ d_satSolver->addClause(c, d_removable);
}
void CnfStream::assertClause(TNode node, SatLiteral a) {
// If a theory literal, we pre-register it
if (theoryLiteral) {
- bool backup = d_assertingLemma;
+ bool backup = d_removable;
d_registrar.preRegister(node);
- d_assertingLemma = backup;
+ d_removable = backup;
}
// Here, you can have it
// If the non-negated node has already been translated, get the translation
if(isTranslated(node)) {
nodeLit = getLiteral(node);
- // If we are asserting a lemma, we need to take the whole tree to level 0
- if (d_assertingLemma) {
- moveToBaseLevel(node);
- }
} else {
// Handle each Boolean operator case
switch(node.getKind()) {
else return ~nodeLit;
}
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
Assert(node.getKind() == AND);
if (!negated) {
// If the node is a conjunction, we handle each conjunct separately
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
conjunct != node_end; ++conjunct ) {
- convertAndAssert(*conjunct, lemma, false);
+ convertAndAssert(*conjunct, false);
}
} else {
// If the node is a disjunction, we construct a clause and assert it
}
}
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
Assert(node.getKind() == OR);
if (!negated) {
// If the node is a disjunction, we construct a clause and assert it
// If the node is a conjunction, we handle each conjunct separately
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
conjunct != node_end; ++conjunct ) {
- convertAndAssert(*conjunct, lemma, true);
+ convertAndAssert(*conjunct, true);
}
}
}
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
if (!negated) {
// p XOR q
SatLiteral p = toCNF(node[0], false);
recordTranslation(node[1]);
}
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
if (!negated) {
// p <=> q
SatLiteral p = toCNF(node[0], false);
recordTranslation(node[1]);
}
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
if (!negated) {
// p => q
SatLiteral p = toCNF(node[0], false);
recordTranslation(node[1]);
} else {// Construct the
// !(p => q) is the same as (p && ~q)
- convertAndAssert(node[0], lemma, false);
- convertAndAssert(node[1], lemma, true);
+ convertAndAssert(node[0], false);
+ convertAndAssert(node[1], true);
}
}
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
// ITE(p, q, r)
SatLiteral p = toCNF(node[0], false);
SatLiteral q = toCNF(node[1], negated);
// At the top level we must ensure that all clauses that are asserted are
// not unit, except for the direct assertions. This allows us to remove the
// clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) {
- Debug("cnf") << "convertAndAssert(" << node << ", lemma = " << lemma << ", negated = " << (negated ? "true" : "false") << ")" << endl;
- d_assertingLemma = lemma;
+void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+ Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+ d_removable = removable;
+ convertAndAssert(node, negated);
+}
+
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+ Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
switch(node.getKind()) {
case AND:
- convertAndAssertAnd(node, lemma, negated);
+ convertAndAssertAnd(node, negated);
break;
case OR:
- convertAndAssertOr(node, lemma, negated);
+ convertAndAssertOr(node, negated);
break;
case IFF:
- convertAndAssertIff(node, lemma, negated);
+ convertAndAssertIff(node, negated);
break;
case XOR:
- convertAndAssertXor(node, lemma, negated);
+ convertAndAssertXor(node, negated);
break;
case IMPLIES:
- convertAndAssertImplies(node, lemma, negated);
+ convertAndAssertImplies(node, negated);
break;
case ITE:
- convertAndAssertIte(node, lemma, negated);
+ convertAndAssertIte(node, negated);
break;
case NOT:
- convertAndAssert(node[0], lemma, !negated);
+ convertAndAssert(node[0], !negated);
break;
default:
// Atoms
/** Top level nodes that we translated */
std::vector<TNode> d_translationTrail;
- /** Nodes belonging to asserted lemmas */
- std::vector<Node> d_lemmas;
-
/** Remove nots from the node */
TNode stripNot(TNode node) {
while (node.getKind() == kind::NOT) {
void undoTranslate(TNode node, int level);
/**
- * Are we asserting a lemma (true) or a permanent clause (false).
+ * Are we asserting a removable clause (true) or a permanent clause (false).
* This is set at the begining of convertAndAssert so that it doesn't
* need to be passed on over the stack.
*/
- bool d_assertingLemma;
+ bool d_removable;
/**
* Asserts the given clause to the sat solver.
/**
* Converts and asserts a formula.
* @param node node to convert and assert
- * @param lemma whether the sat solver can choose to remove the clauses
+ * @param removable whether the sat solver can choose to remove the clauses
* @param negated wheather we are asserting the node negated
*/
- virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0;
+ virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
/**
* Get the node that is represented by the given SatLiteral.
/**
* Convert a given formula to CNF and assert it to the SAT solver.
* @param node the formula to assert
- * @param lemma is this a lemma that is erasable
+ * @param removable is this something that can be erased
* @param negated true if negated
*/
- void convertAndAssert(TNode node, bool lemma, bool negated = false);
+ void convertAndAssert(TNode node, bool removable, bool negated);
/**
* Constructs the stream to use the given sat solver.
private:
+ /**
+ * Same as above, except that removable is rememebered.
+ */
+ void convertAndAssert(TNode node, bool negated);
+
// Each of these formulas handles takes care of a Node of each Kind.
//
// Each handleX(Node &n) is responsible for:
SatLiteral handleAnd(TNode node);
SatLiteral handleOr(TNode node);
- void convertAndAssertAnd(TNode node, bool lemma, bool negated);
- void convertAndAssertOr(TNode node, bool lemma, bool negated);
- void convertAndAssertXor(TNode node, bool lemma, bool negated);
- void convertAndAssertIff(TNode node, bool lemma, bool negated);
- void convertAndAssertImplies(TNode node, bool lemma, bool negated);
- void convertAndAssertIte(TNode node, bool lemma, bool negated);
+ void convertAndAssertAnd(TNode node, bool negated);
+ void convertAndAssertOr(TNode node, bool negated);
+ void convertAndAssertXor(TNode node, bool negated);
+ void convertAndAssertIff(TNode node, bool negated);
+ void convertAndAssertImplies(TNode node, bool negated);
+ void convertAndAssertIte(TNode node, bool negated);
/**
* Transforms the node into CNF recursively.
static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
+class ScopedBool {
+ bool& watch;
+ bool oldValue;
+public:
+ ScopedBool(bool& watch, bool newValue)
+ : watch(watch), oldValue(watch) {
+ watch = newValue;
+ }
+ ~ScopedBool() {
+ watch = oldValue;
+ }
+};
+
+
//=================================================================================================
// Constructor/Destructor:
, context(context)
, assertionLevel(0)
, enable_incremental(enable_incremental)
- , problem_extended(false)
- , in_solve(false)
+ , minisat_busy(false)
// Parameters (user settable):
//
, verbosity (0)
Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
{
int v = nVars();
+
watches .init(mkLit(v, false));
watches .init(mkLit(v, true ));
assigns .push(l_Undef);
- vardata .push(mkVarData(CRef_Undef, 0, assertionLevel));
- //activity .push(0);
+ vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, 0));
activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
seen .push(0);
polarity .push(sign);
decision .push();
trail .capacity(v+1);
- setDecisionVar(v, dvar);
theory .push(theoryAtom);
- // We have extended the problem
- if (in_solve) {
- problem_extended = true;
- insertVarOrder(v);
- }
+ setDecisionVar(v, dvar);
return v;
}
-CRef Solver::reason(Var x) const {
+CRef Solver::reason(Var x) {
+
// If we already have a reason, just return it
if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
// Get the explanation from the theory
SatClause explanation;
proxy->explainPropagation(l, explanation);
+
+ // Sort the literals by trail index level
+ lemma_lt lt(*this);
+ sort(explanation, lt);
Assert(explanation[0] == l);
- // We're actually changing the state, so we hack it into non-const
- Solver* nonconst_this = const_cast<Solver*>(this);
-
// Compute the assertion level for this clause
int explLevel = 0;
for (int i = 0; i < explanation.size(); ++ i) {
}
// Construct the reason (level 0)
- // TODO compute the level
- CRef real_reason = nonconst_this->ca.alloc(explLevel, explanation, true);
- nonconst_this->vardata[x] = mkVarData(real_reason, level(x), intro_level(x));
- nonconst_this->learnts.push(real_reason);
- nonconst_this->attachClause(real_reason);
+ CRef real_reason = ca.alloc(explLevel, explanation, true);
+ vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x));
+ clauses_removable.push(real_reason);
+ attachClause(real_reason);
return real_reason;
}
-bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
+bool Solver::addClause_(vec<Lit>& ps, bool removable)
{
if (!ok) return false;
- bool propagate_first_literal = false;
-
// Check if clause is satisfied and remove false/duplicate literals:
sort(ps);
Lit p; int i, j;
- if (type != CLAUSE_LEMMA) {
- // Problem clause
- for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
- if (value(ps[i]) == l_True || ps[i] == ~p)
- return true;
- else if (value(ps[i]) != l_False && ps[i] != p)
- ps[j++] = p = ps[i];
- ps.shrink(i - j);
- } else {
- // Lemma
- vec<Lit> assigned_lits;
- Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl;
- bool lemmaSatisfied = false;
- for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- if (ps[i] == ~p) {
- // We don't add clauses that represent splits directly, they are decision literals
- // so they will get decided upon and sent to the theory
- Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl;
- return true;
- }
- if (value(ps[i]) == l_Undef) {
- // Anything not having a value gets added
- if (ps[i] != p) {
- ps[j++] = p = ps[i];
- }
- } else {
- // If the literal has a value it gets added to the end of the clause
- p = ps[i];
- if (value(p) == l_True) lemmaSatisfied = true;
- assigned_lits.push(p);
- Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl;
- }
- }
- Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!");
- // If only one literal we could have unit propagation
- if (j == 1 && !lemmaSatisfied) propagate_first_literal = true;
- int max_level = -1;
- int max_level_j = -1;
- for (int assigned_i = 0; assigned_i < assigned_lits.size(); ++ assigned_i) {
- ps[j++] = p = assigned_lits[assigned_i];
- if (level(var(p)) > max_level && value(p) == l_False) {
- max_level = level(var(p));
- max_level_j = j - 1;
- }
- }
- if (value(ps[1]) != l_Undef && max_level != -1) {
- std::swap(ps[1], ps[max_level_j]);
- }
- ps.shrink(i - j);
+
+ // Check the clause for tautologies and similar
+ for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+ if ((ps[i] == ~p) || (value(ps[i]) == l_True && level(var(ps[i])) == 0)) {
+ // Clause can be ignored
+ return true;
+ }
+ if ((ps[i] != p) && (value(ps[i]) != l_False || level(var(ps[i])) > 0)) {
+ // This literal is a keeper
+ ps[j++] = p = ps[i];
+ }
}
- if (ps.size() == 0)
- return ok = false;
- else if (ps.size() == 1){
- if(in_solve) {
- assert(type != CLAUSE_LEMMA);
- assert(value(ps[0]) == l_Undef);
- } else {
- // [MGD] at "pre-solve" time we allow unit T-lemmas
- if(value(ps[0]) == l_True) {
- // this unit T-lemma is extraneous (perhaps it was
- // discovered twice at presolve time)
- return true;
- }
- assert(value(ps[0]) == l_Undef);
- }
+ // Fit to size
+ ps.shrink(i - j);
+
+
+ // If we are in solve or decision level > 0
+ if (minisat_busy || decisionLevel() > 0) {
+ lemmas.push();
+ ps.copyTo(lemmas.last());
+ lemmas_removable.push(removable);
+ } else {
+ // Add the clause and attach if not a lemma
+ if (ps.size() == 0) {
+ return ok = false;
+ } else if (ps.size() == 1) {
uncheckedEnqueue(ps[0]);
return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
- }else{
- CRef cr = ca.alloc(type == CLAUSE_LEMMA ? 0 : assertionLevel, ps, false);
- clauses.push(cr);
+ } else {
+ CRef cr = ca.alloc(assertionLevel, ps, false);
+ clauses_persistent.push(cr);
attachClause(cr);
- if (propagate_first_literal) {
- Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl;
- lemma_propagated_literals.push(ps[0]);
- lemma_propagated_reasons.push(cr);
- propagating_lemmas.push(cr);
- }
- }
-
- if (type == CLAUSE_LEMMA) {
- problem_extended = true;
+ }
}
return true;
Assert(c.size() > 1);
watches[~c[0]].push(Watcher(cr, c[1]));
watches[~c[1]].push(Watcher(cr, c[0]));
- if (c.learnt()) learnts_literals += c.size();
+ if (c.removable()) learnts_literals += c.size();
else clauses_literals += c.size(); }
watches.smudge(~c[1]);
}
- if (c.learnt()) learnts_literals -= c.size();
+ if (c.removable()) learnts_literals -= c.size();
else clauses_literals -= c.size(); }
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
//
-void Solver::cancelUntil(int level, bool re_propagate) {
+void Solver::cancelUntil(int level) {
if (decisionLevel() > level){
// Pop the SMT context
for (int l = trail_lim.size() - level; l > 0; --l)
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
-
- // Re-Propagate the lemmas if asked
- if (re_propagate) {
- rePropagate(level);
- }
- }
-}
-
-CRef Solver::rePropagate(int level) {
- // Propagate the lemma literals
- int i, j;
- for (i = j = propagating_lemmas_lim[level]; i < propagating_lemmas.size(); ++ i) {
- Clause& lemma = ca[propagating_lemmas[i]];
- bool propagating = value(var(lemma[0])) == l_Undef;;
- for(int lit = 1; lit < lemma.size() && propagating; ++ lit) {
- if (value(var(lemma[lit])) != l_False) {
- propagating = false;
- break;
- }
- }
- if (propagating) {
- if (value(lemma[0]) != l_Undef) {
- if (value(lemma[0]) == l_False) {
- // Conflict
- return propagating_lemmas[i];
- } else {
- // Already there
- continue;
- }
- }
- // Propagate
- uncheckedEnqueue(lemma[0], propagating_lemmas[i]);
- // Remember the lemma
- propagating_lemmas[j++] = propagating_lemmas[i];
}
- }
- Assert(i >= j);
- propagating_lemmas.shrink(propagating_lemmas.size() - j);
- Assert(propagating_lemmas_lim.size() >= level);
- propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level);
-
- // No conflict
- return CRef_Undef;
}
void Solver::popTrail() {
max_level = c.level();
}
- if (c.learnt())
+ if (c.removable())
claBumpActivity(c);
for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
{
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
- vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)));
+ vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
trail.push_(p);
if (theory[var(p)]) {
// Enqueue to the theory
{
CRef confl = CRef_Undef;
+ ScopedBool scoped_bool(minisat_busy, true);
+
+ // If we are not in the quick mode add the lemmas that were left begind
+ if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) {
+ confl = updateLemmas();
+ if (confl != CRef_Undef) {
+ return confl;
+ }
+ }
+
// If this is the final check, no need for Boolean propagation and
// theory propagation
if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
- confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
- return confl;
+ // Do the theory check
+ theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+ // If there are lemmas (or conflicts) update them
+ if (lemmas.size() > 0) {
+ return updateLemmas();
+ }
}
// The effort we will be using to theory check
// Keep running until we have checked everything, we
// have no conflict and no new literals have been asserted
- bool new_assertions;
do {
- new_assertions = false;
- while(qhead < trail.size()) {
- confl = propagateBool();
- if (confl != CRef_Undef) break;
- confl = theoryCheck(effort);
- if (confl != CRef_Undef) break;
- }
+ do {
+ // Propagate on the clauses
+ confl = propagateBool();
+
+ // If no conflict, do the theory check
+ if (confl == CRef_Undef) {
+ // Do the theory check
+ theoryCheck(effort);
+ // If there are lemmas (or conflicts) update them
+ if (lemmas.size() > 0) {
+ confl = updateLemmas();
+ }
+ }
+ } while (confl == CRef_Undef && qhead < trail.size());
+ // If still consistent do some theory propagation
if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) {
- new_assertions = propagateTheory();
- if (!new_assertions) break;
+ propagateTheory();
+ if (lemmas.size() > 0) {
+ confl = updateLemmas();
+ }
}
- } while (new_assertions);
+
+ } while (confl == CRef_Undef && qhead < trail.size());
return confl;
}
-bool Solver::propagateTheory() {
+void Solver::propagateTheory() {
std::vector<Lit> propagatedLiterals;
proxy->theoryPropagate(propagatedLiterals);
const unsigned i_end = propagatedLiterals.size();
uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy);
}
proxy->clearPropagatedLiterals();
- return propagatedLiterals.size() > 0;
}
/*_________________________________________________________________________________________________
|
| Note: the propagation queue might be NOT empty
|________________________________________________________________________________________________@*/
-CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
+void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
{
- CRef c = CRef_Undef;
- SatClause clause;
- proxy->theoryCheck(effort, clause);
- int clause_size = clause.size();
- if(clause_size > 0) {
- // Find the max level of the conflict
- int max_level = 0;
- int max_intro_level = 0;
- for (int i = 0; i < clause_size; ++i) {
- Var v = var(clause[i]);
- int current_level = level(v);
- int current_intro_level = intro_level(v);
- Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(v) << " at level " << current_level << std::endl;
- Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!");
- if (current_level > max_level) max_level = current_level;
- if (current_intro_level > max_intro_level) max_intro_level = current_intro_level;
- }
- // Unit conflict, we just duplicate the first literal
- if (clause_size == 1) {
- clause.push(clause[0]);
- Debug("unit-conflict") << "Unit conflict" << proxy->getNode(clause[0]) << std::endl;
- }
- // If smaller than the decision level then pop back so we can analyse
- Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
- Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!");
- if (max_level < decisionLevel()) {
- Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
- cancelUntil(max_level);
- }
- // Create the new clause and attach all the information (level 0)
- c = ca.alloc(max_intro_level, clause, true);
- learnts.push(c);
- attachClause(c);
- }
- return c;
+ proxy->theoryCheck(effort);
}
/*_________________________________________________________________________________________________
void Solver::reduceDB()
{
int i, j;
- double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity
+ double extra_lim = cla_inc / clauses_removable.size(); // Remove any clause below this activity
- sort(learnts, reduceDB_lt(ca));
+ sort(clauses_removable, reduceDB_lt(ca));
// Don't delete binary or locked clauses. From the rest, delete clauses from the first half
// and clauses with activity smaller than 'extra_lim':
- for (i = j = 0; i < learnts.size(); i++){
- Clause& c = ca[learnts[i]];
- if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
- removeClause(learnts[i]);
+ for (i = j = 0; i < clauses_removable.size(); i++){
+ Clause& c = ca[clauses_removable[i]];
+ if (c.size() > 2 && !locked(c) && (i < clauses_removable.size() / 2 || c.activity() < extra_lim))
+ removeClause(clauses_removable[i]);
else
- learnts[j++] = learnts[i];
+ clauses_removable[j++] = clauses_removable[i];
}
- learnts.shrink(i - j);
+ clauses_removable.shrink(i - j);
checkGarbage();
}
return true;
// Remove satisfied clauses:
- removeSatisfied(learnts);
+ removeSatisfied(clauses_removable);
if (remove_satisfied) // Can be turned off.
- removeSatisfied(clauses);
+ removeSatisfied(clauses_persistent);
checkGarbage();
rebuildOrderHeap();
starts++;
TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
- for (;;){
+ for (;;) {
- // If we have more assertions from lemmas, we continue
- if (problem_extended) {
-
- Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl;
+ // Propagate and call the theory solvers
+ CRef confl = propagate(check_type);
+ Assert(lemmas.size() == 0);
- for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
- if (value(var(lemma_propagated_literals[i])) == l_Undef) {
- Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl;
- uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
- }
- }
+ if (confl != CRef_Undef) {
- lemma_propagated_literals.clear();
- lemma_propagated_reasons.clear();
+ conflicts++; conflictC++;
- check_type = CHECK_WITH_PROPAGATION_STANDARD;
- problem_extended = false;
- }
+ if (decisionLevel() == 0) return l_False;
- CRef confl = propagate(check_type);
- if (confl != CRef_Undef){
- // Clear the propagated literals
- lemma_propagated_literals.clear();
- lemma_propagated_reasons.clear();
-
- // CONFLICT
- while (confl != CRef_Undef) {
- conflicts++; conflictC++;
- if (decisionLevel() == 0) return l_False;
-
- // Analyze the conflict
- learnt_clause.clear();
- int max_level = analyze(confl, learnt_clause, backtrack_level);
- cancelUntil(backtrack_level, false);
-
- // Assert the conflict clause and the asserting literal
- if (learnt_clause.size() == 1){
- uncheckedEnqueue(learnt_clause[0]);
- }else{
- CRef cr = ca.alloc(max_level, learnt_clause, true);
- learnts.push(cr);
- attachClause(cr);
- claBumpActivity(ca[cr]);
- uncheckedEnqueue(learnt_clause[0], cr);
- }
+ // Analyze the conflict
+ learnt_clause.clear();
+ int max_level = analyze(confl, learnt_clause, backtrack_level);
+ cancelUntil(backtrack_level);
- // We repropagate lemmas
- confl = rePropagate(backtrack_level);
- };
+ // Assert the conflict clause and the asserting literal
+ if (learnt_clause.size() == 1) {
+ uncheckedEnqueue(learnt_clause[0]);
+ } else {
+ CRef cr = ca.alloc(max_level, learnt_clause, true);
+ clauses_removable.push(cr);
+ attachClause(cr);
+ claBumpActivity(ca[cr]);
+ uncheckedEnqueue(learnt_clause[0], cr);
+ }
varDecayActivity();
claDecayActivity();
(int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
}
- // We have a conflict so, we are going back to standard checks
+ // We have a conflict so, we are going back to standard checks
check_type = CHECK_WITH_PROPAGATION_STANDARD;
- }else{
-
- // NO CONFLICT
- if (problem_extended)
- continue;
+ } else {
// If this was a final check, we are satisfiable
- if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
- return l_True;
+ if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+ // Unless a lemma has added more stuff to the queues
+ if (!order_heap.empty() || qhead < trail.size()) {
+ check_type = CHECK_WITH_PROPAGATION_STANDARD;
+ continue;
+ } else {
+ // Yes, we're truly satisfiable
+ return l_True;
+ }
+ }
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+ if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
// Reached bound on number of conflicts:
progress_estimate = progressEstimate();
cancelUntil(0);
// [mdeters] notify theory engine of restarts for deferred
// theory processing
proxy->notifyRestart();
- return l_Undef; }
+ return l_Undef;
+ }
// Simplify the set of problem clauses:
- if (decisionLevel() == 0 && !simplify())
+ if (decisionLevel() == 0 && !simplify()) {
return l_False;
+ }
- if (learnts.size()-nAssigns() >= max_learnts)
+ if (clauses_removable.size()-nAssigns() >= max_learnts) {
// Reduce the set of learnt clauses:
reduceDB();
+ }
Lit next = lit_Undef;
- while (decisionLevel() < assumptions.size()){
+ while (decisionLevel() < assumptions.size()) {
// Perform user provided assumption:
Lit p = assumptions[decisionLevel()];
- if (value(p) == l_True){
+ if (value(p) == l_True) {
// Dummy decision level:
newDecisionLevel();
- }else if (value(p) == l_False){
+ } else if (value(p) == l_False) {
analyzeFinal(~p, conflict);
return l_False;
- }else{
+ } else {
next = p;
break;
}
}
- if (next == lit_Undef){
+ if (next == lit_Undef) {
// New variable decision:
decisions++;
next = pickBranchLit();
{
Debug("minisat") << "nvars = " << nVars() << std::endl;
- in_solve = true;
+ ScopedBool scoped_bool(minisat_busy, true);
model.clear();
conflict.clear();
if (!ok){
- in_solve = false;
+ minisat_busy = false;
return l_False;
}
// Cancel the trail downto previous push
popTrail();
- in_solve = false;
-
return status;
}
// Cannot use removeClauses here because it is not safe
// to deallocate them at this point. Could be improved.
int cnt = 0;
- for (int i = 0; i < clauses.size(); i++)
- if (!satisfied(ca[clauses[i]]))
+ for (int i = 0; i < clauses_persistent.size(); i++)
+ if (!satisfied(ca[clauses_persistent[i]]))
cnt++;
- for (int i = 0; i < clauses.size(); i++)
- if (!satisfied(ca[clauses[i]])){
- Clause& c = ca[clauses[i]];
+ for (int i = 0; i < clauses_persistent.size(); i++)
+ if (!satisfied(ca[clauses_persistent[i]])){
+ Clause& c = ca[clauses_persistent[i]];
for (int j = 0; j < c.size(); j++)
if (value(c[j]) != l_False)
mapVar(var(c[j]), map, max);
fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
}
- for (int i = 0; i < clauses.size(); i++)
- toDimacs(f, ca[clauses[i]], map, max);
+ for (int i = 0; i < clauses_persistent.size(); i++)
+ toDimacs(f, ca[clauses_persistent[i]], map, max);
if (verbosity > 0)
printf("Wrote %d clauses with %d variables.\n", cnt, max);
for (int i = 0; i < trail.size(); i++){
Var v = var(trail[i]);
- if (hasReason(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
+ if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
ca.reloc(vardata[v].reason, to);
}
// All learnt:
//
- for (int i = 0; i < learnts.size(); i++)
- ca.reloc(learnts[i], to);
+ for (int i = 0; i < clauses_removable.size(); i++)
+ ca.reloc(clauses_removable[i], to);
// All original:
//
- for (int i = 0; i < clauses.size(); i++)
- ca.reloc(clauses[i], to);
-
- // All lemmas
- //
- for (int i = 0; i < lemma_propagated_reasons.size(); i ++)
- ca.reloc(lemma_propagated_reasons[i], to);
- for (int i = 0; i < propagating_lemmas.size(); i ++)
- ca.reloc(propagating_lemmas[i], to);
+ for (int i = 0; i < clauses_persistent.size(); i++)
+ ca.reloc(clauses_persistent[i], to);
}
if (enable_incremental) {
-- assertionLevel;
// Remove all the clauses asserted (and implied) above the new base level
- removeClausesAboveLevel(learnts, assertionLevel);
- removeClausesAboveLevel(clauses, assertionLevel);
+ removeClausesAboveLevel(clauses_removable, assertionLevel);
+ removeClausesAboveLevel(clauses_persistent, assertionLevel);
// Pop the user trail size
popTrail();
setDecisionVar(v, true);
}
+CRef Solver::updateLemmas() {
+
+ Debug("minisat::lemmas") << "Solver::updateLemmas()" << std::endl;
+
+ CRef conflict = CRef_Undef;
+
+ // Decision level to backtrack to
+ int backtrackLevel = decisionLevel();
+
+ // We use this comparison operator
+ lemma_lt lt(*this);
+
+ // Check for propagation and level to backtrack to
+ for (int i = 0; i < lemmas.size(); ++ i)
+ {
+ // The current lemma
+ vec<Lit>& lemma = lemmas[i];
+ // If it's an empty lemma, we have a conflict at zero level
+ if (lemma.size() == 0) {
+ conflict = CRef_Lazy;
+ backtrackLevel = 0;
+ Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
+ continue;
+ }
+ // Sort the lemma to be able to attach
+ sort(lemma, lt);
+ // See if the lemma propagates something
+ if (lemma.size() == 1 || value(lemma[1]) == l_False) {
+ // This lemma propagates, see which level we need to backtrack to
+ int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
+ // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
+ if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
+ if (currentBacktrackLevel < backtrackLevel) {
+ backtrackLevel = currentBacktrackLevel;
+ }
+ }
+ }
+ }
+
+ // Pop so that propagation would be current
+ Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
+ cancelUntil(backtrackLevel);
+
+ // Last index in the trail
+ int backtrack_index = trail.size();
+
+ // Attach all the clauses and enqueue all the propagations
+ for (int i = 0; i < lemmas.size(); ++ i)
+ {
+ // The current lemma
+ vec<Lit>& lemma = lemmas[i];
+ bool removable = lemmas_removable[i];
+
+ // Attach it if non-unit
+ CRef lemma_ref = CRef_Undef;
+ if (lemma.size() > 1) {
+ lemma_ref = ca.alloc(assertionLevel, lemma, removable);
+ if (removable) {
+ clauses_removable.push(lemma_ref);
+ } else {
+ clauses_persistent.push(lemma_ref);
+ }
+ attachClause(lemma_ref);
+ }
+
+ // If the lemma is propagating enqueue it's literal (or set the conflict)
+ if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
+ if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
+ if (value(lemma[0]) == l_False) {
+ // We have a conflict
+ if (lemma.size() > 1) {
+ Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl;
+ conflict = lemma_ref;
+ } else {
+ Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
+ conflict = CRef_Lazy;
+ }
+ } else {
+// if (Debug.isOn("minisat::lemmas")) {
+// Debug("minisat::lemmas") << "Solver::updateLemmas(): " << lemma[0] << " from ";
+// Clause& c = ca[lemma_ref];
+// for (int i = 0; i < c.size(); ++ i) {
+// Debug("minisat::lemmas") << c[i] << "(" << value(c[i]) << "," << level(var(c[i])) << "," << trail_index(var(c[i])) << ") ";
+// }
+// Debug("minisat::lemmas") << std::endl;
+// }
+ uncheckedEnqueue(lemma[0], lemma_ref);
+ }
+ }
+ }
+ }
+
+ // Clear the lemmas
+ lemmas.clear();
+ lemmas_removable.clear();
+ return conflict;
+}
/** Do we allow incremental solving */
bool enable_incremental;
- /** Did the problem get extended in the meantime (i.e. by adding a lemma) */
- bool problem_extended;
-
/** Literals propagated by lemmas */
- vec<Lit> lemma_propagated_literals;
- /** Reasons of literals propagated by lemmas */
- vec<CRef> lemma_propagated_reasons;
- /** Lemmas that propagated something, we need to recheck them after backtracking */
- vec<CRef> propagating_lemmas;
- vec<int> propagating_lemmas_lim;
+ vec< vec<Lit> > lemmas;
+
+ /** Is the lemma removable */
+ vec<bool> lemmas_removable;
/** Shrink 'cs' to contain only clauses below given level */
void removeClausesAboveLevel(vec<CRef>& cs, int level);
/** True if we are currently solving. */
- bool in_solve;
+ bool minisat_busy;
public:
//
Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
- // Types of clauses
- enum ClauseType {
- // Clauses defined by the problem
- CLAUSE_PROBLEM,
- // Lemma clauses added by the theories
- CLAUSE_LEMMA,
- // Conflict clauses
- CLAUSE_CONFLICT
+ // Less than for literals in a lemma
+ struct lemma_lt {
+ Solver& solver;
+ lemma_lt(Solver& solver) : solver(solver) {}
+ bool operator () (Lit x, Lit y) {
+ lbool x_value = solver.value(x);
+ lbool y_value = solver.value(y);
+ // Two unassigned literals are sorted arbitrarily
+ if (x_value == l_Undef && y_value == l_Undef) {
+ return x < y;
+ }
+ // Unassigned literals are put to front
+ if (x_value == l_Undef) return true;
+ if (y_value == l_Undef) return false;
+ // Literals of the same value are sorted by decreasing levels
+ if (x_value == y_value) {
+ return solver.trail_index(var(x)) > solver.trail_index(var(y));
+ } else {
+ // True literals go up front
+ if (x_value == l_True) {
+ return true;
+ } else {
+ return false;
+ }
+ }
+ }
};
+
// CVC4 context push/pop
void push ();
void pop ();
void unregisterVar(Lit lit); // Unregister the literal (set assertion level to -1)
void renewVar(Lit lit, int level = -1); // Register the literal (set assertion level to the given level, or current level if -1)
- bool addClause (const vec<Lit>& ps, ClauseType type); // Add a clause to the solver.
- bool addEmptyClause(ClauseType type); // Add the empty clause, making the solver contradictory.
- bool addClause (Lit p, ClauseType type); // Add a unit clause to the solver.
- bool addClause (Lit p, Lit q, ClauseType type); // Add a binary clause to the solver.
- bool addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver.
- bool addClause_( vec<Lit>& ps, ClauseType type); // Add a clause to the solver without making superflous internal copy. Will
+ bool addClause (const vec<Lit>& ps, bool removable); // Add a clause to the solver.
+ bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory.
+ bool addClause (Lit p, bool removable); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
+ bool addClause_( vec<Lit>& ps, bool removable); // Add a clause to the solver without making superflous internal copy. Will
// change the passed vector 'ps'.
// Solving:
// Helper structures:
//
- struct VarData { CRef reason; int level; int intro_level; };
- static inline VarData mkVarData(CRef cr, int l, int intro_l){ VarData d = {cr, l, intro_l}; return d; }
+ struct VarData { CRef reason; int level; int intro_level; int trail_index; };
+ static inline VarData mkVarData(CRef cr, int l, int intro_l, int trail_i){ VarData d = {cr, l, intro_l, trail_i}; return d; }
struct Watcher {
CRef cref;
// Solver state:
//
- bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
- vec<CRef> clauses; // List of problem clauses.
- vec<CRef> learnts; // List of learnt clauses.
- double cla_inc; // Amount to bump next clause with.
- vec<double> activity; // A heuristic measurement of the activity of a variable.
- double var_inc; // Amount to bump next variable with.
+ bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+ vec<CRef> clauses_persistent; // List of problem clauses.
+ vec<CRef> clauses_removable; // List of learnt clauses.
+ double cla_inc; // Amount to bump next clause with.
+ vec<double> activity; // A heuristic measurement of the activity of a variable.
+ double var_inc; // Amount to bump next variable with.
OccLists<Lit, vec<Watcher>, WatcherDeleted>
- watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
- vec<lbool> assigns; // The current assignments.
- vec<char> polarity; // The preferred polarity of each variable.
- vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
- vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
- vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
- vec<int> trail_user_lim; // Separator indices for different user push levels in 'trail'.
- vec<VarData> vardata; // Stores reason and level for each variable.
- int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
- int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
- int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
- vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
- Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
- double progress_estimate;// Set by 'search()'.
- bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
+ watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+ vec<lbool> assigns; // The current assignments.
+ vec<char> polarity; // The preferred polarity of each variable.
+ vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
+ vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
+ vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
+ vec<int> trail_user_lim; // Separator indices for different user push levels in 'trail'.
+ vec<VarData> vardata; // Stores reason and level for each variable.
+ int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+ int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
+ int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
+ vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
+ Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
+ double progress_estimate; // Set by 'search()'.
+ bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
ClauseAllocator ca;
bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
CRef propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause.
CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause.
- bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted.
- CRef theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause.
- void cancelUntil (int level, bool re_propagate = true); // Backtrack until a certain level.
- CRef rePropagate (int level); // Re-propagate on lemmas, returns a concflict clause if it introduces a conflict
+ void propagateTheory (); // Perform Theory propagation.
+ void theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas.
+ CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one
+ void cancelUntil (int level); // Backtrack until a certain level.
void popTrail (); // Backtrack the trail to the previous push position
int analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
//
int decisionLevel () const; // Gives the current decisionlevel.
uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
- CRef reason (Var x) const;
- bool hasReason (Var x) const; // Does the variable have a reason
+ CRef reason (Var x); // Get the reason of the variable (non const as it might create the explanation on the fly)
+ bool hasReasonClause (Var x) const; // Does the variable have a reason
+ bool isPropagated (Var x) const; // Does the variable have a propagated variables
+ bool isPropagatedBy (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C
+
int level (Var x) const;
int intro_level (Var x) const; // Level at which this variable was introduced
+ int trail_index (Var x) const; // Index in the trail
double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
bool withinBudget () const;
//=================================================================================================
// Implementation of inline methods:
-inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+
+inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; }
+
+inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; }
inline int Solver::level (Var x) const { return vardata[x].level; }
inline int Solver::intro_level(Var x) const { return vardata[x].intro_level; }
+inline int Solver::trail_index(Var x) const { return vardata[x].trail_index; }
+
inline void Solver::insertVarOrder(Var x) {
if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
inline void Solver::claBumpActivity (Clause& c) {
if ( (c.activity() += cla_inc) > 1e20 ) {
// Rescale:
- for (int i = 0; i < learnts.size(); i++)
- ca[learnts[i]].activity() *= 1e-20;
+ for (int i = 0; i < clauses_removable.size(); i++)
+ ca[clauses_removable[i]].activity() *= 1e-20;
cla_inc *= 1e-20; } }
inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
// NOTE: enqueue does not set the ok flag! (only public methods do)
inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
-inline bool Solver::addClause (const vec<Lit>& ps, ClauseType type) { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
-inline bool Solver::addEmptyClause (ClauseType type) { add_tmp.clear(); return addClause_(add_tmp, type); }
-inline bool Solver::addClause (Lit p, ClauseType type) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); }
-inline bool Solver::addClause (Lit p, Lit q, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); }
-inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); }
-inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
-inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); propagating_lemmas_lim.push(propagating_lemmas.size()); context->push(); }
+inline bool Solver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
+inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); }
+inline bool Solver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
+inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
+inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
+inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
inline lbool Solver::modelValue (Var x) const { return model[x]; }
inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
inline int Solver::nAssigns () const { return trail.size(); }
-inline int Solver::nClauses () const { return clauses.size(); }
-inline int Solver::nLearnts () const { return learnts.size(); }
+inline int Solver::nClauses () const { return clauses_persistent.size(); }
+inline int Solver::nLearnts () const { return clauses_removable.size(); }
inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
class Clause {
struct {
unsigned mark : 2;
- unsigned learnt : 1;
+ unsigned removable : 1;
unsigned has_extra : 1;
unsigned reloced : 1;
unsigned size : 27;
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
template<class V>
- Clause(const V& ps, bool use_extra, bool learnt, int level) {
+ Clause(const V& ps, bool use_extra, bool removable, int level) {
header.mark = 0;
- header.learnt = learnt;
+ header.removable = removable;
header.has_extra = use_extra;
header.reloced = 0;
header.size = ps.size();
data[i].lit = ps[i];
if (header.has_extra){
- if (header.learnt)
+ if (header.removable)
data[header.size].act = 0;
else
calcAbstraction(); }
int size () const { return header.size; }
void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
void pop () { shrink(1); }
- bool learnt () const { return header.learnt; }
+ bool removable () const { return header.removable; }
bool has_extra () const { return header.has_extra; }
uint32_t mark () const { return header.mark; }
void mark (uint32_t m) { header.mark = m; }
RegionAllocator<uint32_t>::moveTo(to); }
template<class Lits>
- CRef alloc(int level, const Lits& ps, bool learnt = false)
+ CRef alloc(int level, const Lits& ps, bool removable = false)
{
assert(sizeof(Lit) == sizeof(uint32_t));
assert(sizeof(float) == sizeof(uint32_t));
- bool use_extra = learnt | extra_clause_field;
+ bool use_extra = removable | extra_clause_field;
CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
- new (lea(cid)) Clause(ps, use_extra, learnt, level);
+ new (lea(cid)) Clause(ps, use_extra, removable, level);
return cid;
}
if (c.reloced()) { cr = c.relocation(); return; }
- cr = to.alloc(c.level(), c, c.learnt());
+ cr = to.alloc(c.level(), c, c.removable());
c.relocate(cr);
// Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
- if (to[cr].learnt()) to[cr].activity() = c.activity();
+ if (to[cr].removable()) to[cr].activity() = c.activity();
else if (to[cr].has_extra()) to[cr].calcAbstraction();
}
};
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
- assert(!header.learnt); assert(!other.header.learnt);
+ assert(!header.removable); assert(!other.header.removable);
assert(header.has_extra); assert(other.header.has_extra);
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
return lit_Error;
-bool SimpSolver::addClause_(vec<Lit>& ps, ClauseType type)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
{
#ifndef NDEBUG
for (int i = 0; i < ps.size(); i++)
assert(!isEliminated(var(ps[i])));
#endif
- int nclauses = clauses.size();
+ int nclauses = clauses_persistent.size();
if (use_rcheck && implied(ps))
return true;
- if (!Solver::addClause_(ps, type))
+ if (!Solver::addClause_(ps, removable))
return false;
- if (use_simplification && clauses.size() == nclauses + 1){
- CRef cr = clauses.last();
+ if (use_simplification && clauses_persistent.size() == nclauses + 1){
+ CRef cr = clauses_persistent.last();
const Clause& c = ca[cr];
// NOTE: the clause is added to the queue immediately and then
// Produce clauses in cross product:
vec<Lit>& resolvent = add_tmp;
for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, CLAUSE_CONFLICT))
+ for (int j = 0; j < neg.size(); j++) {
+ bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
+ if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) {
return false;
+ }
+ }
// Free occurs list for this variable:
occurs[v].clear(true);
removeClause(cls[i]);
- if (!addClause_(subst_clause, CLAUSE_PROBLEM))
+ if (!addClause_(subst_clause, c.removable())) {
return ok = false;
+ }
}
return true;
{
occurs.cleanAll();
int i,j;
- for (i = j = 0; i < clauses.size(); i++)
- if (ca[clauses[i]].mark() == 0)
- clauses[j++] = clauses[i];
- clauses.shrink(i - j);
+ for (i = j = 0; i < clauses_persistent.size(); i++)
+ if (ca[clauses_persistent[i]].mark() == 0)
+ clauses_persistent[j++] = clauses_persistent[i];
+ clauses_persistent.shrink(i - j);
}
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false);
- bool addClause (const vec<Lit>& ps, ClauseType type);
- bool addEmptyClause(ClauseType type); // Add the empty clause to the solver.
- bool addClause (Lit p, ClauseType type); // Add a unit clause to the solver.
- bool addClause (Lit p, Lit q, ClauseType type); // Add a binary clause to the solver.
- bool addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver.
- bool addClause_(vec<Lit>& ps, ClauseType type);
+ bool addClause (const vec<Lit>& ps, bool removable);
+ bool addEmptyClause(bool removable); // Add the empty clause to the solver.
+ bool addClause (Lit p, bool removable); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
+ bool addClause_(vec<Lit>& ps, bool removable);
bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
// Variable mode:
elim_heap.update(v); }
-inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseType type) { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addEmptyClause(ClauseType type) { add_tmp.clear(); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause (Lit p, ClauseType type) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause (Lit p, Lit q, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false);
}
-void PropEngine::assertLemma(TNode node) {
+void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
//TODO This comment is now false
// Assert as removable
- d_cnfStream->convertAndAssert(node, true, false);
+ d_cnfStream->convertAndAssert(node, removable, negated);
}
void PropEngine::printSatisfyingAssignment(){
*
* @param node the formula to assert
*/
- void assertLemma(TNode node);
+ void assertLemma(TNode node, bool negated, bool removable);
/**
* Checks the current context for satisfiability.
namespace CVC4 {
namespace prop {
-void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
- Assert(conflict.size() == 0);
- // Try theory propagation
- bool ok = d_theoryEngine->check(effort);
- // If in conflict construct the conflict clause
- if (!ok) {
- // We have a conflict, get it
- Node conflictNode = d_theoryEngine->getConflict();
- Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
- if(conflictNode.getKind() == kind::AND) {
- // Go through the literals and construct the conflict clause
- Node::const_iterator literal_it = conflictNode.begin();
- Node::const_iterator literal_end = conflictNode.end();
- while (literal_it != literal_end) {
- // Get the literal corresponding to the node
- SatLiteral l = d_cnfStream->getLiteral(*literal_it);
- // Add the negation to the conflict clause and continue
- conflict.push(~l);
- literal_it ++;
- }
- } else { // unit conflict
- // Get the literal corresponding to the node
- SatLiteral l = d_cnfStream->getLiteral(conflictNode);
- // construct the unit conflict clause
- conflict.push(~l);
- }
- }
+void SatSolver::theoryCheck(theory::Theory::Effort effort) {
+ d_theoryEngine->check(effort);
}
void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
/** Virtual destructor to make g++ happy */
virtual ~SatInputInterface() { }
/** Assert a clause in the solver. */
- virtual void addClause(SatClause& clause, bool lemma) = 0;
+ virtual void addClause(SatClause& clause, bool removable) = 0;
/** Create a new boolean variable in the solver. */
virtual SatVariable newVar(bool theoryAtom = false) = 0;
/** Get the current decision level of the solver */
bool solve();
- void addClause(SatClause& clause, bool lemma);
+ void addClause(SatClause& clause, bool removable);
SatVariable newVar(bool theoryAtom = false);
- void theoryCheck(theory::Theory::Effort effort, SatClause& conflict);
+ void theoryCheck(theory::Theory::Effort effort);
void explainPropagation(SatLiteral l, SatClause& explanation);
return d_minisat->solve();
}
-inline void SatSolver::addClause(SatClause& clause, bool lemma) {
- d_minisat->addClause(clause, lemma ? Minisat::Solver::CLAUSE_LEMMA : Minisat::Solver::CLAUSE_PROBLEM);
+inline void SatSolver::addClause(SatClause& clause, bool removable) {
+ d_minisat->addClause(clause, removable);
}
inline SatVariable SatSolver::newVar(bool theoryAtom) {
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
*/
-bool TheoryEngine::check(theory::Theory::Effort effort) {
- d_theoryOut.d_conflictNode = Node::null();
+void TheoryEngine::check(theory::Theory::Effort effort) {
+
d_theoryOut.d_propagatedLiterals.clear();
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
- if (!d_theoryOut.d_conflictNode.get().isNull()) { \
- return false; \
+ if (d_theoryOut.d_inConflict) { \
+ return; \
} \
}
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => conflict" << std::endl;
}
-
- return true;
}
void TheoryEngine::propagate() {
// at doing something with the input formula, even if it wouldn't
// otherwise be active.
- d_theoryOut.d_conflictNode = Node::null();
d_theoryOut.d_propagatedLiterals.clear();
try {
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasPresolve) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
- if(!d_theoryOut.d_conflictNode.get().isNull()) { \
+ if(d_theoryOut.d_inConflict) { \
return true; \
} \
}
Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
}
// return whether we have a conflict
- return !d_theoryOut.d_conflictNode.get().isNull();
+ return false;
}
TheoryEngine* d_engine;
context::Context* d_context;
- context::CDO<Node> d_conflictNode;
+ context::CDO<bool> d_inConflict;
context::CDO<Node> d_explanationNode;
/**
d_newFactTimer,
"theory::newFactTimer");
+ /**
+ * Check if the node is in conflict for debug purposes
+ */
+ bool isProperConflict(TNode conflictNode) {
+ bool value;
+ if (conflictNode.getKind() == kind::AND) {
+ for (unsigned i = 0; i < conflictNode.getNumChildren(); ++ i) {
+ if (!d_engine->getPropEngine()->hasValue(conflictNode[i], value)) return false;
+ if (!value) return false;
+ }
+ } else {
+ if (!d_engine->getPropEngine()->hasValue(conflictNode, value)) return false;
+ return value;
+ }
+ return true;
+ }
+
public:
EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
d_engine(engine),
d_context(context),
- d_conflictNode(context),
+ d_inConflict(context, false),
d_explanationNode(context) {
}
void conflict(TNode conflictNode, bool safe)
throw(theory::Interrupted, AssertionException) {
- Trace("theory") << "EngineOutputChannel::conflict("
- << conflictNode << ")" << std::endl;
- d_conflictNode = conflictNode;
+ Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
+ d_inConflict = true;
+
++(d_engine->d_statistics.d_statConflicts);
+
+ // Construct the lemma (note that no CNF caching should happen as all the literals already exists)
+ Assert(isProperConflict(conflictNode));
+ d_engine->newLemma(conflictNode, true, true);
+
if(safe) {
throw theory::Interrupted();
}
++(d_engine->d_statistics.d_statPropagate);
}
- void lemma(TNode node, bool)
+ void lemma(TNode node, bool removable = false)
throw(theory::Interrupted, AssertionException) {
Trace("theory") << "EngineOutputChannel::lemma("
<< node << ")" << std::endl;
++(d_engine->d_statistics.d_statLemma);
- d_engine->newLemma(node);
+
+ d_engine->newLemma(node, false, removable);
}
void explanation(TNode explanationNode, bool)
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
*/
- bool check(theory::Theory::Effort effort);
+ void check(theory::Theory::Effort effort);
/**
* Calls staticLearning() on all theories, accumulating their
d_theoryOut.d_propagatedLiterals.clear();
}
- inline void newLemma(TNode node) {
+ inline void newLemma(TNode node, bool negated, bool removable) {
// Remove the ITEs and assert to prop engine
std::vector<Node> additionalLemmas;
additionalLemmas.push_back(node);
RemoveITE::run(additionalLemmas);
- for (unsigned i = 0; i < additionalLemmas.size(); ++ i) {
- d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]));
+ d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable);
+ for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
+ d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable);
}
}
- /**
- * Returns the last conflict (if any).
- */
- inline Node getConflict() {
- return d_theoryOut.d_conflictNode;
- }
-
void propagate();
inline Node getExplanation(TNode node, theory::Theory* theory) {
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::AND, a, b, c), false);
+ d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
TS_ASSERT( d_satSolver->addClauseCalled() );
}
d_nodeManager->mkNode(kind::OR, c, d),
d_nodeManager->mkNode(
kind::NOT,
- d_nodeManager->mkNode(kind::XOR, e, f)))), false );
+ d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
void testFalse() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false );
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IFF, a, b), false );
+ d_nodeManager->mkNode(kind::IFF, a, b), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IMPLIES, a, b), false );
+ d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
d_nodeManager->mkVar(d_nodeManager->integerType())
),
d_nodeManager->mkVar(d_nodeManager->integerType())
- ), false);
+ ), false, false);
}
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::NOT, a), false );
+ d_nodeManager->mkNode(kind::NOT, a), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::OR, a, b, c), false );
+ d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
void testTrue() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false );
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(a, false);
+ d_cnfStream->convertAndAssert(a, false, false);
TS_ASSERT( d_satSolver->addClauseCalled() );
d_satSolver->reset();
- d_cnfStream->convertAndAssert(b, false);
+ d_cnfStream->convertAndAssert(b, false, false);
TS_ASSERT( d_satSolver->addClauseCalled() );
}
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::XOR, a, b), false );
+ d_nodeManager->mkNode(kind::XOR, a, b), false, false );
TS_ASSERT( d_satSolver->addClauseCalled() );
}
};
projects / cvc5.git / commitdiff