summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/api/java/cvc5/SolverTest.java31
-rw-r--r--test/unit/api/java/cvc5/TermTest.java34
-rw-r--r--test/unit/api/solver_black.cpp27
-rw-r--r--test/unit/api/term_black.cpp34
-rw-r--r--test/unit/theory/type_enumerator_white.cpp12
-rw-r--r--test/unit/util/array_store_all_white.cpp8
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))),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback