diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
commit | ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e (patch) | |
tree | b783098b4d72422826890c46870436cbeae0788d /src | |
parent | 29c72e0fd6d0161de275060bbd05370394f1f708 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/context/context.cpp | 6 | ||||
-rw-r--r-- | src/main/getopt.cpp | 2 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 14 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 22 | ||||
-rw-r--r-- | src/theory/booleans/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 146 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 16 | ||||
-rw-r--r-- | src/theory/theory.h | 13 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 120 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 12 | ||||
-rw-r--r-- | src/util/congruence_closure.h | 45 | ||||
-rw-r--r-- | src/util/options.h | 2 |
15 files changed, 352 insertions, 72 deletions
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<Rational>() == ratZero) { - n = NodeManager::currentNM()->mkConst(ratZero); + out = NodeManager::currentNM()->mkConst(ratZero); break; } } else if((*i).getKind() == CONST_INTEGER) { if((*i).getConst<Integer>() == 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<TNode> toReg; + list<TNode> 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<TNode>::iterator workp = toReg.begin(); + for(list<TNode>::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<TNode>::reverse_iterator i = toReg.rbegin(); + for(list<TNode>::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<RewriteStackElement> 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<TNode> 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<Node>::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<Node> 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<OutputChannel>::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<OutputChannel>::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<OutputChannel>::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<OutputChannel>::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<OutputChannel>::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<OutputChannel>::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<OutputChannel>::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), |