diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 76 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 15 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 12 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 747 |
4 files changed, 490 insertions, 360 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5321a90ec..123613797 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -29,6 +29,7 @@ #include "options/options.h" #include "smt/model.h" #include "smt/smt_engine.h" +#include "theory/logic_info.h" #include "util/random.h" #include "util/result.h" #include "util/utility.h" @@ -3374,26 +3375,70 @@ void Solver::reset(void) const { d_smtEngine->reset(); } */ void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); } +// TODO: issue #2781 +void Solver::setLogicHelper(const std::string& logic) const +{ + CVC4_API_CHECK(!d_smtEngine->isFullyInited()) + << "Invalid call to 'setLogic', solver is already fully initialized"; + try + { + CVC4::LogicInfo logic_info(logic); + d_smtEngine->setLogic(logic_info); + } + catch (CVC4::IllegalArgumentException& e) + { + throw CVC4ApiException(e.getMessage()); + } +} + /** * ( set-info <attribute> ) */ void Solver::setInfo(const std::string& keyword, const std::string& value) const { - // CHECK: - // if keyword == "cvc4-logic": value must be string - // if keyword == "status": must be sat, unsat or unknown - // if keyword == "smt-lib-version": supported? + bool is_cvc4_keyword = false; + + /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */ + if (keyword.length() > 5) + { + std::string prefix = keyword.substr(0, 5); + if (prefix == "cvc4-" || prefix == "cvc4_") + { + is_cvc4_keyword = true; + std::string cvc4key = keyword.substr(5); + CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword) + << "keyword 'cvc4-logic'"; + setLogicHelper(value); + } + } + if (!is_cvc4_keyword) + { + CVC4_API_ARG_CHECK_EXPECTED( + keyword == "source" || keyword == "category" || keyword == "difficulty" + || keyword == "filename" || keyword == "license" + || keyword == "name" || keyword == "notes" + || keyword == "smt-lib-version" || keyword == "status", + keyword) + << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " + "'notes', 'smt-lib-version' or 'status'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" + || value == "2.0" || value == "2.5" + || value == "2.6" || value == "2.6.1", + value) + << "'2.0', '2.5', '2.6' or '2.6.1'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" + || value == "unsat" || value == "unknown", + value) + << "'sat', 'unsat' or 'unknown'"; + } + d_smtEngine->setInfo(keyword, value); } /** * ( set-logic <symbol> ) */ -void Solver::setLogic(const std::string& logic) const -{ - // CHECK: !d_smtEngine->d_fullyInited - d_smtEngine->setLogic(logic); -} +void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); } /** * ( set-option <option> ) @@ -3401,9 +3446,16 @@ void Solver::setLogic(const std::string& logic) const void Solver::setOption(const std::string& option, const std::string& value) const { - // CHECK: option exists? - // CHECK: !d_smtEngine->d_fullInited, else option can't be set - d_smtEngine->setOption(option, value); + CVC4_API_CHECK(!d_smtEngine->isFullyInited()) + << "Invalid call to 'setOption', solver is already fully initialized"; + try + { + d_smtEngine->setOption(option, value); + } + catch (CVC4::OptionException& e) + { + throw CVC4ApiException(e.getMessage()); + } } Term Solver::ensureTermSort(const Term& t, const Sort& s) const diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 1d98f127d..a06f2e415 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -24,8 +24,8 @@ #include <map> #include <memory> #include <set> -#include <string> #include <sstream> +#include <string> #include <unordered_map> #include <unordered_set> #include <vector> @@ -53,9 +53,10 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception { public: CVC4ApiException(const std::string& str) : d_msg(str) {} - CVC4ApiException(const std::stringstream& stream) :d_msg(stream.str()) {} + CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {} std::string getMessage() const { return d_msg; } const char* what() const noexcept override { return d_msg.c_str(); } + private: std::string d_msg; }; @@ -2237,9 +2238,8 @@ class CVC4_PUBLIC Solver * @param ctors the constructor declarations of the datatype sort * @return the datatype sort */ - Sort declareDatatype( - const std::string& symbol, - const std::vector<DatatypeConstructorDecl>& ctors) const; + Sort declareDatatype(const std::string& symbol, + const std::vector<DatatypeConstructorDecl>& ctors) const; /** * Declare 0-arity function symbol. @@ -2489,7 +2489,8 @@ class CVC4_PUBLIC Solver /* Helper to check for API misuse in mkOpTerm functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ - template <typename T> Term mkConstHelper(T t) const; + template <typename T> + Term mkConstHelper(T t) const; /* Helper for mkReal functions that take a string as argument. */ Term mkRealFromStrHelper(std::string s) const; /* Helper for mkBitVector functions that take a string as argument. */ @@ -2499,6 +2500,8 @@ class CVC4_PUBLIC Solver Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const; /* Helper for mkBitVector functions that take an integer as argument. */ Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; + /* Helper for setLogic. */ + void setLogicHelper(const std::string& logic) const; /** * Helper function that ensures that a given term is of sort real (as opposed diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5aa59fad7..e53d1eb55 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -217,8 +217,8 @@ class CVC4_PUBLIC SmtEngine { /** * Whether or not this SmtEngine is fully initialized (post-construction). * This post-construction initialization is automatically triggered by the - * use of the SmtEngine; e.g. when setLogic() is called, or the first - * assertion is made, etc. + * use of the SmtEngine; e.g. when the first formula is asserted, a call + * to simplify() is issued, a scope is pushed, etc. */ bool d_fullyInited; @@ -457,6 +457,14 @@ class CVC4_PUBLIC SmtEngine { ~SmtEngine(); /** + * Return true if this SmtEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SmtEngine; e.g. when the first formula is asserted, a call + * to simplify() is issued, a scope is pushed, etc. + */ + bool isFullyInited() { return d_fullyInited; } + + /** * Set the logic of the script. */ void setLogic( diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 3bfb51200..d2226f278 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -80,173 +80,181 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunRec(); void testDefineFunsRec(); + void testSetInfo(); + void testSetLogic(); + void testSetOption(); + private: - Solver d_solver; + std::unique_ptr<Solver> d_solver; }; -void SolverBlack::setUp() {} +void SolverBlack::setUp() { d_solver.reset(new Solver()); } void SolverBlack::tearDown() {} void SolverBlack::testGetBooleanSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort()); } void SolverBlack::testGetIntegerSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getIntegerSort()); } void SolverBlack::testGetNullSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getNullSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getNullSort()); } void SolverBlack::testGetRealSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getRealSort()); } void SolverBlack::testGetRegExpSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getRegExpSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getRegExpSort()); } void SolverBlack::testGetStringSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getStringSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort()); } void SolverBlack::testGetRoundingmodeSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.getRoundingmodeSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort()); } void SolverBlack::testMkArraySort() { - Sort boolSort = d_solver.getBooleanSort(); - Sort intSort = d_solver.getIntegerSort(); - Sort realSort = d_solver.getRealSort(); - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort fpSort = d_solver.mkFloatingPointSort(3, 5); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, boolSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(intSort, intSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, realSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(fpSort, fpSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, intSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, fpSort)); + Sort boolSort = d_solver->getBooleanSort(); + Sort intSort = d_solver->getIntegerSort(); + Sort realSort = d_solver->getRealSort(); + Sort bvSort = d_solver->mkBitVectorSort(32); + Sort fpSort = d_solver->mkFloatingPointSort(3, 5); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort)); } void SolverBlack::testMkBitVectorSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); - TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVectorSort(32)); + TS_ASSERT_THROWS(d_solver->mkBitVectorSort(0), CVC4ApiException&); } void SolverBlack::testMkFloatingPointSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&); } void SolverBlack::testMkDatatypeSort() { DatatypeDecl dtypeSpec("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); cons.addSelector(head); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); - TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec)); DatatypeDecl throwsDtypeSpec("list"); - TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec), + CVC4ApiException&); } void SolverBlack::testMkFunctionSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), - CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, - d_solver.getIntegerSort())); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort( + d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort())); + Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), + d_solver->getIntegerSort()); TS_ASSERT_THROWS( - d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, - d_solver.getIntegerSort()), + d_solver->mkFunctionSort(funSort, d_solver->getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkFunctionSort(d_solver->getIntegerSort(), funSort), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort( + {d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()}, + d_solver->getIntegerSort())); + Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), + d_solver->getIntegerSort()); + TS_ASSERT_THROWS( + d_solver->mkFunctionSort({funSort2, d_solver->mkUninterpretedSort("u")}, + d_solver->getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkFunctionSort( + {d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")}, + funSort2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), - d_solver.mkUninterpretedSort("u")}, - funSort2), - CVC4ApiException&); } void SolverBlack::testMkParamSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("T")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkParamSort("T")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkParamSort("")); } void SolverBlack::testMkPredicateSort() { TS_ASSERT_THROWS_NOTHING( - d_solver.mkPredicateSort({d_solver.getIntegerSort()})); - TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); + d_solver->mkPredicateSort({d_solver->getIntegerSort()})); + TS_ASSERT_THROWS(d_solver->mkPredicateSort({}), CVC4ApiException&); + Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), + d_solver->getIntegerSort()); TS_ASSERT_THROWS( - d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), + d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}), CVC4ApiException&); } void SolverBlack::testMkRecordSort() { std::vector<std::pair<std::string, Sort>> fields = { - std::make_pair("b", d_solver.getBooleanSort()), - std::make_pair("bv", d_solver.mkBitVectorSort(8)), - std::make_pair("i", d_solver.getIntegerSort())}; + std::make_pair("b", d_solver->getBooleanSort()), + std::make_pair("bv", d_solver->mkBitVectorSort(8)), + std::make_pair("i", d_solver->getIntegerSort())}; std::vector<std::pair<std::string, Sort>> empty; - TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(fields)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(empty)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(fields)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty)); } void SolverBlack::testMkSetSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getBooleanSort())); - TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getIntegerSort())); - TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.mkBitVectorSort(4))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getIntegerSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->mkBitVectorSort(4))); } void SolverBlack::testMkUninterpretedSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("u")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("")); } void SolverBlack::testMkSortConstructorSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("s", 2)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("", 2)); - TS_ASSERT_THROWS(d_solver.mkSortConstructorSort("", 0), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSortConstructorSort("s", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSortConstructorSort("", 2)); + TS_ASSERT_THROWS(d_solver->mkSortConstructorSort("", 0), CVC4ApiException&); } void SolverBlack::testMkTupleSort() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), + TS_ASSERT_THROWS_NOTHING(d_solver->mkTupleSort({d_solver->getIntegerSort()})); + Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), + d_solver->getIntegerSort()); + TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}), CVC4ApiException&); } @@ -254,116 +262,118 @@ void SolverBlack::testMkBitVector() { uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2; uint64_t val2 = 2; - 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(8, "01010101", 2).toString(), + 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(8, "01010101", 2).toString(), "0bin01010101"); - TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "F", 16).toString(), "0bin00001111"); + TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), + "0bin00001111"); } 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)); + 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)); } void SolverBlack::testMkBoolean() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(true)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(false)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(true)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(false)); } void SolverBlack::testMkRoundingMode() { TS_ASSERT_THROWS_NOTHING( - d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } void SolverBlack::testMkUninterpretedConst() { TS_ASSERT_THROWS_NOTHING( - d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - TS_ASSERT_THROWS(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException&); + d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1)); + TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1), + CVC4ApiException&); } void SolverBlack::testMkAbstractValue() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue(std::string("1"))); - TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("0")), + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue(std::string("1"))); + TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("0")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("-1")), + TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("-1")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("1.2")), + TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("1.2")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkAbstractValue("1/2"), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkAbstractValue("asdf"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkAbstractValue("1/2"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkAbstractValue("asdf"), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint32_t)1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint64_t)1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)-1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)-1)); - TS_ASSERT_THROWS(d_solver.mkAbstractValue(0), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((uint32_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int32_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((uint64_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int64_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int32_t)-1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int64_t)-1)); + TS_ASSERT_THROWS(d_solver->mkAbstractValue(0), CVC4ApiException&); } void SolverBlack::testMkFloatingPoint() { - Term t1 = d_solver.mkBitVector(8); - Term t2 = d_solver.mkBitVector(4); - Term t3 = d_solver.mkReal(2); + Term t1 = d_solver->mkBitVector(8); + Term t2 = d_solver->mkBitVector(4); + Term t3 = d_solver->mkReal(2); if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPoint(3, 5, t1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1)); } else { - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t1), CVC4ApiException&); } - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(0, 5, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(0, 5, t1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 0, t1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&); } void SolverBlack::testMkEmptySet() { - TS_ASSERT_THROWS(d_solver.mkEmptySet(d_solver.getBooleanSort()), + TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkEmptySet(Sort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort())); } void SolverBlack::testMkFalse() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse()); - TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); } void SolverBlack::testMkNaN() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkNaN(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkNaN(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkNaN(3, 5), CVC4ApiException&); } } @@ -371,11 +381,11 @@ void SolverBlack::testMkNegZero() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkNegZero(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkNegZero(3, 5), CVC4ApiException&); } } @@ -383,11 +393,11 @@ void SolverBlack::testMkNegInf() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkNegInf(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkNegInf(3, 5), CVC4ApiException&); } } @@ -395,11 +405,11 @@ void SolverBlack::testMkPosInf() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkPosInf(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkPosInf(3, 5), CVC4ApiException&); } } @@ -407,349 +417,406 @@ void SolverBlack::testMkPosZero() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkPosZero(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkPosZero(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkPosZero(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkPosZero(3, 5), CVC4ApiException&); } } void SolverBlack::testMkOpTerm() { // mkOpTerm(Kind kind, Kind k) - TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(CHAIN_OP, EQUAL)); - TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL), + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(CHAIN_OP, EQUAL)); + TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL), CVC4ApiException&); // mkOpTerm(Kind kind, const std::string& arg) - TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(RECORD_UPDATE_OP, "asdf")); - TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"), + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf")); + TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"), CVC4ApiException&); // mkOpTerm(Kind kind, uint32_t arg) - TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(DIVISIBLE_OP, 1)); - TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1), + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1)); + TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1), CVC4ApiException&); // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) - TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1)); - TS_ASSERT_THROWS(d_solver.mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1)); + TS_ASSERT_THROWS(d_solver->mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&); } -void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver.mkPi()); } +void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); } void SolverBlack::testMkReal() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("123")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("1.23")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("1/23")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("12/3")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(".2")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("2.")); - TS_ASSERT_THROWS(d_solver.mkReal(nullptr), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(""), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("asdf"), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("1.2/3"), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("."), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("/"), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("2/"), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal("/2"), CVC4ApiException&); - - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("123"))); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("1.23"))); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("1/23"))); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("12/3"))); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string(".2"))); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("2."))); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("asdf")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string(".")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("/")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("2/")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkReal(std::string("/2")), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("1.23")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("1/23")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("12/3")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(".2")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("2.")); + TS_ASSERT_THROWS(d_solver->mkReal(nullptr), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(""), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("asdf"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("1.2/3"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("."), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("/"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("2/"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal("/2"), CVC4ApiException&); + + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("1.23"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("1/23"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("12/3"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string(".2"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("2."))); + TS_ASSERT_THROWS(d_solver->mkReal(std::string("")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(std::string("asdf")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(std::string("1.2/3")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(std::string(".")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(std::string("/")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(std::string("2/")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkReal(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.mkReal(val1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val2)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val3)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val1, val1)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val2, val2)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val3, val3)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4, val4)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val3)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val1, val1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val2, val2)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val3, val3)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4, val4)); } void SolverBlack::testMkRegexpEmpty() { - Sort strSort = d_solver.getStringSort(); - Term s = d_solver.mkVar("s", strSort); + Sort strSort = d_solver->getStringSort(); + Term s = d_solver->mkVar("s", strSort); TS_ASSERT_THROWS_NOTHING( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty())); + d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty())); } void SolverBlack::testMkRegexpSigma() { - Sort strSort = d_solver.getStringSort(); - Term s = d_solver.mkVar("s", strSort); + Sort strSort = d_solver->getStringSort(); + Term s = d_solver->mkVar("s", strSort); TS_ASSERT_THROWS_NOTHING( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); + d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma())); } void SolverBlack::testMkSepNil() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkSepNil(d_solver.getBooleanSort())); - TS_ASSERT_THROWS(d_solver.mkSepNil(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort())); + TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&); } void SolverBlack::testMkString() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkString("")); - TS_ASSERT_THROWS_NOTHING(d_solver.mkString("asdfasdf")); - TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf").toString(), + TS_ASSERT_THROWS_NOTHING(d_solver->mkString("")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkString("asdfasdf")); + TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf").toString(), "\"asdf\\\\nasdf\""); - TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf", true).toString(), + TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf", true).toString(), "\"asdf\\nasdf\""); } void SolverBlack::testMkTerm() { - Sort bv32 = d_solver.mkBitVectorSort(32); - Term a = d_solver.mkVar("a", bv32); - Term b = d_solver.mkVar("b", bv32); + Sort bv32 = d_solver->mkBitVectorSort(32); + Term a = d_solver->mkVar("a", bv32); + Term b = d_solver->mkVar("b", bv32); 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()}; - OpTerm opterm1 = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); - OpTerm opterm2 = d_solver.mkOpTerm(DIVISIBLE_OP, 1); - OpTerm opterm3 = d_solver.mkOpTerm(CHAIN_OP, EQUAL); + 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()}; + OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); + OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); + OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); // mkTerm(Kind kind) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(PI)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(REGEXP_EMPTY)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(REGEXP_SIGMA)); - TS_ASSERT_THROWS(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(REGEXP_EMPTY)); + 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())); + 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&); - TS_ASSERT_THROWS(d_solver.mkTerm(NOT, a), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(NOT, a), CVC4ApiException&); // mkTerm(Kind kind, Term child1, Term child2) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(EQUAL, a, b)); - TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b)); + TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, Term(), b), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()), CVC4ApiException&); // mkTerm(Kind kind, Term child1, Term child2, Term child3) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm( - ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( + ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue())); TS_ASSERT_THROWS( - d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()), + d_solver->mkTerm(ITE, Term(), d_solver->mkTrue(), d_solver->mkTrue()), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()), + d_solver->mkTerm(ITE, d_solver->mkTrue(), Term(), d_solver->mkTrue()), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()), + d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), Term()), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b), + d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b), CVC4ApiException&); // mkTerm(Kind kind, const std::vector<Term>& children) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(EQUAL, v1)); - TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, v3), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1)); + TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&); // mkTerm(OpTerm opTerm, Term child) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm1, a)); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm2, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, Term()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); // mkTerm(OpTerm opTerm, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING( - d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(2))); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, d_solver.mkReal(1), Term()), + d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, Term(), d_solver.mkReal(1)), + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), CVC4ApiException&); // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm( - opterm3, d_solver.mkReal(1), d_solver.mkReal(1), d_solver.mkReal(2))); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(1), Term()), + d_solver->mkTerm( + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), CVC4ApiException&); // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const - TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm3, v4)); - TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, v5), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v4)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v5), CVC4ApiException&); } void SolverBlack::testMkTrue() { - TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue()); - TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTrue()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTrue()); } 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->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->mkReal("5")})); - TS_ASSERT_THROWS(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}), + TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkTuple({d_solver.mkBitVectorSort(4)}, - {d_solver.mkBitVector("101", 2)}), + TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->mkBitVectorSort(4)}, + {d_solver->mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()}, + {d_solver->mkReal("5.3")}), CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}), - CVC4ApiException&); } void SolverBlack::testMkUniverseSet() { - TS_ASSERT_THROWS(d_solver.mkUniverseSet(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkUniverseSet(d_solver.getBooleanSort())); + TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort())); } 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)); + 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)); } 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)); + 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("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); - TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), + d_solver->declareFun("f3", {bvSort, d_solver->getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver->declareFun("f4", {bvSort, funSort}, bvSort), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), + TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort), CVC4ApiException&); } 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); - 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)); - TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), + 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); + 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)); + TS_ASSERT_THROWS(d_solver->defineFun("fff", {b1}, bvSort, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), + TS_ASSERT_THROWS(d_solver->defineFun("ffff", {b1}, funSort2, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), + TS_ASSERT_THROWS(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f3, {b1}, v1), CVC4ApiException&); } void SolverBlack::testDefineFunRec() { - 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); - 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)); - TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), + 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); + 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)); + TS_ASSERT_THROWS(d_solver->defineFunRec("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec("ffff", {b1}, funSort2, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), + TS_ASSERT_THROWS(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), + TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1, b11}, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec(f3, {b1}, v1), CVC4ApiException&); } void SolverBlack::testDefineFunsRec() { - Sort uSort = d_solver.mkUninterpretedSort("u"); - 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); + Sort uSort = d_solver->mkUninterpretedSort("u"); + 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); TS_ASSERT_THROWS_NOTHING( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); + d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), + d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), + TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), + d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), + CVC4ApiException&); +} + +void SolverBlack::testSetInfo() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4-logic", "QF_BV")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4_logic", "QF_BV")); + TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "asdf"), CVC4ApiException&); + + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("source", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("category", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("difficulty", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("filename", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("license", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("name", "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("notes", "asdf")); + + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.0")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.5")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.6")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.6.1")); + TS_ASSERT_THROWS(d_solver->setInfo("smt-lib-version", ".0"), + CVC4ApiException&); + + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "sat")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unsat")); + TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unknown")); + TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&); + + d_solver->assertFormula(d_solver->mkTrue()); + TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "QF_BV"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->setInfo("cvc4_logic", "QF_BV"), CVC4ApiException&); +} + +void SolverBlack::testSetLogic() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->setLogic("AUFLIRA")); + TS_ASSERT_THROWS(d_solver->setLogic("AF_BV"), CVC4ApiException&); + d_solver->assertFormula(d_solver->mkTrue()); + TS_ASSERT_THROWS(d_solver->setLogic("AUFLIRA"), CVC4ApiException&); +} + +void SolverBlack::testSetOption() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->setOption("bv-sat-solver", "minisat")); + TS_ASSERT_THROWS(d_solver->setOption("bv-sat-solver", "1"), + CVC4ApiException&); + d_solver->assertFormula(d_solver->mkTrue()); + TS_ASSERT_THROWS(d_solver->setOption("bv-sat-solver", "minisat"), + CVC4ApiException&); } |