From: Dejan Jovanović Date: Wed, 16 May 2012 17:53:41 +0000 (+0000) Subject: Changes to SAT solver: X-Git-Tag: cvc5-1.0.0~8164 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ec347a55a3b32e9d92d8a6a5d683cb9f3f3fee5;p=cvc5.git Changes to SAT solver: * allowing propagation of false literals (handles conflict) * allowing lemmas during BCP (bug 337) * UF does direct propagation, without checking for literal value anymore --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 71f252291..d220c4dbb 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -655,16 +655,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl; assert(value(p) == l_Undef); assigns[var(p)] = lbool(!sign(p)); - if(trail_index(var(p)) != -1) { - // This var is already represented in the trail, presumably from - // an earlier incarnation as a unit clause (it has been - // unregistered and renewed since then) - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail_index(var(p))); - trail[trail_index(var(p))] = p; - } else { - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); - trail.push_(p); - } + vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); + trail.push_(p); if (theory[var(p)]) { // Enqueue to the theory proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); @@ -680,8 +672,8 @@ CRef Solver::propagate(TheoryCheckType type) ScopedBool scoped_bool(minisat_busy, true); - // If we are not in the quick mode add the lemmas that were left behind - if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) { + // Add lemmas that we're left behind + if (lemmas.size() > 0) { confl = updateLemmas(); if (confl != CRef_Undef) { return confl; @@ -707,7 +699,7 @@ CRef Solver::propagate(TheoryCheckType type) // Keep running until we have checked everything, we // have no conflict and no new literals have been asserted - do { + do { // Propagate on the clauses confl = propagateBool(); @@ -725,8 +717,26 @@ CRef Solver::propagate(TheoryCheckType type) if (lemmas.size() > 0) { confl = updateLemmas(); } + } else { + // Even though in conflict, we still need to discharge the lemmas + if (lemmas.size() > 0) { + // Remember the trail size + int oldLevel = decisionLevel(); + // Update the lemmas + CRef lemmaConflict = updateLemmas(); + // If we get a conflict, we prefer it since it's earlier in the trail + if (lemmaConflict != CRef_Undef) { + // Lemma conflict takes precedence, since it's earlier in the trail + confl = lemmaConflict; + } else { + // Otherwise, the Boolean conflict is canceled in the case we popped the trail + if (oldLevel > decisionLevel()) { + confl = CRef_Undef; + } + } + } } - } while (confl == CRef_Undef && qhead < trail.size()); + } while (confl == CRef_Undef && qhead < trail.size()); return confl; } @@ -749,10 +759,14 @@ void Solver::propagateTheory() { if (value(p) == l_Undef) { uncheckedEnqueue(p, CRef_Lazy); } else { - // but we check that this is the case and that they agree - Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl; - Assert(trail_index(var(p)) >= oldTrailSize); - Assert(value(p) == l_True, "a literal was theory-propagated, and so was its negation"); + if (value(p) == l_False) { + Debug("minisat") << "Conflict in theory propagation" << std::endl; + SatClause explanation_cl; + proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); + vec explanation; + MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + addClause(explanation, true); + } } } } @@ -999,12 +1013,12 @@ lbool Solver::search(int nof_conflicts) if (confl != CRef_Undef) { - conflicts++; conflictC++; + conflicts++; conflictC++; - if (decisionLevel() == 0) { - PROOF( ProofManager::getSatProof()->finalizeProof(confl); ) - return l_False; - } + if (decisionLevel() == 0) { + PROOF( ProofManager::getSatProof()->finalizeProof(confl); ) + return l_False; + } // Analyze the conflict learnt_clause.clear(); @@ -1017,7 +1031,7 @@ lbool Solver::search(int nof_conflicts) PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); ) - } else { + } else { CRef cr = ca.alloc(max_level, learnt_clause, true); clauses_removable.push(cr); attachClause(cr); diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 4a2a5f135..e1ef51d09 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -30,7 +30,7 @@ std::string PreRegisterVisitor::toString() const { bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { - Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TheoryId currentTheoryId = Theory::theoryOf(current); @@ -134,7 +134,7 @@ std::string SharedTermsVisitor::toString() const { bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { - Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TNodeVisitedMap::const_iterator find = d_visited.find(current); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5a8a75aab..0ab188dc4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -772,14 +772,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Node normalizedLiteral = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedLiteral)) { // If there is a literal, propagate it to SAT - if (d_propEngine->hasValue(normalizedLiteral, value)) { - // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; - Assert(value); - } else { - SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); - d_propagatedSharedLiterals.push_back(sharedLiteral); - } + SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); + d_propagatedSharedLiterals.push_back(sharedLiteral); } // Assert to interested theories Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cddd01b07..7f173a0c4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -112,21 +112,7 @@ void TheoryUF::propagate(Effort level) { for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; - bool satValue; - Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector assumptions; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; - } + d_out->propagate(literal); } } }/* TheoryUF::propagate(Effort) */