diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-rw-r--r-- | test/unit/api/solver_black.h | 108 |
1 files changed, 75 insertions, 33 deletions
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); |