summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/expr/expr_public.h78
-rw-r--r--test/unit/theory/theory_black.h6
-rw-r--r--test/unit/theory/type_enumerator_white.h21
-rw-r--r--test/unit/util/CMakeLists.txt2
-rw-r--r--test/unit/util/array_store_all_black.h83
-rw-r--r--test/unit/util/array_store_all_white.h94
6 files changed, 155 insertions, 129 deletions
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 86de45fe9..f8ccd23d4 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -23,6 +23,9 @@
#include "base/exception.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
#include "options/options.h"
using namespace CVC4;
@@ -85,7 +88,6 @@ class ExprPublic : public CxxTest::TestSuite {
delete c_bool_and;
delete b_bool;
delete a_bool;
-
delete d_slv;
}
catch (Exception& e)
@@ -369,40 +371,46 @@ class ExprPublic : public CxxTest::TestSuite {
TS_ASSERT(cons_1_nil.isConst());
TS_ASSERT(cons_1_cons_2_nil.isConst());
- ArrayType arrType = d_em->mkArrayType(d_em->integerType(), d_em->integerType());
- Expr zero = d_em->mkConst(Rational(0));
- Expr one = d_em->mkConst(Rational(1));
- Expr storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
- TS_ASSERT(storeAll.isConst());
-
- Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
- TS_ASSERT(!arr.isConst());
- arr = d_em->mkExpr(STORE, storeAll, zero, one);
- TS_ASSERT(arr.isConst());
- Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, one);
- TS_ASSERT(arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, zero, one);
- TS_ASSERT(!arr2.isConst());
-
- arrType = d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
- zero = d_em->mkConst(BitVector(1,unsigned(0)));
- one = d_em->mkConst(BitVector(1,unsigned(1)));
- storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
- TS_ASSERT(storeAll.isConst());
-
- arr = d_em->mkExpr(STORE, storeAll, zero, zero);
- TS_ASSERT(!arr.isConst());
- arr = d_em->mkExpr(STORE, storeAll, zero, one);
- TS_ASSERT(arr.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, zero);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, one);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, zero, one);
- TS_ASSERT(!arr2.isConst());
-
+ {
+ ExprManagerScope ems(*d_em);
+ ArrayType arrType =
+ d_em->mkArrayType(d_em->integerType(), d_em->integerType());
+ Expr zero = d_em->mkConst(Rational(0));
+ Expr one = d_em->mkConst(Rational(1));
+ Expr storeAll = d_em->mkConst(
+ ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
+ TS_ASSERT(storeAll.isConst());
+
+ Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+
+ arrType =
+ d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
+ zero = d_em->mkConst(BitVector(1, unsigned(0)));
+ one = d_em->mkConst(BitVector(1, unsigned(1)));
+ storeAll = d_em->mkConst(
+ ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
+ TS_ASSERT(storeAll.isConst());
+
+ arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+ }
}
void testGetConst() {
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 45d13d416..b1b79ec07 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -62,7 +62,7 @@ class TheoryBlack : public CxxTest::TestSuite {
TypeNode arrType = d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
- Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
TS_ASSERT(storeAll.isConst());
Node arr = d_nm->mkNode(STORE, storeAll, zero, zero);
@@ -85,7 +85,7 @@ class TheoryBlack : public CxxTest::TestSuite {
arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(1), d_nm->mkBitVectorType(1));
zero = d_nm->mkConst(BitVector(1,unsigned(0)));
one = d_nm->mkConst(BitVector(1,unsigned(1)));
- storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
TS_ASSERT(storeAll.isConst());
arr = d_nm->mkNode(STORE, storeAll, zero, zero);
@@ -113,7 +113,7 @@ class TheoryBlack : public CxxTest::TestSuite {
one = d_nm->mkConst(BitVector(2,unsigned(1)));
Node two = d_nm->mkConst(BitVector(2,unsigned(2)));
Node three = d_nm->mkConst(BitVector(2,unsigned(3)));
- storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), one.toExpr()));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType, one));
TS_ASSERT(storeAll.isConst());
arr = d_nm->mkNode(STORE, storeAll, zero, zero);
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index f8ce734ec..b996919ee 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -234,13 +234,20 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
TS_ASSERT( ! te.isFinished() );
// ensure that certain items were found
- ArrayType arrayType(d_em->mkArrayType(d_em->integerType(), d_em->integerType()));
- Node zeroes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(0))));
- Node ones = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(1))));
- Node twos = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(2))));
- Node threes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(3))));
- Node fours = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(4))));
- Node tens = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(10))));
+ TypeNode arrayType =
+ d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
+ Node zeroes =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(0))));
+ Node ones =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(1))));
+ Node twos =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(2))));
+ Node threes =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(3))));
+ Node fours =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(4))));
+ Node tens =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(10))));
Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 0748e1059..5bccc9137 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,7 +1,7 @@
#-----------------------------------------------------------------------------#
# Add unit tests
-cvc4_add_unit_test_black(array_store_all_black util)
+cvc4_add_unit_test_white(array_store_all_white util)
cvc4_add_unit_test_white(assert_white util)
cvc4_add_unit_test_black(binary_heap_black util)
cvc4_add_unit_test_black(bitvector_black util)
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
deleted file mode 100644
index bf0163317..000000000
--- a/test/unit/util/array_store_all_black.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/********************* */
-/*! \file array_store_all_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::ArrayStoreAll
- **
- ** Black box testing of CVC4::ArrayStoreAll.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-#include "expr/array_store_all.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/type.h"
-#include "test_utils.h"
-
-using namespace CVC4;
-using namespace std;
-
-class ArrayStoreAllBlack : public CxxTest::TestSuite {
- public:
- void setUp() override
- {
- d_slv = new api::Solver();
- d_em = d_slv->getExprManager();
- }
-
- void tearDown() override { delete d_slv; }
-
- void testStoreAll() {
- Type usort = d_em->mkSort("U");
- ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()),
- d_em->mkConst(Rational(9, 2)));
- ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort),
- d_em->mkConst(UninterpretedConstant(usort, 0)));
- ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()),
- d_em->mkConst(Rational(0)));
- ArrayStoreAll(
- d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()),
- d_em->mkConst(Rational(0)));
- }
-
- void testTypeErrors()
- {
- TS_ASSERT_THROWS(ArrayStoreAll(d_em->integerType(),
- d_em->mkConst(UninterpretedConstant(
- d_em->mkSort("U"), 0))),
- IllegalArgumentException&);
- TS_ASSERT_THROWS(
- ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))),
- IllegalArgumentException&);
- TS_ASSERT_THROWS(
- ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")),
- d_em->mkConst(Rational(9, 2))),
- IllegalArgumentException&);
- }
-
- void testConstError() {
- Type usort = d_em->mkSort("U");
- TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
- d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)));
- TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
- d_em->integerType(), d_em->mkVar("x", d_em->integerType())));
- TS_ASSERT_THROWS_ANYTHING(
- ArrayStoreAll(d_em->integerType(),
- d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)),
- d_em->mkConst(Rational(0)))));
- }
-
- private:
- api::Solver* d_slv;
- ExprManager* d_em;
-}; /* class ArrayStoreAllBlack */
diff --git a/test/unit/util/array_store_all_white.h b/test/unit/util/array_store_all_white.h
new file mode 100644
index 000000000..fb7857003
--- /dev/null
+++ b/test/unit/util/array_store_all_white.h
@@ -0,0 +1,94 @@
+/********************* */
+/*! \file array_store_all_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::ArrayStoreAll
+ **
+ ** Black box testing of CVC4::ArrayStoreAll.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+#include "expr/array_store_all.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/type.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "test_utils.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ArrayStoreAllWhite : public CxxTest::TestSuite
+{
+ public:
+ void setUp() override
+ {
+ d_slv = new api::Solver();
+ d_scope = new smt::SmtScope(d_slv->getSmtEngine());
+ d_nm = d_slv->getSmtEngine()->d_nodeManager;
+ }
+
+ void tearDown() override
+ {
+ delete d_scope;
+ delete d_slv;
+ }
+
+ void testStoreAll()
+ {
+ TypeNode usort = d_nm->mkSort("U");
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()),
+ d_nm->mkConst(Rational(9, 2)));
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort),
+ d_nm->mkConst(UninterpretedConstant(usort.toType(), 0)));
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()),
+ d_nm->mkConst(Rational(0)));
+ ArrayStoreAll(
+ d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()),
+ d_nm->mkConst(Rational(0)));
+ }
+
+ void testTypeErrors()
+ {
+ TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(),
+ d_nm->mkConst(UninterpretedConstant(
+ d_nm->mkSort("U").toType(), 0))),
+ IllegalArgumentException&);
+ TS_ASSERT_THROWS(
+ ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))),
+ IllegalArgumentException&);
+ TS_ASSERT_THROWS(
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")),
+ d_nm->mkConst(Rational(9, 2))),
+ IllegalArgumentException&);
+ }
+
+ void testConstError()
+ {
+ TypeNode usort = d_nm->mkSort("U");
+ TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+ d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort)));
+ TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+ d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType())));
+ TS_ASSERT_THROWS_ANYTHING(
+ ArrayStoreAll(d_nm->integerType(),
+ d_nm->mkNode(kind::PLUS,
+ d_nm->mkConst(Rational(1)),
+ d_nm->mkConst(Rational(0)))));
+ }
+
+ private:
+ api::Solver* d_slv;
+ smt::SmtScope* d_scope;
+ NodeManager* d_nm;
+}; /* class ArrayStoreAllBlack */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback