diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 8caac6fb7..7688379d9 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -139,18 +139,15 @@ void TheoryUF::preRegisterTerm(TNode node) { } } -bool TheoryUF::propagate(TNode atom, bool isTrue) { - Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ")" << std::endl; +bool TheoryUF::propagate(TNode literal) { + Debug("uf") << "TheoryUF::propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << "): already in conflict" << std::endl; + Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; return false; } - // The literal - TNode literal = isTrue ? (Node) atom : atom.notNode(); - // See if the literal has been asserted already bool satValue = false; bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue); @@ -158,13 +155,13 @@ bool TheoryUF::propagate(TNode atom, bool isTrue) { // If asserted, we're done or in conflict if (isAsserted) { if (satValue) { - Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => already known" << std::endl; + Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl; return true; } else { - Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => conflict" << std::endl; + Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl; std::vector<TNode> assumptions; if (literal != d_false) { - TNode negatedLiteral = isTrue ? atom.notNode() : (Node) atom; + TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); assumptions.push_back(negatedLiteral); } explain(literal, assumptions); @@ -175,7 +172,7 @@ bool TheoryUF::propagate(TNode atom, bool isTrue) { } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => enqueuing for propagation" << std::endl; + Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); return true; @@ -195,6 +192,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { case kind::NOT: lhs = literal[0]; rhs = d_false; + break; case kind::CONST_BOOLEAN: // we get to explain true = false, since we set false to be the trigger of this lhs = d_true; |