diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-13 19:48:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 21:48:07 -0500 |
commit | 78c0daa482b35b95c90dd058ee4dd8a981e1337f (patch) | |
tree | c45fe72ac96032b0e6f7ea53798443671ad08d86 /test/unit | |
parent | 84fe644cb1956119b7b35ede06ee93583eae1925 (diff) |
Use TypeNode/Node in ArrayStoreAll (#4728)
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/expr_public.h | 78 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 6 | ||||
-rw-r--r-- | test/unit/theory/type_enumerator_white.h | 21 | ||||
-rw-r--r-- | test/unit/util/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/unit/util/array_store_all_black.h | 83 | ||||
-rw-r--r-- | test/unit/util/array_store_all_white.h | 94 |
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 */ |