From 1c2b7c593fa1c12575eb37e56a5c66a1a190ad81 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 28 Sep 2010 22:44:00 +0000 Subject: [PATCH] fix predicate bug in UF; code cleanup in theory.cpp --- src/theory/theory.cpp | 4 +- src/theory/uf/morgan/theory_uf_morgan.cpp | 78 ++++++++++++++++--- src/theory/uf/morgan/theory_uf_morgan.h | 2 +- test/regress/regress0/uf/Makefile.am | 2 + .../regress0/uf/NEQ016_size5_reduced2a.smt | 14 ++++ .../regress0/uf/NEQ016_size5_reduced2b.smt | 14 ++++ 6 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/uf/NEQ016_size5_reduced2a.smt create mode 100644 test/regress/regress0/uf/NEQ016_size5_reduced2b.smt diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index c93f26deb..b1eb195c7 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -31,7 +31,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ case Theory::MIN_EFFORT: os << "MIN_EFFORT"; break; case Theory::QUICK_CHECK: - os << "QUICK_CHECK:"; break; + os << "QUICK_CHECK"; break; case Theory::STANDARD: os << "STANDARD"; break; case Theory::FULL_EFFORT: @@ -40,7 +40,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ Unreachable(); } return os; -} +}/* ostream& operator<<(ostream&, Theory::Effort) */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index a11fc06d4..a0b4651bb 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -37,10 +37,14 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : d_conflict(), d_trueNode(), d_falseNode(), + d_trueEqFalseNode(), d_activeAssertions(ctxt) { - TypeNode boolType = NodeManager::currentNM()->booleanType(); - d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType); - d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType); + NodeManager* nm = NodeManager::currentNM(); + TypeNode boolType = nm->booleanType(); + d_trueNode = nm->mkVar("TRUE_UF", boolType); + d_falseNode = nm->mkVar("FALSE_UF", boolType); + d_trueEqFalseNode = nm->mkNode(kind::IFF, d_trueNode, d_falseNode); + addDisequality(d_trueEqFalseNode); d_cc.addTerm(d_trueNode); d_cc.addTerm(d_falseNode); } @@ -81,17 +85,38 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) { NodeBuilder<> nb(kind::AND); if(explanation.getKind() == kind::AND) { - for(Node::iterator i = explanation.begin(); - i != explanation.end(); + for(TNode::iterator i = TNode(explanation).begin(); + i != TNode(explanation).end(); ++i) { - nb << *i; + TNode n = *i; + Assert(n.getKind() == kind::EQUAL || + n.getKind() == kind::IFF); + Assert(n[0] != d_trueNode && + n[0] != d_falseNode); + if(n[1] == d_trueNode) { + nb << n[0]; + } else if(n[1] == d_falseNode) { + nb << n[0].notNode(); + } else { + nb << n; + } } } else { Assert(explanation.getKind() == kind::EQUAL || explanation.getKind() == kind::IFF); - nb << explanation; + Assert(explanation[0] != d_trueNode && + explanation[0] != d_falseNode); + if(explanation[1] == d_trueNode) { + nb << explanation[0]; + } else if(explanation[1] == d_falseNode) { + nb << explanation[0].notNode(); + } else { + nb << explanation; + } + } + if(diseq != d_trueEqFalseNode) { + nb << diseq.notNode(); } - nb << diseq.notNode(); // by construction this should be true Assert(nb.getNumChildren() > 1); @@ -158,8 +183,16 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { return; } + // should have already found such a conflict + Assert(find(d_trueNode) != find(d_falseNode)); + d_unionFind[a] = b; + if(Debug.isOn("uf") && find(d_trueNode) == find(d_falseNode)) { + Debug("uf") << "ok, pay attention now.." << std::endl; + dump(); + } + DiseqLists::iterator deq_i = d_disequalities.find(a); if(deq_i != d_disequalities.end()) { // a set of other trees we are already disequal to @@ -260,6 +293,8 @@ void TheoryUFMorgan::check(Effort level) { Debug("uf") << "uf: begin check(" << level << ")" << std::endl; while(!done()) { + Assert(d_conflict.isNull()); + Node assertion = get(); d_activeAssertions.push_back(assertion); @@ -289,6 +324,13 @@ void TheoryUFMorgan::check(Effort level) { d_cc.addTerm(assertion); d_cc.addEquality(eq); + if(!d_conflict.isNull()) { + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } + if(Debug.isOn("uf")) { Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl; @@ -354,6 +396,13 @@ void TheoryUFMorgan::check(Effort level) { d_cc.addTerm(assertion[0]); d_cc.addEquality(eq); + if(!d_conflict.isNull()) { + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } + if(Debug.isOn("uf")) { Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl; @@ -372,7 +421,9 @@ void TheoryUFMorgan::check(Effort level) { dump(); } } - Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl; + Assert(d_conflict.isNull()); + Debug("uf") << "uf check() done = " << (done() ? "true" : "false") + << std::endl; for(CDList::const_iterator diseqIter = d_disequality.begin(); diseqIter != d_disequality.end(); @@ -385,9 +436,11 @@ void TheoryUFMorgan::check(Effort level) { << " right: " << right << std::endl << " find(L): " << debugFind(left) << std::endl << " find(R): " << debugFind(right) << std::endl - << " areCong: " << d_cc.areCongruent(left, right) << std::endl; + << " areCong: " << d_cc.areCongruent(left, right) + << std::endl; } - Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right)); + Assert((debugFind(left) == debugFind(right)) == + d_cc.areCongruent(left, right)); } Debug("uf") << "uf: end check(" << level << ")" << std::endl; @@ -413,7 +466,8 @@ void TheoryUFMorgan::dump() { for(UnionFind::const_iterator i = d_unionFind.begin(); i != d_unionFind.end(); ++i) { - Debug("uf") << " " << (*i).first << " ==> " << (*i).second << std::endl; + Debug("uf") << " " << (*i).first << " ==> " << (*i).second + << std::endl; } Debug("uf") << "Disequality lists:" << std::endl; for(DiseqLists::const_iterator i = d_disequalities.begin(); diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index a00e7d15d..d17eb87f5 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -91,7 +91,7 @@ private: Node d_conflict; - Node d_trueNode, d_falseNode; + Node d_trueNode, d_falseNode, d_trueEqFalseNode; context::CDList d_activeAssertions; diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index a5ab380ce..1471d8814 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,6 +19,8 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ + NEQ016_size5_reduced2a.smt \ + NEQ016_size5_reduced2b.smt \ dead_dnd002.smt \ iso_brn001.smt \ simple.01.cvc \ diff --git a/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt b/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt new file mode 100644 index 000000000..8ea53b45e --- /dev/null +++ b/test/regress/regress0/uf/NEQ016_size5_reduced2a.smt @@ -0,0 +1,14 @@ +(benchmark NEQ016_size5.smt +:logic QF_UF +:extrapreds ((p4 U)) +:extrafuns ((c_4 U)) +:extrafuns ((c7 U)) +:extrafuns ((c_0 U)) +:status unsat +:formula +(and +(not (p4 c_0)) +(= c_0 c7) +(p4 c7) +) +) diff --git a/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt b/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt new file mode 100644 index 000000000..029506d75 --- /dev/null +++ b/test/regress/regress0/uf/NEQ016_size5_reduced2b.smt @@ -0,0 +1,14 @@ +(benchmark NEQ016_size5.smt +:logic QF_UF +:extrapreds ((p4 U)) +:extrafuns ((c_4 U)) +:extrafuns ((c7 U)) +:extrafuns ((c_0 U)) +:status unsat +:formula +(and +(not (p4 c_0)) +(p4 c7) +(= c_0 c7) +) +) -- 2.30.2