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();
}
/* -------------------------------------------------------------------------- */
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);
Term Solver::mkRealFromStrHelper(const std::string& s) const
{
+ //////// all checks before this line
try
{
CVC4::Rational r = s.find('/') != std::string::npos
}
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;
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
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));
}
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);
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));
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.
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));
}
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)
{
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)
{
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);
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 =
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(
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);
}
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)
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);
bool Solver::isValidInteger(const std::string& s) const
{
+ //////// all checks before this line
if (s.length() == 0)
{
// string should not be empty
bool Solver::supportsFloatingPoint() const
{
+ CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Configuration::isBuiltWithSymFPU();
+ ////////
+ CVC4_API_TRY_CATCH_END;
}
/* Sorts Handling */
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;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->booleanType());
////////
CVC4_API_TRY_CATCH_END;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->integerType());
////////
CVC4_API_TRY_CATCH_END;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->realType());
////////
CVC4_API_TRY_CATCH_END;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->regExpType());
////////
CVC4_API_TRY_CATCH_END;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->stringType());
////////
CVC4_API_TRY_CATCH_END;
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;
{
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));
////////
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;
<< "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;
{
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;
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;
}
{
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;
{
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));
////////
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));
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(
this,
getNodeManager()->mkSort(symbol, NodeManager::SORT_FLAG_PLACEHOLDER));
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;
}
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;
{
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;
{
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;
{
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;
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return Sort(this, getNodeManager()->mkSort(symbol));
////////
CVC4_API_TRY_CATCH_END;
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;
{
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;
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;
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;
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;
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 */
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;
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;
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);
////////
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);
////////
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);
////////
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 */
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 */
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 */
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;
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;
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;
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;
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);
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);
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;
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;
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;
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())
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));
////////
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));
////////
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)));
////////
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));
////////
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));
////////
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;
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));
////////
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
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
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>()));
////////
{
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);
{
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);
{
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 */
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 */
{
NodeManagerScope scope(getNodeManager());
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return DatatypeDecl(this, name, isCoDatatype);
////////
CVC4_API_TRY_CATCH_END;
{
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;
{
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;
{
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;
{
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;
{
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;
{
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});
////////
{
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;
CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_SOLVER_CHECK_OP(op);
checkMkTerm(op.d_kind, 0);
+ //////// all checks before this line
if (!op.isIndexedHelper())
{
{
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;
{
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;
{
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;
{
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;
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);
}
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)
{
{
CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK(kind);
-
+ //////// all checks before this line
Op res;
switch (kind)
{
{
CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK(kind);
+ //////// all checks before this line
Op res;
switch (kind)
{
CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK(kind);
+ //////// all checks before this line
Op res;
switch (kind)
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;
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);
////////
|| 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;
}
{
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;
|| 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);
////////
|| 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);
////////
|| 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);
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));
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())
{
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));
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;
}
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 '"
}
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;
<< "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;
}
"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 '"
}
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);
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];
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)
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());
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;
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();
////////
"(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
"(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());
{
CVC4_API_TRY_CATCH_BEGIN;
CVC4_API_SOLVER_CHECK_TERM(term);
+ //////// all checks before this line
return getValueHelper(term);
////////
CVC4_API_TRY_CATCH_END;
"(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]));
}
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));
////////
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));
////////
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;
"(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;
"(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;
<< "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();
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)
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);
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)
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);
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;
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 "
<< "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;
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;
*/
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();
void Solver::resetAssertions(void) const
{
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
d_smtEngine->resetAssertions();
////////
CVC4_API_TRY_CATCH_END;
|| value == "unsat" || value == "unknown",
value)
<< "'sat', 'unsat' or 'unknown'";
-
+ //////// all checks before this line
d_smtEngine->setInfo(keyword, value);
////////
CVC4_API_TRY_CATCH_END;
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;
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;
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 */
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;
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;
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;
}
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);
////////
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;
}
{
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;
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)
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();
Result Solver::checkSynth() const
{
CVC4_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
return d_smtEngine->checkSynth();
////////
CVC4_API_TRY_CATCH_END;
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;
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;
{
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());
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;
projects / cvc5.git / commitdiff