From 5938faaf034a761f3462d8e03b86b1726a332f68 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 3 Jun 2020 20:56:24 -0700 Subject: New C++ Api: First batch of API guards. (#4557) This is the first batch of API guards, mainly extending existing guards in the Solver object with checks that Ops, Terms, Sorts, and datatype objects are associated to this solver object. This further changes how DatatypeConstructorDecl objects are created. Previously, they were not created via the Solver object (while DatatypeDecl was). Now, they are created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl objects are created. --- examples/api/datatypes-new.cpp | 12 +- examples/api/python/datatypes.py | 12 +- src/api/cvc4cpp.cpp | 210 ++++++++++++++++++++++----- src/api/cvc4cpp.h | 47 ++++-- src/api/python/cvc4.pxd | 2 +- src/api/python/cvc4.pxi | 17 ++- src/parser/cvc/Cvc.g | 43 +++--- src/parser/smt2/Smt2.g | 7 +- src/parser/tptp/Tptp.g | 4 +- test/unit/api/datatype_api_black.h | 29 ++-- test/unit/api/solver_black.h | 286 ++++++++++++++++++++++++++++++++++--- test/unit/api/sort_black.h | 30 ++-- test/unit/api/term_black.h | 4 +- 13 files changed, 559 insertions(+), 144 deletions(-) diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 9cfc7992c..500cb0710 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -91,8 +91,8 @@ void test(Solver& slv, Sort& consListSort) DatatypeDecl paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort); // give the datatype a name - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); + DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); paramCons.addSelector("head", sort); paramCons.addSelectorSelf("tail"); paramConsListSpec.addConstructor(paramCons); @@ -144,11 +144,11 @@ int main() DatatypeDecl consListSpec = slv.mkDatatypeDecl("list"); // give the datatype a name - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", slv.getIntegerSort()); cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil"); consListSpec.addConstructor(nil); std::cout << "spec is:" << std::endl << consListSpec << std::endl; @@ -167,10 +167,10 @@ int main() << ">>> Alternatively, use declareDatatype" << std::endl; std::cout << std::endl; - DatatypeConstructorDecl cons2("cons"); + DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); cons2.addSelector("head", slv.getIntegerSort()); cons2.addSelectorSelf("tail"); - DatatypeConstructorDecl nil2("nil"); + DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); std::vector ctors = {cons2, nil2}; Sort consListSort2 = slv.declareDatatype("list2", ctors); test(slv, consListSort2); diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index ded268d69..1a67f5661 100755 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -65,8 +65,8 @@ def test(slv, consListSort): # constructor "cons". sort = slv.mkParamSort("T") paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort) - paramCons = pycvc4.DatatypeConstructorDecl("cons") - paramNil = pycvc4.DatatypeConstructorDecl("nil") + paramCons = slv.mkDatatypeConstructorDecl("cons") + paramNil = slv.mkDatatypeConstructorDecl("nil") paramCons.addSelector("head", sort) paramCons.addSelectorSelf("tail") paramConsListSpec.addConstructor(paramCons) @@ -102,11 +102,11 @@ if __name__ == "__main__": # symbols are assigned to its constructors, selectors, and testers. consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name - cons = pycvc4.DatatypeConstructorDecl("cons") + cons = slv.mkDatatypeConstructorDecl("cons") cons.addSelector("head", slv.getIntegerSort()) cons.addSelectorSelf("tail") consListSpec.addConstructor(cons) - nil = pycvc4.DatatypeConstructorDecl("nil") + nil = slv.mkDatatypeConstructorDecl("nil") consListSpec.addConstructor(nil) print("spec is {}".format(consListSpec)) @@ -122,10 +122,10 @@ if __name__ == "__main__": print("### Alternatively, use declareDatatype") - cons2 = pycvc4.DatatypeConstructorDecl("cons") + cons2 = slv.mkDatatypeConstructorDecl("cons") cons2.addSelector("head", slv.getIntegerSort()) cons2.addSelectorSelf("tail") - nil2 = pycvc4.DatatypeConstructorDecl("nil") + nil2 = slv.mkDatatypeConstructorDecl("nil") ctors = [cons2, nil2] consListSort2 = slv.declareDatatype("list2", ctors) test(slv, consListSort2) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 0bfb9a325..f225da333 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -702,8 +702,6 @@ class CVC4ApiExceptionStream CVC4_API_CHECK(isDefinedKind(kind)) \ << "Invalid kind '" << kindToString(kind) << "'"; -#define CVC4_API_SORT_CHECK_SOLVER(sort) - #define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 \ @@ -726,12 +724,12 @@ class CVC4ApiExceptionStream & CVC4ApiExceptionStream().ostream() \ << "Invalid size of argument '" << #arg << "', expected " -#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ - CVC4_PREDICT_TRUE(cond) \ - ? (void)0 \ - : OstreamVoider() \ - & CVC4ApiExceptionStream().ostream() \ - << "Invalid " << what << " '" << arg << "' at index" << idx \ +#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid " << what << " '" << arg << "' at index " << idx \ << ", expected " #define CVC4_API_SOLVER_TRY_CATCH_BEGIN \ @@ -741,6 +739,19 @@ class CVC4ApiExceptionStream } \ catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } + +#define CVC4_API_SOLVER_CHECK_SORT(sort) \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; + +#define CVC4_API_SOLVER_CHECK_TERM(term) \ + CVC4_API_CHECK(this == term.d_solver) \ + << "Given term is not associated with this solver"; + +#define CVC4_API_SOLVER_CHECK_OP(op) \ + CVC4_API_CHECK(this == op.d_solver) \ + << "Given operator is not associated with this solver"; + } // namespace /* -------------------------------------------------------------------------- */ @@ -1612,6 +1623,7 @@ Term::const_iterator::const_iterator(const const_iterator& it) { if (it.d_orig_expr != nullptr) { + d_solver = it.d_solver; d_orig_expr = it.d_orig_expr; d_pos = it.d_pos; } @@ -1619,6 +1631,7 @@ Term::const_iterator::const_iterator(const const_iterator& it) Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) { + d_solver = it.d_solver; d_orig_expr = it.d_orig_expr; d_pos = it.d_pos; return *this; @@ -1630,7 +1643,8 @@ bool Term::const_iterator::operator==(const const_iterator& it) const { return false; } - return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos); + return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr) + && (d_pos == it.d_pos); } bool Term::const_iterator::operator!=(const const_iterator& it) const @@ -1756,8 +1770,14 @@ size_t TermHashFunction::operator()(const Term& t) const /* DatatypeConstructorDecl -------------------------------------------------- */ -DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) - : d_ctor(new CVC4::DatatypeConstructor(name)) +DatatypeConstructorDecl::DatatypeConstructorDecl() + : d_solver(nullptr), d_ctor(nullptr) +{ +} + +DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv, + const std::string& name) + : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name)) { } @@ -1804,10 +1824,13 @@ std::ostream& operator<<(std::ostream& out, /* DatatypeDecl ------------------------------------------------------------- */ +DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} + DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, bool isCoDatatype) - : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype)) + : d_solver(slv), + d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype)) { } @@ -1815,7 +1838,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, Sort param, bool isCoDatatype) - : d_dtype(new CVC4::Datatype(slv->getExprManager(), + : d_solver(slv), + d_dtype(new CVC4::Datatype(slv->getExprManager(), name, std::vector{*param.d_type}, isCoDatatype)) @@ -1826,6 +1850,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, const std::vector& params, bool isCoDatatype) + : d_solver(slv) { std::vector tparams; for (const Sort& p : params) @@ -1838,8 +1863,6 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, bool DatatypeDecl::isNullHelper() const { return !d_dtype; } -DatatypeDecl::DatatypeDecl() {} - DatatypeDecl::~DatatypeDecl() {} void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) @@ -2683,8 +2706,11 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "parameter term", children[i], i) + !children[i].isNull(), "child term", children[i], i) << "non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == children[i].d_solver, "child term", children[i], i) + << "a child term associated to this solver object"; } std::vector echildren = termVectorToExprs(children); @@ -2749,13 +2775,24 @@ std::vector Solver::mkDatatypeSortsInternal( CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::vector datatypes; - for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; i++) - { - CVC4_API_ARG_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0, - dtypedecls[i]) + for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver, + "datatype declaration", + dtypedecls[i], + i) + << "a datatype declaration associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0, + "datatype declaration", + dtypedecls[i], + i) << "a datatype declaration with at least one constructor"; datatypes.push_back(dtypedecls[i].getDatatype()); } + for (auto& sort : unresolvedSorts) + { + CVC4_API_SOLVER_CHECK_SORT(sort); + } std::set utypes = sortSetToTypes(unresolvedSorts); std::vector dtypes = d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes); @@ -2778,6 +2815,7 @@ std::vector Solver::sortVectorToTypes( std::vector res; for (const Sort& s : sorts) { + CVC4_API_SOLVER_CHECK_SORT(s); res.push_back(*s.d_type); } return res; @@ -2789,6 +2827,7 @@ std::vector Solver::termVectorToExprs( std::vector res; for (const Term& t : terms) { + CVC4_API_SOLVER_CHECK_TERM(t); res.push_back(*t.d_expr); } return res; @@ -2877,6 +2916,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const << "non-null index sort"; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; + CVC4_API_SOLVER_CHECK_SORT(indexSort); + CVC4_API_SOLVER_CHECK_SORT(elemSort); return Sort(this, d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type)); @@ -2908,6 +2949,8 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(this == dtypedecl.d_solver) + << "Given datatype declaration is not associated with this solver"; CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) << "a datatype declaration with at least one constructor"; @@ -2934,6 +2977,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; + CVC4_API_SOLVER_CHECK_SORT(domain); + CVC4_API_SOLVER_CHECK_SORT(codomain); CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain) << "first-class sort as domain sort for function sort"; CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain) @@ -2956,12 +3001,16 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !sorts[i].isNull(), "parameter sort", sorts[i], i) << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sorts[i].d_solver, "parameter sort", sorts[i], i) + << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( sorts[i].isFirstClass(), "parameter sort", sorts[i], i) << "first-class sort as parameter sort for function sort"; } CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; + CVC4_API_SOLVER_CHECK_SORT(codomain); CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain) << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ @@ -2990,6 +3039,9 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !sorts[i].isNull(), "parameter sort", sorts[i], i) << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sorts[i].d_solver, "parameter sort", sorts[i], i) + << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( sorts[i].isFirstClass(), "parameter sort", sorts[i], i) << "first-class sort as parameter sort for predicate sort"; @@ -3012,6 +3064,9 @@ Sort Solver::mkRecordSort( CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !p.second.isNull(), "parameter sort", p.second, i) << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == p.second.d_solver, "parameter sort", p.second, i) + << "sort associated to this solver object"; i += 1; f.emplace_back(p.first, *p.second.d_type); } @@ -3026,6 +3081,7 @@ Sort Solver::mkSetSort(Sort elemSort) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; + CVC4_API_SOLVER_CHECK_SORT(elemSort); return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type)); @@ -3058,6 +3114,9 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !sorts[i].isNull(), "parameter sort", sorts[i], i) << "non-null sort"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sorts[i].d_solver, "parameter sort", sorts[i], i) + << "sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) << "non-function-like sort as parameter sort for tuple sort"; @@ -3207,6 +3266,8 @@ Term Solver::mkEmptySet(Sort s) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s) << "null sort or set sort"; + CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s) + << "set sort associated to this solver object"; return mkValHelper(CVC4::EmptySet(*s.d_type)); @@ -3217,6 +3278,7 @@ Term Solver::mkSepNil(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); (void)res.getType(true); /* kick off type checking */ @@ -3272,6 +3334,7 @@ Term Solver::mkUniverseSet(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); @@ -3324,7 +3387,10 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const Term Solver::mkConstArray(Sort sort, Term val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(sort); CVC4_API_ARG_CHECK_NOT_NULL(val); + CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort())) << "Value does not match element sort."; @@ -3405,6 +3471,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); return mkValHelper( CVC4::UninterpretedConstant(*sort.d_type, index)); @@ -3448,6 +3515,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) << "a bit-vector constant with bit-width '" << bw << "'"; CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_ARG_CHECK_EXPECTED( val.getSort().isBitVector() && val.d_expr->isConst(), val) << "bit-vector constant"; @@ -3465,6 +3533,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type) : d_exprMgr->mkVar(symbol, *sort.d_type); @@ -3481,6 +3550,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type) : d_exprMgr->mkBoundVar(symbol, *sort.d_type); @@ -3490,6 +3560,15 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const CVC4_API_SOLVER_TRY_CATCH_END; } +/* Create datatype constructor declarations */ +/* -------------------------------------------------------------------------- */ + +DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( + const std::string& name) +{ + return DatatypeConstructorDecl(this, name); +} + /* Create datatype declarations */ /* -------------------------------------------------------------------------- */ @@ -3526,6 +3605,7 @@ Term Solver::mkTerm(Kind kind, Term child) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(child); checkMkTerm(kind, 1); Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); @@ -3540,6 +3620,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); checkMkTerm(kind, 2); Expr res = @@ -3564,6 +3646,7 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const Term Solver::mkTerm(Op op) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); Term res; if (op.isIndexedHelper()) @@ -3585,7 +3668,9 @@ Term Solver::mkTerm(Op op) const Term Solver::mkTerm(Op op, Term child) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(child); const CVC4::Kind int_kind = extToIntKind(op.d_kind); Expr res; @@ -3607,8 +3692,11 @@ Term Solver::mkTerm(Op op, Term child) const Term Solver::mkTerm(Op op, Term child1, Term child2) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); const CVC4::Kind int_kind = extToIntKind(op.d_kind); Expr res; @@ -3630,9 +3718,13 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); + CVC4_API_SOLVER_CHECK_TERM(child3); const CVC4::Kind int_kind = extToIntKind(op.d_kind); Expr res; @@ -3656,11 +3748,15 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const Term Solver::mkTerm(Op op, const std::vector& children) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); for (size_t i = 0, size = children.size(); i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "parameter term", children[i], i) + !children[i].isNull(), "child term", children[i], i) << "non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == children[i].d_solver, "child term", children[i], i) + << "child term associated to this solver object"; } const CVC4::Kind int_kind = extToIntKind(op.d_kind); @@ -3690,6 +3786,12 @@ Term Solver::mkTuple(const std::vector& sorts, std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == terms[i].d_solver, "child term", terms[i], i) + << "child term associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sorts[i].d_solver, "child sort", sorts[i], i) + << "child sort associated to this solver object"; args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); } @@ -3913,12 +4015,13 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const /* Non-SMT-LIB commands */ /* -------------------------------------------------------------------------- */ -Term Solver::simplify(const Term& t) +Term Solver::simplify(const Term& term) { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(t); + CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->simplify(*t.d_expr)); + return Term(this, d_smtEngine->simplify(*term.d_expr)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3932,6 +4035,7 @@ Result Solver::checkEntailed(Term term) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_SOLVER_CHECK_TERM(term); CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr); return Result(r); @@ -3949,6 +4053,7 @@ Result Solver::checkEntailed(const std::vector& terms) const "(try --incremental)"; for (const Term& term : terms) { + CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); } @@ -3967,10 +4072,11 @@ Result Solver::checkEntailed(const std::vector& terms) const */ void Solver::assertFormula(Term term) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(term); + CVC4_API_ARG_CHECK_NOT_NULL(term); d_smtEngine->assertFormula(*term.d_expr); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -3978,10 +4084,15 @@ void Solver::assertFormula(Term term) const */ Result Solver::checkSat(void) const { - // CHECK: - // if d_queryMade -> incremental enabled + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(!d_smtEngine->isQueryMade() + || CVC4::options::incrementalSolving()) + << "Cannot make multiple queries unless incremental solving is enabled " + "(try --incremental)"; CVC4::Result r = d_smtEngine->checkSat(); return Result(r); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -3989,10 +4100,16 @@ Result Solver::checkSat(void) const */ Result Solver::checkSatAssuming(Term assumption) const { - // CHECK: - // if assumptions.size() > 0: incremental enabled? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(!d_smtEngine->isQueryMade() + || CVC4::options::incrementalSolving()) + << "Cannot make multiple queries unless incremental solving is enabled " + "(try --incremental)"; + CVC4_API_SOLVER_CHECK_TERM(assumption); CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr); return Result(r); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4000,11 +4117,21 @@ Result Solver::checkSatAssuming(Term assumption) const */ Result Solver::checkSatAssuming(const std::vector& assumptions) const { - // CHECK: - // if assumptions.size() > 0: incremental enabled? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 + || CVC4::options::incrementalSolving()) + << "Cannot make multiple queries unless incremental solving is enabled " + "(try --incremental)"; + for (const Term& term : assumptions) + { + CVC4_API_SOLVER_CHECK_TERM(term); + CVC4_API_ARG_CHECK_NOT_NULL(term); + } std::vector eassumptions = termVectorToExprs(assumptions); CVC4::Result r = d_smtEngine->checkSat(eassumptions); return Result(r); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4014,14 +4141,21 @@ Sort Solver::declareDatatype( const std::string& symbol, const std::vector& ctors) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors) << "a datatype declaration with at least one constructor"; DatatypeDecl dtdecl(this, symbol); - for (const DatatypeConstructorDecl& ctor : ctors) + for (size_t i = 0, size = ctors.size(); i < size; i++) { - dtdecl.addConstructor(ctor); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver, + "datatype constructor declaration", + ctors[i], + i) + << "datatype constructor declaration associated to this solver object"; + dtdecl.addConstructor(ctors[i]); } return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype)); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4031,14 +4165,19 @@ Term Solver::declareFun(const std::string& symbol, const std::vector& sorts, Sort sort) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == sorts[i].d_solver, "parameter sort", sorts[i], i) + << "parameter sort associated to this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( sorts[i].isFirstClass(), "parameter sort", sorts[i], i) << "first-class sort as parameter sort for function sort"; } CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as function codomain sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); Assert(!sort.isFunction()); /* A function sort is not first-class. */ Type type = *sort.d_type; if (!sorts.empty()) @@ -4047,6 +4186,7 @@ Term Solver::declareFun(const std::string& symbol, type = d_exprMgr->mkFunctionType(types, type); } return Term(this, d_exprMgr->mkVar(symbol, type)); + CVC4_API_SOLVER_TRY_CATCH_END; } /** diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 87be7b74c..855ba4400 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1167,14 +1167,13 @@ class DatatypeIterator; class CVC4_PUBLIC DatatypeConstructorDecl { friend class DatatypeDecl; + friend class Solver; public: /** - * Constructor. - * @param name the name of the datatype constructor - * @return the DatatypeConstructorDecl + * Nullary constructor for Cython. */ - DatatypeConstructorDecl(const std::string& name); + DatatypeConstructorDecl(); /** * Add datatype selector declaration. @@ -1198,6 +1197,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; private: + /** + * Constructor. + * @param slv the associated solver object + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ + DatatypeConstructorDecl(const Solver* slv, const std::string& name); + + /** + * The associated solver object. + */ + const Solver* d_solver; + /** * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. @@ -1219,7 +1231,7 @@ class CVC4_PUBLIC DatatypeDecl public: /** - * Nullary constructor for Cython + * Nullary constructor for Cython. */ DatatypeDecl(); @@ -1240,6 +1252,9 @@ class CVC4_PUBLIC DatatypeDecl /** Is this Datatype declaration parametric? */ bool isParametric() const; + /** + * @return true if this DatatypeDecl is a null object + */ bool isNull() const; /** @@ -1257,7 +1272,7 @@ class CVC4_PUBLIC DatatypeDecl private: /** * Constructor. - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param isCoDatatype true if a codatatype is to be constructed * @return the DatatypeDecl @@ -1269,7 +1284,7 @@ class CVC4_PUBLIC DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param param the sort parameter * @param isCoDatatype true if a codatatype is to be constructed @@ -1282,7 +1297,7 @@ class CVC4_PUBLIC DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the solver that created this datatype declaration + * @param slv the associated solver object * @param name the name of the datatype * @param params a list of sort parameters * @param isCoDatatype true if a codatatype is to be constructed @@ -1292,9 +1307,17 @@ class CVC4_PUBLIC DatatypeDecl const std::vector& params, bool isCoDatatype = false); - // helper for isNull() to avoid calling API functions from other API functions + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ bool isNullHelper() const; + /** + * The associated solver object. + */ + const Solver* d_solver; + /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -2679,6 +2702,12 @@ class CVC4_PUBLIC Solver */ Term mkVar(Sort sort, const std::string& symbol = std::string()) const; + /* .................................................................... */ + /* Create datatype constructor declarations */ + /* .................................................................... */ + + DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); + /* .................................................................... */ /* Create datatype declarations */ /* .................................................................... */ diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 1c7071958..2ca4b3645 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -54,7 +54,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeConstructorDecl: - DatatypeConstructorDecl(const string& name) except + void addSelector(const string& name, Sort sort) except + void addSelectorSelf(const string& name) except + string toString() except + @@ -160,6 +159,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": # default value for symbol defined in cvc4cpp.h Term mkConst(Sort sort) except + Term mkVar(Sort sort, const string& symbol) except + + DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except + DatatypeDecl mkDatatypeDecl(const string& name) except + DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except + DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index fa5313f0e..e742e0061 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -134,12 +134,14 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: - cdef c_DatatypeConstructorDecl* cddc - def __cinit__(self, str name): - self.cddc = new c_DatatypeConstructorDecl(name.encode()) + cdef c_DatatypeConstructorDecl cddc + + def __cinit__(self): + pass def addSelector(self, str name, Sort sort): self.cddc.addSelector(name.encode(), sort.csort) + def addSelectorSelf(self, str name): self.cddc.addSelectorSelf(name.encode()) @@ -156,7 +158,7 @@ cdef class DatatypeDecl: pass def addConstructor(self, DatatypeConstructorDecl ctor): - self.cdd.addConstructor(ctor.cddc[0]) + self.cdd.addConstructor(ctor.cddc) def isParametric(self): return self.cdd.isParametric() @@ -675,6 +677,11 @@ cdef class Solver: ( symbol).encode()) return term + def mkDatatypeConstructorDecl(self, str name): + cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl() + ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode()) + return ddc + def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None): cdef DatatypeDecl dd = DatatypeDecl() cdef vector[c_Sort] v @@ -790,7 +797,7 @@ cdef class Solver: cdef vector[c_DatatypeConstructorDecl] v for c in ctors: - v.push_back(( c).cddc[0]) + v.push_back(( c).cddc) sort.csort = self.csolver.declareDatatype(symbol.encode(), v) return sort diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fdb6a081c..e604c7769 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::api::Sort& t, PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); api::Term func = PARSER_STATE->mkVar( *i, - api::Sort(PARSER_STATE->getSolver(), t.getType()), + api::Sort(SOLVER, t.getType()), ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); Command* decl = @@ -1654,9 +1654,7 @@ tupleStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()), - f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1689,9 +1687,7 @@ recordStore[CVC4::api::Term& f] } const Datatype & dt = ((DatatypeType)t.getType()).getDatatype(); f2 = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()), - f); + api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1835,10 +1831,9 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()), - f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][id].getSelector()), + f); } | k=numeral { @@ -1853,10 +1848,9 @@ postfixTerm[CVC4::api::Term& f] PARSER_STATE->parseError(ss.str()); } const Datatype & dt = ((DatatypeType)type.getType()).getDatatype(); - f = SOLVER->mkTerm( - api::APPLY_SELECTOR, - api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()), - f); + f = SOLVER->mkTerm(api::APPLY_SELECTOR, + api::Term(SOLVER, dt[0][k].getSelector()), + f); } ) )* @@ -1896,8 +1890,7 @@ relationTerm[CVC4::api::Term& f] types.push_back(f.getSort()); api::Sort t = SOLVER->mkTupleSort(types); const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype()); - args.insert(args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN @@ -2147,9 +2140,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert( - args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } } @@ -2160,7 +2151,7 @@ simpleTerm[CVC4::api::Term& f] api::Sort dtype = SOLVER->mkTupleSort(types); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); f = MK_TERM(api::APPLY_CONSTRUCTOR, - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + api::Term(SOLVER, dt[0].getConstructor())); } /* empty record literal */ @@ -2170,7 +2161,7 @@ simpleTerm[CVC4::api::Term& f] std::vector>()); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); f = MK_TERM(api::APPLY_CONSTRUCTOR, - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + api::Term(SOLVER, dt[0].getConstructor())); } /* empty set literal */ | LBRACE RBRACE @@ -2268,8 +2259,7 @@ simpleTerm[CVC4::api::Term& f] } api::Sort dtype = SOLVER->mkRecordSort(typeIds); const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype(); - args.insert(args.begin(), - api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor())); + args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor())); f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } @@ -2377,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type] std::unique_ptr ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { - ctor.reset(new CVC4::api::DatatypeConstructorDecl(id)); + { + ctor.reset(new CVC4::api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id))); } ( LPAREN selector[&ctor] diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f29e03380..62bf7e974 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret, PARSER_STATE->getUnresolvedSorts().clear(); - ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]); + ret = api::Sort(SOLVER, datatypeTypes[0]); }; // SyGuS grammar term. @@ -1798,7 +1798,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] if (Datatype::datatypeOf(ef).isParametric()) { type = api::Sort( - PARSER_STATE->getSolver(), + SOLVER, Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] .getSpecializedConstructorType(expr.getSort().getType())); } @@ -2521,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type] } : symbol[id,CHECK_NONE,SYM_VARIABLE] { - ctor = new api::DatatypeConstructorDecl(id); + ctor = new api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id)); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c1d60ca31..e26709595 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; @@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index b404dfb13..c9eaf103e 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -43,10 +43,10 @@ void DatatypeBlack::tearDown() {} void DatatypeBlack::testMkDatatypeSort() { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype d = listSort.getDatatype(); @@ -75,22 +75,22 @@ void DatatypeBlack::testMkDatatypeSorts() unresTypes.insert(unresList); DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); - DatatypeConstructorDecl node("node"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); node.addSelector("left", unresTree); node.addSelector("right", unresTree); tree.addConstructor(node); - DatatypeConstructorDecl leaf("leaf"); + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); leaf.addSelector("data", unresList); tree.addConstructor(leaf); DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("car", unresTree); cons.addSelector("cdr", unresTree); list.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); list.addConstructor(nil); std::vector dtdecls; @@ -130,13 +130,13 @@ void DatatypeBlack::testDatatypeStructs() // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); Sort nullSort; TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); @@ -152,11 +152,11 @@ void DatatypeBlack::testDatatypeStructs() // create datatype sort to test DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); - DatatypeConstructorDecl ca("A"); + DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); dtypeSpecEnum.addConstructor(ca); - DatatypeConstructorDecl cb("B"); + DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); dtypeSpecEnum.addConstructor(cb); - DatatypeConstructorDecl cc("C"); + DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); dtypeSpecEnum.addConstructor(cc); Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); Datatype dtEnum = dtypeSortEnum.getDatatype(); @@ -165,7 +165,8 @@ void DatatypeBlack::testDatatypeStructs() // create codatatype DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); - DatatypeConstructorDecl consStream("cons"); + DatatypeConstructorDecl consStream = + d_solver.mkDatatypeConstructorDecl("cons"); consStream.addSelector("head", intSort); consStream.addSelectorSelf("tail"); dtypeSpecStream.addConstructor(consStream); @@ -204,11 +205,11 @@ void DatatypeBlack::testDatatypeNames() DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); TS_ASSERT(dtypeSpec.getName() == std::string("list")); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 90d4c10c1..7e925df54 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -39,6 +39,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkBitVectorSort(); void testMkFloatingPointSort(); void testMkDatatypeSort(); + void testMkDatatypeSorts(); void testMkFunctionSort(); void testMkOp(); void testMkParamSort(); @@ -96,9 +97,15 @@ class SolverBlack : public CxxTest::TestSuite void testPop3(); void testSimplify(); + + void testAssertFormula(); void testCheckEntailed(); void testCheckEntailed1(); void testCheckEntailed2(); + void testCheckSat(); + void testCheckSatAssuming(); + void testCheckSatAssuming1(); + void testCheckSatAssuming2(); void testSetInfo(); void testSetLogic(); @@ -173,6 +180,8 @@ void SolverBlack::testMkArraySort() 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)); + Solver slv; + TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&); } void SolverBlack::testMkBitVectorSort() @@ -191,17 +200,64 @@ void SolverBlack::testMkFloatingPointSort() void SolverBlack::testMkDatatypeSort() { DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver->getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec)); + + Solver slv; + TS_ASSERT_THROWS(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException&); + DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list"); TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); } +void SolverBlack::testMkDatatypeSorts() +{ + Solver slv; + + DatatypeDecl dtypeSpec1 = d_solver->mkDatatypeDecl("list1"); + DatatypeConstructorDecl cons1 = d_solver->mkDatatypeConstructorDecl("cons1"); + cons1.addSelector("head1", d_solver->getIntegerSort()); + dtypeSpec1.addConstructor(cons1); + DatatypeConstructorDecl nil1 = d_solver->mkDatatypeConstructorDecl("nil1"); + dtypeSpec1.addConstructor(nil1); + DatatypeDecl dtypeSpec2 = d_solver->mkDatatypeDecl("list2"); + DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons2"); + cons2.addSelector("head2", d_solver->getIntegerSort()); + dtypeSpec2.addConstructor(cons2); + DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil2"); + dtypeSpec2.addConstructor(nil2); + std::vector decls = {dtypeSpec1, dtypeSpec2}; + TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(decls)); + + TS_ASSERT_THROWS(slv.mkDatatypeSorts(decls), CVC4ApiException&); + + DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list"); + std::vector throwsDecls = {throwsDtypeSpec}; + TS_ASSERT_THROWS(d_solver->mkDatatypeSorts(throwsDecls), CVC4ApiException&); + + /* with unresolved sorts */ + Sort unresList = d_solver->mkUninterpretedSort("ulist"); + std::set unresSorts = {unresList}; + DatatypeDecl ulist = d_solver->mkDatatypeDecl("ulist"); + DatatypeConstructorDecl ucons = d_solver->mkDatatypeConstructorDecl("ucons"); + ucons.addSelector("car", unresList); + ucons.addSelector("cdr", unresList); + ulist.addConstructor(ucons); + DatatypeConstructorDecl unil = d_solver->mkDatatypeConstructorDecl("unil"); + ulist.addConstructor(unil); + std::vector udecls = {ulist}; + TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(udecls, unresSorts)); + + TS_ASSERT_THROWS(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException&); + + /* Note: More tests are in datatype_api_black. */ +} + void SolverBlack::testMkFunctionSort() { TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort( @@ -228,6 +284,23 @@ void SolverBlack::testMkFunctionSort() {d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")}, funSort2), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.mkFunctionSort(d_solver->mkUninterpretedSort("u"), + d_solver->getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkFunctionSort(slv.mkUninterpretedSort("u"), + d_solver->getIntegerSort()), + CVC4ApiException&); + std::vector sorts1 = {d_solver->getBooleanSort(), + slv.getIntegerSort(), + d_solver->getIntegerSort()}; + std::vector sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()}; + TS_ASSERT_THROWS_NOTHING(slv.mkFunctionSort(sorts2, slv.getIntegerSort())); + TS_ASSERT_THROWS(slv.mkFunctionSort(sorts1, slv.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkFunctionSort(sorts2, d_solver->getIntegerSort()), + CVC4ApiException&); } void SolverBlack::testMkParamSort() @@ -246,6 +319,10 @@ void SolverBlack::testMkPredicateSort() TS_ASSERT_THROWS( d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.mkPredicateSort({d_solver->getIntegerSort()}), + CVC4ApiException&); } void SolverBlack::testMkRecordSort() @@ -259,6 +336,9 @@ void SolverBlack::testMkRecordSort() TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty)); Sort recSort = d_solver->mkRecordSort(fields); TS_ASSERT_THROWS_NOTHING(recSort.getDatatype()); + + Solver slv; + TS_ASSERT_THROWS(slv.mkRecordSort(fields), CVC4ApiException&); } void SolverBlack::testMkSetSort() @@ -266,6 +346,9 @@ 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))); + Solver slv; + TS_ASSERT_THROWS(slv.mkSetSort(d_solver->mkBitVectorSort(4)), + CVC4ApiException&); } void SolverBlack::testMkUninterpretedSort() @@ -288,6 +371,10 @@ void SolverBlack::testMkTupleSort() d_solver->getIntegerSort()); TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.mkTupleSort({d_solver->getIntegerSort()}), + CVC4ApiException&); } void SolverBlack::testMkBitVector() @@ -332,6 +419,8 @@ void SolverBlack::testMkVar() 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&); + Solver slv; + TS_ASSERT_THROWS(slv.mkVar(boolSort, "x"), CVC4ApiException&); } void SolverBlack::testMkBoolean() @@ -352,6 +441,9 @@ void SolverBlack::testMkUninterpretedConst() d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1)); TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.mkUninterpretedConst(d_solver->getBooleanSort(), 1), + CVC4ApiException&); } void SolverBlack::testMkAbstractValue() @@ -393,13 +485,23 @@ void SolverBlack::testMkFloatingPoint() 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&); + + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + Solver slv; + TS_ASSERT_THROWS(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException&); + } } void SolverBlack::testMkEmptySet() { + Solver slv; + Sort s = d_solver->mkSetSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(s)); TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()), CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort())); + TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } void SolverBlack::testMkFalse() @@ -558,6 +660,8 @@ void SolverBlack::testMkSepNil() { TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort())); TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.mkSepNil(d_solver->getIntegerSort()), CVC4ApiException&); } void SolverBlack::testMkString() @@ -592,6 +696,7 @@ void SolverBlack::testMkTerm() std::vector v4 = {d_solver->mkReal(1), d_solver->mkReal(2)}; std::vector v5 = {d_solver->mkReal(1), Term()}; std::vector v6 = {}; + Solver slv; // mkTerm(Kind kind) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI)); @@ -603,6 +708,7 @@ void SolverBlack::testMkTerm() 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(slv.mkTerm(NOT, d_solver->mkTrue()), CVC4ApiException&); // mkTerm(Kind kind, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b)); @@ -610,6 +716,7 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkTerm(EQUAL, a, b), CVC4ApiException&); // mkTerm(Kind kind, Term child1, Term child2, Term child3) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( @@ -626,6 +733,10 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS( d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b), CVC4ApiException&); + TS_ASSERT_THROWS( + slv.mkTerm( + ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()), + CVC4ApiException&); // mkTerm(Kind kind, const std::vector& children) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1)); @@ -643,15 +754,17 @@ void SolverBlack::testMkTermFromOp() std::vector v2 = {d_solver->mkReal(1), Term()}; std::vector v3 = {}; std::vector v4 = {d_solver->mkReal(5)}; + Solver slv; + // simple operator terms Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); Op opterm2 = d_solver->mkOp(DIVISIBLE, 1); - // list datatype + // list datatype Sort sort = d_solver->mkParamSort("T"); DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl cons("cons"); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil"); cons.addSelector("head", sort); cons.addSelectorSelf("tail"); listDecl.addConstructor(cons); @@ -661,6 +774,7 @@ void SolverBlack::testMkTermFromOp() listSort.instantiate(std::vector{d_solver->getIntegerSort()}); Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); + // list datatype constructor and selector operator terms Term consTerm1 = list.getConstructorTerm("cons"); Term consTerm2 = list.getConstructor("cons").getConstructorTerm(); @@ -684,6 +798,7 @@ void SolverBlack::testMkTermFromOp() TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException&); // mkTerm(Op op, Term child) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); @@ -695,24 +810,29 @@ void SolverBlack::testMkTermFromOp() TS_ASSERT_THROWS( d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&); // mkTerm(Op op, Term child1, Term child2) const - TS_ASSERT_THROWS( - d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)), - CVC4ApiException&); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0), d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); + TS_ASSERT_THROWS( + d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, + consTerm1, + d_solver->mkReal(0), + d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)), + CVC4ApiException&); - // mkTerm(Op op, Term child1, Term child2, Term child3) - // const + // mkTerm(Op op, Term child1, Term child2, Term child3) const TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( @@ -724,6 +844,7 @@ void SolverBlack::testMkTermFromOp() TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkTerm(opterm2, v4), CVC4ApiException&); } void SolverBlack::testMkTrue() @@ -747,12 +868,22 @@ void SolverBlack::testMkTuple() TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()}, {d_solver->mkReal("5.3")}), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS( + slv.mkTuple({d_solver->mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}), + 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&); + Solver slv; + TS_ASSERT_THROWS(slv.mkUniverseSet(d_solver->getBooleanSort()), + CVC4ApiException&); } void SolverBlack::testMkConst() @@ -768,6 +899,9 @@ void SolverBlack::testMkConst() 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&); + + Solver slv; + TS_ASSERT_THROWS(slv.mkConst(boolSort), CVC4ApiException&); } void SolverBlack::testMkConstArray() @@ -778,23 +912,29 @@ void SolverBlack::testMkConstArray() Term constArr = d_solver->mkConstArray(arrSort, zero); TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero)); + TS_ASSERT_THROWS(d_solver->mkConstArray(Sort(), zero), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&); + Solver slv; + Term zero2 = slv.mkReal(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&); } void SolverBlack::testDeclareDatatype() { - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil"); std::vector ctors1 = {nil}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); - DatatypeConstructorDecl cons("cons"); - DatatypeConstructorDecl nil2("nil"); + DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil"); std::vector ctors2 = {cons, nil2}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); - DatatypeConstructorDecl cons2("cons"); - DatatypeConstructorDecl nil3("nil"); + DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil3 = d_solver->mkDatatypeConstructorDecl("nil"); std::vector ctors3 = {cons2, nil3}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3)); std::vector ctors4; @@ -802,6 +942,9 @@ void SolverBlack::testDeclareDatatype() CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.declareDatatype(std::string("a"), ctors1), + CVC4ApiException&); } void SolverBlack::testDeclareFun() @@ -817,6 +960,8 @@ void SolverBlack::testDeclareFun() CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.declareFun("f1", {}, bvSort), CVC4ApiException&); } void SolverBlack::testDeclareSort() @@ -959,11 +1104,11 @@ void SolverBlack::testGetOp() // Test Datatypes -- more complicated DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver->getIntegerSort()); cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil"); consListSpec.addConstructor(nil); Sort consListSort = d_solver->mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); @@ -1059,11 +1204,11 @@ void SolverBlack::testSimplify() Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver->getIntegerSort()); cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil"); consListSpec.addConstructor(nil); Sort consListSort = d_solver->mkDatatypeSort(consListSpec); @@ -1081,6 +1226,8 @@ void SolverBlack::testSimplify() TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b)); TS_ASSERT(d_solver->mkTrue() != x_eq_b); TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b)); + Solver slv; + TS_ASSERT_THROWS(slv.simplify(x), CVC4ApiException&); Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1"); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1)); @@ -1123,12 +1270,22 @@ void SolverBlack::testSimplify() TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2)); } +void SolverBlack::testAssertFormula() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->assertFormula(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->assertFormula(Term()), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.assertFormula(d_solver->mkTrue()), CVC4ApiException&); +} + void SolverBlack::testCheckEntailed() { d_solver->setOption("incremental", "false"); TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&); } void SolverBlack::testCheckEntailed1() @@ -1142,6 +1299,8 @@ void SolverBlack::testCheckEntailed1() TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z)); + Solver slv; + TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&); } void SolverBlack::testCheckEntailed2() @@ -1191,6 +1350,91 @@ void SolverBlack::testCheckEntailed2() TS_ASSERT_THROWS( d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&); +} + +void SolverBlack::testCheckSat() +{ + d_solver->setOption("incremental", "false"); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSat()); + TS_ASSERT_THROWS(d_solver->checkSat(), CVC4ApiException&); +} + +void SolverBlack::testCheckSatAssuming() +{ + d_solver->setOption("incremental", "false"); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkSatAssuming(d_solver->mkTrue()), + CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&); +} + +void SolverBlack::testCheckSatAssuming1() +{ + Sort boolSort = d_solver->getBooleanSort(); + Term x = d_solver->mkConst(boolSort, "x"); + Term y = d_solver->mkConst(boolSort, "y"); + Term z = d_solver->mkTerm(AND, x, y); + d_solver->setOption("incremental", "true"); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkSatAssuming(Term()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(z)); + Solver slv; + TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&); +} + +void SolverBlack::testCheckSatAssuming2() +{ + d_solver->setOption("incremental", "true"); + + Sort uSort = d_solver->mkUninterpretedSort("u"); + Sort intSort = d_solver->getIntegerSort(); + Sort boolSort = d_solver->getBooleanSort(); + Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort); + Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort); + + Term n = Term(); + // Constants + Term x = d_solver->mkConst(uSort, "x"); + Term y = d_solver->mkConst(uSort, "y"); + // Functions + 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); + // Terms + 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); + Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero); + Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y); + // Assertions + Term assertions = + d_solver->mkTerm(AND, + std::vector{ + d_solver->mkTerm(LEQ, zero, f_x), // 0 <= f(x) + d_solver->mkTerm(LEQ, zero, f_y), // 0 <= f(y) + d_solver->mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); + + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue())); + d_solver->assertFormula(assertions); + TS_ASSERT_THROWS_NOTHING( + d_solver->checkSatAssuming(d_solver->mkTerm(DISTINCT, x, y))); + TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming( + {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)})); + TS_ASSERT_THROWS(d_solver->checkSatAssuming(n), CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->checkSatAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}), + CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&); } void SolverBlack::testSetLogic() diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 42d2dcb25..437b5cf26 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -63,10 +63,10 @@ void SortBlack::testGetDatatype() { // create datatype sort, check should not fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); @@ -80,11 +80,11 @@ void SortBlack::testDatatypeSorts() Sort intSort = d_solver.getIntegerSort(); // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); @@ -121,8 +121,9 @@ void SortBlack::testInstantiate() // instantiate parametric datatype, check should not fail Sort sort = d_solver.mkParamSort("T"); DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); + DatatypeConstructorDecl paramCons = + d_solver.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil"); paramCons.addSelector("head", sort); paramDtypeSpec.addConstructor(paramCons); paramDtypeSpec.addConstructor(paramNil); @@ -131,10 +132,10 @@ void SortBlack::testInstantiate() paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()})); // instantiate non-parametric datatype sort, check should fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); TS_ASSERT_THROWS( @@ -265,8 +266,9 @@ void SortBlack::testGetDatatypeParamSorts() // create parametric datatype, check should not fail Sort sort = d_solver.mkParamSort("T"); DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); + DatatypeConstructorDecl paramCons = + d_solver.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil"); paramCons.addSelector("head", sort); paramDtypeSpec.addConstructor(paramCons); paramDtypeSpec.addConstructor(paramNil); @@ -274,10 +276,10 @@ void SortBlack::testGetDatatypeParamSorts() TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); // create non-parametric datatype sort, check should fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); @@ -287,10 +289,10 @@ void SortBlack::testGetDatatypeArity() { // create datatype sort, check should not fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index d8f022201..a3cbd028f 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -197,8 +197,8 @@ void TermBlack::testGetOp() // Test Datatypes Ops Sort sort = d_solver.mkParamSort("T"); DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl cons("cons"); - DatatypeConstructorDecl nil("nil"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); cons.addSelector("head", sort); cons.addSelectorSelf("tail"); listDecl.addConstructor(cons); -- cgit v1.2.3