diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 31 |
1 files changed, 13 insertions, 18 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4cdc5e240..e4a3ac78c 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -139,14 +139,14 @@ void TheoryUF::check(Effort level) { } } - - if (d_thss != NULL && ! d_conflict) { - d_thss->check(level); - if( d_thss->isConflict() ){ - d_conflict = true; + if(! d_conflict ){ + if (d_thss != NULL) { + d_thss->check(level); + if( d_thss->isConflict() ){ + d_conflict = true; + } } } - }/* TheoryUF::check() */ void TheoryUF::preRegisterTerm(TNode node) { @@ -217,7 +217,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); @@ -336,10 +336,10 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { if(n.getKind() == kind::OR && n.getNumChildren() == 2 && n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { + (n[0][0].getKind() == kind::EQUAL) && + (n[0][1].getKind() == kind::EQUAL) && + (n[1][0].getKind() == kind::EQUAL) && + (n[1][1].getKind() == kind::EQUAL)) { // now we have (a = b && c = d) || (e = f && g = h) Debug("diamonds") << "has form of a diamond!" << endl; @@ -396,7 +396,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { (a == h && d == e) ) { // learn: n implies a == d Debug("diamonds") << "+ C holds" << endl; - Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); + Node newEquality = a.eqNode(d); Debug("diamonds") << " ==> " << newEquality << endl; learned << n.impNode(newEquality); } else { @@ -533,12 +533,7 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; - - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b),pf); - } else { - d_conflictNode = explain(a.eqNode(b),pf); - } + d_conflictNode = explain(a.eqNode(b),pf); ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; |