From d52bc44199583e3c06816c1d30f61e8075820c1b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 17 Mar 2021 17:28:59 -0700 Subject: New C++ Api: Comprehensive guards for member functions of class Solver. (#6153) --- src/api/checks.h | 324 +++++++++++++++++++- src/api/cvc4cpp.cpp | 864 +++++++++++++++++++++++----------------------------- src/api/cvc4cpp.h | 29 +- 3 files changed, 706 insertions(+), 511 deletions(-) (limited to 'src/api') diff --git a/src/api/checks.h b/src/api/checks.h index 85322048c..c2869f463 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -334,21 +334,321 @@ namespace api { /* Checks for class Solver. */ /* -------------------------------------------------------------------------- */ -/** Sort checks for member functions of class Solver. */ -#define CVC4_API_SOLVER_CHECK_SORT(sort) \ - CVC4_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; +/* Sort checks. ------------------------------------------------------------- */ -/** Term checks for member functions of class Solver. */ -#define CVC4_API_SOLVER_CHECK_TERM(term) \ - CVC4_API_CHECK(this == term.d_solver) \ - << "Given term is not associated with this solver"; +/** + * Sort checks for member functions of class Solver. + * Check if given sort is not null and associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + } while (0) + +/** + * Sort checks for member functions of class Solver. + * Check if each sort in the given container of sorts is not null and + * associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_SORTS(sorts) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : sorts) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == s.d_solver, "sort", sorts, i) \ + << "a sort associated with this solver"; \ + i += 1; \ + } \ + } while (0) + +/** + * Sort checks for member functions of class Solver. + * Check if each sort in the given container of sorts is not null, associated + * with this solver, and not function-like. + */ +#define CVC4_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : sorts) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == s.d_solver, "sort", sorts, i) \ + << "a sorts associated with this solver"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + !s.isFunctionLike(), "sort", sorts, i) \ + << "non-function-like sort"; \ + i += 1; \ + } \ + } while (0) + +/** + * Domain sort check for member functions of class Solver. + * Check if domain sort is not null, associated with this solver, and a + * first-class sort. + */ +#define CVC4_API_SOLVER_CHECK_DOMAIN_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ + << "first-class sort as domain sort"; \ + } while (0) + +/** + * Domain sort checks for member functions of class Solver. + * Check if each domain sort in the given container of sorts is not null, + * associated with this solver, and a first-class sort. + */ +#define CVC4_API_SOLVER_CHECK_DOMAIN_SORTS(sorts) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : sorts) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("domain sort", s, sorts, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == s.d_solver, "domain sort", sorts, i) \ + << "a sort associated with this solver object"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + s.isFirstClass(), "domain sort", sorts, i) \ + << "first-class sort as domain sort"; \ + i += 1; \ + } \ + } while (0) + +/** + * Codomain sort check for member functions of class Solver. + * Check if codomain sort is not null, associated with this solver, and a + * first-class sort. + */ +#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ + << "first-class sort as codomain sort"; \ + } while (0) + +/* Term checks. ------------------------------------------------------------- */ + +/** + * Term checks for member functions of class Solver. + * Check if given term is not null and associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_TERM(term) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(term); \ + CVC4_API_CHECK(this == term.d_solver) \ + << "Given term is not associated with this solver"; \ + } while (0) + +/** + * Term checks for member functions of class Solver. + * Check if each term in the given container of terms is not null and + * associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_TERMS(terms) \ + do \ + { \ + size_t i = 0; \ + for (const auto& t : terms) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("terms", t, terms, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == t.d_solver, "term", terms, i) \ + << "a term associated with this solver"; \ + i += 1; \ + } \ + } while (0) -/** Op checks for member functions of class Solver. */ -#define CVC4_API_SOLVER_CHECK_OP(op) \ - CVC4_API_CHECK(this == op.d_solver) \ - << "Given operator is not associated with this solver"; +/** + * Term checks for member functions of class Solver. + * Check if given term is not null, associated with this solver, and of given + * sort. + */ +#define CVC4_API_SOLVER_CHECK_TERM_WITH_SORT(term, sort) \ + do \ + { \ + CVC4_API_SOLVER_CHECK_TERM(term); \ + CVC4_API_CHECK(term.getSort() == sort) \ + << "Expected term with sort " << sort; \ + } while (0) +/** + * Term checks for member functions of class Solver. + * Check if each term in the given container is not null, associated with this + * solver, and of the given sort. + */ +#define CVC4_API_SOLVER_CHECK_TERMS_WITH_SORT(terms, sort) \ + do \ + { \ + size_t i = 0; \ + for (const auto& t : terms) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == t.d_solver, "term", terms, i) \ + << "a term associated with this solver"; \ + CVC4_API_CHECK(t.getSort() == sort) \ + << "Expected term with sort " << sort << " at index " << i << " in " \ + << #terms; \ + i += 1; \ + } \ + } while (0) + +/** + * Bound variable checks for member functions of class Solver. + * Check if each term in the given container is not null, associated with this + * solver, and a bound variable. + */ +#define CVC4_API_SOLVER_CHECK_BOUND_VARS(bound_vars) \ + do \ + { \ + size_t i = 0; \ + for (const auto& bv : bound_vars) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + "bound variable", bv, bound_vars, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == bv.d_solver, "bound variable", bound_vars, i) \ + << "a term associated with this solver object"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + bv.d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, \ + "bound variable", \ + bound_vars, \ + i) \ + << "a bound variable"; \ + i += 1; \ + } \ + } while (0) + +/** + * Bound variable checks for member functions of class Solver that define + * functions. + * Check if each term in the given container is not null, associated with this + * solver, a bound variable, matches theh corresponding sort in 'domain_sorts', + * and is a first-class term. + */ +#define CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN( \ + fun, bound_vars, domain_sorts) \ + do \ + { \ + size_t size = bound_vars.size(); \ + CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) \ + << "'" << domain_sorts.size() << "'"; \ + size_t i = 0; \ + for (const auto& bv : bound_vars) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + "bound variable", bv, bound_vars, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == bv.d_solver, "bound variable", bound_vars, i) \ + << "a term associated with this solver object"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + bv.d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, \ + "bound variable", \ + bound_vars, \ + i) \ + << "a bound variable"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + domain_sorts[i] == bound_vars[i].getSort(), \ + "sort of parameter", \ + bound_vars, \ + i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + domain_sorts[i].isFirstClass(), "domain sort", domain_sorts, i) \ + << "first-class sort of parameter of defined function"; \ + i += 1; \ + } \ + } while (0) + +/* Op checks. --------------------------------------------------------------- */ + +/** + * Op checks for member functions of class Solver. + * Check if given operator is not null and associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_OP(op) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(op); \ + CVC4_API_CHECK(this == op.d_solver) \ + << "Given operator is not associated with this solver"; \ + } while (0) + +/* Datatype checks. --------------------------------------------------------- */ + +/** + * DatatypeDecl checks for member functions of class Solver. + * Check if given datatype declaration is not null and associated with this + * solver. + */ +#define CVC4_API_SOLVER_CHECK_DTDECL(decl) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(decl); \ + CVC4_API_CHECK(this == decl.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"; \ + } while (0) + +/** + * DatatypeDecl checks for member functions of class Solver. + * Check if each datatype declaration in the given container of declarations is + * not null and associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_DTDECLS(decls) \ + do \ + { \ + size_t i = 0; \ + for (const auto& d : decls) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + "datatype declaration", d, decls, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == d.d_solver, "datatype declaration", decls, i) \ + << "a datatype declaration associated with this solver"; \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + d.getNumConstructors() > 0, "datatype declaration", decls, i) \ + << "a datatype declaration with at least one constructor"; \ + i += 1; \ + } \ + } while (0) + +/** + * DatatypeConstructorDecl checks for member functions of class Solver. + * Check if each datatype constructor declaration in the given container of + * declarations is not null and associated with this solver. + */ +#define CVC4_API_SOLVER_CHECK_DTCTORDECLS(decls) \ + do \ + { \ + size_t i = 0; \ + for (const auto& d : decls) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL( \ + "datatype constructor declaration", d, decls, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this == d.d_solver, "datatype constructor declaration", decls, i) \ + << "a datatype constructor declaration associated with this solver " \ + "object"; \ + i += 1; \ + } \ + } while (0) } // namespace api } // namespace cvc4 #endif diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 84c95c9a1..4ccff9930 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3988,9 +3988,9 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, CVC4_API_TRY_CATCH_END; } -std::ostream& operator<<(std::ostream& out, const Grammar& g) +std::ostream& operator<<(std::ostream& out, const Grammar& grammar) { - return out << g.toString(); + return out << grammar.toString(); } /* -------------------------------------------------------------------------- */ @@ -4084,7 +4084,7 @@ void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const template Term Solver::mkValHelper(T t) const { - NodeManagerScope scope(getNodeManager()); + //////// all checks before this line Node res = getNodeManager()->mkConst(t); (void)res.getType(true); /* kick off type checking */ return Term(this, res); @@ -4092,6 +4092,7 @@ Term Solver::mkValHelper(T t) const Term Solver::mkRealFromStrHelper(const std::string& s) const { + //////// all checks before this line try { CVC4::Rational r = s.find('/') != std::string::npos @@ -4101,6 +4102,8 @@ Term Solver::mkRealFromStrHelper(const std::string& s) const } catch (const std::invalid_argument& e) { + /* Catch to throw with a more meaningful error message. To be caught in + * enclosing CVC4_API_TRY_CATCH_* block to throw CVC4ApiException. */ std::stringstream message; message << "Cannot construct Real or Int from string argument '" << s << "'" << std::endl; @@ -4110,12 +4113,9 @@ Term Solver::mkRealFromStrHelper(const std::string& s) const Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const { - CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; - + //////// all checks before this line return mkValHelper(CVC4::BitVector(size, val)); - //////// - CVC4_API_TRY_CATCH_END; } Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const @@ -4123,7 +4123,7 @@ Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; - + //////// all checks before this line return mkValHelper(CVC4::BitVector(s, base)); } @@ -4134,6 +4134,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; + //////// all checks before this line Integer val(s, base); @@ -4162,6 +4163,7 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const uint32_t val = static_cast(std::stoul(s, 0, 16)); CVC4_API_CHECK(val < String::num_codes()) << "Not a valid code point for hexadecimal character " << s; + //////// all checks before this line std::vector cpts; cpts.push_back(val); return mkValHelper(CVC4::String(cpts)); @@ -4170,6 +4172,7 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks + //////// all checks before this line Node value = d_smtEngine->getValue(*term.d_node); Term res = Term(this, value); // May need to wrap in real cast so that user know this is a real. @@ -4184,6 +4187,7 @@ Term Solver::getValueHelper(const Term& term) const Sort Solver::mkTupleSortHelper(const std::vector& sorts) const { // Note: Sorts are checked in the caller to avoid double checks + //////// all checks before this line std::vector typeNodes = Sort::sortVectorToTypeNodes(sorts); return Sort(this, getNodeManager()->mkTupleType(typeNodes)); } @@ -4193,7 +4197,7 @@ Term Solver::mkTermFromKind(Kind kind) const CVC4_API_KIND_CHECK_EXPECTED( kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; - + //////// all checks before this line Node res; if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { @@ -4213,21 +4217,11 @@ Term Solver::mkTermFromKind(Kind kind) const 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(), "child term", children, i) - << "non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == children[i].d_solver, "child term", children, i) - << "a child term associated to this solver object"; - } + // Note: Kind and children are checked in the caller to avoid double checks + //////// all checks before this line std::vector echildren = Term::termVectorToNodes(children); CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)) - << "Not a defined internal kind : " << k << " " << kind; - Node res; if (echildren.size() > 2) { @@ -4308,24 +4302,15 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const Term Solver::mkTermHelper(const Op& op, const std::vector& children) const { - CVC4_API_SOLVER_CHECK_OP(op); + // Note: Op and children are checked in the caller to avoid double checks + checkMkTerm(op.d_kind, children.size()); + //////// all checks before this line if (!op.isIndexedHelper()) { return mkTermHelper(op.d_kind, children); } - for (size_t i = 0, size = children.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !children[i].isNull(), "child term", children, i) - << "non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == children[i].d_solver, "child term", children, i) - << "child term associated to this solver object"; - } - checkMkTerm(op.d_kind, children.size()); - const CVC4::Kind int_kind = extToIntKind(op.d_kind); std::vector echildren = Term::termVectorToNodes(children); @@ -4342,30 +4327,15 @@ std::vector Solver::mkDatatypeSortsInternal( const std::vector& dtypedecls, const std::set& unresolvedSorts) const { + // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid + // double checks + //////// all checks before this line + std::vector datatypes; 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) - << "a datatype declaration associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0, - "datatype declaration", - dtypedecls, - i) - << "a datatype declaration with at least one constructor"; datatypes.push_back(dtypedecls[i].getDatatype()); } - size_t i = 0; - for (auto& sort : unresolvedSorts) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sort.isNull(), "unresolved sort", unresolvedSorts, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sort.d_solver, "unresolved sort", unresolvedSorts, i) - << "an unresolved sort associated to this solver object"; - i += 1; - } std::set utypes = Sort::sortSetToTypeNodes(unresolvedSorts); std::vector dtypes = @@ -4378,35 +4348,23 @@ Term Solver::synthFunHelper(const std::string& symbol, const std::vector& boundVars, const Sort& sort, bool isInv, - Grammar* g) const + Grammar* grammar) const { - CVC4_API_ARG_CHECK_NOT_NULL(sort); - + // Note: boundVars, sort and grammar are checked in the caller to avoid + // double checks. std::vector varTypes; - for (size_t i = 0, n = boundVars.size(); i < n; ++i) + for (const auto& bv : boundVars) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == boundVars[i].d_solver, "bound variable", boundVars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "bound variable", boundVars, i) - << "a non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - boundVars, - i) - << "a bound variable"; - varTypes.push_back(boundVars[i].d_node->getType()); - } - CVC4_API_SOLVER_CHECK_SORT(sort); - - if (g != nullptr) - { - CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType() == *sort.d_type) - << "Invalid Start symbol for Grammar g, Expected Start's sort to be " - << *sort.d_type << " but found " << g->d_ntSyms[0].d_node->getType(); + if (grammar) + { + CVC4_API_CHECK(grammar->d_ntSyms[0].d_node->getType() == *sort.d_type) + << "Invalid Start symbol for grammar, Expected Start's sort to be " + << *sort.d_type << " but found " + << grammar->d_ntSyms[0].d_node->getType(); + } + varTypes.push_back(bv.d_node->getType()); } + //////// all checks before this line TypeNode funType = varTypes.empty() ? *sort.d_type : getNodeManager()->mkFunctionType( @@ -4418,7 +4376,10 @@ Term Solver::synthFunHelper(const std::string& symbol, std::vector bvns = Term::termVectorToNodes(boundVars); d_smtEngine->declareSynthFun( - fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); + fun, + grammar == nullptr ? funType : *grammar->resolve().d_type, + isInv, + bvns); return Term(this, fun); } @@ -4429,6 +4390,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const CVC4_API_CHECK(term.getSort() == sort || (term.getSort().isInteger() && sort.isReal())) << "Expected conversion from Int to Real"; + //////// all checks before this line Sort t = term.getSort(); if (term.getSort() == sort) @@ -4460,6 +4422,8 @@ Term Solver::ensureRealSort(const Term& t) const CVC4_API_ARG_CHECK_EXPECTED( t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), " an integer or real term"); + // Note: Term is checked in the caller to avoid double checks + //////// all checks before this line if (t.getSort() == getIntegerSort()) { Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node); @@ -4470,6 +4434,7 @@ Term Solver::ensureRealSort(const Term& t) const bool Solver::isValidInteger(const std::string& s) const { + //////// all checks before this line if (s.length() == 0) { // string should not be empty @@ -4533,7 +4498,11 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const bool Solver::supportsFloatingPoint() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Configuration::isBuiltWithSymFPU(); + //////// + CVC4_API_TRY_CATCH_END; } /* Sorts Handling */ @@ -4541,7 +4510,9 @@ bool Solver::supportsFloatingPoint() const Sort Solver::getNullSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, TypeNode()); //////// CVC4_API_TRY_CATCH_END; @@ -4551,6 +4522,7 @@ Sort Solver::getBooleanSort(void) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->booleanType()); //////// CVC4_API_TRY_CATCH_END; @@ -4560,6 +4532,7 @@ Sort Solver::getIntegerSort(void) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->integerType()); //////// CVC4_API_TRY_CATCH_END; @@ -4569,6 +4542,7 @@ Sort Solver::getRealSort(void) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->realType()); //////// CVC4_API_TRY_CATCH_END; @@ -4578,6 +4552,7 @@ Sort Solver::getRegExpSort(void) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->regExpType()); //////// CVC4_API_TRY_CATCH_END; @@ -4587,6 +4562,7 @@ Sort Solver::getStringSort(void) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->stringType()); //////// CVC4_API_TRY_CATCH_END; @@ -4598,6 +4574,7 @@ Sort Solver::getRoundingModeSort(void) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + //////// all checks before this line return Sort(this, getNodeManager()->roundingModeType()); //////// CVC4_API_TRY_CATCH_END; @@ -4609,13 +4586,9 @@ Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort) - << "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); - + //////// all checks before this line return Sort( this, getNodeManager()->mkArrayType(*indexSort.d_type, *elemSort.d_type)); //////// @@ -4627,7 +4600,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; - + //////// all checks before this line return Sort(this, getNodeManager()->mkBitVectorType(size)); //////// CVC4_API_TRY_CATCH_END; @@ -4641,7 +4614,7 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const << "Expected CVC4 to be compiled with SymFPU support"; CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; - + //////// all checks before this line return Sort(this, getNodeManager()->mkFloatingPointType(exp, sig)); //////// CVC4_API_TRY_CATCH_END; @@ -4651,11 +4624,8 @@ Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const { NodeManagerScope scope(getNodeManager()); CVC4_API_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"; - + CVC4_API_SOLVER_CHECK_DTDECL(dtypedecl); + //////// all checks before this line return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl.d_dtype)); //////// CVC4_API_TRY_CATCH_END; @@ -4665,9 +4635,10 @@ std::vector Solver::mkDatatypeSorts( const std::vector& dtypedecls) const { NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_CHECK_DTDECLS(dtypedecls); CVC4_API_TRY_CATCH_BEGIN; - std::set unresolvedSorts; - return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + //////// all checks before this line + return mkDatatypeSortsInternal(dtypedecls, {}); //////// CVC4_API_TRY_CATCH_END; } @@ -4678,6 +4649,9 @@ std::vector Solver::mkDatatypeSorts( { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_DTDECLS(dtypedecls); + CVC4_API_SOLVER_CHECK_SORTS(unresolvedSorts); + //////// all checks before this line return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); //////// CVC4_API_TRY_CATCH_END; @@ -4687,16 +4661,9 @@ Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const { NodeManagerScope scope(getNodeManager()); CVC4_API_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) - << "first-class sort as codomain sort for function sort"; - Assert(!codomain.isFunction()); /* A function sort is not first-class. */ - + CVC4_API_SOLVER_CHECK_DOMAIN_SORT(domain); + CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(codomain); + //////// all checks before this line return Sort( this, getNodeManager()->mkFunctionType(*domain.d_type, *codomain.d_type)); //////// @@ -4710,25 +4677,9 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; - for (size_t i = 0, size = sorts.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts, i) - << "sort associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts, 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. */ - + CVC4_API_SOLVER_CHECK_DOMAIN_SORTS(sorts); + CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(codomain); + //////// all checks before this line std::vector argTypes = Sort::sortVectorToTypeNodes(sorts); return Sort(this, getNodeManager()->mkFunctionType(argTypes, *codomain.d_type)); @@ -4740,6 +4691,7 @@ Sort Solver::mkParamSort(const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort( this, getNodeManager()->mkSort(symbol, NodeManager::SORT_FLAG_PLACEHOLDER)); @@ -4753,21 +4705,11 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; - for (size_t i = 0, size = sorts.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts, i) - << "sort associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts, i) - << "first-class sort as parameter sort for predicate sort"; - } - std::vector types = Sort::sortVectorToTypeNodes(sorts); - - return Sort(this, getNodeManager()->mkPredicateType(types)); + CVC4_API_SOLVER_CHECK_DOMAIN_SORTS(sorts); + //////// all checks before this line + return Sort( + this, + getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts))); //////// CVC4_API_TRY_CATCH_END; } @@ -4778,19 +4720,17 @@ Sort Solver::mkRecordSort( NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; std::vector> f; - size_t i = 0; - for (const auto& p : fields) + for (size_t i = 0, size = fields.size(); i < size; ++i) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !p.second.isNull(), "parameter sort", fields, i) + const auto& p = fields[i]; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!p.second.isNull(), "sort", fields, i) << "non-null sort"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == p.second.d_solver, "parameter sort", fields, i) - << "sort associated to this solver object"; - i += 1; + this == p.second.d_solver, "sort", fields, i) + << "sort associated with this solver object"; f.emplace_back(p.first, *p.second.d_type); } - + //////// all checks before this line return Sort(this, getNodeManager()->mkRecordType(f)); //////// CVC4_API_TRY_CATCH_END; @@ -4800,10 +4740,8 @@ Sort Solver::mkSetSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) - << "non-null element sort"; CVC4_API_SOLVER_CHECK_SORT(elemSort); - + //////// all checks before this line return Sort(this, getNodeManager()->mkSetType(*elemSort.d_type)); //////// CVC4_API_TRY_CATCH_END; @@ -4813,10 +4751,8 @@ Sort Solver::mkBagSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) - << "non-null element sort"; CVC4_API_SOLVER_CHECK_SORT(elemSort); - + //////// all checks before this line return Sort(this, getNodeManager()->mkBagType(*elemSort.d_type)); //////// CVC4_API_TRY_CATCH_END; @@ -4826,10 +4762,8 @@ Sort Solver::mkSequenceSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) - << "non-null element sort"; CVC4_API_SOLVER_CHECK_SORT(elemSort); - + //////// all checks before this line return Sort(this, getNodeManager()->mkSequenceType(*elemSort.d_type)); //////// CVC4_API_TRY_CATCH_END; @@ -4839,6 +4773,7 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Sort(this, getNodeManager()->mkSort(symbol)); //////// CVC4_API_TRY_CATCH_END; @@ -4850,7 +4785,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol, NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; - + //////// all checks before this line return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); //////// CVC4_API_TRY_CATCH_END; @@ -4860,18 +4795,8 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - for (size_t i = 0, size = sorts.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isNull(), "parameter sort", sorts, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "parameter sort", sorts, i) - << "sort associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !sorts[i].isFunctionLike(), "parameter sort", sorts, i) - << "non-function-like sort as parameter sort for tuple sort"; - } + CVC4_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts); + //////// all checks before this line return mkTupleSortHelper(sorts); //////// CVC4_API_TRY_CATCH_END; @@ -4882,7 +4807,9 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const Term Solver::mkTrue(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Term(this, d_nodeMgr->mkConst(true)); //////// CVC4_API_TRY_CATCH_END; @@ -4890,7 +4817,9 @@ Term Solver::mkTrue(void) const Term Solver::mkFalse(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Term(this, d_nodeMgr->mkConst(false)); //////// CVC4_API_TRY_CATCH_END; @@ -4898,7 +4827,9 @@ Term Solver::mkFalse(void) const Term Solver::mkBoolean(bool val) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return Term(this, d_nodeMgr->mkConst(val)); //////// CVC4_API_TRY_CATCH_END; @@ -4906,8 +4837,9 @@ Term Solver::mkBoolean(bool val) const Term Solver::mkPi() const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - + //////// all checks before this line Node res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI); (void)res.getType(true); /* kick off type checking */ @@ -4918,11 +4850,13 @@ Term Solver::mkPi() const Term Solver::mkInteger(const std::string& s) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer "; Term integer = mkRealFromStrHelper(s); CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s) - << " an integer"; + << " a string representing an integer"; + //////// all checks before this line return integer; //////// CVC4_API_TRY_CATCH_END; @@ -4930,7 +4864,9 @@ Term Solver::mkInteger(const std::string& s) const Term Solver::mkInteger(int64_t val) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line Term integer = mkValHelper(CVC4::Rational(val)); Assert(integer.getSort() == getIntegerSort()); return integer; @@ -4940,12 +4876,14 @@ Term Solver::mkInteger(int64_t val) const Term Solver::mkReal(const std::string& s) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP * throws an std::invalid_argument exception. For consistency, we treat it * as invalid. */ CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) << "a string representing a real or rational value."; + //////// all checks before this line Term rational = mkRealFromStrHelper(s); return ensureRealSort(rational); //////// @@ -4954,7 +4892,9 @@ Term Solver::mkReal(const std::string& s) const Term Solver::mkReal(int64_t val) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line Term rational = mkValHelper(CVC4::Rational(val)); return ensureRealSort(rational); //////// @@ -4963,7 +4903,9 @@ Term Solver::mkReal(int64_t val) const Term Solver::mkReal(int64_t num, int64_t den) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line Term rational = mkValHelper(CVC4::Rational(num, den)); return ensureRealSort(rational); //////// @@ -4972,8 +4914,9 @@ Term Solver::mkReal(int64_t num, int64_t den) const Term Solver::mkRegexpEmpty() const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - + //////// all checks before this line Node res = d_nodeMgr->mkNode(CVC4::kind::REGEXP_EMPTY, std::vector()); (void)res.getType(true); /* kick off type checking */ @@ -4984,8 +4927,9 @@ Term Solver::mkRegexpEmpty() const Term Solver::mkRegexpSigma() const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - + //////// all checks before this line Node res = d_nodeMgr->mkNode(CVC4::kind::REGEXP_SIGMA, std::vector()); (void)res.getType(true); /* kick off type checking */ @@ -4994,39 +4938,40 @@ Term Solver::mkRegexpSigma() const CVC4_API_TRY_CATCH_END; } -Term Solver::mkEmptySet(const Sort& s) const +Term Solver::mkEmptySet(const Sort& sort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s) + CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isSet(), sort) << "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)); + CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort) + << "set sort associated with this solver object"; + //////// all checks before this line + return mkValHelper(CVC4::EmptySet(*sort.d_type)); //////// CVC4_API_TRY_CATCH_END; } -Term Solver::mkEmptyBag(const Sort& s) const +Term Solver::mkEmptyBag(const Sort& sort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s) + CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isBag(), sort) << "null sort or bag sort"; - - CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s) - << "bag sort associated to this solver object"; - - return mkValHelper(CVC4::EmptyBag(*s.d_type)); + CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort) + << "bag sort associated with this solver object"; + //////// all checks before this line + return mkValHelper(CVC4::EmptyBag(*sort.d_type)); //////// CVC4_API_TRY_CATCH_END; } Term Solver::mkSepNil(const Sort& sort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); (void)res.getType(true); /* kick off type checking */ @@ -5037,7 +4982,9 @@ Term Solver::mkSepNil(const Sort& sort) const Term Solver::mkString(const std::string& s, bool useEscSequences) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkValHelper(CVC4::String(s, useEscSequences)); //////// CVC4_API_TRY_CATCH_END; @@ -5045,7 +4992,9 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const Term Solver::mkString(const unsigned char c) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkValHelper(CVC4::String(std::string(1, c))); //////// CVC4_API_TRY_CATCH_END; @@ -5053,7 +5002,9 @@ Term Solver::mkString(const unsigned char c) const Term Solver::mkString(const std::vector& s) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkValHelper(CVC4::String(s)); //////// CVC4_API_TRY_CATCH_END; @@ -5061,7 +5012,9 @@ Term Solver::mkString(const std::vector& s) const Term Solver::mkChar(const std::string& s) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkCharFromStrHelper(s); //////// CVC4_API_TRY_CATCH_END; @@ -5069,10 +5022,10 @@ Term Solver::mkChar(const std::string& s) const Term Solver::mkEmptySequence(const Sort& sort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line std::vector seq; Node res = d_nodeMgr->mkConst(Sequence(*sort.d_type, seq)); return Term(this, res); @@ -5082,9 +5035,10 @@ Term Solver::mkEmptySequence(const Sort& sort) const Term Solver::mkUniverseSet(const Sort& sort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); + //////// all checks before this line Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); @@ -5097,7 +5051,9 @@ Term Solver::mkUniverseSet(const Sort& sort) const Term Solver::mkBitVector(uint32_t size, uint64_t val) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkBVFromIntHelper(size, val); //////// CVC4_API_TRY_CATCH_END; @@ -5105,7 +5061,9 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const Term Solver::mkBitVector(const std::string& s, uint32_t base) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkBVFromStrHelper(s, base); //////// CVC4_API_TRY_CATCH_END; @@ -5115,7 +5073,9 @@ Term Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return mkBVFromStrHelper(size, s, base); //////// CVC4_API_TRY_CATCH_END; @@ -5123,15 +5083,15 @@ Term Solver::mkBitVector(uint32_t size, Term Solver::mkConstArray(const Sort& sort, const Term& val) const { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC4_API_ARG_CHECK_NOT_NULL(sort); - CVC4_API_ARG_CHECK_NOT_NULL(val); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_SOLVER_CHECK_TERM(val); - CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; + CVC4_API_ARG_CHECK_EXPECTED(sort.isArray(), sort) << "an array sort"; CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort())) - << "Value does not match element sort."; + << "Value does not match element sort"; + //////// all checks before this line + // handle the special case of (CAST_TO_REAL n) where n is an integer Node n = *val.d_node; if (val.isCastedReal()) @@ -5148,10 +5108,11 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - + //////// all checks before this line return mkValHelper( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); //////// @@ -5160,10 +5121,11 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - + //////// all checks before this line return mkValHelper( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); //////// @@ -5172,10 +5134,11 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - + //////// all checks before this line return mkValHelper( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); //////// @@ -5184,10 +5147,11 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - + //////// all checks before this line return mkValHelper( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); //////// @@ -5196,10 +5160,11 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - + //////// all checks before this line return mkValHelper( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); //////// @@ -5208,9 +5173,11 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const Term Solver::mkRoundingMode(RoundingMode rm) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + //////// all checks before this line return mkValHelper(s_rmodes.at(rm)); //////// CVC4_API_TRY_CATCH_END; @@ -5218,10 +5185,10 @@ Term Solver::mkRoundingMode(RoundingMode rm) const Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line return mkValHelper( CVC4::UninterpretedConstant(*sort.d_type, index)); //////// @@ -5230,12 +5197,14 @@ Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const Term Solver::mkAbstractValue(const std::string& index) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; CVC4::Integer idx(index, 10); CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) << "a string representing an integer > 0"; + //////// all checks before this line return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(idx))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away @@ -5245,9 +5214,10 @@ Term Solver::mkAbstractValue(const std::string& index) const Term Solver::mkAbstractValue(uint64_t index) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; - + //////// all checks before this line return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(Integer(index)))); // do not call getType(), for abstract values, type can not be computed @@ -5258,20 +5228,20 @@ Term Solver::mkAbstractValue(uint64_t index) const Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; + CVC4_API_SOLVER_CHECK_TERM(val); CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; uint32_t bw = exp + sig; 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_node->isConst(), val) << "bit-vector constant"; - + //////// all checks before this line return mkValHelper( CVC4::FloatingPoint(exp, sig, val.d_node->getConst())); //////// @@ -5285,9 +5255,8 @@ Term Solver::mkConst(const Sort& sort, const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line Node res = d_nodeMgr->mkVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ increment_vars_consts_stats(sort, false); @@ -5300,9 +5269,8 @@ Term Solver::mkConst(const Sort& sort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line Node res = d_nodeMgr->mkVar(*sort.d_type); (void)res.getType(true); /* kick off type checking */ increment_vars_consts_stats(sort, false); @@ -5318,9 +5286,8 @@ Term Solver::mkVar(const Sort& sort, const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line Node res = symbol.empty() ? d_nodeMgr->mkBoundVar(*sort.d_type) : d_nodeMgr->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ @@ -5337,7 +5304,11 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( const std::string& name) { NodeManagerScope scope(getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return DatatypeConstructorDecl(this, name); + //////// + CVC4_API_TRY_CATCH_END; } /* Create datatype declarations */ @@ -5347,6 +5318,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return DatatypeDecl(this, name, isCoDatatype); //////// CVC4_API_TRY_CATCH_END; @@ -5358,8 +5330,8 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(param); CVC4_API_SOLVER_CHECK_SORT(param); + //////// all checks before this line return DatatypeDecl(this, name, param, isCoDatatype); //////// CVC4_API_TRY_CATCH_END; @@ -5371,15 +5343,8 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - for (size_t i = 0, size = params.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !params[i].isNull(), "parameter sort", params, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == params[i].d_solver, "parameter sort", params, i) - << "sort associated to this solver object"; - } + CVC4_API_SOLVER_CHECK_SORTS(params); + //////// all checks before this line return DatatypeDecl(this, name, params, isCoDatatype); //////// CVC4_API_TRY_CATCH_END; @@ -5392,6 +5357,8 @@ Term Solver::mkTerm(Kind kind) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + //////// all checks before this line return mkTermFromKind(kind); //////// CVC4_API_TRY_CATCH_END; @@ -5401,6 +5368,9 @@ Term Solver::mkTerm(Kind kind, const Term& child) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + CVC4_API_SOLVER_CHECK_TERM(child); + //////// all checks before this line return mkTermHelper(kind, std::vector{child}); //////// CVC4_API_TRY_CATCH_END; @@ -5410,6 +5380,10 @@ Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); + //////// all checks before this line return mkTermHelper(kind, std::vector{child1, child2}); //////// CVC4_API_TRY_CATCH_END; @@ -5422,6 +5396,11 @@ Term Solver::mkTerm(Kind kind, { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); + CVC4_API_SOLVER_CHECK_TERM(child3); + //////// all checks before this line // need to use internal term call to check e.g. associative construction return mkTermHelper(kind, std::vector{child1, child2, child3}); //////// @@ -5432,6 +5411,9 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + CVC4_API_SOLVER_CHECK_TERMS(children); + //////// all checks before this line return mkTermHelper(kind, children); //////// CVC4_API_TRY_CATCH_END; @@ -5443,6 +5425,7 @@ Term Solver::mkTerm(const Op& op) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_OP(op); checkMkTerm(op.d_kind, 0); + //////// all checks before this line if (!op.isIndexedHelper()) { @@ -5462,6 +5445,9 @@ Term Solver::mkTerm(const Op& op, const Term& child) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); + CVC4_API_SOLVER_CHECK_TERM(child); + //////// all checks before this line return mkTermHelper(op, std::vector{child}); //////// CVC4_API_TRY_CATCH_END; @@ -5471,6 +5457,10 @@ Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); + //////// all checks before this line return mkTermHelper(op, std::vector{child1, child2}); //////// CVC4_API_TRY_CATCH_END; @@ -5483,6 +5473,11 @@ Term Solver::mkTerm(const Op& op, { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); + CVC4_API_SOLVER_CHECK_TERM(child1); + CVC4_API_SOLVER_CHECK_TERM(child2); + CVC4_API_SOLVER_CHECK_TERM(child3); + //////// all checks before this line return mkTermHelper(op, std::vector{child1, child2, child3}); //////// CVC4_API_TRY_CATCH_END; @@ -5492,6 +5487,9 @@ Term Solver::mkTerm(const Op& op, const std::vector& children) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_OP(op); + CVC4_API_SOLVER_CHECK_TERMS(children); + //////// all checks before this line return mkTermHelper(op, children); //////// CVC4_API_TRY_CATCH_END; @@ -5504,19 +5502,12 @@ Term Solver::mkTuple(const std::vector& sorts, CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; + CVC4_API_SOLVER_CHECK_SORTS(sorts); + CVC4_API_SOLVER_CHECK_TERMS(terms); + //////// all checks before this line std::vector args; for (size_t i = 0, size = sorts.size(); i < size; i++) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!sorts[i].isNull(), "sort", sorts, i) - << "non-null sort"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i) - << "non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "child term", terms, i) - << "child term associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == sorts[i].d_solver, "child sort", sorts, i) - << "child sort associated to this solver object"; args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); } @@ -5538,18 +5529,23 @@ Term Solver::mkTuple(const std::vector& sorts, Op Solver::mkOp(Kind kind) const { CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end()) << "Expected a kind for a non-indexed operator."; + //////// all checks before this line return Op(this, kind); + //////// CVC4_API_TRY_CATCH_END } Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE), kind) << "RECORD_UPDATE or DIVISIBLE"; + //////// all checks before this line Op res; if (kind == RECORD_UPDATE) { @@ -5578,7 +5574,7 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); - + //////// all checks before this line Op res; switch (kind) { @@ -5670,6 +5666,7 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); + //////// all checks before this line Op res; switch (kind) @@ -5743,6 +5740,7 @@ Op Solver::mkOp(Kind kind, const std::vector& args) const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); + //////// all checks before this line Op res; switch (kind) @@ -5773,11 +5771,10 @@ Op Solver::mkOp(Kind kind, const std::vector& args) const Term Solver::simplify(const Term& term) { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - + //////// all checks before this line return Term(this, d_smtEngine->simplify(*term.d_node)); //////// CVC4_API_TRY_CATCH_END; @@ -5785,15 +5782,14 @@ Term Solver::simplify(const Term& term) Result Solver::checkEntailed(const Term& term) const { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_smtEngine->isQueryMade() || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; - CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); - + //////// all checks before this line CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node); return Result(r); //////// @@ -5808,15 +5804,9 @@ Result Solver::checkEntailed(const std::vector& terms) const || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; - for (const Term& term : terms) - { - CVC4_API_SOLVER_CHECK_TERM(term); - CVC4_API_ARG_CHECK_NOT_NULL(term); - } - - std::vector exprs = Term::termVectorToNodes(terms); - CVC4::Result r = d_smtEngine->checkEntailed(exprs); - return Result(r); + CVC4_API_SOLVER_CHECK_TERMS(terms); + //////// all checks before this line + return d_smtEngine->checkEntailed(Term::termVectorToNodes(terms)); //////// CVC4_API_TRY_CATCH_END; } @@ -5831,7 +5821,8 @@ void Solver::assertFormula(const Term& term) const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort()); + //////// all checks before this line d_smtEngine->assertFormula(*term.d_node); //////// CVC4_API_TRY_CATCH_END; @@ -5848,6 +5839,7 @@ Result Solver::checkSat(void) const || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; + //////// all checks before this line CVC4::Result r = d_smtEngine->checkSat(); return Result(r); //////// @@ -5865,7 +5857,8 @@ Result Solver::checkSatAssuming(const Term& assumption) const || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; - CVC4_API_SOLVER_CHECK_TERM(assumption); + CVC4_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); + //////// all checks before this line CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node); return Result(r); //////// @@ -5883,10 +5876,11 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; + CVC4_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); + //////// all checks before this line for (const Term& term : assumptions) { CVC4_API_SOLVER_CHECK_TERM(term); - CVC4_API_ARG_CHECK_NOT_NULL(term); } std::vector eassumptions = Term::termVectorToNodes(assumptions); CVC4::Result r = d_smtEngine->checkSat(eassumptions); @@ -5905,12 +5899,11 @@ Sort Solver::declareDatatype( CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors) << "a datatype declaration with at least one constructor"; + CVC4_API_SOLVER_CHECK_DTCTORDECLS(ctors); + //////// all checks before this line DatatypeDecl dtdecl(this, symbol); for (size_t i = 0, size = ctors.size(); i < size; i++) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == ctors[i].d_solver, "datatype constructor declaration", ctors, i) - << "datatype constructor declaration associated to this solver object"; dtdecl.addConstructor(ctors[i]); } return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl.d_dtype)); @@ -5926,19 +5919,10 @@ Term Solver::declareFun(const std::string& symbol, const Sort& sort) const { CVC4_API_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) - << "parameter sort associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - sorts[i].isFirstClass(), "parameter sort", sorts, 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. */ + CVC4_API_SOLVER_CHECK_DOMAIN_SORTS(sorts); + CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort); + //////// all checks before this line + TypeNode type = *sort.d_type; if (!sorts.empty()) { @@ -5956,6 +5940,7 @@ Term Solver::declareFun(const std::string& symbol, Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line if (arity == 0) { return Sort(this, getNodeManager()->mkSort(symbol)); @@ -5975,41 +5960,31 @@ Term Solver::defineFun(const std::string& symbol, bool global) const { CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) - << "first-class sort as codomain sort for function sort"; - std::vector domain_types; - for (size_t i = 0, size = bound_vars.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - bound_vars, - i) - << "a bound variable"; - CVC4::TypeNode t = bound_vars[i].d_node->getType(); - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - t.isFirstClass(), "sort of parameter", bound_vars, i) - << "first-class sort of parameter of defined function"; - domain_types.push_back(t); - } - CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort); CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; - NodeManager* nm = getNodeManager(); - TypeNode type = *sort.d_type; - if (!domain_types.empty()) + + std::vector domain_sorts; + for (const auto& bv : bound_vars) { - type = nm->mkFunctionType(domain_types, type); + domain_sorts.push_back(bv.getSort()); } - Node fun = d_nodeMgr->mkVar(symbol, type); - std::vector ebound_vars = Term::termVectorToNodes(bound_vars); - d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global); - return Term(this, fun); + Sort fun_sort = + domain_sorts.empty() + ? sort + : Sort(this, + getNodeManager()->mkFunctionType( + Sort::sortVectorToTypeNodes(domain_sorts), *sort.d_type)); + Term fun = mkConst(fun_sort, symbol); + + CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); + //////// all checks before this line + + d_smtEngine->defineFunction( + *fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global); + return fun; //////// CVC4_API_TRY_CATCH_END; } @@ -6020,31 +5995,12 @@ Term Solver::defineFun(const Term& fun, bool global) const { CVC4_API_TRY_CATCH_BEGIN; - + CVC4_API_SOLVER_CHECK_TERM(fun); + CVC4_API_SOLVER_CHECK_TERM(term); if (fun.getSort().isFunction()) { std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); - size_t size = bound_vars.size(); - CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) - << "'" << domain_sorts.size() << "'"; - for (size_t i = 0; i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - bound_vars, - i) - << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - domain_sorts[i] == bound_vars[i].getSort(), - "sort of parameter", - bound_vars, - i) - << "'" << domain_sorts[i] << "'"; - } + CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); Sort codomain = fun.getSort().getFunctionCodomainSort(); CVC4_API_CHECK(codomain == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" @@ -6052,12 +6008,11 @@ Term Solver::defineFun(const Term& fun, } else { + CVC4_API_SOLVER_CHECK_BOUND_VARS(bound_vars); CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun) << "function or nullary symbol"; } - - CVC4_API_SOLVER_CHECK_TERM(term); - + //////// all checks before this line std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); return fun; @@ -6084,42 +6039,32 @@ Term Solver::defineFunRec(const std::string& symbol, << "recursive function definitions require a logic with uninterpreted " "functions"; - CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) - << "first-class sort as function codomain sort"; - Assert(!sort.isFunction()); /* A function sort is not first-class. */ - std::vector domain_types; - for (size_t i = 0, size = bound_vars.size(); i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - bound_vars, - i) - << "a bound variable"; - CVC4::TypeNode t = bound_vars[i].d_node->getType(); - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - t.isFirstClass(), "sort of parameter", bound_vars, i) - << "first-class sort of parameter of defined function"; - domain_types.push_back(t); - } - CVC4_API_SOLVER_CHECK_SORT(sort); + CVC4_API_SOLVER_CHECK_TERM(term); + CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; - CVC4_API_SOLVER_CHECK_TERM(term); - NodeManager* nm = getNodeManager(); - TypeNode type = *sort.d_type; - if (!domain_types.empty()) + + std::vector domain_sorts; + for (const auto& bv : bound_vars) { - type = nm->mkFunctionType(domain_types, type); + domain_sorts.push_back(bv.getSort()); } - Node fun = d_nodeMgr->mkVar(symbol, type); - std::vector ebound_vars = Term::termVectorToNodes(bound_vars); - d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_node, global); - return Term(this, fun); + Sort fun_sort = + domain_sorts.empty() + ? sort + : Sort(this, + getNodeManager()->mkFunctionType( + Sort::sortVectorToTypeNodes(domain_sorts), *sort.d_type)); + Term fun = mkConst(fun_sort, symbol); + + CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); + //////// all checks before this line + + d_smtEngine->defineFunctionRec( + *fun.d_node, Term::termVectorToNodes(bound_vars), *term.d_node, global); + + return fun; //////// CVC4_API_TRY_CATCH_END; } @@ -6140,30 +6085,11 @@ Term Solver::defineFunRec(const Term& fun, "functions"; CVC4_API_SOLVER_CHECK_TERM(fun); + CVC4_API_SOLVER_CHECK_TERM(term); if (fun.getSort().isFunction()) { std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); - size_t size = bound_vars.size(); - CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) - << "'" << domain_sorts.size() << "'"; - for (size_t i = 0; i < size; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bound_vars[i].d_solver, "bound variable", bound_vars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - bound_vars, - i) - << "a bound variable"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - domain_sorts[i] == bound_vars[i].getSort(), - "sort of parameter", - bound_vars, - i) - << "'" << domain_sorts[i] << "'"; - } + CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); Sort codomain = fun.getSort().getFunctionCodomainSort(); CVC4_API_CHECK(codomain == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" @@ -6171,11 +6097,12 @@ Term Solver::defineFunRec(const Term& fun, } else { + CVC4_API_SOLVER_CHECK_BOUND_VARS(bound_vars); CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun) << "function or nullary symbol"; } + //////// all checks before this line - CVC4_API_SOLVER_CHECK_TERM(term); std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( *fun.d_node, ebound_vars, *term.d_node, global); @@ -6201,10 +6128,15 @@ void Solver::defineFunsRec(const std::vector& funs, d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF)) << "recursive function definitions require a logic with uninterpreted " "functions"; + CVC4_API_SOLVER_CHECK_TERMS(funs); + CVC4_API_SOLVER_CHECK_TERMS(terms); size_t funs_size = funs.size(); CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars) << "'" << funs_size << "'"; + CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == terms.size(), terms) + << "'" << funs_size << "'"; + for (size_t j = 0; j < funs_size; ++j) { const Term& fun = funs[j]; @@ -6213,50 +6145,28 @@ void Solver::defineFunsRec(const std::vector& funs, CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == fun.d_solver, "function", funs, j) - << "function associated to this solver object"; + << "function associated with this solver object"; CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( this == term.d_solver, "term", terms, j) - << "term associated to this solver object"; + << "term associated with this solver object"; if (fun.getSort().isFunction()) { std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); - size_t size = bvars.size(); - CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars) - << "'" << domain_sorts.size() << "'"; - for (size_t i = 0; i < size; ++i) - { - for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == bvars[k].d_solver, "bound variable", bvars, k) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - bvars, - k) - << "a bound variable"; - } - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - domain_sorts[i] == bvars[i].getSort(), - "sort of parameter", - bvars, - i) - << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j - << "]"; - } + CVC4_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bvars, domain_sorts); Sort codomain = fun.getSort().getFunctionCodomainSort(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - codomain == term.getSort(), "sort of function body", term, j) + codomain == term.getSort(), "sort of function body", terms, j) << "'" << codomain << "'"; } else { + CVC4_API_SOLVER_CHECK_BOUND_VARS(bvars); CVC4_API_ARG_CHECK_EXPECTED(bvars.size() == 0, fun) << "function or nullary symbol"; } } + //////// all checks before this line std::vector efuns = Term::termVectorToNodes(funs); std::vector> ebound_vars; for (const auto& v : bound_vars) @@ -6283,6 +6193,7 @@ void Solver::echo(std::ostream& out, const std::string& str) const std::vector Solver::getAssertions(void) const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line std::vector assertions = d_smtEngine->getAssertions(); /* Can not use * return std::vector(assertions.begin(), assertions.end()); @@ -6305,7 +6216,7 @@ std::string Solver::getInfo(const std::string& flag) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; - + //////// all checks before this line return d_smtEngine->getInfo(flag).toString(); //////// CVC4_API_TRY_CATCH_END; @@ -6317,6 +6228,7 @@ std::string Solver::getInfo(const std::string& flag) const std::string Solver::getOption(const std::string& option) const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line SExpr res = d_smtEngine->getOption(option); return res.toString(); //////// @@ -6338,6 +6250,7 @@ std::vector Solver::getUnsatAssumptions(void) const "(try --produce-unsat-assumptions)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; + //////// all checks before this line std::vector uassumptions = d_smtEngine->getUnsatAssumptions(); /* Can not use @@ -6365,6 +6278,7 @@ std::vector Solver::getUnsatCore(void) const "(try --produce-unsat-cores)"; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; + //////// all checks before this line UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use * return std::vector(core.begin(), core.end()); @@ -6386,6 +6300,7 @@ Term Solver::getValue(const Term& term) const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); + //////// all checks before this line return getValueHelper(term); //////// CVC4_API_TRY_CATCH_END; @@ -6403,12 +6318,12 @@ std::vector Solver::getValue(const std::vector& terms) const "(try --produce-models)"; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) << "Cannot get value unless after a SAT or unknown response."; + CVC4_API_SOLVER_CHECK_TERMS(terms); + //////// all checks before this line + std::vector res; for (size_t i = 0, n = terms.size(); i < n; ++i) { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "term", terms, i) - << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ res.push_back(getValueHelper(terms[i])); } @@ -6419,10 +6334,10 @@ std::vector Solver::getValue(const std::vector& terms) const Term Solver::getQuantifierElimination(const Term& q) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(q); CVC4_API_SOLVER_CHECK_TERM(q); - NodeManagerScope scope(getNodeManager()); + //////// all checks before this line return Term(this, d_smtEngine->getQuantifierElimination(q.getNode(), true, true)); //////// @@ -6431,10 +6346,10 @@ Term Solver::getQuantifierElimination(const Term& q) const Term Solver::getQuantifierEliminationDisjunct(const Term& q) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(q); CVC4_API_SOLVER_CHECK_TERM(q); - NodeManagerScope scope(getNodeManager()); + //////// all checks before this line return Term( this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); //////// @@ -6451,6 +6366,7 @@ void Solver::declareSeparationHeap(const Sort& locSort, d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; + //////// all checks before this line d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); //////// CVC4_API_TRY_CATCH_END; @@ -6469,6 +6385,7 @@ Term Solver::getSeparationHeap() const "(try --produce-models)"; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) << "Can only get separtion heap term after sat or unknown response."; + //////// all checks before this line return Term(this, d_smtEngine->getSepHeapExpr()); //////// CVC4_API_TRY_CATCH_END; @@ -6487,6 +6404,7 @@ Term Solver::getSeparationNilTerm() const "(try --produce-models)"; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) << "Can only get separtion nil term after sat or unknown response."; + //////// all checks before this line return Term(this, d_smtEngine->getSepNilExpr()); //////// CVC4_API_TRY_CATCH_END; @@ -6503,7 +6421,7 @@ void Solver::pop(uint32_t nscopes) const << "Cannot pop when not solving incrementally (use --incremental)"; CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; - + //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) { d_smtEngine->pop(); @@ -6517,6 +6435,7 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(conj); + //////// all checks before this line Node result; bool success = d_smtEngine->getInterpol(*conj.d_node, result); if (success) @@ -6528,14 +6447,17 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const CVC4_API_TRY_CATCH_END; } -bool Solver::getInterpolant(const Term& conj, Grammar& g, Term& output) const +bool Solver::getInterpolant(const Term& conj, + Grammar& grammar, + Term& output) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(conj); + //////// all checks before this line Node result; bool success = - d_smtEngine->getInterpol(*conj.d_node, *g.resolve().d_type, result); + d_smtEngine->getInterpol(*conj.d_node, *grammar.resolve().d_type, result); if (success) { output = Term(this, result); @@ -6550,6 +6472,7 @@ bool Solver::getAbduct(const Term& conj, Term& output) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(conj); + //////// all checks before this line Node result; bool success = d_smtEngine->getAbduct(*conj.d_node, result); if (success) @@ -6561,14 +6484,15 @@ bool Solver::getAbduct(const Term& conj, Term& output) const CVC4_API_TRY_CATCH_END; } -bool Solver::getAbduct(const Term& conj, Grammar& g, Term& output) const +bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(conj); + //////// all checks before this line Node result; bool success = - d_smtEngine->getAbduct(*conj.d_node, *g.resolve().d_type, result); + d_smtEngine->getAbduct(*conj.d_node, *grammar.resolve().d_type, result); if (success) { output = Term(this, result); @@ -6580,13 +6504,14 @@ bool Solver::getAbduct(const Term& conj, Grammar& g, Term& output) const void Solver::blockModel() const { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) << "Can only block model after sat or unknown response."; + //////// all checks before this line d_smtEngine->blockModel(); //////// CVC4_API_TRY_CATCH_END; @@ -6594,6 +6519,7 @@ void Solver::blockModel() const void Solver::blockModelValues(const std::vector& terms) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " @@ -6602,15 +6528,8 @@ void Solver::blockModelValues(const std::vector& terms) const << "Can only block model values after sat or unknown response."; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; - for (size_t i = 0, tsize = terms.size(); i < tsize; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i) - << "a non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "term", terms, i) - << "a term associated to this solver object"; - } - NodeManagerScope scope(getNodeManager()); + CVC4_API_SOLVER_CHECK_TERMS(terms); + //////// all checks before this line d_smtEngine->blockModelValues(Term::termVectorToNodes(terms)); //////// CVC4_API_TRY_CATCH_END; @@ -6618,8 +6537,9 @@ void Solver::blockModelValues(const std::vector& terms) const void Solver::printInstantiations(std::ostream& out) const { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line d_smtEngine->printInstantiations(out); //////// CVC4_API_TRY_CATCH_END; @@ -6630,11 +6550,11 @@ void Solver::printInstantiations(std::ostream& out) const */ void Solver::push(uint32_t nscopes) const { - CVC4_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot push when not solving incrementally (use --incremental)"; - + //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) { d_smtEngine->push(); @@ -6649,6 +6569,7 @@ void Solver::push(uint32_t nscopes) const void Solver::resetAssertions(void) const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line d_smtEngine->resetAssertions(); //////// CVC4_API_TRY_CATCH_END; @@ -6677,7 +6598,7 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const || value == "unsat" || value == "unknown", value) << "'sat', 'unsat' or 'unknown'"; - + //////// all checks before this line d_smtEngine->setInfo(keyword, value); //////// CVC4_API_TRY_CATCH_END; @@ -6692,6 +6613,7 @@ void Solver::setLogic(const std::string& logic) const CVC4_API_CHECK(!d_smtEngine->isFullyInited()) << "Invalid call to 'setLogic', solver is already fully initialized"; CVC4::LogicInfo logic_info(logic); + //////// all checks before this line d_smtEngine->setLogic(logic_info); //////// CVC4_API_TRY_CATCH_END; @@ -6706,6 +6628,7 @@ void Solver::setOption(const std::string& option, CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_smtEngine->isFullyInited()) << "Invalid call to 'setOption', solver is already fully initialized"; + //////// all checks before this line d_smtEngine->setOption(option, value); //////// CVC4_API_TRY_CATCH_END; @@ -6714,9 +6637,8 @@ void Solver::setOption(const std::string& option, Term Solver::mkSygusVar(const Sort& sort, const std::string& symbol) const { CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(sort); CVC4_API_SOLVER_CHECK_SORT(sort); - + //////// all checks before this line Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ @@ -6733,39 +6655,9 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) << "a non-empty vector"; - - for (size_t i = 0, n = boundVars.size(); i < n; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == boundVars[i].d_solver, "bound variable", boundVars, i) - << "bound variable associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !boundVars[i].isNull(), "bound variable", boundVars, i) - << "a non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "bound variable", - boundVars, - i) - << "a bound variable"; - } - - for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == ntSymbols[i].d_solver, "non-terminal", ntSymbols, i) - << "term associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !ntSymbols[i].isNull(), "non-terminal", ntSymbols, i) - << "a non-null term"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, - "non-terminal", - ntSymbols, - i) - << "a bound variable"; - } - + CVC4_API_SOLVER_CHECK_BOUND_VARS(boundVars); + CVC4_API_SOLVER_CHECK_BOUND_VARS(ntSymbols); + //////// all checks before this line return Grammar(this, boundVars, ntSymbols); //////// CVC4_API_TRY_CATCH_END; @@ -6776,6 +6668,9 @@ Term Solver::synthFun(const std::string& symbol, const Sort& sort) const { CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_BOUND_VARS(boundVars); + CVC4_API_SOLVER_CHECK_SORT(sort); + //////// all checks before this line return synthFunHelper(symbol, boundVars, sort); //////// CVC4_API_TRY_CATCH_END; @@ -6784,10 +6679,13 @@ Term Solver::synthFun(const std::string& symbol, Term Solver::synthFun(const std::string& symbol, const std::vector& boundVars, Sort sort, - Grammar& g) const + Grammar& grammar) const { CVC4_API_TRY_CATCH_BEGIN; - return synthFunHelper(symbol, boundVars, sort, false, &g); + CVC4_API_SOLVER_CHECK_BOUND_VARS(boundVars); + CVC4_API_SOLVER_CHECK_SORT(sort); + //////// all checks before this line + return synthFunHelper(symbol, boundVars, sort, false, &grammar); //////// CVC4_API_TRY_CATCH_END; } @@ -6796,6 +6694,8 @@ Term Solver::synthInv(const std::string& symbol, const std::vector& boundVars) const { CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_BOUND_VARS(boundVars); + //////// all checks before this line return synthFunHelper( symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true); //////// @@ -6804,11 +6704,16 @@ Term Solver::synthInv(const std::string& symbol, Term Solver::synthInv(const std::string& symbol, const std::vector& boundVars, - Grammar& g) const + Grammar& grammar) const { CVC4_API_TRY_CATCH_BEGIN; - return synthFunHelper( - symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true, &g); + CVC4_API_SOLVER_CHECK_BOUND_VARS(boundVars); + //////// all checks before this line + return synthFunHelper(symbol, + boundVars, + Sort(this, getNodeManager()->booleanType()), + true, + &grammar); //////// CVC4_API_TRY_CATCH_END; } @@ -6817,12 +6722,11 @@ void Solver::addSygusConstraint(const Term& term) const { NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_EXPECTED( term.d_node->getType() == getNodeManager()->booleanType(), term) << "boolean term"; - + //////// all checks before this line d_smtEngine->assertSygusConstraint(*term.d_node); //////// CVC4_API_TRY_CATCH_END; @@ -6834,13 +6738,9 @@ void Solver::addSygusInvConstraint(Term inv, Term post) const { CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(inv); CVC4_API_SOLVER_CHECK_TERM(inv); - CVC4_API_ARG_CHECK_NOT_NULL(pre); CVC4_API_SOLVER_CHECK_TERM(pre); - CVC4_API_ARG_CHECK_NOT_NULL(trans); CVC4_API_SOLVER_CHECK_TERM(trans); - CVC4_API_ARG_CHECK_NOT_NULL(post); CVC4_API_SOLVER_CHECK_TERM(post); CVC4_API_ARG_CHECK_EXPECTED(inv.d_node->getType().isFunction(), inv) @@ -6856,6 +6756,7 @@ void Solver::addSygusInvConstraint(Term inv, CVC4_API_CHECK(post.d_node->getType() == invType) << "Expected inv and post to have the same sort"; + //////// all checks before this line const std::vector& invArgTypes = invType.getArgTypes(); @@ -6883,6 +6784,7 @@ void Solver::addSygusInvConstraint(Term inv, Result Solver::checkSynth() const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line return d_smtEngine->checkSynth(); //////// CVC4_API_TRY_CATCH_END; @@ -6891,7 +6793,6 @@ Result Solver::checkSynth() const Term Solver::getSynthSolution(Term term) const { CVC4_API_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULL(term); CVC4_API_SOLVER_CHECK_TERM(term); std::map map; @@ -6902,7 +6803,7 @@ Term Solver::getSynthSolution(Term term) const std::map::const_iterator it = map.find(*term.d_node); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; - + //////// all checks before this line return Term(this, it->second); //////// CVC4_API_TRY_CATCH_END; @@ -6913,21 +6814,13 @@ std::vector Solver::getSynthSolutions( { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector"; - - for (size_t i = 0, n = terms.size(); i < n; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - this == terms[i].d_solver, "parameter term", terms, i) - << "parameter term associated to this solver object"; - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !terms[i].isNull(), "parameter term", terms, i) - << "non-null term"; - } + CVC4_API_SOLVER_CHECK_TERMS(terms); std::map map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; + //////// all checks before this line std::vector synthSolution; synthSolution.reserve(terms.size()); @@ -6951,6 +6844,7 @@ std::vector Solver::getSynthSolutions( void Solver::printSynthSolution(std::ostream& out) const { CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line d_smtEngine->printSynthSolution(out); //////// CVC4_API_TRY_CATCH_END; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 7e169a6c8..2d2b8a2e5 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2786,17 +2786,17 @@ class CVC4_EXPORT Solver /** * Create a constant representing an empty set of the given sort. - * @param s the sort of the set elements. + * @param sort the sort of the set elements. * @return the empty set constant */ - Term mkEmptySet(const Sort& s) const; + Term mkEmptySet(const Sort& sort) const; /** * Create a constant representing an empty bag of the given sort. - * @param s the sort of the bag elements. + * @param sort the sort of the bag elements. * @return the empty bag constant */ - Term mkEmptyBag(const Sort& s) const; + Term mkEmptyBag(const Sort& sort) const; /** * Create a separation logic nil term. @@ -2823,7 +2823,8 @@ class CVC4_EXPORT Solver /** * Create a String constant. - * @param s a list of unsigned values this constant represents as string + * @param s a list of unsigned (unicode) values this constant represents as + * string * @return the String constant */ Term mkString(const std::vector& s) const; @@ -3363,12 +3364,12 @@ class CVC4_EXPORT Solver * SMT-LIB: ( get-interpol ) * Requires to enable option 'produce-interpols'. * @param conj the conjecture term - * @param g the grammar for the interpolant I + * @param grammar the grammar for the interpolant I * @param output a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj. * @return true if it gets I successfully, false otherwise. */ - bool getInterpolant(const Term& conj, Grammar& g, Term& output) const; + bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const; /** * Get an abduct. @@ -3387,13 +3388,13 @@ class CVC4_EXPORT Solver * SMT-LIB: ( get-abduct ) * Requires enabling option 'produce-abducts' * @param conj the conjecture term - * @param g the grammar for the abduct C + * @param grammar the grammar for the abduct C * @param output a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is * given in the input by conj * @return true if it gets C successfully, false otherwise */ - bool getAbduct(const Term& conj, Grammar& g, Term& output) const; + bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const; /** * Block the current model. Can be called only if immediately preceded by a @@ -3503,13 +3504,13 @@ class CVC4_EXPORT Solver * @param symbol the name of the function * @param boundVars the parameters to this function * @param sort the sort of the return value of this function - * @param g the syntactic constraints + * @param grammar the syntactic constraints * @return the function */ Term synthFun(const std::string& symbol, const std::vector& boundVars, Sort sort, - Grammar& g) const; + Grammar& grammar) const; /** * Synthesize invariant. @@ -3528,12 +3529,12 @@ class CVC4_EXPORT Solver * @param symbol the name of the invariant * @param boundVars the parameters to this invariant * @param sort the sort of the return value of this invariant - * @param g the syntactic constraints + * @param grammar the syntactic constraints * @return the invariant */ Term synthInv(const std::string& symbol, const std::vector& boundVars, - Grammar& g) const; + Grammar& grammar) const; /** * Add a forumla to the set of Sygus constraints. @@ -3674,7 +3675,7 @@ class CVC4_EXPORT Solver const std::vector& boundVars, const Sort& sort, bool isInv = false, - Grammar* g = nullptr) const; + Grammar* grammar = nullptr) const; /** Check whether string s is a valid decimal integer. */ bool isValidInteger(const std::string& s) const; -- cgit v1.2.3