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/uf | |
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/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 16 |
1 files changed, 1 insertions, 15 deletions
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) */ |