summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/Makefile.am9
-rw-r--r--src/theory/uf/morgan/Makefile.am12
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.cpp348
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h186
-rw-r--r--src/theory/uf/theory_uf.h191
-rw-r--r--src/theory/uf/tim/Makefile.am14
-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.h229
10 files changed, 835 insertions, 212 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback