diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-15 09:35:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-15 09:35:27 -0600 |
commit | 829b3c2798c1f2c0bb313d7eff2c1e76f0184ae2 (patch) | |
tree | 6855fbf1b5bf7b11958a222f70e9301156931c0b /test/unit/util | |
parent | 9aeb23f2ae58e4f6dd2b53dbb47cf8c173e56d83 (diff) | |
parent | 94c4d5b54e7840fa36d76e7c3d52e19c31a1dbc1 (diff) |
Merge branch 'master' into refactorEagerSolverrefactorEagerSolver
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/array_store_all_white.cpp | 24 | ||||
-rw-r--r-- | test/unit/util/datatype_black.cpp | 4 |
2 files changed, 17 insertions, 11 deletions
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 1272926db..887a214dd 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -18,6 +18,8 @@ #include "test_smt.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace test { @@ -30,15 +32,15 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TypeNode usort = d_nodeManager->mkSort("U"); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(9, 2))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->integerType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); } TEST_F(TestUtilWhiteArrayStoreAll, type_errors) @@ -47,13 +49,14 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors) d_nodeManager->mkConst(UninterpretedConstant( d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); - ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(Rational(9, 2))), - IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), + IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->mkSort("U")), - d_nodeManager->mkConst(Rational(9, 2))), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), IllegalArgumentException); } @@ -70,9 +73,10 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkNode(kind::PLUS, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkConst(Rational(0)))), + d_nodeManager->mkNode( + kind::PLUS, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))), IllegalArgumentException); } } // namespace test diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 760bb2f75..15dde0cc2 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -21,6 +21,8 @@ #include "test_smt.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace test { @@ -247,7 +249,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) const DType& ldt = listType.getDType(); Node updater = ldt[0][0].getUpdater(); Node gt = listType.mkGroundTerm(); - Node zero = d_nodeManager->mkConst(Rational(0)); + Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero); |