diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/java/cvc5/SolverTest.java | 31 | ||||
-rw-r--r-- | test/unit/api/java/cvc5/TermTest.java | 34 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 27 | ||||
-rw-r--r-- | test/unit/api/term_black.cpp | 34 | ||||
-rw-r--r-- | test/unit/theory/type_enumerator_white.cpp | 12 | ||||
-rw-r--r-- | test/unit/util/array_store_all_white.cpp | 8 |
6 files changed, 33 insertions, 113 deletions
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..9694510d9 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -386,35 +386,6 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO)); } - @Test void mkUninterpretedConst() throws CVC5ApiException - { - assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - assertThrows( - CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1)); - Solver slv = new Solver(); - assertThrows( - CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - } - - @Test void mkAbstractValue() throws CVC5ApiException - { - assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2")); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf")); - - assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1)); - // java does not have specific types for unsigned integers, therefore the two lines below do not - // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1)); - // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0)); - } - @Test void mkFloatingPoint() throws CVC5ApiException { Term t1 = d_solver.mkBitVector(8); @@ -2342,4 +2313,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -}
\ No newline at end of file +} diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java index 98f668006..a4b51ab1d 100644 --- a/test/unit/api/java/cvc5/TermTest.java +++ b/test/unit/api/java/cvc5/TermTest.java @@ -834,16 +834,17 @@ class TermTest @Test void getAbstractValue() throws CVC5ApiException { - Term v1 = d_solver.mkAbstractValue(1); - Term v2 = d_solver.mkAbstractValue("15"); - Term v3 = d_solver.mkAbstractValue("18446744073709551617"); - - assertTrue(v1.isAbstractValue()); - assertTrue(v2.isAbstractValue()); - assertTrue(v3.isAbstractValue()); - assertEquals("1", v1.getAbstractValue()); - assertEquals("15", v2.getAbstractValue()); - assertEquals("18446744073709551617", v3.getAbstractValue()); + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + assertTrue(d_solver.checkSat().isSat()); + Term vx = d_solver.getValue(x); + Term vy = d_solver.getValue(y); + assertEquals(vx.isAbstractValue(), vy.isAbstractValue()); + assertDoesNotThrow(() -> vx.getAbstractValue()); + assertDoesNotThrow(() -> vy.getAbstractValue()); } @Test void getTuple() @@ -948,19 +949,6 @@ class TermTest assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue())); } - @Test void getUninterpretedConst() throws CVC5ApiException - { - Sort s = d_solver.mkUninterpretedSort("test"); - Term t1 = d_solver.mkUninterpretedConst(s, 3); - Term t2 = d_solver.mkUninterpretedConst(s, 5); - - assertTrue(t1.isUninterpretedValue()); - assertTrue(t2.isUninterpretedValue()); - - assertEquals(new Pair<Sort, Integer>(s, 3), t1.getUninterpretedValue()); - assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue()); - } - @Test void substitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..5669f9803 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,33 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - -TEST_F(TestApiBlackSolver, mkAbstractValue) -{ - ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException); - - ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1)); - ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkFloatingPoint) { Term t1 = d_solver.mkBitVector(8); diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 7cfbe2527..3c4493ac6 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -885,16 +885,17 @@ TEST_F(TestApiBlackTerm, getBitVector) TEST_F(TestApiBlackTerm, getAbstractValue) { - Term v1 = d_solver.mkAbstractValue(1); - Term v2 = d_solver.mkAbstractValue("15"); - Term v3 = d_solver.mkAbstractValue("18446744073709551617"); - - ASSERT_TRUE(v1.isAbstractValue()); - ASSERT_TRUE(v2.isAbstractValue()); - ASSERT_TRUE(v3.isAbstractValue()); - ASSERT_EQ("1", v1.getAbstractValue()); - ASSERT_EQ("15", v2.getAbstractValue()); - ASSERT_EQ("18446744073709551617", v3.getAbstractValue()); + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + ASSERT_TRUE(d_solver.checkSat().isSat()); + Term vx = d_solver.getValue(x); + Term vy = d_solver.getValue(y); + ASSERT_TRUE(vx.isAbstractValue()); + ASSERT_TRUE(vy.isAbstractValue()); + ASSERT_EQ(vx.getAbstractValue(), vy.getAbstractValue()); } TEST_F(TestApiBlackTerm, getTuple) @@ -994,19 +995,6 @@ TEST_F(TestApiBlackTerm, getSequence) ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue()); } -TEST_F(TestApiBlackTerm, getUninterpretedConst) -{ - Sort s = d_solver.mkUninterpretedSort("test"); - Term t1 = d_solver.mkUninterpretedConst(s, 3); - Term t2 = d_solver.mkUninterpretedConst(s, 5); - - ASSERT_TRUE(t1.isUninterpretedValue()); - ASSERT_TRUE(t2.isUninterpretedValue()); - - ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue()); - ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue()); -} - TEST_F(TestApiBlackTerm, substitute) { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index bb7ef871c..f62fd7971 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,10 +22,10 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "options/language.h" #include "test_smt.h" #include "theory/type_enumerator.h" +#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/rational.h" @@ -61,13 +61,13 @@ TEST_F(TestTheoryWhiteTypeEnumerator, uf) TypeNode sort = d_nodeManager->mkSort("T"); TypeNode sort2 = d_nodeManager->mkSort("U"); TypeEnumerator te(sort); - ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0))); + ASSERT_EQ(*te, d_nodeManager->mkConst(AbstractValue(sort, 0))); for (size_t i = 1; i < 100; ++i) { - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2))); + ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort2, i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(AbstractValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort, i + 2))); } } diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 1272926db..d7bc4b412 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,8 +14,8 @@ */ #include "expr/array_store_all.h" -#include "expr/uninterpreted_constant.h" #include "test_smt.h" +#include "util/abstract_value.h" #include "util/rational.h" namespace cvc5 { @@ -32,7 +32,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) d_nodeManager->realType()), d_nodeManager->mkConst(Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), - d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); + d_nodeManager->mkConst(AbstractValue(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), d_nodeManager->mkConst(Rational(0))); @@ -44,8 +44,8 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TEST_F(TestUtilWhiteArrayStoreAll, type_errors) { ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(UninterpretedConstant( - d_nodeManager->mkSort("U"), 0))), + d_nodeManager->mkConst( + AbstractValue(d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), d_nodeManager->mkConst(Rational(9, 2))), |