From: Tim King Date: Fri, 26 Feb 2010 18:58:17 +0000 (+0000) Subject: TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently... X-Git-Tag: cvc5-1.0.0~9217 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3311e8276fb6221d9e100be2b1eec88d8f119fef;p=cvc5.git 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 --- 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& n) { - n.printAst(Warning(), 0); - Warning().flush(); -} - -void CVC4_PUBLIC debugPrint(const NodeTemplate& 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 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 /** * 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 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 @@ -675,6 +675,32 @@ template 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& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} + +static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate& 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 -#include +#include #include @@ -293,13 +293,13 @@ Node TheoryImpl::get() { d_facts.pop(); if(! fact.getAttribute(RegisteredAttr())) { - std::vector toReg; + std::list 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::iterator workp = toReg.begin(); + for(std::list::iterator workp = toReg.begin(); workp != toReg.end(); ++workp) { @@ -323,7 +323,7 @@ Node TheoryImpl::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::reverse_iterator i = toReg.rend(); + for(std::list::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(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 { private: - + //TODO document + context::CDList 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 + +#include "theory/theory.h" +#include "theory/uf/theory_uf.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "context/context.h" + +#include + +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 > 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); + } +};