summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/api/reset_assertions.cpp4
-rw-r--r--test/api/sep_log_api.cpp4
-rw-r--r--test/regress/regress0/get-value-reals-ints.smt22
-rw-r--r--test/regress/regress0/get-value-reals.smt22
-rw-r--r--test/unit/api/grammar_black.h4
-rw-r--r--test/unit/api/python/test_grammar.py4
-rw-r--r--test/unit/api/python/test_term.py14
-rw-r--r--test/unit/api/python/test_to_python_obj.py19
-rw-r--r--test/unit/api/solver_black.h108
-rw-r--r--test/unit/api/term_black.h69
-rw-r--r--test/unit/theory/theory_sets_type_rules_white.h2
11 files changed, 123 insertions, 109 deletions
diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 73629a0d0..2168d053e 100644
--- a/test/api/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
@@ -31,7 +31,7 @@ int main()
Sort real = slv.getRealSort();
Term x = slv.mkConst(real, "x");
- Term four = slv.mkReal(4);
+ Term four = slv.mkInteger(4);
Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
slv.assertFormula(xEqFour);
std::cout << slv.checkSat() << std::endl;
@@ -43,7 +43,7 @@ int main()
Sort arrayType = slv.mkArraySort(indexType, elementType);
Term array = slv.mkConst(arrayType, "array");
Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
- Term ten = slv.mkReal(10);
+ Term ten = slv.mkInteger(10);
Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
slv.assertFormula(arrayAtFour_eq_ten);
std::cout << slv.checkSat() << std::endl;
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index f0a55cf79..1b1efb07e 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -135,10 +135,10 @@ int validate_getters(void)
Sort integer = slv.getIntegerSort();
/* A "random" constant */
- Term random_constant = slv.mkReal(0xDEADBEEF);
+ Term random_constant = slv.mkInteger(0xDEADBEEF);
/* Another random constant */
- Term expr_nil_val = slv.mkReal(0xFBADBEEF);
+ Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
/* Our nil term */
Term nil = slv.mkSepNil(integer);
diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2
index b75f535d5..c8d3bb348 100644
--- a/test/regress/regress0/get-value-reals-ints.smt2
+++ b/test/regress/regress0/get-value-reals-ints.smt2
@@ -1,5 +1,5 @@
; EXPECT: sat
-; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6)))
+; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2.0) 1.0)) (neg_int (- 6)))
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)
(set-logic QF_LIRA)
diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
index 09ec0917f..d27581114 100644
--- a/test/regress/regress0/get-value-reals.smt2
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -1,5 +1,5 @@
; EXPECT: sat
-; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
+; EXPECT: ((pos_int (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2.0) 1.0)))
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)
(set-logic QF_LRA)
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
index bf0d97e9d..afbd09d0f 100644
--- a/test/unit/api/grammar_black.h
+++ b/test/unit/api/grammar_black.h
@@ -57,7 +57,7 @@ void GrammarBlack::testAddRule()
TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
CVC4ApiException&);
- TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+ TS_ASSERT_THROWS(g.addRule(start, d_solver->mkInteger(0)), CVC4ApiException&);
d_solver->synthFun("f", {}, boolean, g);
@@ -83,7 +83,7 @@ void GrammarBlack::testAddRules()
TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&);
TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}),
CVC4ApiException&);
- TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+ TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkInteger(0)}), CVC4ApiException&);
d_solver->synthFun("f", {}, boolean, g);
diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index 0321f03d0..5a0d5101f 100644
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -38,7 +38,7 @@ def test_add_rule():
with pytest.raises(Exception):
g.addRule(nts, solver.mkBoolean(false))
with pytest.raises(Exception):
- g.addRule(start, solver.mkReal(0))
+ g.addRule(start, solver.mkInteger(0))
# expecting no errors
solver.synthFun("f", {}, boolean, g)
@@ -68,7 +68,7 @@ def test_add_rules():
with pytest.raises(Exception):
g.addRules(nts, {solver.mkBoolean(False)})
with pytest.raises(Exception):
- g.addRules(start, {solver.mkReal(0)})
+ g.addRules(start, {solver.mkInteger(0)})
#Expecting no errors
solver.synthFun("f", {}, boolean, g)
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 9c25b584f..a0c1b4681 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -103,26 +103,12 @@ def test_get_op():
assert fx.getOp() == solver.mkOp(kinds.ApplyUf)
-def test_is_const():
- solver = pycvc4.Solver()
- intsort = solver.getIntegerSort()
- one = solver.mkReal(1)
- x = solver.mkConst(intsort, 'x')
- xpone = solver.mkTerm(kinds.Plus, x, one)
- onepone = solver.mkTerm(kinds.Plus, one, one)
- assert not x.isValue()
- assert one.isValue()
- assert not xpone.isValue()
- assert not onepone.isValue()
-
def test_const_sequence_elements():
solver = pycvc4.Solver()
realsort = solver.getRealSort()
seqsort = solver.mkSequenceSort(realsort)
s = solver.mkEmptySequence(seqsort)
- assert s.isValue()
-
assert s.getKind() == kinds.ConstSequence
# empty sequence has zero elements
cs = s.getConstSequenceElements()
diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py
index 3ce08f6b8..eb15e7469 100644
--- a/test/unit/api/python/test_to_python_obj.py
+++ b/test/unit/api/python/test_to_python_obj.py
@@ -15,7 +15,7 @@ def testGetBool():
def testGetInt():
solver = pycvc4.Solver()
- two = solver.mkReal(2)
+ two = solver.mkInteger(2)
assert two.toPythonObj() == 2
@@ -27,7 +27,7 @@ def testGetReal():
neg34 = solver.mkReal("-3/4")
assert neg34.toPythonObj() == Fraction(-3, 4)
- neg1 = solver.mkReal("-1")
+ neg1 = solver.mkInteger("-1")
assert neg1.toPythonObj() == -1
@@ -40,12 +40,10 @@ def testGetBV():
def testGetArray():
solver = pycvc4.Solver()
arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
- zero_array = solver.mkConstArray(arrsort, solver.mkReal(0))
- stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2))
- stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3))
- stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5))
-
- assert stores.isValue()
+ zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0))
+ stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2))
+ stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3))
+ stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5))
array_dict = stores.toPythonObj()
@@ -58,10 +56,7 @@ def testGetArray():
def testGetSymbol():
solver = pycvc4.Solver()
- x = solver.mkConst(solver.getBooleanSort(), "x")
-
- with pytest.raises(RuntimeError):
- x.toPythonObj()
+ solver.mkConst(solver.getBooleanSort(), "x")
def testGetString():
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 8b8c6dd58..1324e3890 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -72,6 +72,7 @@ class SolverBlack : public CxxTest::TestSuite
void testMkPi();
void testMkPosInf();
void testMkPosZero();
+ void testMkInteger();
void testMkReal();
void testMkRegexpEmpty();
void testMkRegexpSigma();
@@ -598,7 +599,7 @@ void SolverBlack::testMkFloatingPoint()
{
Term t1 = d_solver->mkBitVector(8);
Term t2 = d_solver->mkBitVector(4);
- Term t3 = d_solver->mkReal(2);
+ Term t3 = d_solver->mkInteger(2);
if (CVC4::Configuration::isBuiltWithSymFPU())
{
TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1));
@@ -742,6 +743,47 @@ void SolverBlack::testMkOp()
void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
+void SolverBlack::testMkInteger()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger("123"));
+ TS_ASSERT_THROWS(d_solver->mkInteger("1.23"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("1/23"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("12/3"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(".2"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("2."), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(""), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("asdf"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("1.2/3"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("."), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("/"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("2/"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger("/2"), CVC4ApiException&);
+
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123")));
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.23")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1/23")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("12/3")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".2")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2.")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("asdf")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.2/3")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2/")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/2")), CVC4ApiException&);
+
+ int32_t val1 = 1;
+ int64_t val2 = -1;
+ uint32_t val3 = 1;
+ uint64_t val4 = -1;
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+}
+
void SolverBlack::testMkReal()
{
TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123"));
@@ -839,8 +881,8 @@ void SolverBlack::testMkTerm()
std::vector<Term> v1 = {a, b};
std::vector<Term> v2 = {a, Term()};
std::vector<Term> v3 = {a, d_solver->mkTrue()};
- std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
- std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
+ std::vector<Term> v4 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+ std::vector<Term> v5 = {d_solver->mkInteger(1), Term()};
std::vector<Term> v6 = {};
Solver slv;
@@ -896,10 +938,10 @@ void SolverBlack::testMkTermFromOp()
Sort bv32 = d_solver->mkBitVectorSort(32);
Term a = d_solver->mkConst(bv32, "a");
Term b = d_solver->mkConst(bv32, "b");
- std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
- std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
+ std::vector<Term> v1 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+ std::vector<Term> v2 = {d_solver->mkInteger(1), Term()};
std::vector<Term> v3 = {};
- std::vector<Term> v4 = {d_solver->mkReal(5)};
+ std::vector<Term> v4 = {d_solver->mkInteger(5)};
Solver slv;
// simple operator terms
@@ -948,13 +990,13 @@ void SolverBlack::testMkTermFromOp()
// mkTerm(Op op, Term child) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkInteger(1)));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
TS_ASSERT_THROWS(
- d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkInteger(0)),
CVC4ApiException&);
TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
@@ -962,19 +1004,19 @@ void SolverBlack::testMkTermFromOp()
TS_ASSERT_THROWS_NOTHING(
d_solver->mkTerm(APPLY_CONSTRUCTOR,
consTerm1,
- d_solver->mkReal(0),
+ d_solver->mkInteger(0),
d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
TS_ASSERT_THROWS(
- d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+ d_solver->mkTerm(opterm2, d_solver->mkInteger(1), d_solver->mkInteger(2)),
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkInteger(1), Term()),
CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkInteger(1)),
CVC4ApiException&);
TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
consTerm1,
- d_solver->mkReal(0),
+ d_solver->mkInteger(0),
d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
CVC4ApiException&);
@@ -982,7 +1024,7 @@ void SolverBlack::testMkTermFromOp()
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
TS_ASSERT_THROWS(
d_solver->mkTerm(
- opterm2, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+ opterm2, d_solver->mkInteger(1), d_solver->mkInteger(1), Term()),
CVC4ApiException&);
// mkTerm(Op op, const std::vector<Term>& children) const
@@ -1004,7 +1046,7 @@ void SolverBlack::testMkTuple()
TS_ASSERT_THROWS_NOTHING(d_solver->mkTuple(
{d_solver->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}));
TS_ASSERT_THROWS_NOTHING(
- d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkReal("5")}));
+ d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkInteger("5")}));
TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}),
CVC4ApiException&);
@@ -1054,7 +1096,7 @@ void SolverBlack::testMkConstArray()
{
Sort intSort = d_solver->getIntegerSort();
Sort arrSort = d_solver->mkArraySort(intSort, intSort);
- Term zero = d_solver->mkReal(0);
+ Term zero = d_solver->mkInteger(0);
Term constArr = d_solver->mkConstArray(arrSort, zero);
TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
@@ -1064,7 +1106,7 @@ void SolverBlack::testMkConstArray()
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
Solver slv;
- Term zero2 = slv.mkReal(0);
+ Term zero2 = slv.mkInteger(0);
Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
@@ -1454,7 +1496,7 @@ void SolverBlack::testGetOp()
Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
Term listcons1 = d_solver->mkTerm(
- APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil);
+ APPLY_CONSTRUCTOR, consTerm, d_solver->mkInteger(1), listnil);
Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
TS_ASSERT(listnil.hasOp());
@@ -1542,8 +1584,8 @@ void SolverBlack::testGetUnsatCore3()
Term y = d_solver->mkConst(uSort, "y");
Term f = d_solver->mkConst(uToIntSort, "f");
Term p = d_solver->mkConst(intPredSort, "p");
- Term zero = d_solver->mkReal(0);
- Term one = d_solver->mkReal(1);
+ Term zero = d_solver->mkInteger(0);
+ Term one = d_solver->mkInteger(1);
Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1601,8 +1643,8 @@ void SolverBlack::testGetValue3()
Term z = d_solver->mkConst(uSort, "z");
Term f = d_solver->mkConst(uToIntSort, "f");
Term p = d_solver->mkConst(intPredSort, "p");
- Term zero = d_solver->mkReal(0);
- Term one = d_solver->mkReal(1);
+ Term zero = d_solver->mkInteger(0);
+ Term one = d_solver->mkInteger(1);
Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1985,11 +2027,11 @@ void SolverBlack::testSimplify()
Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
- Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23"));
+ Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkInteger("23"));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
TS_ASSERT(i1 != i2);
TS_ASSERT(i1 != d_solver->simplify(i2));
- Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0));
+ Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkInteger(0));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
TS_ASSERT(i1 != i3);
TS_ASSERT(i1 == d_solver->simplify(i3));
@@ -1998,7 +2040,7 @@ void SolverBlack::testSimplify()
Term dt1 = d_solver->mkTerm(
APPLY_CONSTRUCTOR,
consList.getConstructorTerm("cons"),
- d_solver->mkReal(0),
+ d_solver->mkInteger(0),
d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
Term dt2 = d_solver->mkTerm(
@@ -2075,8 +2117,8 @@ void SolverBlack::testCheckEntailed2()
Term f = d_solver->mkConst(uToIntSort, "f");
Term p = d_solver->mkConst(intPredSort, "p");
// Values
- Term zero = d_solver->mkReal(0);
- Term one = d_solver->mkReal(1);
+ Term zero = d_solver->mkInteger(0);
+ Term one = d_solver->mkInteger(1);
// Terms
Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2158,8 +2200,8 @@ void SolverBlack::testCheckSatAssuming2()
Term f = d_solver->mkConst(uToIntSort, "f");
Term p = d_solver->mkConst(intPredSort, "p");
// Values
- Term zero = d_solver->mkReal(0);
- Term one = d_solver->mkReal(1);
+ Term zero = d_solver->mkInteger(0);
+ Term one = d_solver->mkInteger(1);
// Terms
Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2279,7 +2321,7 @@ void SolverBlack::testSynthFun()
g1.addRule(start1, d_solver->mkBoolean(false));
Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
- g2.addRule(start2, d_solver->mkReal(0));
+ g2.addRule(start2, d_solver->mkInteger(0));
TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean));
TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean));
@@ -2314,7 +2356,7 @@ void SolverBlack::testSynthInv()
g1.addRule(start1, d_solver->mkBoolean(false));
Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
- g2.addRule(start2, d_solver->mkReal(0));
+ g2.addRule(start2, d_solver->mkInteger(0));
TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {}));
TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x}));
@@ -2328,7 +2370,7 @@ void SolverBlack::testAddSygusConstraint()
{
Term nullTerm;
Term boolTerm = d_solver->mkBoolean(true);
- Term intTerm = d_solver->mkReal(1);
+ Term intTerm = d_solver->mkInteger(1);
TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
@@ -2344,7 +2386,7 @@ void SolverBlack::testAddSygusInvConstraint()
Sort real = d_solver->getRealSort();
Term nullTerm;
- Term intTerm = d_solver->mkReal(1);
+ Term intTerm = d_solver->mkInteger(1);
Term inv = d_solver->declareFun("inv", {real}, boolean);
Term pre = d_solver->declareFun("pre", {real}, boolean);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 786b60bb3..bebfc6e1f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -42,7 +42,6 @@ class TermBlack : public CxxTest::TestSuite
void testTermCompare();
void testTermChildren();
void testSubstitute();
- void testIsValue();
void testConstArray();
void testConstSequenceElements();
@@ -100,7 +99,7 @@ void TermBlack::testGetKind()
Term p = d_solver.mkVar(funSort2, "p");
TS_ASSERT_THROWS_NOTHING(p.getKind());
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS_NOTHING(zero.getKind());
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -146,7 +145,7 @@ void TermBlack::testGetSort()
TS_ASSERT_THROWS_NOTHING(p.getSort());
TS_ASSERT(p.getSort() == funSort2);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS_NOTHING(zero.getSort());
TS_ASSERT(zero.getSort() == intSort);
@@ -227,7 +226,7 @@ void TermBlack::testGetOp()
Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
Term consTerm = d_solver.mkTerm(
- APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm);
+ APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
@@ -272,7 +271,7 @@ void TermBlack::testNotTerm()
TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
Term p = d_solver.mkVar(funSort2, "p");
TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
@@ -308,7 +307,7 @@ void TermBlack::testAndTerm()
TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
@@ -374,7 +373,7 @@ void TermBlack::testOrTerm()
TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
@@ -440,7 +439,7 @@ void TermBlack::testXorTerm()
TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
@@ -506,7 +505,7 @@ void TermBlack::testEqTerm()
TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
@@ -572,7 +571,7 @@ void TermBlack::testImpTerm()
TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
@@ -639,7 +638,7 @@ void TermBlack::testIteTerm()
Term p = d_solver.mkVar(funSort2, "p");
TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
- Term zero = d_solver.mkReal(0);
+ Term zero = d_solver.mkInteger(0);
TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -660,17 +659,17 @@ void TermBlack::testIteTerm()
void TermBlack::testTermAssignment()
{
- Term t1 = d_solver.mkReal(1);
+ Term t1 = d_solver.mkInteger(1);
Term t2 = t1;
- t2 = d_solver.mkReal(2);
- TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+ t2 = d_solver.mkInteger(2);
+ TS_ASSERT_EQUALS(t1, d_solver.mkInteger(1));
}
void TermBlack::testTermCompare()
{
- Term t1 = d_solver.mkReal(1);
- Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
- Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+ Term t1 = d_solver.mkInteger(1);
+ Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+ Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
TS_ASSERT(t2 >= t3);
TS_ASSERT(t2 <= t3);
TS_ASSERT((t1 > t2) != (t1 < t2));
@@ -680,8 +679,8 @@ void TermBlack::testTermCompare()
void TermBlack::testTermChildren()
{
// simple term 2+3
- Term two = d_solver.mkReal(2);
- Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
+ Term two = d_solver.mkInteger(2);
+ Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
TS_ASSERT(t1[0] == two);
TS_ASSERT(t1.getNumChildren() == 2);
Term tnull;
@@ -702,7 +701,7 @@ void TermBlack::testTermChildren()
void TermBlack::testSubstitute()
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
- Term one = d_solver.mkReal(1);
+ Term one = d_solver.mkInteger(1);
Term ttrue = d_solver.mkTrue();
Term xpx = d_solver.mkTerm(PLUS, x, x);
Term onepone = d_solver.mkTerm(PLUS, one, one);
@@ -750,34 +749,27 @@ void TermBlack::testSubstitute()
TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
}
-void TermBlack::testIsValue()
-{
- Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
- Term one = d_solver.mkReal(1);
- Term xpone = d_solver.mkTerm(PLUS, x, one);
- Term onepone = d_solver.mkTerm(PLUS, one, one);
- TS_ASSERT(!x.isValue());
- TS_ASSERT(one.isValue());
- TS_ASSERT(!xpone.isValue());
- TS_ASSERT(!onepone.isValue());
- Term tnull;
- TS_ASSERT_THROWS(tnull.isValue(), CVC4ApiException&);
-}
-
void TermBlack::testConstArray()
{
Sort intsort = d_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
Term a = d_solver.mkConst(arrsort, "a");
- Term one = d_solver.mkReal(1);
+ Term one = d_solver.mkInteger(1);
Term constarr = d_solver.mkConstArray(arrsort, one);
- TS_ASSERT(!a.isValue());
- TS_ASSERT(constarr.isValue());
-
TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
+
+ arrsort =
+ d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+ Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
+ Term stores = d_solver.mkTerm(
+ STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+ stores =
+ d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+ stores =
+ d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
}
void TermBlack::testConstSequenceElements()
@@ -786,7 +778,6 @@ void TermBlack::testConstSequenceElements()
Sort seqsort = d_solver.mkSequenceSort(realsort);
Term s = d_solver.mkEmptySequence(seqsort);
- TS_ASSERT(s.isValue());
TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
// empty sequence has zero elements
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index c098ca9b8..f06c1f77d 100644
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -56,7 +56,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
Sort realSort = d_slv->getRealSort();
Sort intSort = d_slv->getIntegerSort();
Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
- Term one = d_slv->mkReal(1);
+ Term one = d_slv->mkInteger(1);
Term singletonInt = d_slv->mkSingleton(intSort, one);
Term singletonReal = d_slv->mkSingleton(realSort, one);
// (union
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback