summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/Makefile.am6
-rw-r--r--test/unit/expr/node_black.h167
-rw-r--r--test/unit/expr/node_builder_black.h67
-rw-r--r--test/unit/expr/node_manager_white.h56
-rw-r--r--test/unit/theory/theory_black.h16
-rw-r--r--test/unit/theory/theory_uf_white.h31
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback