diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/error.cvc | 2 | ||||
-rwxr-xr-x | test/regress/run_regression | 12 | ||||
-rw-r--r-- | test/unit/expr/attribute_black.h | 3 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 17 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 27 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 27 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_white.h | 27 |
7 files changed, 69 insertions, 46 deletions
diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index 09a69e212..982731b34 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,4 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared +% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared p : BOOL; % EXIT: 1 diff --git a/test/regress/run_regression b/test/regress/run_regression index 65ab6c31a..439c8e6c9 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -77,7 +77,17 @@ else echo "$expected_error" >"$experrfile" fi -("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" +cvc4dir=`dirname "$cvc4"` +cvc4dirfull=`cd "$cvc4dir" && pwd` +if [ -z "$cvc4dirfull" ]; then + error "getting directory of \`$cvc4 !?" +fi +cvc4base=`basename "$cvc4"` +cvc4full="$cvc4dirfull/$cvc4base" +( cd `dirname "$benchmark"`; + "$cvc4full" --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" +) > "$outfile" 2> "$errfile" diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index eb728c62c..e87c8d708 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -70,7 +70,8 @@ public: typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute; void testDeallocation() { - Node* node = new Node(d_nodeManager->mkVar()); + Type* booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkVar(booleanType)); MyData* data; MyData* data1; MyDataAttribute attr; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 64c768a13..e0d9d6bf4 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -60,6 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite { Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -67,6 +68,8 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); + + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -150,9 +153,9 @@ public: //Debug.on("boolattr"); - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); + Node a = d_nm->mkVar(d_booleanType); + Node b = d_nm->mkVar(d_booleanType); + Node c = d_nm->mkVar(d_booleanType); Debug("boolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -280,10 +283,10 @@ public: //Debug.on("boolattr"); - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node unnamed = d_nm->mkVar(); + Node a = d_nm->mkVar(d_booleanType); + Node b = d_nm->mkVar(d_booleanType); + Node c = d_nm->mkVar(d_booleanType); + Node unnamed = d_nm->mkVar(d_booleanType); a.setAttribute(VarNameAttr(), "a"); b.setAttribute(VarNameAttr(), "b"); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index d420c6e26..9e199aa9a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -36,6 +36,7 @@ private: Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -43,6 +44,8 @@ public: d_ctxt = new Context; d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); + + d_booleanType = d_nodeManager->booleanType(); } void tearDown() { @@ -94,12 +97,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkVar(); + b = d_nodeManager->mkVar(d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(); + Node d = d_nodeManager->mkVar(d_booleanType); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -134,12 +137,12 @@ public: Node a, b, c; - b = d_nodeManager->mkVar(); + b = d_nodeManager->mkVar(d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(); + Node d = d_nodeManager->mkVar(d_booleanType); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a, !(a==a))); @@ -196,7 +199,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar()); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType)); b = c; TS_ASSERT(b==c); @@ -317,8 +320,8 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + Node a = d_nodeManager->mkVar(d_booleanType); + Node b = d_nodeManager->mkVar(d_booleanType); Node cnd = d_nodeManager->mkNode(PLUS, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -380,8 +383,8 @@ public: void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + Node a = d_nodeManager->mkVar(d_booleanType); + Node b = d_nodeManager->mkVar(d_booleanType); Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); @@ -463,9 +466,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkVar(); - Node y = d_nodeManager->mkVar(); - Node z = d_nodeManager->mkVar(); + Node x = d_nodeManager->mkVar(d_booleanType); + Node y = d_nodeManager->mkVar(d_booleanType); + Node z = d_nodeManager->mkVar(d_booleanType); Node n = b << x << y << z << kind::AND; { // iterator diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 2a7b3623e..eec6949f0 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -37,6 +37,7 @@ private: Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -44,7 +45,9 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); + specKind = PLUS; + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -209,9 +212,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nm->mkVar(); - Node y = d_nm->mkVar(); - Node z = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); + Node y = d_nm->mkVar(d_booleanType); + Node z = d_nm->mkVar(d_booleanType); b << x << y << z << AND; { @@ -460,9 +463,9 @@ public: } void testAppend() { - Node x = d_nm->mkVar(); - Node y = d_nm->mkVar(); - Node z = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); + Node y = d_nm->mkVar(d_booleanType); + Node z = d_nm->mkVar(d_booleanType); Node m = d_nm->mkNode(AND, y, z, x); Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); Node o = d_nm->mkNode(XOR, y, x); @@ -587,12 +590,12 @@ public: } void testConvenienceBuilders() { - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node d = d_nm->mkVar(); - Node e = d_nm->mkVar(); - Node f = d_nm->mkVar(); + Node a = d_nm->mkVar(d_booleanType); + Node b = d_nm->mkVar(d_booleanType); + Node c = d_nm->mkVar(d_booleanType); + Node d = d_nm->mkVar(d_booleanType); + Node e = d_nm->mkVar(d_booleanType); + Node f = d_nm->mkVar(d_booleanType); Node m = a && b; Node n = a && b || c; diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index a204d79b7..369be5a16 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -31,7 +31,6 @@ using namespace CVC4::context; using namespace std; - /** * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel @@ -95,6 +94,8 @@ class TheoryUFWhite : public CxxTest::TestSuite { TheoryUF* d_euf; + Type* d_booleanType; + public: TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} @@ -105,6 +106,8 @@ public: d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); d_euf = new TheoryUF(d_ctxt, d_outputChannel); + + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -116,8 +119,8 @@ public: } void testPushPopChain() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); + Node f = d_nm->mkVar(d_booleanType); 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); @@ -171,8 +174,8 @@ public: /* 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 x = d_nm->mkVar(d_booleanType); + Node f = d_nm->mkVar(d_booleanType); 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); @@ -196,7 +199,7 @@ public: /* test that !(x == x) is inconsistent */ void testSelfInconsistent() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_neq_x = (x.eqNode(x)).notNode(); d_euf->assertFact(x_neq_x); @@ -209,7 +212,7 @@ public: /* test that (x == x) is consistent */ void testSelfConsistent() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_eq_x = x.eqNode(x); d_euf->assertFact(x_eq_x); @@ -225,8 +228,8 @@ public: f(x) != x } is inconsistent */ void testChain() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); + Node f = d_nm->mkVar(d_booleanType); 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); @@ -256,7 +259,7 @@ public: void testPushPopA() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_eq_x = x.eqNode(x); d_ctxt->push(); @@ -267,8 +270,8 @@ public: } void testPushPopB() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); + Node f = d_nm->mkVar(d_booleanType); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_x_eq_x = f_x.eqNode(x); |