diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 6 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 167 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 67 | ||||
-rw-r--r-- | test/unit/expr/node_manager_white.h | 56 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 16 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_white.h | 31 |
6 files changed, 235 insertions, 108 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1d5bcc230..b80d3bea3 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ parser/parser_black \ @@ -14,10 +15,7 @@ UNIT_TESTS = \ theory/theory_uf_white \ util/assert_white \ util/configuration_white \ - util/output_white \ - util/integer_black \ - util/integer_white \ - util/rational_white + util/output_white # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 21c19a8f9..c92ea31f5 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -196,7 +196,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar()); b = c; TS_ASSERT(b==c); @@ -210,18 +210,16 @@ public: void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation - * in the black box tests. - */ - + * in the black box tests. */ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a"); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b"); TS_ASSERT(a<b || b<a); TS_ASSERT(!(a<b && b<a)); - Node c = d_nodeManager->mkNode(NULL_EXPR); - Node d = d_nodeManager->mkNode(NULL_EXPR); + Node c = d_nodeManager->mkNode(AND, a, b); + Node d = d_nodeManager->mkNode(AND, a, b); TS_ASSERT(!(c<d)); TS_ASSERT(!(d<c)); @@ -233,48 +231,47 @@ public: * But what would be a convincing test of this property? */ - //Simple test of descending descendant property + // simple test of descending descendant property Node child = d_nodeManager->mkNode(TRUE); Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); - //Slightly less simple test of DD property. + // slightly less simple test of DD property std::vector<Node> chain; - int N = 500; - Node curr = d_nodeManager->mkNode(NULL_EXPR); - for(int i=0;i<N;i++) { + const int N = 500; + Node curr = d_nodeManager->mkNode(OR, a, b); + chain.push_back(curr); + for(int i = 0; i < N; ++i) { + curr = d_nodeManager->mkNode(AND, curr, curr); chain.push_back(curr); - curr = d_nodeManager->mkNode(AND, curr); } - for(int i=0;i<N;i++) { - for(int j=i+1;j<N;j++) { + for(int i = 0; i < N; ++i) { + for(int j = i + 1; j < N; ++j) { Node chain_i = chain[i]; Node chain_j = chain[j]; - TS_ASSERT(chain_i<chain_j); + TS_ASSERT(chain_i < chain_j); } } - } void testEqNode() { - /*Node eqNode(const Node& right) const;*/ + /* Node eqNode(const Node& right) const; */ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); Node eq = left.eqNode(right); - TS_ASSERT(EQUAL == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(eq[0] == left); TS_ASSERT(eq[1] == right); } void testNotNode() { - /* Node notNode() const;*/ + /* Node notNode() const; */ Node child = d_nodeManager->mkNode(TRUE); Node parent = child.notNode(); @@ -320,14 +317,16 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node cnd = d_nodeManager->mkNode(PLUS); + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); + + Node cnd = d_nodeManager->mkNode(PLUS, a, b); Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); Node ite = cnd.iteNode(thenBranch, elseBranch); - - TS_ASSERT(ITE == ite.getKind()); - TS_ASSERT(3 == ite.getNumChildren()); + TS_ASSERT(ITE == ite.getKind()); + TS_ASSERT(3 == ite.getNumChildren()); TS_ASSERT(*(ite.begin()) == cnd); TS_ASSERT(*(++ite.begin()) == thenBranch); @@ -378,20 +377,24 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testKindSingleton(Kind k) { - Node n = d_nodeManager->mkNode(k); - TS_ASSERT(k == n.getKind()); - } - void testGetKind() { /*inline Kind getKind() const; */ - testKindSingleton(NOT); - testKindSingleton(NULL_EXPR); - testKindSingleton(ITE); - testKindSingleton(SKOLEM); - } + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); + + Node n = d_nodeManager->mkNode(NOT, a); + TS_ASSERT(NOT == n.getKind()); + + n = d_nodeManager->mkNode(IFF, a, b); + TS_ASSERT(IFF == n.getKind()); + n = d_nodeManager->mkNode(PLUS, a, b); + TS_ASSERT(PLUS == n.getKind()); + + n = d_nodeManager->mkNode(UMINUS, a); + TS_ASSERT(UMINUS == n.getKind()); + } void testGetOperator() { Type* sort = d_nodeManager->mkSort("T"); @@ -400,50 +403,65 @@ public: Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); - Node fa = d_nodeManager->mkNode(kind::APPLY, f, a); + Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); TS_ASSERT( fa.hasOperator() ); TS_ASSERT( !f.hasOperator() ); TS_ASSERT( !a.hasOperator() ); + TS_ASSERT( fa.getNumChildren() == 1 ); + TS_ASSERT( f.getNumChildren() == 0 ); + TS_ASSERT( a.getNumChildren() == 0 ); + TS_ASSERT( f == fa.getOperator() ); +#ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( f.getOperator(), AssertionException ); TS_ASSERT_THROWS( a.getOperator(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } - void testNaryExpForSize(Kind k, int N){ + void testNaryExpForSize(Kind k, int N) { NodeBuilder<> nbz(k); - for(int i=0;i<N;i++){ - nbz << Node::null(); + Node trueNode = d_nodeManager->mkNode(TRUE); + for(int i = 0; i < N; ++i) { + nbz << trueNode; } Node result = nbz; - TS_ASSERT( N == result.getNumChildren()); + TS_ASSERT( N == result.getNumChildren() ); } - void testNumChildren(){ + void testNumChildren() { /*inline size_t getNumChildren() const;*/ + Node trueNode = d_nodeManager->mkNode(TRUE); + //test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); //test 1 - TS_ASSERT(1 == (Node::null().notNode()).getNumChildren()); + TS_ASSERT(1 == trueNode.notNode().getNumChildren()); //test 2 - TS_ASSERT(2 == (Node::null().andNode(Node::null())).getNumChildren() ); + TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren()); //Bigger tests srand(0); int trials = 500; - for(int i=0;i<trials; i++){ - int N = rand() % 1000; - testNaryExpForSize(NOT, N); + for(int i = 0; i < trials; ++i) { + int N = rand() % 1000 + 2; + testNaryExpForSize(AND, N); } +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( testNaryExpForSize(AND, 0), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(AND, 1), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(NOT, 0), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(NOT, 2), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } - void testIterator(){ + void testIterator() { NodeBuilder<> b; Node x = d_nodeManager->mkVar(); Node y = d_nodeManager->mkVar(); @@ -468,7 +486,7 @@ public: } } - void testToString(){ + void testToString() { Type* booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar(booleanType, "w"); @@ -481,7 +499,7 @@ public: TS_ASSERT(n.toString() == "(AND (OR w x) y z)"); } - void testToStream(){ + void testToStream() { Type* booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar(booleanType, "w"); @@ -490,9 +508,54 @@ public: Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; + Node o = NodeBuilder<>() << n << n << kind::XOR; stringstream sstr; n.toStream(sstr); TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + o.toStream(sstr); + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << Node::setdepth(0) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(0) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << Node::setdepth(1) << n; + TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)"); + + sstr.str(string()); + sstr << Node::setdepth(1) << o; + TS_ASSERT(sstr.str() == "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); + + sstr.str(string()); + sstr << Node::setdepth(2) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(2) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); + + sstr.str(string()); + sstr << Node::setdepth(3) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(3) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); } }; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 46e524f59..cae2e0637 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -56,8 +56,8 @@ public: template <unsigned N> void push_back(NodeBuilder<N>& nb, int n){ - for(int i=0; i<n; ++i){ - nb << Node::null(); + for(int i = 0; i < n; ++i){ + nb << d_nm->mkNode(TRUE); } } @@ -295,8 +295,7 @@ public: Node i_0 = d_nm->mkNode(FALSE); Node i_2 = d_nm->mkNode(TRUE); - Node i_K = d_nm->mkNode(NOT); - + Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_DEBUG TS_ASSERT_THROWS_ANYTHING(arr[-1];); @@ -314,23 +313,26 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - push_back(arr, K-3); + push_back(arr, K - 3); TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + for(int i = 3; i < K; ++i) { + TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + } arr << i_K; - TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + for(int i = 3; i < K; ++i) { + TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + } TS_ASSERT_EQUALS(arr[K], i_K); #ifdef CVC4_DEBUG Node n = arr; - TS_ASSERT_THROWS_ANYTHING(arr[0];); + TS_ASSERT_THROWS_ANYTHING(arr[0]); #endif } @@ -383,10 +385,10 @@ public: void testStreamInsertionKind() { /* NodeBuilder& operator<<(const Kind& k); */ -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS NodeBuilder<> spec(specKind); - TS_ASSERT_THROWS_ANYTHING( spec << PLUS; ); -#endif + TS_ASSERT_THROWS( spec << PLUS, AssertionException ); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> noSpec; noSpec << specKind; @@ -399,26 +401,32 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); + nb << d_nm->mkNode(TRUE) << d_nm->mkNode(FALSE); Node n = nb;// avoid warning on clear() nb.clear(PLUS); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING( nb << PLUS; ); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(n = nb, AssertionException); + nb.clear(PLUS); +#endif /* CVC4_ASSERTIONS */ + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( nb << PLUS, AssertionException ); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> testRef; TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS NodeBuilder<> testTwo; - TS_ASSERT_THROWS_ANYTHING(testTwo << specKind << PLUS;); -#endif + TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> testMixOrder1; - TS_ASSERT_EQUALS((testMixOrder1<< specKind << d_nm->mkNode(TRUE)).getKind(), + TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkNode(TRUE)).getKind(), specKind); NodeBuilder<> testMixOrder2; - TS_ASSERT_EQUALS((testMixOrder2<< d_nm->mkNode(TRUE)<<specKind).getKind(), + TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkNode(TRUE) << specKind).getKind(), specKind); } @@ -433,10 +441,10 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS Node n = nb; - TS_ASSERT_THROWS_ANYTHING(nb << n;); -#endif + TS_ASSERT_THROWS(nb << n, AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> overflow(specKind); TS_ASSERT_EQUALS(overflow.getKind(), specKind); @@ -518,9 +526,9 @@ public: TS_ASSERT_EQUALS(nexplicit.getKind(), specKind); TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(Node blah = implicit); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(Node blah = implicit, AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testToStream() { @@ -535,9 +543,8 @@ public: string astr, bstr, cstr; stringstream astream, bstream, cstream; - push_back(a,K/2); - push_back(b,K/2); - push_back(c,K/2); + push_back(a, K / 2); + push_back(b, K / 2); a.toStream(astream); b.toStream(bstream); @@ -661,7 +668,7 @@ public: // build one-past-the-end for(size_t j = 0; j <= n; ++j) { - b << Node::null(); + b << d_nm->mkNode(TRUE); } } } catch(Exception e) { diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h new file mode 100644 index 000000000..a43e32908 --- /dev/null +++ b/test/unit/expr/node_manager_white.h @@ -0,0 +1,56 @@ +/********************* */ +/** node_manager_white.h + ** 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) + ** 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::NodeManager. + **/ + +#include <cxxtest/TestSuite.h> + +#include <string> + +#include "expr/node_manager.h" +#include "context/context.h" + +#include "util/rational.h" +#include "util/integer.h" + +using namespace CVC4; +using namespace CVC4::expr; +using namespace CVC4::context; + +class NodeManagerWhite : public CxxTest::TestSuite { + + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_scope; + delete d_nm; + delete d_ctxt; + } + + void testMkConstInt() { + Integer i = "3"; + Node n = d_nm->mkConst(i); + Node m = d_nm->mkConst(i); + TS_ASSERT_EQUALS(n.getId(), m.getId()); + } +}; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 908ab81fc..5941b3e5d 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -211,10 +211,13 @@ public: void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); - 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); + Type* typeX = d_nm->booleanType(); + Type* typeF = d_nm->mkFunctionType(typeX, typeX); + + Node x = d_nm->mkVar(typeX, "x"); + Node f = d_nm->mkVar(typeF, "f"); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_x_eq_x = f_x.eqNode(x); Node x_eq_f_f_x = x.eqNode(f_f_x); @@ -225,11 +228,12 @@ public: TS_ASSERT_EQUALS(got, f_x_eq_x); - TS_ASSERT_EQUALS(4, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(5, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end()); @@ -239,7 +243,7 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(6, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(7, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 6958634e6..7be68aaa1 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -118,11 +118,11 @@ public: void testPushPopChain() { 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 f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); + Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); + Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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); @@ -173,9 +173,9 @@ public: 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_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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(); @@ -198,13 +198,12 @@ public: 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(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); - TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0)); + TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); } @@ -228,11 +227,11 @@ public: 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 f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); + Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); + Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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); @@ -270,7 +269,7 @@ public: void testPushPopB() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_x_eq_x = f_x.eqNode(x); d_euf->assertFact( f_x_eq_x ); |