diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/api/reset_assertions.cpp | 4 | ||||
-rw-r--r-- | test/api/sep_log_api.cpp | 4 | ||||
-rw-r--r-- | test/regress/regress0/get-value-reals-ints.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/get-value-reals.smt2 | 2 | ||||
-rw-r--r-- | test/unit/api/grammar_black.h | 4 | ||||
-rw-r--r-- | test/unit/api/python/test_grammar.py | 4 | ||||
-rw-r--r-- | test/unit/api/python/test_term.py | 14 | ||||
-rw-r--r-- | test/unit/api/python/test_to_python_obj.py | 19 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 108 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 69 | ||||
-rw-r--r-- | test/unit/theory/theory_sets_type_rules_white.h | 2 |
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 |