From ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 19 Aug 2010 23:49:58 +0000 Subject: UF theory bug fixes, code cleanup, and extra debugging output. Enabled new UF theory by default. Added some UF regressions. Some work on the whole equality-over-bool-removed-in-favor-of-IFF thing. (Congruence closure module and other things have to handle IFF as a special case of equality, etc..) Added pre-rewriting to TheoryBool which rewrites: * (IFF true x) => x * (IFF false x) => (NOT x) * (IFF x true) => x * (IFF x false) => (NOT x) * (IFF x x) => true * (IFF x (NOT x)) => false * (IFF (NOT x) x) => false * (ITE true x y) => x * (ITE false x y) => y * (ITE cond x x) => x Added post-rewriting that does all of the above, plus normalize IFF and ITE: * (IFF x y) => (IFF y x), if y < x * (ITE (NOT cond) x y) => (ITE cond y x) (Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.) A little more debugging output from CNF stream, context pushes/pops, ITE removal. Some more documentation. Fixed some typos. --- src/context/context.cpp | 6 +- src/main/getopt.cpp | 2 +- src/prop/cnf_stream.cpp | 14 +- src/theory/arith/arith_rewriter.cpp | 7 +- src/theory/arith/theory_arith.cpp | 22 +++- src/theory/booleans/Makefile.am | 1 + src/theory/booleans/theory_bool.cpp | 146 +++++++++++++++++++++ src/theory/booleans/theory_bool.h | 4 + src/theory/builtin/theory_builtin.cpp | 16 ++- src/theory/theory.h | 13 ++ src/theory/theory_engine.cpp | 14 +- src/theory/uf/morgan/theory_uf_morgan.cpp | 120 +++++++++++++---- src/theory/uf/morgan/theory_uf_morgan.h | 12 +- src/util/congruence_closure.h | 45 +++++-- src/util/options.h | 2 +- test/regress/regress0/uf/Makefile.am | 1 + test/regress/regress0/uf/eq_diamond14.reduced.smt | 1 - test/regress/regress0/uf/eq_diamond14.reduced2.smt | 102 ++++++++++++++ test/regress/regress0/uf/pred.smt | 18 +++ test/regress/run_regression | 2 +- 20 files changed, 474 insertions(+), 74 deletions(-) create mode 100644 src/theory/booleans/theory_bool.cpp create mode 100644 test/regress/regress0/uf/eq_diamond14.reduced2.smt create mode 100644 test/regress/regress0/uf/pred.smt diff --git a/src/context/context.cpp b/src/context/context.cpp index 0028aaad5..5d8e88db0 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -61,7 +61,8 @@ Context::~Context() throw(AssertionException) { void Context::push() { - Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl; + Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to " + << getLevel() + 1 << "] {" << std::endl; // Create a new memory region d_pCMM->push(); @@ -100,7 +101,8 @@ void Context::pop() { pCNO = pCNO->d_pCNOnext; } - Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl; + Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to " + << getLevel() << "]" << std::endl; } diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index b15f4ae66..08bcbaa7c 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -262,7 +262,7 @@ throw(OptionException) { printf("morgan\n"); exit(1); } else { - throw OptionException(string("unknown language for --uf: `") + + throw OptionException(string("unknown option for --uf: `") + optarg + "'. Try --uf help."); } } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 5f8eb12b9..c719c66da 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -100,10 +100,10 @@ Node CnfStream::getNode(const SatLiteral& literal) { } SatLiteral CnfStream::convertAtom(TNode node) { - Assert(!isCached(node), "atom already mapped!"); - Debug("cnf") << "convertAtom(" << node << ")" << endl; + Assert(!isCached(node), "atom already mapped!"); + bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); @@ -245,6 +245,8 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); + Debug("cnf") << "handleIff(" << iffNode << ")" << endl; + // Convert the children to CNF SatLiteral a = toCNF(iffNode[0]); SatLiteral b = toCNF(iffNode[1]); @@ -287,7 +289,7 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); - Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; + Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; SatLiteral condLit = toCNF(iteNode[0]); SatLiteral thenLit = toCNF(iteNode[1]); @@ -353,8 +355,10 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { nodeLit = handleAnd(node); break; case EQUAL: - if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) { - nodeLit = handleIff(node[0].iffNode(node[1])); + if(node[0].getType().isBoolean()) { + // should have an IFF instead + Unreachable("= Bool Bool shouldn't be possible ?!"); + //nodeLit = handleIff(node[0].iffNode(node[1])); } else { nodeLit = convertAtom(node); } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 9b10f5a62..ba1445df8 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -43,7 +43,7 @@ Kind multKind(Kind k, int sgn); * Also writes relations with constants on both sides to TRUE or FALSE. * If it can, it returns true and sets res to this value. * - * This is for optimizing rewriteAtom() to avoid the more compuationally + * This is for optimizing rewriteAtom() to avoid the more computationally * expensive general rewriting procedure. * * If simplification is not done, it returns Node::null() @@ -476,8 +476,7 @@ Node ArithRewriter::rewriteTerm(TNode t){ Node sub = makeUnaryMinusNode(t[0]); return rewrite(sub); }else{ - Unreachable(); - return Node::null(); + Unhandled(t); } } @@ -533,7 +532,7 @@ Kind multKind(Kind k, int sgn){ case GEQ: return LEQ; case GT: return LT; default: - Unhandled(); + Unhandled(k); } return NULL_EXPR; }else{ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ab8884228..157c45160 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -316,6 +316,9 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ } RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { + // ensure a hard link to the node we're returning + Node out; + // Look for multiplications with a 0 argument and rewrite the whole // thing as 0 if(n.getKind() == MULT) { @@ -324,23 +327,34 @@ RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { for(TNode::iterator i = n.begin(); i != n.end(); ++i) { if((*i).getKind() == CONST_RATIONAL) { if((*i).getConst() == ratZero) { - n = NodeManager::currentNM()->mkConst(ratZero); + out = NodeManager::currentNM()->mkConst(ratZero); break; } } else if((*i).getKind() == CONST_INTEGER) { if((*i).getConst() == intZero) { if(n.getType().isInteger()) { - n = NodeManager::currentNM()->mkConst(intZero); + out = NodeManager::currentNM()->mkConst(intZero); break; } else { - n = NodeManager::currentNM()->mkConst(ratZero); + out = NodeManager::currentNM()->mkConst(ratZero); break; } } } } + } else if(n.getKind() == EQUAL) { + if(n[0] == n[1]) { + out = NodeManager::currentNM()->mkConst(true); + } + } + + if(out.isNull()) { + // no preRewrite to perform + return RewriteComplete(Node(n)); + } else { + // out is always a constant, so doesn't need to be rewritten again + return RewriteComplete(out); } - return RewriteComplete(Node(n)); } Node TheoryArith::rewrite(TNode n){ diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 3bd8b5a39..c8a9b4dbd 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ theory_bool.h \ + theory_bool.cpp \ theory_bool_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp new file mode 100644 index 000000000..a7e343fdc --- /dev/null +++ b/src/theory/booleans/theory_bool.cpp @@ -0,0 +1,146 @@ +/********************* */ +/*! \file theory_bool.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The theory of booleans. + ** + ** The theory of booleans. + **/ + +#include "theory/theory.h" +#include "theory/booleans/theory_bool.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + + +RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) { + if(n.getKind() == kind::IFF) { + NodeManager* nodeManager = NodeManager::currentNM(); + Node tt = nodeManager->mkConst(true); + Node ff = nodeManager->mkConst(false); + + // rewrite simple cases of IFF + if(n[0] == tt) { + // IFF true x + return RewriteAgain(n[1]); + } else if(n[1] == tt) { + // IFF x true + return RewriteAgain(n[0]); + } else if(n[0] == ff) { + // IFF false x + return RewriteAgain(n[1].notNode()); + } else if(n[1] == ff) { + // IFF x false + return RewriteAgain(n[0].notNode()); + } else if(n[0] == n[1]) { + // IFF x x + return RewriteComplete(tt); + } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { + // IFF (NOT x) x + return RewriteComplete(ff); + } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + // IFF x (NOT x) + return RewriteComplete(ff); + } + } else if(n.getKind() == kind::ITE) { + // non-Boolean-valued ITEs should have been removed in place of + // a variable + Assert(n.getType().isBoolean()); + + NodeManager* nodeManager = NodeManager::currentNM(); + + // rewrite simple cases of ITE + if(n[0] == nodeManager->mkConst(true)) { + // ITE true x y + return RewriteAgain(n[1]); + } else if(n[0] == nodeManager->mkConst(false)) { + // ITE false x y + return RewriteAgain(n[2]); + } else if(n[1] == n[2]) { + // ITE c x x + return RewriteAgain(n[1]); + } + } + + return RewriteComplete(n); +} + + +RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) { + if(n.getKind() == kind::IFF) { + NodeManager* nodeManager = NodeManager::currentNM(); + Node tt = nodeManager->mkConst(true); + Node ff = nodeManager->mkConst(false); + + // rewrite simple cases of IFF + if(n[0] == tt) { + // IFF true x + return RewriteComplete(n[1]); + } else if(n[1] == tt) { + // IFF x true + return RewriteComplete(n[0]); + } else if(n[0] == ff) { + // IFF false x + return RewriteAgain(n[1].notNode()); + } else if(n[1] == ff) { + // IFF x false + return RewriteAgain(n[0].notNode()); + } else if(n[0] == n[1]) { + // IFF x x + return RewriteComplete(tt); + } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { + // IFF (NOT x) x + return RewriteComplete(ff); + } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + // IFF x (NOT x) + return RewriteComplete(ff); + } + + if(n[1] < n[0]) { + // normalize (IFF x y) ==> (IFF y x), if y < x + return RewriteComplete(n[1].iffNode(n[0])); + } + } else if(n.getKind() == kind::ITE) { + // non-Boolean-valued ITEs should have been removed in place of + // a variable + Assert(n.getType().isBoolean()); + + NodeManager* nodeManager = NodeManager::currentNM(); + + // rewrite simple cases of ITE + if(n[0] == nodeManager->mkConst(true)) { + // ITE true x y + return RewriteComplete(n[1]); + } else if(n[0] == nodeManager->mkConst(false)) { + // ITE false x y + return RewriteComplete(n[2]); + } else if(n[1] == n[2]) { + // ITE c x x + return RewriteComplete(n[1]); + } + + if(n[0].getKind() == kind::NOT) { + // rewrite (ITE (NOT c) x y) to (ITE c y x) + Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]); + return RewriteComplete(out); + } + } + + return RewriteComplete(n); +} + + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 4d8620146..f492041b8 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -45,6 +45,10 @@ public: void check(Effort e) { Unimplemented(); } void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + + RewriteResponse preRewrite(TNode n, bool topLevel); + RewriteResponse postRewrite(TNode n, bool topLevel); + std::string identify() const { return std::string("TheoryBool"); } }; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 174e10d2f..ba258aafd 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -20,8 +20,6 @@ #include "expr/kind.h" using namespace std; -using namespace CVC4; -using namespace CVC4::theory::builtin; namespace CVC4 { namespace theory { @@ -33,8 +31,10 @@ Node TheoryBuiltin::blastDistinct(TNode in) { if(in.getNumChildren() == 2) { // if this is the case exactly 1 != pair will be generated so the // AND is not required - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? + kind::IFF : kind::EQUAL, + in[0], in[1]); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); return neq; } // assume that in.getNumChildren() > 2 => diseqs.size() > 1 @@ -42,12 +42,14 @@ Node TheoryBuiltin::blastDistinct(TNode in) { for(TNode::iterator i = in.begin(); i != in.end(); ++i) { TNode::iterator j = i; while(++j != in.end()) { - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? + kind::IFF : kind::EQUAL, + *i, *j); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); diseqs.push_back(neq); } } - Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); + Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); return out; } diff --git a/src/theory/theory.h b/src/theory/theory.h index 64a3b8f06..1cce09439 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -313,6 +313,19 @@ public: * rewrite a term to a strictly larger term that contains itself, as * this will cause a loop of hard Node links in the cache (and thus * memory leakage). + * + * Be careful with the return value. If a preRewrite() can return a + * sub-expression, and that sub-expression can be a member of the + * same theory and could be rewritten, make sure to return + * RewriteAgain instead of RewriteComplete. This is an easy mistake + * to make, as preRewrite() is often a short-circuiting version of + * the same rewrites that occur in postRewrite(); however, in the + * postRewrite() case, the subexpressions have all been + * post-rewritten. In the preRewrite() case, they have NOT yet been + * pre-rewritten. For example, (ITE true (ITE true x y) z) should + * pre-rewrite to x; but if the outer preRewrite() returns + * RewriteComplete, the result of the pre-rewrite will be + * (ITE true x y). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8db81902d..47d823009 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,19 +52,20 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { // } } else if (fact.getKind() == kind::EQUAL) { + // FIXME: kind::IFF as well ? // Automatically track all asserted equalities in the shared term manager d_engine->getSharedTermManager()->addEq(fact); } if(! fact.getAttribute(RegisteredAttr())) { - std::list toReg; + list toReg; toReg.push_back(fact); - Debug("theory") << "Theory::get(): registering new atom" << std::endl; + Debug("theory") << "Theory::get(): registering new atom" << endl; /* Essentially this is doing a breadth-first numbering of * non-registered subterms with children. Any non-registered * leaves are immediately registered. */ - for(std::list::iterator workp = toReg.begin(); + for(list::iterator workp = toReg.begin(); workp != toReg.end(); ++workp) { @@ -108,7 +109,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { * and the above registration of leaves, this should ensure that * all subterms in the entire tree were registered in * reverse-topological order. */ - for(std::list::reverse_iterator i = toReg.rbegin(); + for(list::reverse_iterator i = toReg.rbegin(); i != toReg.rend(); ++i) { @@ -234,6 +235,7 @@ Node TheoryEngine::removeITEs(TNode node) { Node cachedRewrite; NodeManager *nodeManager = NodeManager::currentNM(); if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) { + Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; return cachedRewrite.isNull() ? Node(node) : cachedRewrite; } @@ -353,6 +355,9 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { Node noItes = removeITEs(in); Node out; + Debug("theory-rewrite") << "removeITEs of: " << in << endl + << " is: " << noItes << endl; + // descend top-down into the theory rewriters vector stack; stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel)); @@ -523,7 +528,6 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { rse.d_node.toString().c_str(), rewrittenAgain.toString().c_str()); } - setPostRewriteCache(original, wasTopLevel, rse.d_node); out = rse.d_node; diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index a480a4d21..f3c16e515 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -21,7 +21,6 @@ #include "util/congruence_closure.h" using namespace CVC4; -using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; @@ -37,7 +36,8 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : d_disequality(ctxt), d_conflict(), d_trueNode(), - d_falseNode() { + d_falseNode(), + d_activeAssertions(ctxt) { TypeNode boolType = NodeManager::currentNM()->booleanType(); d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType); d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType); @@ -52,7 +52,8 @@ RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) { if(topLevel) { Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl; Node ret(n); - if(n.getKind() == EQUAL) { + if(n.getKind() == kind::EQUAL || + n.getKind() == kind::IFF) { if(n[0] == n[1]) { ret = NodeManager::currentNM()->mkConst(true); } @@ -86,7 +87,8 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) { nb << *i; } } else { - Assert(explanation.getKind() == kind::EQUAL); + Assert(explanation.getKind() == kind::EQUAL || + explanation.getKind() == kind::IFF); nb << explanation; } nb << diseq.notNode(); @@ -121,15 +123,6 @@ TNode TheoryUFMorgan::debugFind(TNode a) const { } } -void TheoryUFMorgan::unionClasses(TNode a, TNode b) { - if(a == b) { - return; - } - Assert(d_unionFind.find(a) == d_unionFind.end()); - Assert(d_unionFind.find(b) == d_unionFind.end()); - d_unionFind[a] = b; -} - void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { Debug("uf") << "uf: notified of merge " << a << std::endl << " and " << b << std::endl; @@ -138,6 +131,12 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { return; } + merge(a, b); +} + +void TheoryUFMorgan::merge(TNode a, TNode b) { + Assert(d_conflict.isNull()); + // make "a" the one with shorter diseqList DiseqLists::iterator deq_ia = d_disequalities.find(a); DiseqLists::iterator deq_ib = d_disequalities.find(b); @@ -154,7 +153,12 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { b = find(b); Debug("uf") << "uf: uf reps are " << a << std::endl << " and " << b << std::endl; - unionClasses(a, b); + + if(a == b) { + return; + } + + d_unionFind[a] = b; DiseqLists::iterator deq_i = d_disequalities.find(a); if(deq_i != d_disequalities.end()) { @@ -163,7 +167,7 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { std::set alreadyDiseqs; DiseqLists::iterator deq_ib = d_disequalities.find(b); if(deq_ib != d_disequalities.end()) { - DiseqList* deq = (*deq_i).second; + DiseqList* deq = (*deq_ib).second; for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { TNode deqn = *j; TNode s = deqn[0]; @@ -185,7 +189,8 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { Debug("uf") << " deq(a) ==> " << *j << std::endl; TNode deqn = *j; - Assert(deqn.getKind() == kind::EQUAL); + Assert(deqn.getKind() == kind::EQUAL || + deqn.getKind() == kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; Debug("uf") << " s ==> " << s << std::endl @@ -219,7 +224,8 @@ void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { Debug("uf") << "appending " << eq << std::endl << " to diseq list of " << of << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); Assert(of == debugFind(of)); DiseqLists::iterator deq_i = d_disequalities.find(of); DiseqList* deq; @@ -234,10 +240,11 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { } void TheoryUFMorgan::addDisequality(TNode eq) { - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); - Node a = eq[0]; - Node b = eq[1]; + TNode a = eq[0]; + TNode b = eq[1]; appendToDiseqList(find(a), eq); appendToDiseqList(find(b), eq); @@ -249,10 +256,13 @@ void TheoryUFMorgan::check(Effort level) { while(!done()) { Node assertion = get(); + d_activeAssertions.push_back(assertion); + Debug("uf") << "uf check(): " << assertion << std::endl; switch(assertion.getKind()) { - case EQUAL: + case kind::EQUAL: + case kind::IFF: d_cc.addEquality(assertion); if(!d_conflict.isNull()) { Node conflict = constructConflict(d_conflict); @@ -260,18 +270,29 @@ void TheoryUFMorgan::check(Effort level) { d_out->conflict(conflict, false); return; } + merge(assertion[0], assertion[1]); break; - case APPLY_UF: + case kind::APPLY_UF: { // predicate - Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode); + + // assert it's a predicate + Assert(assertion.getOperator().getType().getRangeType().isBoolean()); + + Node eq = NodeManager::currentNM()->mkNode(kind::IFF, + assertion, d_trueNode); d_cc.addTerm(assertion); d_cc.addEquality(eq); - Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl; + Debug("uf") << "true == false ? " + << (find(d_trueNode) == find(d_falseNode)) << std::endl; + Assert(find(d_trueNode) != find(d_falseNode)); + + merge(eq[0], eq[1]); } break; - case NOT: - if(assertion[0].getKind() == kind::EQUAL) { + case kind::NOT: + if(assertion[0].getKind() == kind::EQUAL || + assertion[0].getKind() == kind::IFF) { Node a = assertion[0][0]; Node b = assertion[0][1]; @@ -311,17 +332,31 @@ void TheoryUFMorgan::check(Effort level) { // to this disequality. Assert(!d_cc.areCongruent(a, b)); } else { + // negation of a predicate Assert(assertion[0].getKind() == kind::APPLY_UF); - Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion[0], d_falseNode); + + // assert it's a predicate + Assert(assertion[0].getOperator().getType().getRangeType().isBoolean()); + + Node eq = NodeManager::currentNM()->mkNode(kind::IFF, assertion[0], d_falseNode); d_cc.addTerm(assertion[0]); d_cc.addEquality(eq); - Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl; + + Debug("uf") << "true == false ? " + << (find(d_trueNode) == find(d_falseNode)) << std::endl; + Assert(find(d_trueNode) != find(d_falseNode)); + + merge(eq[0], eq[1]); } break; default: Unhandled(assertion.getKind()); } + + if(Debug.isOn("uf")) { + dump(); + } } Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl; @@ -346,3 +381,32 @@ void TheoryUFMorgan::propagate(Effort level) { Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl; Debug("uf") << "uf: end propagate(" << level << ")" << std::endl; } + +void TheoryUFMorgan::dump() { + Debug("uf") << "============== THEORY_UF ==============" << std::endl; + Debug("uf") << "Active assertions list:" << std::endl; + for(context::CDList::const_iterator i = d_activeAssertions.begin(); + i != d_activeAssertions.end(); + ++i) { + Debug("uf") << " " << *i << std::endl; + } + Debug("uf") << "Congruence union-find:" << std::endl; + for(UnionFind::const_iterator i = d_unionFind.begin(); + i != d_unionFind.end(); + ++i) { + Debug("uf") << " " << (*i).first << " ==> " << (*i).second << std::endl; + } + Debug("uf") << "Disequality lists:" << std::endl; + for(DiseqLists::const_iterator i = d_disequalities.begin(); + i != d_disequalities.end(); + ++i) { + Debug("uf") << " " << (*i).first << ":" << std::endl; + DiseqList* dl = (*i).second; + for(DiseqList::const_iterator j = dl->begin(); + j != dl->end(); + ++j) { + Debug("uf") << " " << *j << std::endl; + } + } + Debug("uf") << "=======================================" << std::endl; +} diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 1a1ade250..a00e7d15d 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -93,6 +93,8 @@ private: Node d_trueNode, d_falseNode; + context::CDList d_activeAssertions; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -165,7 +167,6 @@ private: TNode find(TNode a); TNode debugFind(TNode a) const; - void unionClasses(TNode a, TNode b); void appendToDiseqList(TNode of, TNode eq); void addDisequality(TNode eq); @@ -176,6 +177,15 @@ private: */ void notifyCongruent(TNode a, TNode b); + /** + * Internally handle a congruence, whether generated by the CC + * module or from a theory check(). Merges the classes from a and b + * and looks for a conflict. If there is one, sets d_conflict. + */ + void merge(TNode a, TNode b); + + void dump(); + };/* class TheoryUFMorgan */ }/* CVC4::theory::uf::morgan namespace */ diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 058f9c193..7d7e26bbe 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -159,8 +159,9 @@ public: */ void addEquality(TNode inputEq) { Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl; - Assert(inputEq.getKind() == kind::EQUAL); - NodeBuilder<> eqb(kind::EQUAL); + Assert(inputEq.getKind() == kind::EQUAL || + inputEq.getKind() == kind::IFF); + NodeBuilder<> eqb(inputEq.getKind()); if(inputEq[1].getKind() == kind::APPLY_UF && inputEq[0].getKind() != kind::APPLY_UF) { eqb << flatten(inputEq[1]) << inputEq[0]; @@ -190,7 +191,7 @@ public: EqMap::iterator i = d_eqMap.find(t); if(i == d_eqMap.end()) { Node v = NodeManager::currentNM()->mkSkolem(t.getType()); - addEq(NodeManager::currentNM()->mkNode(kind::EQUAL, t, v), TNode::null()); + addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); d_eqMap.insert(t, v); return v; } else { @@ -272,7 +273,8 @@ public: */ inline Node explain(TNode eq) throw(CongruenceClosureException, AssertionException) { - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); return explain(eq[0], eq[1]); } @@ -299,7 +301,8 @@ private: return TNode::null(); } else { TNode l = (*i).second; - Assert(l.getKind() == kind::EQUAL); + Assert(l.getKind() == kind::EQUAL || + l.getKind() == kind::IFF); return l; } } @@ -309,7 +312,8 @@ private: */ inline void setLookup(TNode a, TNode b) { Assert(a.getKind() == kind::TUPLE); - Assert(b.getKind() == kind::EQUAL); + Assert(b.getKind() == kind::EQUAL || + b.getKind() == kind::IFF); d_lookup[a] = b; } @@ -325,7 +329,8 @@ private: */ inline void appendToUseList(TNode of, TNode eq) { Debug("cc") << "adding " << eq << " to use list of " << of << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); Assert(of == find(of)); UseLists::iterator usei = d_useList.find(of); UseList* ul; @@ -389,7 +394,8 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { d_proofRewrite[eq] = inputEq; Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); Assert(eq[1].getKind() != kind::APPLY_UF); if(areCongruent(eq[0], eq[1])) { Debug("cc") << "CC -- redundant, ignoring...\n"; @@ -466,7 +472,8 @@ void CongruenceClosure::propagate(TNode seed) { Debug("cc") << "=== e is " << e << " ===" << std::endl; TNode a, b; - if(e.getKind() == kind::EQUAL) { + if(e.getKind() == kind::EQUAL || + e.getKind() == kind::IFF) { // e is an equality a = b (a, b are constants) a = e[0]; @@ -481,8 +488,10 @@ void CongruenceClosure::propagate(TNode seed) { Assert(e.getKind() == kind::TUPLE); Assert(e.getNumChildren() == 2); - Assert(e[0].getKind() == kind::EQUAL); - Assert(e[1].getKind() == kind::EQUAL); + Assert(e[0].getKind() == kind::EQUAL || + e[0].getKind() == kind::IFF); + Assert(e[1].getKind() == kind::EQUAL || + e[1].getKind() == kind::IFF); // tuple is (eq, lookup) a = e[0][1]; @@ -576,7 +585,8 @@ void CongruenceClosure::propagate(TNode seed) { ++i) { TNode eq = *i; Debug("cc") << "CC -- useList: " << eq << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); // change from paper // use list elts can have form (apply c..) = x OR x = (apply c..) Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF); @@ -730,7 +740,8 @@ Node CongruenceClosure::normalize(TNode t) const Node theLookup = lookup(ap); if(allConstants && !theLookup.isNull()) { - Assert(theLookup.getKind() == kind::EQUAL); + Assert(theLookup.getKind() == kind::EQUAL || + theLookup.getKind() == kind::IFF); Assert(theLookup[0].getKind() == kind::APPLY_UF); Assert(theLookup[1].getKind() != kind::APPLY_UF); return find(theLookup[1]); @@ -769,7 +780,8 @@ void CongruenceClosure::explainAlongPath(TNode a, TNode c, std::l while(a != c) { Node b = d_proof[a]; Node e = d_proofLabel[a]; - if(e.getKind() == kind::EQUAL) { + if(e.getKind() == kind::EQUAL || + e.getKind() == kind::IFF) { pf.push_back(e); } else { Assert(e.getKind() == kind::TUPLE); @@ -900,6 +912,11 @@ std::ostream& operator<<(std::ostream& out, out << " " << (*i).first << " => " << n << std::endl; } + out << "Care set:" << std::endl; + for(typename CongruenceClosure::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) { + out << " " << *i << std::endl; + } + out << "==============================================" << std::endl; return out; diff --git a/src/util/options.h b/src/util/options.h index c2ac7b225..c79bc93b1 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -71,7 +71,7 @@ struct CVC4_PUBLIC Options { err(0), verbosity(0), lang(parser::LANG_AUTO), - uf_implementation(TIM), + uf_implementation(MORGAN), parseOnly(false), semanticChecks(true), memoryMap(false), diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 105baad86..f5c97241e 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,6 +19,7 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.smt \ eq_diamond14.reduced.smt \ + eq_diamond14.reduced2.smt \ dead_dnd002.smt \ iso_brn001.smt \ simple.01.cvc \ diff --git a/test/regress/regress0/uf/eq_diamond14.reduced.smt b/test/regress/regress0/uf/eq_diamond14.reduced.smt index b41e4536d..6af6ac5be 100644 --- a/test/regress/regress0/uf/eq_diamond14.reduced.smt +++ b/test/regress/regress0/uf/eq_diamond14.reduced.smt @@ -32,7 +32,6 @@ :extrafuns ((y1 V)) :extrafuns ((x1 V)) :extrafuns ((y0 V)) -:status unknown :formula (flet ($n1 (= x0 y0)) (flet ($n2 (= y0 x1)) diff --git a/test/regress/regress0/uf/eq_diamond14.reduced2.smt b/test/regress/regress0/uf/eq_diamond14.reduced2.smt new file mode 100644 index 000000000..019a935c4 --- /dev/null +++ b/test/regress/regress0/uf/eq_diamond14.reduced2.smt @@ -0,0 +1,102 @@ +(benchmark eq_diamond14 +:logic QF_UF +:extrasorts (V) +:extrafuns ((z9 V)) +:extrafuns ((x10 V)) +:extrafuns ((x9 V)) +:extrafuns ((x13 V)) +:extrafuns ((x0 V)) +:extrafuns ((z12 V)) +:extrafuns ((x12 V)) +:extrafuns ((y12 V)) +:extrafuns ((z11 V)) +:extrafuns ((x11 V)) +:extrafuns ((y11 V)) +:extrafuns ((z10 V)) +:extrafuns ((y10 V)) +:extrafuns ((y8 V)) +:extrafuns ((x8 V)) +:extrafuns ((y7 V)) +:extrafuns ((x7 V)) +:extrafuns ((z6 V)) +:extrafuns ((x6 V)) +:extrafuns ((y6 V)) +:extrafuns ((z5 V)) +:extrafuns ((x5 V)) +:extrafuns ((y5 V)) +:extrafuns ((y4 V)) +:extrafuns ((x4 V)) +:extrafuns ((y3 V)) +:extrafuns ((x3 V)) +:extrafuns ((y2 V)) +:extrafuns ((x2 V)) +:extrafuns ((y1 V)) +:extrafuns ((x1 V)) +:extrafuns ((y0 V)) +:status unsat +:formula +(flet ($n1 (= x0 y0)) +(flet ($n2 (= y0 x1)) +(flet ($n3 (and $n1 $n2)) +(flet ($n4 (= x1 y1)) +(flet ($n5 (= y1 x2)) +(flet ($n6 (and $n4 $n5)) +(flet ($n7 (= x2 y2)) +(flet ($n8 (= y2 x3)) +(flet ($n9 (and $n7 $n8)) +(flet ($n10 (= x3 y3)) +(flet ($n11 (= y3 x4)) +(flet ($n12 (and $n10 $n11)) +(flet ($n13 (= x4 y4)) +(flet ($n14 (= y4 x5)) +(flet ($n15 (and $n13 $n14)) +(flet ($n16 false) +(flet ($n17 (= y5 x6)) +(flet ($n18 (and $n16 $n17)) +(flet ($n19 (= x5 z5)) +(flet ($n20 (= x6 z5)) +(flet ($n21 (and $n19 $n20)) +(flet ($n22 (or $n18 $n21)) +(flet ($n23 (= x6 y6)) +(flet ($n24 (= y6 x7)) +(flet ($n25 (and $n23 $n24)) +(flet ($n26 (= x6 z6)) +(flet ($n27 (= x7 z6)) +(flet ($n28 (and $n26 $n27)) +(flet ($n29 (or $n25 $n28)) +(flet ($n30 (= x7 y7)) +(flet ($n31 (= y7 x8)) +(flet ($n32 (and $n30 $n31)) +(flet ($n33 (= x8 y8)) +(flet ($n34 (= y8 x9)) +(flet ($n35 (and $n33 $n34)) +(flet ($n36 (= x10 y10)) +(flet ($n37 (= y10 x11)) +(flet ($n38 (and $n36 $n37)) +(flet ($n39 (= x10 z10)) +(flet ($n40 (= x11 z10)) +(flet ($n41 (and $n39 $n40)) +(flet ($n42 (or $n38 $n41)) +(flet ($n43 (= x11 y11)) +(flet ($n44 (= y11 x12)) +(flet ($n45 (and $n43 $n44)) +(flet ($n46 (= x11 z11)) +(flet ($n47 (= x12 z11)) +(flet ($n48 (and $n46 $n47)) +(flet ($n49 (or $n45 $n48)) +(flet ($n50 (= x12 y12)) +(flet ($n51 (= y12 x13)) +(flet ($n52 (and $n50 $n51)) +(flet ($n53 (= x12 z12)) +(flet ($n54 (= x13 z12)) +(flet ($n55 (and $n53 $n54)) +(flet ($n56 (or $n52 $n55)) +(flet ($n57 (= x0 x13)) +(flet ($n58 (not $n57)) +(flet ($n59 (= x9 z9)) +(flet ($n60 (= x10 z9)) +(flet ($n61 (and $n59 $n60)) +(flet ($n62 (or $n16 $n61)) +(flet ($n63 (and $n3 $n6 $n9 $n12 $n15 $n22 $n29 $n32 $n35 $n42 $n49 $n56 $n58 $n62)) +$n63 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uf/pred.smt b/test/regress/regress0/uf/pred.smt new file mode 100644 index 000000000..e6f82727e --- /dev/null +++ b/test/regress/regress0/uf/pred.smt @@ -0,0 +1,18 @@ +(benchmark euf_simp1.smt +:status sat +:logic QF_UF +:category { crafted } + +:extrafuns ((x U)) +:extrafuns ((y U)) +:extrapreds ((f U)) + + + +:formula +(and + (f x) + (iff (f x) (f y)) + (not (f y)) +) +) diff --git a/test/regress/run_regression b/test/regress/run_regression index b26792a78..a6ea0797b 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -132,7 +132,7 @@ cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" echo running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"` ( cd `dirname "$benchmark"`; - "$cvc4full" --segv-nospin `basename "$benchmark"`; + "$cvc4full" -d extra-checking --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" -- cgit v1.2.3