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/theory | |
| 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/theory')
| -rw-r--r-- | test/unit/theory/theory_black.h | 6 | ||||
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 21 |
2 files changed, 17 insertions, 10 deletions
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)); |