diff options
Diffstat (limited to 'test/unit/expr/expr_public.h')
| -rw-r--r-- | test/unit/expr/expr_public.h | 78 |
1 files changed, 43 insertions, 35 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() { |