diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-rw-r--r-- | test/unit/api/solver_black.h | 160 |
1 files changed, 96 insertions, 64 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index fcc68d981..289fc26f0 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -2,9 +2,9 @@ /*! \file solver_black.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz + ** Aina Niemetz, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -76,7 +76,10 @@ class SolverBlack : public CxxTest::TestSuite void testMkUniverseSet(); void testMkVar(); + void testDeclareDatatype(); void testDeclareFun(); + void testDeclareSort(); + void testDefineFun(); void testDefineFunRec(); void testDefineFunsRec(); @@ -263,16 +266,23 @@ void SolverBlack::testMkBitVector() { uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2; uint64_t val2 = 2; + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16)); TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("10", 10)); + TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2), + d_solver->mkBitVector("a", 16)); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(), "0bin01010101"); TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), @@ -284,12 +294,12 @@ void SolverBlack::testMkBoundVar() Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); - TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort)); - TS_ASSERT_THROWS(d_solver->mkBoundVar("a", Sort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(std::string("b"), boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar("", funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, "")); + TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&); } void SolverBlack::testMkBoolean() @@ -440,6 +450,8 @@ void SolverBlack::testMkOpTerm() // mkOpTerm(Kind kind, uint32_t arg) TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1)); TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1), CVC4ApiException&); @@ -499,7 +511,7 @@ void SolverBlack::testMkReal() void SolverBlack::testMkRegexpEmpty() { Sort strSort = d_solver->getStringSort(); - Term s = d_solver->mkVar("s", strSort); + Term s = d_solver->mkConst(strSort, "s"); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty())); } @@ -507,7 +519,7 @@ void SolverBlack::testMkRegexpEmpty() void SolverBlack::testMkRegexpSigma() { Sort strSort = d_solver->getStringSort(); - Term s = d_solver->mkVar("s", strSort); + Term s = d_solver->mkConst(strSort, "s"); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma())); } @@ -531,8 +543,8 @@ void SolverBlack::testMkString() void SolverBlack::testMkTerm() { Sort bv32 = d_solver->mkBitVectorSort(32); - Term a = d_solver->mkVar("a", bv32); - Term b = d_solver->mkVar("b", bv32); + Term a = d_solver->mkConst(bv32, "a"); + Term b = d_solver->mkConst(bv32, "b"); std::vector<Term> v1 = {a, b}; std::vector<Term> v2 = {a, Term()}; std::vector<Term> v3 = {a, d_solver->mkTrue()}; @@ -546,11 +558,6 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(REGEXP_SIGMA)); TS_ASSERT_THROWS(d_solver->mkTerm(CONST_BITVECTOR), CVC4ApiException&); - // mkTerm(Kind kind, Sort sort) const - TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(SEP_NIL, d_solver->getBooleanSort())); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(SEP_NIL, Sort())); - // mkTerm(Kind kind, Term child) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue())); TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&); @@ -589,8 +596,8 @@ void SolverBlack::testMkTerm() void SolverBlack::testMkTermFromOpTerm() { Sort bv32 = d_solver->mkBitVectorSort(32); - Term a = d_solver->mkVar("a", bv32); - Term b = d_solver->mkVar("b", bv32); + 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> v3 = {}; @@ -612,7 +619,7 @@ void SolverBlack::testMkTermFromOpTerm() Sort listSort = d_solver->mkDatatypeSort(listDecl); Sort intListSort = listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()}); - Term c = d_solver->declareFun("c", intListSort); + Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms OpTerm consTerm1 = list.getConstructorTerm("cons"); @@ -725,12 +732,30 @@ void SolverBlack::testMkVar() Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); - TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort)); - TS_ASSERT_THROWS(d_solver->mkVar("a", Sort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(std::string("b"), boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort, std::string("b"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(intSort, std::string("i"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "f")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "")); + TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&); +} + +void SolverBlack::testDeclareDatatype() +{ + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil("nil"); + std::vector<DatatypeConstructorDecl> ctors1 = {nil}; + std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil}; + std::vector<DatatypeConstructorDecl> ctors3; + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2)); + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3), + CVC4ApiException&); } void SolverBlack::testDeclareFun() @@ -738,32 +763,39 @@ void SolverBlack::testDeclareFun() Sort bvSort = d_solver->mkBitVectorSort(32); Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f1", bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f2", funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f1", {}, bvSort)); TS_ASSERT_THROWS_NOTHING( d_solver->declareFun("f3", {bvSort, d_solver->getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver->declareFun("f2", {}, funSort), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareFun("f4", {bvSort, funSort}, bvSort), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort), CVC4ApiException&); } +void SolverBlack::testDeclareSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 0)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("", 2)); +} + void SolverBlack::testDefineFun() { Sort bvSort = d_solver->mkBitVectorSort(32); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar("b1", bvSort); - Term b11 = d_solver->mkBoundVar("b1", bvSort); - Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort()); - Term b3 = d_solver->mkBoundVar("b3", funSort2); - Term v1 = d_solver->mkBoundVar("v1", bvSort); - Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); - Term v3 = d_solver->mkVar("v3", funSort2); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1)); @@ -786,16 +818,16 @@ void SolverBlack::testDefineFunRec() Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar("b1", bvSort); - Term b11 = d_solver->mkBoundVar("b1", bvSort); - Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort()); - Term b3 = d_solver->mkBoundVar("b3", funSort2); - Term v1 = d_solver->mkBoundVar("v1", bvSort); - Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); - Term v3 = d_solver->mkVar("v3", funSort2); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1)); @@ -820,18 +852,18 @@ void SolverBlack::testDefineFunsRec() Sort bvSort = d_solver->mkBitVectorSort(32); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); - Term b1 = d_solver->mkBoundVar("b1", bvSort); - Term b11 = d_solver->mkBoundVar("b1", bvSort); - Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort()); - Term b3 = d_solver->mkBoundVar("b3", funSort2); - Term b4 = d_solver->mkBoundVar("b4", uSort); - Term v1 = d_solver->mkBoundVar("v1", bvSort); - Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); - Term v3 = d_solver->mkVar("v3", funSort2); - Term v4 = d_solver->mkVar("v4", uSort); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term b1 = d_solver->mkVar(bvSort, "b1"); + Term b11 = d_solver->mkVar(bvSort, "b1"); + Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); + Term b3 = d_solver->mkVar(funSort2, "b3"); + Term b4 = d_solver->mkVar(uSort, "b4"); + Term v1 = d_solver->mkVar(bvSort, "v1"); + Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v3 = d_solver->mkConst(funSort2, "v3"); + Term v4 = d_solver->mkConst(uSort, "v4"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + Term f3 = d_solver->mkConst(bvSort, "f3"); TS_ASSERT_THROWS_NOTHING( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); TS_ASSERT_THROWS( |