From e24352317b31bfcc9e3be53909e152cfdcd72a28 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 30 Mar 2010 04:59:16 +0000 Subject: Highlights of this commit are: * add NodeManagerWhite unit test * change kind::APPLY to kind::APPLY_UF * better APPLY handling: operators are no longer considered children * more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed * extend DSL for kind declarations + new "theory" command declares a theory and its header. theory_def.h no longer required. + arity enforced on operators + constant mapping, hashing, equality * CONSTANT metakinds supported (via Node::getConst(), for example, Node::getConst() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind) * added CONST_RATIONAL and CONST_INTEGER kinds * builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager * Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5) * getters added to Node, TNode, NodeValue, etc., for operators and metakinds * build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand. * DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite(). * add gmpxx detection and inclusion * better Asserts throughout, some documentation, cleanup --- test/unit/Makefile.am | 6 +- test/unit/expr/node_black.h | 167 +++++++++++++++++++++++++----------- test/unit/expr/node_builder_black.h | 67 ++++++++------- test/unit/expr/node_manager_white.h | 56 ++++++++++++ test/unit/theory/theory_black.h | 16 ++-- test/unit/theory/theory_uf_white.h | 31 ++++--- 6 files changed, 235 insertions(+), 108 deletions(-) create mode 100644 test/unit/expr/node_manager_white.h (limited to 'test') 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(amkNode(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(!(cmkNode(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 chain; - int N = 500; - Node curr = d_nodeManager->mkNode(NULL_EXPR); - for(int i=0;imkNode(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;imkNode(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;imkNode(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 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 void push_back(NodeBuilder& nb, int n){ - for(int i=0; imkNode(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;imkNode(TRUE)); + } arr << i_K; - TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i=3;imkNode(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)<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 + +#include + +#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 ); -- cgit v1.2.3