summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.cpp20
-rw-r--r--src/expr/node.h36
-rw-r--r--src/theory/theory.h8
-rw-r--r--src/theory/uf/theory_uf.cpp24
-rw-r--r--src/theory/uf/theory_uf.h9
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/theory/theory_uf_white.h203
7 files changed, 254 insertions, 47 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 213171124..5c3f1b771 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -20,26 +20,6 @@ namespace CVC4 {
namespace expr {
#ifdef CVC4_DEBUG
-
-/**
- * Pretty printer for use within gdb. This is not intended to be used
- * outside of gdb. This writes to the Warning() stream and immediately
- * flushes the stream.
- *
- * Note that this function cannot be a template, since the compiler
- * won't instantiate it. Even if we explicitly instantiate. (Odd?)
- * So we implement twice.
- */
-void CVC4_PUBLIC debugPrint(const NodeTemplate<true>& n) {
- n.printAst(Warning(), 0);
- Warning().flush();
-}
-
-void CVC4_PUBLIC debugPrint(const NodeTemplate<false>& n) {
- n.printAst(Warning(), 0);
- Warning().flush();
-}
-
#endif /* CVC4_DEBUG */
}/* CVC4::expr namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 06f368583..25f0b7453 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -65,8 +65,8 @@ template<bool ref_count>
class NodeTemplate {
/**
- * The NodeValue has access to the private constructors, so that the iterators
- * can can create new nodes.
+ * The NodeValue has access to the private constructors, so that the
+ * iterators can can create new nodes.
*/
friend class NodeValue;
@@ -100,8 +100,8 @@ template<bool ref_count>
/**
* Assigns the expression value and does reference counting. No assumptions
- * are made on the expression, and should only be used if we know what we are
- * doing.
+ * are made on the expression, and should only be used if we know what we
+ * are doing.
*
* @param ev the expression value to assign
*/
@@ -575,7 +575,7 @@ template<bool ref_count>
if(ref_count)
d_nv->dec();
Assert(ref_count || d_nv->d_rc > 0,
- "Temporary node pointing to an expired node");
+ "Temporary node pointing to an expired node");
}
template<bool ref_count>
@@ -675,6 +675,32 @@ template<bool ref_count>
return NodeManager::currentNM()->getType(*this);
}
+
+
+/**
+ * Pretty printer for use within gdb. This is not intended to be used
+ * outside of gdb. This writes to the Warning() stream and immediately
+ * flushes the stream.
+ *
+ * Note that this function cannot be a template, since the compiler
+ * won't instantiate it. Even if we explicitly instantiate. (Odd?)
+ * So we implement twice.
+ *
+ * Tim's Note: I moved this into the node.h file because this allows gdb
+ * to find the symbol, and use it, which is the first standard this code needs
+ * to meet. A cleaner solution is welcomed.
+ */
+static void CVC4_PUBLIC debugPrintNode(const NodeTemplate<true>& n) {
+ n.printAst(Warning(), 0);
+ Warning().flush();
+}
+
+static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate<false>& n) {
+ n.printAst(Warning(), 0);
+ Warning().flush();
+}
+
+
}/* CVC4 namespace */
#endif /* __CVC4__NODE_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e079d67bd..f5b1e9b44 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -22,7 +22,7 @@
#include "context/context.h"
#include <queue>
-#include <vector>
+#include <list>
#include <typeinfo>
@@ -293,13 +293,13 @@ Node TheoryImpl<T>::get() {
d_facts.pop();
if(! fact.getAttribute(RegisteredAttr())) {
- std::vector<TNode> toReg;
+ std::list<TNode> toReg;
toReg.push_back(fact);
/* Essentially this is doing a breadth-first numbering of
* non-registered subterms with children. Any non-registered
* leaves are immediately registered. */
- for(std::vector<TNode>::iterator workp = toReg.begin();
+ for(std::list<TNode>::iterator workp = toReg.begin();
workp != toReg.end();
++workp) {
@@ -323,7 +323,7 @@ Node TheoryImpl<T>::get() {
* and the above registration of leaves, this should ensure that
* all subterms in the entire tree were registered in
* reverse-topological order. */
- for(std::vector<TNode>::reverse_iterator i = toReg.rend();
+ for(std::list<TNode>::reverse_iterator i = toReg.rend();
i != toReg.rbegin();
++i) {
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:
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 9fba9f7ff..5290381c3 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -7,6 +7,7 @@ UNIT_TESTS = \
parser/parser_black \
context/context_black \
context/context_mm_black \
+ theory/theory_uf_white \
util/assert_white \
util/configuration_white \
util/output_white
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
new file mode 100644
index 000000000..5aeb5f8a5
--- /dev/null
+++ b/test/unit/theory/theory_uf_white.h
@@ -0,0 +1,203 @@
+/********************* */
+/** theory_uf_white.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** 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.
+ **
+ ** White box testing of CVC4::theory::uf::TheoryUF.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+
+using namespace std;
+
+
+/**
+ * Very basic OutputChannel for testing simple Theory Behaviour.
+ * Stores a call sequence for the output channel
+ */
+enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION};
+class TestOutputChannel : public OutputChannel {
+private:
+ void push(OutputChannelCallType call, TNode n){
+ d_callHistory.push_back(make_pair(call,n));
+ }
+public:
+ vector< pair<OutputChannelCallType, Node> > d_callHistory;
+
+ TestOutputChannel() {}
+
+ ~TestOutputChannel() {}
+
+ void safePoint() throw(Interrupted) {}
+
+ void conflict(TNode n, bool safe = false) throw(Interrupted){
+ push(CONFLICT, n);
+ }
+
+ void propagate(TNode n, bool safe = false) throw(Interrupted){
+ push(PROPOGATE, n);
+ }
+
+ void lemma(TNode n, bool safe = false) throw(Interrupted){
+ push(LEMMA, n);
+ }
+ void explanation(TNode n, bool safe = false) throw(Interrupted){
+ push(EXPLANATION, n);
+ }
+
+ void clear(){
+ d_callHistory.clear();
+ }
+ Node getIthNode(int i){
+ Node tmp = (d_callHistory[i]).second;
+ return tmp;
+ }
+
+ OutputChannelCallType getIthCallType(int i){
+ return (d_callHistory[i]).first;
+ }
+
+ unsigned getNumCalls(){
+ return d_callHistory.size();
+ }
+};
+
+class TheoryUFWhite : public CxxTest::TestSuite {
+
+ NodeManagerScope *d_scope;
+ NodeManager *d_nm;
+
+ TestOutputChannel d_outputChannel;
+ Theory::Effort level;
+
+ Context* d_context;
+ TheoryUF* d_euf;
+
+public:
+
+ TheoryUFWhite(): level(Theory::FULL_EFFORT) { }
+
+ void setUp() {
+ d_nm = new NodeManager();
+ d_scope = new NodeManagerScope(d_nm);
+
+ d_context = new Context();
+
+ d_outputChannel.clear();
+ d_euf = new TheoryUF(d_context, d_outputChannel);
+ }
+
+ void tearDown() {
+ delete d_euf;
+ delete d_context;
+ delete d_scope;
+ delete d_nm;
+ }
+
+ /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
+ void testSimpleChain(){
+ Node x = d_nm->mkVar();
+ Node f = d_nm->mkVar();
+ Node f_x = d_nm->mkNode(kind::APPLY, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
+ Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x);
+
+ Node f_f_x_eq_x = f_f_x.eqNode(x);
+ Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode();
+
+ Node expectedConflict = f_f_f_x_neq_f_x.andNode(f_f_x_eq_x);
+
+ d_euf->assertFact(f_f_x_eq_x);
+ d_euf->assertFact(f_f_f_x_neq_f_x);
+ d_euf->check(level);
+
+ TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+ TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+
+ Node realConflict = d_outputChannel.getIthNode(0);
+ TS_ASSERT_EQUALS(expectedConflict, realConflict);
+
+ }
+
+ /* test that !(x == x) is inconsistent */
+ void testSelfInconsistent(){
+ Node x = d_nm->mkVar();
+ Node x_neq_x = (x.eqNode(x)).notNode();
+ Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x);
+
+ d_euf->assertFact(x_neq_x);
+ d_euf->check(level);
+
+ TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+ TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0));
+ TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+ }
+
+ /* test that (x == x) is consistent */
+ void testSelfConsistent(){
+ Node x = d_nm->mkVar();
+ Node x_eq_x = x.eqNode(x);
+
+ d_euf->assertFact(x_eq_x);
+ d_euf->check(level);
+
+ TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls());
+ }
+
+
+ /* test that
+ {f(f(f(x))) == x,
+ f(f(f(f(f(x))))) = x,
+ f(x) != x
+ } is inconsistent */
+ void testChain(){
+ Node x = d_nm->mkVar();
+ Node f = d_nm->mkVar();
+ Node f_x = d_nm->mkNode(kind::APPLY, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
+ Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x);
+ Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x);
+ Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x);
+
+ Node f3_x_eq_x = f_f_f_x.eqNode(x);
+ Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x);
+ Node f1_x_neq_x = f_x.eqNode(x).notNode();
+
+ Node expectedConflict = d_nm->mkNode(kind::AND,
+ f1_x_neq_x,
+ f3_x_eq_x,
+ f5_x_eq_x
+ );
+
+ d_euf->assertFact( f3_x_eq_x );
+ d_euf->assertFact( f5_x_eq_x );
+ d_euf->assertFact( f1_x_neq_x );
+ d_euf->check(level);
+
+ TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+ TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+ Node realConflict = d_outputChannel.getIthNode(0);
+ TS_ASSERT_EQUALS(expectedConflict, realConflict);
+ }
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback