d_propagatedLiterals.push_back(literal);
} else {
// Otherwise it might be a shared-term (dis-)equality
- Node normalizedEquality = Rewriter::rewrite(literal);
- if (d_propEngine->isSatLiteral(normalizedEquality)) {
+ Node normalizedLiteral = Rewriter::rewrite(literal);
+ if (d_propEngine->isSatLiteral(normalizedLiteral)) {
// If there is a literal, just enqueue it, same as above
bool value;
- if (d_propEngine->hasValue(normalizedEquality, value)) {
+ 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 << " (" << normalizedEquality << ") propagated by " << theory << " but already has a sat value" << std::endl;
- Assert((value && (literal.getKind() != kind::NOT)) || (!value && literal.getKind() == kind::NOT));
+ Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+ Assert(value);
} else {
- d_propagatedLiterals.push_back(normalizedEquality);
+ d_propagatedLiterals.push_back(normalizedLiteral);
}
}
// Otherwise, we assert it to all interested theories
SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId));
if (find == d_sharedAssertions.end()) {
// Not a shared assertion, just add it since it must be SAT literal
- builder << eqLiteral;
+ builder << Rewriter::rewrite(eqLiteral);
} else {
TheoryId explainingTheory = (*find).second.theory;
if (explainingTheory == theory::THEORY_LAST) {
}
}
}
-
} 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);
} 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);