diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-14 09:31:21 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-14 09:31:21 +0000 |
| commit | ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e (patch) | |
| tree | eb972e4e0c0c61e3b1e1ddfc3637dec80e038d51 /src/theory/uf | |
| parent | 6d04f19e1c1fbf7714fbb95dc62648ac44b419dd (diff) | |
some more bug fixes (TNode -> Node, normalize literals in explanations)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e2462f244..2344adc70 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -137,9 +137,10 @@ void TheoryUF::propagate(Effort level) { } else { if (!satValue) { Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl; + Node negatedLiteral; std::vector<TNode> assumptions; if (literal != d_false) { - TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); + negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); assumptions.push_back(negatedLiteral); } explain(literal, assumptions); @@ -206,8 +207,9 @@ bool TheoryUF::propagate(TNode literal) { } else { Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl; std::vector<TNode> assumptions; + Node negatedLiteral; if (literal != d_false) { - TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); + negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); assumptions.push_back(negatedLiteral); } explain(literal, assumptions); |