diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 17:53:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 17:53:41 +0000 |
commit | 5ec347a55a3b32e9d92d8a6a5d683cb9f3f3fee5 (patch) | |
tree | 871a53d147d218f926d53421b48db872c9d6747d /src/theory | |
parent | 9154e647013e4575f60807d5b73582bccfd052e2 (diff) |
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
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 16 |
3 files changed, 5 insertions, 25 deletions
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<TNode> 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) */ |