summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-17 17:28:59 -0700
committerGitHub <noreply@github.com>2021-03-18 00:28:59 +0000
commitd52bc44199583e3c06816c1d30f61e8075820c1b (patch)
tree9aee93b037ab78374dc1781f93ebdc016d19c80d
parenta3e250159a0179c61965f4c9f059f99758f79e8e (diff)
New C++ Api: Comprehensive guards for member functions of class Solver. (#6153)
Diffstat
-rw-r--r--src/api/checks.h324
-rw-r--r--src/api/cvc4cpp.cpp864
-rw-r--r--src/api/cvc4cpp.h29
3 files changed, 706 insertions, 511 deletions
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 <typename T>
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>(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>(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<uint32_t>(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<unsigned> cpts;
cpts.push_back(val);
return mkValHelper<CVC4::String>(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<Sort>& sorts) const
{
// Note: Sorts are checked in the caller to avoid double checks
+ //////// all checks before this line
std::vector<TypeNode> 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<Term>& 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<Node> 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<Term>& children) const
Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& 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<Node> echildren = Term::termVectorToNodes(children);
@@ -4342,30 +4327,15 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
const std::vector<DatatypeDecl>& dtypedecls,
const std::set<Sort>& unresolvedSorts) const
{
+ // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
+ // double checks
+ //////// all checks before this line
+
std::vector<CVC4::DType> 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<TypeNode> utypes = Sort::sortSetToTypeNodes(unresolvedSorts);
std::vector<CVC4::TypeNode> dtypes =
@@ -4378,35 +4348,23 @@ Term Solver::synthFunHelper(const std::string& symbol,
const std::vector<Term>& 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<TypeNode> 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<Node> 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<Sort> Solver::mkDatatypeSorts(
const std::vector<DatatypeDecl>& dtypedecls) const
{
NodeManagerScope scope(getNodeManager());
+ CVC4_API_SOLVER_CHECK_DTDECLS(dtypedecls);
CVC4_API_TRY_CATCH_BEGIN;
- std::set<Sort> unresolvedSorts;
- return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
+ //////// all checks before this line
+ return mkDatatypeSortsInternal(dtypedecls, {});
////////
CVC4_API_TRY_CATCH_END;
}
@@ -4678,6 +4649,9 @@ std::vector<Sort> 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<Sort>& 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<TypeNode> 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<Sort>& 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<TypeNode> 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<std::pair<std::string, TypeNode>> 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<Sort>& 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<Sort>& 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<bool>(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<bool>(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<bool>(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>(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>(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>(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<CVC4::Node>());
(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<CVC4::Node>());
(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>(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>(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>(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>(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>(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>(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<uint32_t>& s) const
{
+ NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return mkValHelper<CVC4::String>(CVC4::String(s));
////////
CVC4_API_TRY_CATCH_END;
@@ -5061,7 +5012,9 @@ Term Solver::mkString(const std::vector<uint32_t>& 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<Node> 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<CVC4::FloatingPoint>(
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<CVC4::FloatingPoint>(
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<CVC4::FloatingPoint>(
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<CVC4::FloatingPoint>(
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<CVC4::FloatingPoint>(
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<CVC4::RoundingMode>(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>(
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>(
CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>()));
////////
@@ -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<Term>{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<Term>{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<Term>{child1, child2, child3});
////////
@@ -5432,6 +5411,9 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& 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<Term>{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<Term>{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<Term>{child1, child2, child3});
////////
CVC4_API_TRY_CATCH_END;
@@ -5492,6 +5487,9 @@ Term Solver::mkTerm(const Op& op, const std::vector<Term>& 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<Sort>& 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<CVC4::Node> 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<Sort>& 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<uint32_t>& 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<uint32_t>& 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<Term>& 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<Node> 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<Term>& 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<Node> 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<TypeNode> 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<Sort> 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<Node> 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<Sort> 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<Node> 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<TypeNode> 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<Sort> 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<Node> 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<Sort> 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<Node> 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<Term>& 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<Term>& 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<Sort> 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<Node> efuns = Term::termVectorToNodes(funs);
std::vector<std::vector<Node>> 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<Term> Solver::getAssertions(void) const
{
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
std::vector<Node> assertions = d_smtEngine->getAssertions();
/* Can not use
* return std::vector<Term>(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<Term> 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<Node> uassumptions = d_smtEngine->getUnsatAssumptions();
/* Can not use
@@ -6365,6 +6278,7 @@ std::vector<Term> 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<Term>(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<Term> Solver::getValue(const std::vector<Term>& 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<Term> 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<Term> Solver::getValue(const std::vector<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<TypeNode>& 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<CVC4::Node, CVC4::Node> map;
@@ -6902,7 +6803,7 @@ Term Solver::getSynthSolution(Term term) const
std::map<CVC4::Node, CVC4::Node>::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<Term> 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<CVC4::Node, CVC4::Node> 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<Term> synthSolution;
synthSolution.reserve(terms.size());
@@ -6951,6 +6844,7 @@ std::vector<Term> 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<uint32_t>& s) const;
@@ -3363,12 +3364,12 @@ class CVC4_EXPORT Solver
* SMT-LIB: ( get-interpol <conj> <g> )
* 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 <conj> <g> )
* 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<Term>& 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<Term>& 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<Term>& 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback