diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
commit | 3311e8276fb6221d9e100be2b1eec88d8f119fef (patch) | |
tree | ef0ceebcd85b1153a25af7438c4bae96fe5aecb8 /src/theory/uf | |
parent | 12cc3d32407cabbc8c3ed3d980199a020b61a883 (diff) |
TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 24 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 9 |
2 files changed, 15 insertions, 18 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 2a5eb682e..0c58d45e4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -26,13 +26,9 @@ using namespace CVC4::theory::uf; -//TODO remove -Node getOperator(Node x) { return Node::null(); } - - - TheoryUF::TheoryUF(Context* c, OutputChannel& out) : TheoryImpl<TheoryUF>(c, out), + d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c), @@ -47,6 +43,7 @@ void TheoryUF::preRegisterTerm(TNode n){ void TheoryUF::registerTerm(TNode n){ d_registered.push_back(n); + n.printAst(Warning()); ECData* ecN; @@ -148,7 +145,7 @@ bool TheoryUF::equiv(TNode x, TNode y){ if(x.getNumChildren() != y.getNumChildren()) return false; - if(getOperator(x) != getOperator(y)) + if(x.getOperator() != y.getOperator()) return false; TNode::iterator xIter = x.begin(); @@ -213,7 +210,8 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){ for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){ if(equiv(Px->data,Py->data)){ - d_pending.push_back((Px->data).eqNode(Py->data)); + Node pendingEq = (Px->data).eqNode(Py->data); + d_pending.push_back(pendingEq); } } } @@ -229,8 +227,11 @@ void TheoryUF::merge(){ TNode x = assertion[0]; TNode y = assertion[1]; - ECData* ecX = ccFind(x.getAttribute(ECAttr())); - ECData* ecY = ccFind(y.getAttribute(ECAttr())); + ECData* tmpX = x.getAttribute(ECAttr()); + ECData* tmpY = y.getAttribute(ECAttr()); + + ECData* ecX = ccFind(tmpX); + ECData* ecY = ccFind(tmpY); if(ecX == ecY) continue; @@ -241,8 +242,8 @@ void TheoryUF::merge(){ Node TheoryUF::constructConflict(TNode diseq){ NodeBuilder<> nb(kind::AND); nb << diseq; - for(unsigned i=0; i<d_pending.size(); ++i) - nb << d_pending[i]; + for(unsigned i=0; i<d_assertions.size(); ++i) + nb << d_assertions[i]; return nb; } @@ -253,6 +254,7 @@ void TheoryUF::check(Effort level){ switch(assertion.getKind()){ case EQUAL: + d_assertions.push_back(assertion); d_pending.push_back(assertion); merge(); break; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4fc835223..34b6719d7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -33,15 +33,10 @@ class TheoryUF : public TheoryImpl<TheoryUF> { private: - + //TODO document + context::CDList<Node> d_assertions; /** - * The associated context. Needed for allocating context dependent objects - * and objects in context dependent memory. - */ - context::Context* d_context; - - /** * List of pending equivalence class merges. * * Tricky part: |