diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/kinds | 1 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 22 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 53 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 9 | ||||
-rw-r--r-- | src/theory/uf/morgan/Makefile.am | 12 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 348 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 186 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 191 | ||||
-rw-r--r-- | src/theory/uf/tim/Makefile.am | 14 | ||||
-rw-r--r-- | src/theory/uf/tim/ecdata.cpp (renamed from src/theory/uf/ecdata.cpp) | 9 | ||||
-rw-r--r-- | src/theory/uf/tim/ecdata.h (renamed from src/theory/uf/ecdata.h) | 8 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.cpp (renamed from src/theory/uf/theory_uf.cpp) | 41 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 229 |
13 files changed, 895 insertions, 228 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index dfa94a66d..d3b9d12fb 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -127,3 +127,4 @@ constant TYPE_CONSTANT \ "expr/type_constant.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" +operator TUPLE_TYPE 2: "tuple type" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 354bf02bd..42c9902e5 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -44,7 +44,7 @@ class EqualityTypeRule { std::stringstream ss; ss << "Types do not match in equation "; ss << "[" << lhsType << "<>" << rhsType << "]"; - + throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -54,7 +54,8 @@ class EqualityTypeRule { } return booleanType; } -}; +};/* class EqualityTypeRule */ + class DistinctTypeRule { public: @@ -71,7 +72,22 @@ public: } return nodeManager->booleanType(); } -}; +};/* class DistinctTypeRule */ + + +class TupleTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + std::vector<TypeNode> types; + for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); + child_it != child_it_end; + ++child_it) { + types.push_back((*child_it).getType(check)); + } + return nodeManager->mkTupleType(types); + } +};/* class TupleTypeRule */ + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 54204ae3f..cc0e663fa 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,10 +30,13 @@ #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/uf/morgan/theory_uf_morgan.h" #include "theory/arith/theory_arith.h" #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" +#include "util/options.h" #include "util/stats.h" namespace CVC4 { @@ -134,6 +137,12 @@ class TheoryEngine { theory::bv::TheoryBV* d_bv; /** + * Debugging flag to ensure that shutdown() is called before the + * destructor. + */ + bool d_hasShutDown; + + /** * Check whether a node is in the pre-rewrite cache or not. */ static bool inPreRewriteCache(TNode n, bool topLevel) throw() { @@ -193,16 +202,26 @@ public: /** * Construct a theory engine. */ - TheoryEngine(context::Context* ctxt) : + TheoryEngine(context::Context* ctxt, const Options* opts) : d_propEngine(NULL), d_theoryOut(this, ctxt), + d_hasShutDown(false), d_statistics() { d_sharedTermManager = new SharedTermManager(this, ctxt); d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); - d_uf = new theory::uf::TheoryUF(2, ctxt, d_theoryOut); + switch(opts->uf_implementation) { + case Options::TIM: + d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); + break; + case Options::MORGAN: + d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); + break; + default: + Unhandled(opts->uf_implementation); + } d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); @@ -222,12 +241,24 @@ public: d_theoryOfTable.registerTheory(d_bv); } + ~TheoryEngine() { + Assert(d_hasShutDown); + + delete d_bv; + delete d_arrays; + delete d_arith; + delete d_uf; + delete d_bool; + delete d_builtin; + + delete d_sharedTermManager; + } + SharedTermManager* getSharedTermManager() { return d_sharedTermManager; } - void setPropEngine(prop::PropEngine* propEngine) - { + void setPropEngine(prop::PropEngine* propEngine) { Assert(d_propEngine == NULL); d_propEngine = propEngine; } @@ -238,21 +269,17 @@ public: * ordering issues between PropEngine and Theory. */ void shutdown() { + // Set this first; if a Theory shutdown() throws an exception, + // at least the destruction of the TheoryEngine won't confound + // matters. + d_hasShutDown = true; + d_builtin->shutdown(); d_bool->shutdown(); d_uf->shutdown(); d_arith->shutdown(); d_arrays->shutdown(); d_bv->shutdown(); - - delete d_bv; - delete d_arrays; - delete d_arith; - delete d_uf; - delete d_bool; - delete d_builtin; - - delete d_sharedTermManager; } /** diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 4e399aeb7..85b41bdbe 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -6,10 +6,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ - ecdata.h \ - ecdata.cpp \ theory_uf.h \ - theory_uf.cpp \ theory_uf_type_rules.h +libuf_la_LIBADD = \ + @builddir@/tim/libuftim.la \ + @builddir@/morgan/libufmorgan.la + +SUBDIRS = tim morgan + EXTRA_DIST = kinds diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am new file mode 100644 index 000000000..e9faa88df --- /dev/null +++ b/src/theory/uf/morgan/Makefile.am @@ -0,0 +1,12 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libufmorgan.la + +libufmorgan_la_SOURCES = \ + theory_uf_morgan.h \ + theory_uf_morgan.cpp + +EXTRA_DIST = diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp new file mode 100644 index 000000000..a480a4d21 --- /dev/null +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -0,0 +1,348 @@ +/********************* */ +/*! \file theory_uf_morgan.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan + ** 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 Implementation of the theory of uninterpreted functions. + ** + ** Implementation of the theory of uninterpreted functions. + **/ + +#include "theory/uf/morgan/theory_uf_morgan.h" +#include "expr/kind.h" +#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; +using namespace CVC4::theory::uf::morgan; + +TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : + TheoryUF(id, ctxt, out), + d_assertions(ctxt), + d_ccChannel(this), + d_cc(ctxt, &d_ccChannel), + d_unionFind(ctxt), + d_disequalities(ctxt), + d_disequality(ctxt), + d_conflict(), + d_trueNode(), + d_falseNode() { + TypeNode boolType = NodeManager::currentNM()->booleanType(); + d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType); + d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType); + d_cc.addTerm(d_trueNode); + d_cc.addTerm(d_falseNode); +} + +TheoryUFMorgan::~TheoryUFMorgan() { +} + +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[0] == n[1]) { + ret = NodeManager::currentNM()->mkConst(true); + } + } + Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl; + return RewriteComplete(ret); + } else { + return RewriteComplete(n); + } +} + +void TheoryUFMorgan::preRegisterTerm(TNode n) { + Debug("uf") << "uf: preRegisterTerm(" << n << ")" << std::endl; +} + +void TheoryUFMorgan::registerTerm(TNode n) { + Debug("uf") << "uf: registerTerm(" << n << ")" << std::endl; +} + +Node TheoryUFMorgan::constructConflict(TNode diseq) { + Debug("uf") << "uf: begin constructConflict()" << std::endl; + Debug("uf") << "uf: using diseq == " << diseq << std::endl; + + Node explanation = d_cc.explain(diseq[0], diseq[1]); + + NodeBuilder<> nb(kind::AND); + if(explanation.getKind() == kind::AND) { + for(Node::iterator i = explanation.begin(); + i != explanation.end(); + ++i) { + nb << *i; + } + } else { + Assert(explanation.getKind() == kind::EQUAL); + nb << explanation; + } + nb << diseq.notNode(); + + // by construction this should be true + Assert(nb.getNumChildren() > 1); + + Node conflict = nb; + Debug("uf") << "conflict constructed : " << conflict << std::endl; + + Debug("uf") << "uf: ending constructConflict()" << std::endl; + + return conflict; +} + +TNode TheoryUFMorgan::find(TNode a) { + UnionFind::iterator i = d_unionFind.find(a); + if(i == d_unionFind.end()) { + return a; + } else { + return d_unionFind[a] = find((*i).second); + } +} + +// no path compression +TNode TheoryUFMorgan::debugFind(TNode a) const { + UnionFind::iterator i = d_unionFind.find(a); + if(i == d_unionFind.end()) { + return a; + } else { + return debugFind((*i).second); + } +} + +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; + if(!d_conflict.isNull()) { + // if already a conflict, we don't care + return; + } + + // make "a" the one with shorter diseqList + DiseqLists::iterator deq_ia = d_disequalities.find(a); + DiseqLists::iterator deq_ib = d_disequalities.find(b); + if(deq_ia != d_disequalities.end()) { + if(deq_ib == d_disequalities.end() || + (*deq_ia).second->size() > (*deq_ib).second->size()) { + TNode tmp = a; + a = b; + b = tmp; + Debug("uf") << " swapping to make a shorter diseqList" << std::endl; + } + } + a = find(a); + b = find(b); + Debug("uf") << "uf: uf reps are " << a << std::endl + << " and " << b << std::endl; + unionClasses(a, b); + + DiseqLists::iterator deq_i = d_disequalities.find(a); + if(deq_i != d_disequalities.end()) { + // a set of other trees we are already disequal to + // (for the optimization below) + std::set<TNode> alreadyDiseqs; + DiseqLists::iterator deq_ib = d_disequalities.find(b); + if(deq_ib != d_disequalities.end()) { + DiseqList* deq = (*deq_i).second; + for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { + TNode deqn = *j; + TNode s = deqn[0]; + TNode t = deqn[1]; + TNode sp = find(s); + TNode tp = find(t); + Assert(sp == b || tp == b); + if(sp == b) { + alreadyDiseqs.insert(tp); + } else { + alreadyDiseqs.insert(sp); + } + } + } + + DiseqList* deq = (*deq_i).second; + Debug("uf") << "a == " << a << std::endl; + Debug("uf") << "size of deq(a) is " << deq->size() << std::endl; + 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); + TNode s = deqn[0]; + TNode t = deqn[1]; + Debug("uf") << " s ==> " << s << std::endl + << " t ==> " << t << std::endl + << " find(s) ==> " << debugFind(s) << std::endl + << " find(t) ==> " << debugFind(t) << std::endl; + TNode sp = find(s); + TNode tp = find(t); + if(sp == tp) { + d_conflict = deqn; + return; + } + Assert(sp == b || tp == b); + // optimization: don't put redundant diseq's in the list + if(sp == b) { + if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { + appendToDiseqList(b, deqn); + alreadyDiseqs.insert(tp); + } + } else { + if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { + appendToDiseqList(b, deqn); + alreadyDiseqs.insert(sp); + } + } + } + Debug("uf") << "end" << std::endl; + } +} + +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(of == debugFind(of)); + DiseqLists::iterator deq_i = d_disequalities.find(of); + DiseqList* deq; + if(deq_i == d_disequalities.end()) { + deq = new(getContext()->getCMM()) DiseqList(true, getContext()); + d_disequalities.insertDataFromContextMemory(of, deq); + } else { + deq = (*deq_i).second; + } + deq->push_back(eq); + Debug("uf") << " size is now " << deq->size() << std::endl; +} + +void TheoryUFMorgan::addDisequality(TNode eq) { + Assert(eq.getKind() == kind::EQUAL); + + Node a = eq[0]; + Node b = eq[1]; + + appendToDiseqList(find(a), eq); + appendToDiseqList(find(b), eq); +} + +void TheoryUFMorgan::check(Effort level) { + Debug("uf") << "uf: begin check(" << level << ")" << std::endl; + + while(!done()) { + Node assertion = get(); + + Debug("uf") << "uf check(): " << assertion << std::endl; + + switch(assertion.getKind()) { + case EQUAL: + d_cc.addEquality(assertion); + if(!d_conflict.isNull()) { + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } + break; + case APPLY_UF: + { // predicate + Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode); + d_cc.addTerm(assertion); + d_cc.addEquality(eq); + Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl; + Assert(find(d_trueNode) != find(d_falseNode)); + } + break; + case NOT: + if(assertion[0].getKind() == kind::EQUAL) { + Node a = assertion[0][0]; + Node b = assertion[0][1]; + + addDisequality(assertion[0]); + d_disequality.push_back(assertion[0]); + + d_cc.addTerm(a); + d_cc.addTerm(b); + + Debug("uf") << " a ==> " << a << std::endl + << " b ==> " << b << std::endl + << " find(a) ==> " << debugFind(a) << std::endl + << " find(b) ==> " << debugFind(b) << std::endl; + + // There are two ways to get a conflict here. + if(!d_conflict.isNull()) { + // We get a conflict this way if we weren't watching a, b + // before and we were just now notified (via + // notifyCongruent()) when we called addTerm() above that + // they are congruent. We make this a separate case (even + // though the check in the "else if.." below would also + // catch it, so that we can clear out d_conflict. + Node conflict = constructConflict(d_conflict); + d_conflict = Node::null(); + d_out->conflict(conflict, false); + return; + } else if(find(a) == find(b)) { + // We get a conflict this way if we WERE previously watching + // a, b and were notified previously (via notifyCongruent()) + // that they were congruent. + Node conflict = constructConflict(assertion[0]); + d_out->conflict(conflict, false); + return; + } + + // If we get this far, there should be nothing conflicting due + // to this disequality. + Assert(!d_cc.areCongruent(a, b)); + } else { + Assert(assertion[0].getKind() == kind::APPLY_UF); + Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, 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; + Assert(find(d_trueNode) != find(d_falseNode)); + } + break; + default: + Unhandled(assertion.getKind()); + } + } + Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl; + + for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); + diseqIter != d_disequality.end(); + ++diseqIter) { + + TNode left = (*diseqIter)[0]; + TNode right = (*diseqIter)[1]; + Debug("uf") << "testing left: " << left << std::endl + << " right: " << right << std::endl + << " find(L): " << debugFind(left) << std::endl + << " find(R): " << debugFind(right) << std::endl + << " areCong: " << d_cc.areCongruent(left, right) << std::endl; + Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right)); + } + + Debug("uf") << "uf: end check(" << level << ")" << std::endl; +} + +void TheoryUFMorgan::propagate(Effort level) { + Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl; + Debug("uf") << "uf: end propagate(" << level << ")" << std::endl; +} diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h new file mode 100644 index 000000000..1a1ade250 --- /dev/null +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -0,0 +1,186 @@ +/********************* */ +/*! \file theory_uf_morgan.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** 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 This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. + ** + ** This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. It is based on the Nelson-Oppen algorithm given in + ** "Fast Decision Procedures Based on Congruence Closure" + ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) + ** This has been extended to work in a context-dependent way. + ** This interacts heavily with the data-structures given in ecdata.h . + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H +#define __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H + +#include "expr/node.h" +#include "expr/attribute.h" + +#include "theory/theory.h" +#include "theory/uf/theory_uf.h" + +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdlist.h" +#include "util/congruence_closure.h" + +namespace CVC4 { +namespace theory { +namespace uf { +namespace morgan { + +class TheoryUFMorgan : public TheoryUF { + +private: + + class CongruenceChannel { + TheoryUFMorgan* d_uf; + + public: + CongruenceChannel(TheoryUFMorgan* uf) : d_uf(uf) {} + void notifyCongruent(TNode a, TNode b) { + d_uf->notifyCongruent(a, b); + } + };/* class CongruenceChannel */ + friend class CongruenceChannel; + + /** + * List of all of the non-negated literals from the assertion queue. + * This is used only for conflict generation. + * This differs from pending as the program generates new equalities that + * are not in this list. + * This will probably be phased out in future version. + */ + context::CDList<Node> d_assertions; + + /** + * Our channel connected to the congruence closure module. + */ + CongruenceChannel d_ccChannel; + + /** + * Instance of the congruence closure module. + */ + CongruenceClosure<CongruenceChannel> d_cc; + + typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind; + UnionFind d_unionFind; + + typedef context::CDList<Node> DiseqList; + typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists; + + /** List of all disequalities this theory has seen. */ + DiseqLists d_disequalities; + + context::CDList<Node> d_disequality; + + Node d_conflict; + + Node d_trueNode, d_falseNode; + +public: + + /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ + TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out); + + /** Destructor for the TheoryUF object. */ + ~TheoryUFMorgan(); + + /** + * Registers a previously unseen [in this context] node n. + * For TheoryUF, this sets up and maintains invaraints about + * equivalence class data-structures. + * + * Overloads a void registerTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void registerTerm(TNode n); + + /** + * Currently this does nothing. + * + * Overloads a void preRegisterTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void preRegisterTerm(TNode n); + + /** + * Checks whether the set of literals provided to the theory is consistent. + * + * If this is called at any effort level, it computes the congruence closure + * of all of the positive literals in the context. + * + * If this is called at full effort it checks if any of the negative literals + * are inconsistent with the congruence closure. + * + * Overloads void check(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void check(Effort level); + + /** + * Rewrites a node in the theory of uninterpreted functions. + * This is fairly basic and only ensures that atoms that are + * unsatisfiable or a valid are rewritten to false or true respectively. + */ + RewriteResponse postRewrite(TNode n, bool topLevel); + + /** + * Propagates theory literals. + * + * Overloads void propagate(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void propagate(Effort level); + + /** + * Explains a previously reported conflict. Currently does nothing. + * + * Overloads void explain(TNode n, Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void explain(TNode n, Effort level) {} + + std::string identify() const { return std::string("TheoryUFMorgan"); } + +private: + + /** Constructs a conflict from an inconsistent disequality. */ + Node constructConflict(TNode diseq); + + 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); + + /** + * Receives a notification from the congruence closure module that + * two nodes have been merged into the same congruence class. + */ + void notifyCongruent(TNode a, TNode b); + +};/* class TheoryUFMorgan */ + +}/* CVC4::theory::uf::morgan namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f0be0668a..f745cf402 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,8 +1,8 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** 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) @@ -11,16 +11,10 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. - ** - ** This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. It is based on the Nelson-Oppen algorithm given in - ** "Fast Decision Procedures Based on Congruence Closure" - ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) - ** This has been extended to work in a context-dependent way. - ** This interacts heavily with the data-structures given in ecdata.h . + ** \brief This is the interface to TheoryUF implementations ** + ** This is the interface to TheoryUF implementations. All + ** implementations of TheoryUF should inherit from this class. **/ #include "cvc4_private.h" @@ -34,191 +28,20 @@ #include "theory/theory.h" #include "context/context.h" -#include "context/cdo.h" -#include "context/cdlist.h" -#include "theory/uf/ecdata.h" namespace CVC4 { namespace theory { namespace uf { class TheoryUF : public Theory { - -private: - - /** - * List of all of the non-negated literals from the assertion queue. - * This is used only for conflict generation. - * This differs from pending as the program generates new equalities that - * are not in this list. - * This will probably be phased out in future version. - */ - context::CDList<Node> d_assertions; - - /** - * List of pending equivalence class merges. - * - * Tricky part: - * Must keep a hard link because new equality terms are created and appended - * to this list. - */ - context::CDList<Node> d_pending; - - /** Index of the next pending equality to merge. */ - context::CDO<unsigned> d_currentPendingIdx; - - /** List of all disequalities this theory has seen. */ - context::CDList<Node> d_disequality; - - /** - * List of all of the terms that are registered in the current context. - * When registerTerm is called on a term we want to guarentee that there - * is a hard link to the term for the duration of the context in which - * register term is called. - * This invariant is enough for us to use soft links where we want is the - * current implementation as well as making ECAttr() not context dependent. - * Soft links used both in ECData, and Link. - */ - context::CDList<Node> d_registered; - public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(int id, context::Context* c, OutputChannel& out); - - /** Destructor for the TheoryUF object. */ - ~TheoryUF(); - - - - /** - * Registers a previously unseen [in this context] node n. - * For TheoryUF, this sets up and maintains invaraints about - * equivalence class data-structures. - * - * Overloads a void registerTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void registerTerm(TNode n); - - /** - * Currently this does nothing. - * - * Overloads a void preRegisterTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void preRegisterTerm(TNode n); - - /** - * Checks whether the set of literals provided to the theory is consistent. - * - * If this is called at any effort level, it computes the congruence closure - * of all of the positive literals in the context. - * - * If this is called at full effort it checks if any of the negative literals - * are inconsistent with the congruence closure. - * - * Overloads void check(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void check(Effort level); - - - /** - * Rewrites a node in the theory of uninterpreted functions. - * This is fairly basic and only ensures that atoms that are - * unsatisfiable or a valid are rewritten to false or true respectively. - */ - Node rewrite(TNode n); - - /** - * Plug in old rewrite to the new (pre,post)rewrite interface. - */ - RewriteResponse postRewrite(TNode n, bool topLevel) { - return RewriteComplete(topLevel ? rewrite(n) : Node(n)); - } - - /** - * Propagates theory literals. Currently does nothing. - * - * Overloads void propagate(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void propagate(Effort level) {} - - /** - * Explains a previously reported conflict. Currently does nothing. - * - * Overloads void explain(TNode n, Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void explain(TNode n, Effort level) {} - - std::string identify() const { return std::string("TheoryUF"); } - -private: - /** - * Checks whether 2 nodes are already in the same equivalence class tree. - * This should only be used internally, and it should only be called when - * the only thing done with the equivalence classes is an equality check. - * - * @returns true iff ccFind(x) == ccFind(y); - */ - bool sameCongruenceClass(TNode x, TNode y); - - /** - * Checks whether Node x and Node y are currently congruent - * using the equivalence class data structures. - * @returns true iff - * |x| = n = |y| and - * x.getOperator() == y.getOperator() and - * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i]) - */ - bool equiv(TNode x, TNode y); - - /** - * Merges 2 equivalence classes, checks wether any predecessors need to - * be set equal to complete congruence closure. - * The class with the smaller class size will be merged. - * @pre ecX->isClassRep() - * @pre ecY->isClassRep() - */ - void ccUnion(ECData* ecX, ECData* ecY); - - /** - * Returns the representative of the equivalence class. - * May modify the find pointers associated with equivalence classes. - */ - ECData* ccFind(ECData* x); - - /** Performs Congruence Closure to reflect the new additions to d_pending. */ - void merge(); - - /** Constructs a conflict from an inconsistent disequality. */ - Node constructConflict(TNode diseq); + TheoryUF(int id, context::Context* ctxt, OutputChannel& out) + : Theory(id, ctxt, out) {} };/* class TheoryUF */ - -/** - * Cleanup function for ECData. This will be used for called whenever - * a ECAttr is being destructed. - */ -struct ECCleanupStrategy { - static void cleanup(ECData* ec) { - Debug("ufgc") << "cleaning up ECData " << ec << "\n"; - ec->deleteSelf(); - } -};/* struct ECCleanupStrategy */ - -/** Unique name to use for constructing ECAttr. */ -struct ECAttrTag {}; - -/** - * ECAttr is the attribute that maps a node to an equivalence class. - */ -typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; - }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am new file mode 100644 index 000000000..647783885 --- /dev/null +++ b/src/theory/uf/tim/Makefile.am @@ -0,0 +1,14 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libuftim.la + +libuftim_la_SOURCES = \ + ecdata.h \ + ecdata.cpp \ + theory_uf_tim.h \ + theory_uf_tim.cpp + +EXTRA_DIST = diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp index 822f3a95b..52a110ff2 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/tim/ecdata.cpp @@ -17,12 +17,13 @@ ** context-dependent object. **/ -#include "theory/uf/ecdata.h" +#include "theory/uf/tim/ecdata.h" using namespace CVC4; -using namespace context; -using namespace theory; -using namespace uf; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; +using namespace CVC4::theory::uf::tim; ECData::ECData(Context * context, TNode n) : ContextObj(context), diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/tim/ecdata.h index bff0a67a2..5e72f0042 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/tim/ecdata.h @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__ECDATA_H -#define __CVC4__THEORY__UF__ECDATA_H +#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H +#define __CVC4__THEORY__UF__TIM__ECDATA_H #include "expr/node.h" #include "context/context.h" @@ -30,6 +30,7 @@ namespace CVC4 { namespace theory { namespace uf { +namespace tim { /** * Link is a context dependent linked list of nodes. @@ -252,8 +253,9 @@ public: };/* class ECData */ +}/* CVC4::theory::uf::tim namespace */ }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__ECDATA_H */ +#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/tim/theory_uf_tim.cpp index 9060568b2..ccc37a24b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/tim/theory_uf_tim.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf.cpp +/*! \file theory_uf_tim.cpp ** \verbatim ** Original author: taking ** Major contributors: mdeters @@ -16,8 +16,8 @@ ** Implementation of the theory of uninterpreted functions. **/ -#include "theory/uf/theory_uf.h" -#include "theory/uf/ecdata.h" +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/uf/tim/ecdata.h" #include "expr/kind.h" using namespace CVC4; @@ -25,9 +25,10 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; +using namespace CVC4::theory::uf::tim; -TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) : - Theory(id, c, out), +TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) : + TheoryUF(id, c, out), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), @@ -35,10 +36,10 @@ TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) : d_registered(c) { } -TheoryUF::~TheoryUF() { +TheoryUFTim::~TheoryUFTim() { } -Node TheoryUF::rewrite(TNode n){ +Node TheoryUFTim::rewrite(TNode n){ Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl; Node ret(n); if(n.getKind() == EQUAL){ @@ -50,12 +51,12 @@ Node TheoryUF::rewrite(TNode n){ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl; return ret; } -void TheoryUF::preRegisterTerm(TNode n) { +void TheoryUFTim::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; } -void TheoryUF::registerTerm(TNode n) { +void TheoryUFTim::registerTerm(TNode n) { Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; @@ -147,13 +148,13 @@ void TheoryUF::registerTerm(TNode n) { } -bool TheoryUF::sameCongruenceClass(TNode x, TNode y) { +bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) { return ccFind(x.getAttribute(ECAttr())) == ccFind(y.getAttribute(ECAttr())); } -bool TheoryUF::equiv(TNode x, TNode y) { +bool TheoryUFTim::equiv(TNode x, TNode y) { Assert(x.getKind() == kind::APPLY_UF); Assert(y.getKind() == kind::APPLY_UF); @@ -189,7 +190,7 @@ bool TheoryUF::equiv(TNode x, TNode y) { * many better algorithms use eager path compression. * 2) Elminate recursion. */ -ECData* TheoryUF::ccFind(ECData * x) { +ECData* TheoryUFTim::ccFind(ECData * x) { if(x->getFind() == x) { return x; } else { @@ -208,7 +209,7 @@ ECData* TheoryUF::ccFind(ECData * x) { */ } -void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { +void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) { ECData* nslave; ECData* nmaster; @@ -234,7 +235,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { ECData::takeOverDescendantWatchList(nslave, nmaster); } -void TheoryUF::merge() { +void TheoryUFTim::merge() { while(d_currentPendingIdx < d_pending.size() ) { Node assertion = d_pending[d_currentPendingIdx]; d_currentPendingIdx = d_currentPendingIdx + 1; @@ -259,7 +260,7 @@ void TheoryUF::merge() { } } -Node TheoryUF::constructConflict(TNode diseq) { +Node TheoryUFTim::constructConflict(TNode diseq) { Debug("uf") << "uf: begin constructConflict()" << std::endl; NodeBuilder<> nb(kind::AND); @@ -278,13 +279,13 @@ Node TheoryUF::constructConflict(TNode diseq) { return conflict; } -void TheoryUF::check(Effort level) { +void TheoryUFTim::check(Effort level) { Debug("uf") << "uf: begin check(" << level << ")" << std::endl; while(!done()) { Node assertion = get(); - Debug("uf") << "TheoryUF::check(): " << assertion << std::endl; + Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl; switch(assertion.getKind()) { case EQUAL: @@ -293,13 +294,17 @@ void TheoryUF::check(Effort level) { merge(); break; case NOT: + Assert(assertion[0].getKind() == EQUAL, + "predicates not supported in this UF implementation"); d_disequality.push_back(assertion[0]); break; + case APPLY_UF: + Unhandled("predicates not supported in this UF implementation"); default: Unhandled(assertion.getKind()); } - Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl; + Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl; } //Make sure all outstanding merges are completed. diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h new file mode 100644 index 000000000..1591cc05c --- /dev/null +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -0,0 +1,229 @@ +/********************* */ +/*! \file theory_uf.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** 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 This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. + ** + ** This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. It is based on the Nelson-Oppen algorithm given in + ** "Fast Decision Procedures Based on Congruence Closure" + ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) + ** This has been extended to work in a context-dependent way. + ** This interacts heavily with the data-structures given in ecdata.h . + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H +#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H + +#include "expr/node.h" +#include "expr/attribute.h" + +#include "theory/theory.h" + +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdlist.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/tim/ecdata.h" + +namespace CVC4 { +namespace theory { +namespace uf { +namespace tim { + +class TheoryUFTim : public TheoryUF { + +private: + + /** + * List of all of the non-negated literals from the assertion queue. + * This is used only for conflict generation. + * This differs from pending as the program generates new equalities that + * are not in this list. + * This will probably be phased out in future version. + */ + context::CDList<Node> d_assertions; + + /** + * List of pending equivalence class merges. + * + * Tricky part: + * Must keep a hard link because new equality terms are created and appended + * to this list. + */ + context::CDList<Node> d_pending; + + /** Index of the next pending equality to merge. */ + context::CDO<unsigned> d_currentPendingIdx; + + /** List of all disequalities this theory has seen. */ + context::CDList<Node> d_disequality; + + /** + * List of all of the terms that are registered in the current context. + * When registerTerm is called on a term we want to guarentee that there + * is a hard link to the term for the duration of the context in which + * register term is called. + * This invariant is enough for us to use soft links where we want is the + * current implementation as well as making ECAttr() not context dependent. + * Soft links used both in ECData, and Link. + */ + context::CDList<Node> d_registered; + +public: + + /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ + TheoryUFTim(int id, context::Context* c, OutputChannel& out); + + /** Destructor for the TheoryUF object. */ + ~TheoryUFTim(); + + + + /** + * Registers a previously unseen [in this context] node n. + * For TheoryUF, this sets up and maintains invaraints about + * equivalence class data-structures. + * + * Overloads a void registerTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void registerTerm(TNode n); + + /** + * Currently this does nothing. + * + * Overloads a void preRegisterTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void preRegisterTerm(TNode n); + + /** + * Checks whether the set of literals provided to the theory is consistent. + * + * If this is called at any effort level, it computes the congruence closure + * of all of the positive literals in the context. + * + * If this is called at full effort it checks if any of the negative literals + * are inconsistent with the congruence closure. + * + * Overloads void check(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void check(Effort level); + + + /** + * Rewrites a node in the theory of uninterpreted functions. + * This is fairly basic and only ensures that atoms that are + * unsatisfiable or a valid are rewritten to false or true respectively. + */ + Node rewrite(TNode n); + + /** + * Plug in old rewrite to the new (pre,post)rewrite interface. + */ + RewriteResponse postRewrite(TNode n, bool topLevel) { + return RewriteComplete(topLevel ? rewrite(n) : Node(n)); + } + + /** + * Propagates theory literals. Currently does nothing. + * + * Overloads void propagate(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void propagate(Effort level) {} + + /** + * Explains a previously reported conflict. Currently does nothing. + * + * Overloads void explain(TNode n, Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void explain(TNode n, Effort level) {} + + std::string identify() const { return std::string("TheoryUFTim"); } + +private: + /** + * Checks whether 2 nodes are already in the same equivalence class tree. + * This should only be used internally, and it should only be called when + * the only thing done with the equivalence classes is an equality check. + * + * @returns true iff ccFind(x) == ccFind(y); + */ + bool sameCongruenceClass(TNode x, TNode y); + + /** + * Checks whether Node x and Node y are currently congruent + * using the equivalence class data structures. + * @returns true iff + * |x| = n = |y| and + * x.getOperator() == y.getOperator() and + * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i]) + */ + bool equiv(TNode x, TNode y); + + /** + * Merges 2 equivalence classes, checks wether any predecessors need to + * be set equal to complete congruence closure. + * The class with the smaller class size will be merged. + * @pre ecX->isClassRep() + * @pre ecY->isClassRep() + */ + void ccUnion(ECData* ecX, ECData* ecY); + + /** + * Returns the representative of the equivalence class. + * May modify the find pointers associated with equivalence classes. + */ + ECData* ccFind(ECData* x); + + /** Performs Congruence Closure to reflect the new additions to d_pending. */ + void merge(); + + /** Constructs a conflict from an inconsistent disequality. */ + Node constructConflict(TNode diseq); + +};/* class TheoryUFTim */ + + +/** + * Cleanup function for ECData. This will be used for called whenever + * a ECAttr is being destructed. + */ +struct ECCleanupStrategy { + static void cleanup(ECData* ec) { + Debug("ufgc") << "cleaning up ECData " << ec << "\n"; + ec->deleteSelf(); + } +};/* struct ECCleanupStrategy */ + +/** Unique name to use for constructing ECAttr. */ +struct ECAttrTag {}; + +/** + * ECAttr is the attribute that maps a node to an equivalence class. + */ +typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; + +}/* CVC4::theory::uf::tim namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ |