From: Aina Niemetz Date: Sun, 23 Sep 2018 17:55:10 +0000 (-0700) Subject: New C++ API: Add checks for Terms/OpTerms. (#2455) X-Git-Tag: cvc5-1.0.0~4524 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa2f106f94eb7914a463fb75dce09f9d26510616;p=cvc5.git New C++ API: Add checks for Terms/OpTerms. (#2455) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a3b951dd2..c626b7275 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -21,6 +21,8 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/kind.h" +#include "expr/metakind.h" +#include "expr/node_manager.h" #include "expr/type.h" #include "options/main_options.h" #include "options/options.h" @@ -566,6 +568,20 @@ CVC4::Kind extToIntKind(Kind k) } return it->second; } + +uint32_t minArity(Kind k) +{ + Assert(isDefinedKind(k)); + Assert(isDefinedIntKind(extToIntKind(k))); + return CVC4::ExprManager::minArity(extToIntKind(k)); +} + +uint32_t maxArity(Kind k) +{ + Assert(isDefinedKind(k)); + Assert(isDefinedIntKind(extToIntKind(k))); + return CVC4::ExprManager::maxArity(extToIntKind(k)); +} } // namespace std::string kindToString(Kind k) @@ -625,6 +641,10 @@ class CVC4ApiExceptionStream CVC4_API_CHECK(cond) << "Invalid kind '" << kindToString(kind) \ << "', expected " << expected_kind_str; +#define CVC4_API_ARG_CHECK_EXPECTED(cond, arg, expected_arg_str) \ + CVC4_API_CHECK(cond) << "Invalid argument '" << (arg).toString() << "' for " \ + << #arg << ", expected " << expected_arg_str; + } // namespace /* -------------------------------------------------------------------------- */ @@ -708,7 +728,6 @@ Sort::~Sort() {} Sort& Sort::operator=(const Sort& s) { - // CHECK: valid sort s? if (this != &s) { *d_type = *s.d_type; @@ -716,119 +735,43 @@ Sort& Sort::operator=(const Sort& s) return *this; } -bool Sort::operator==(const Sort& s) const -{ - // CHECK: valid sort s? - return *d_type == *s.d_type; -} +bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } -bool Sort::operator!=(const Sort& s) const -{ - // CHECK: valid sort s? - return *d_type != *s.d_type; -} +bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } -bool Sort::isBoolean() const -{ - // CHECK: valid sort s? - return d_type->isBoolean(); -} +bool Sort::isBoolean() const { return d_type->isBoolean(); } -bool Sort::isInteger() const -{ - // CHECK: valid sort s? - return d_type->isInteger(); -} +bool Sort::isInteger() const { return d_type->isInteger(); } -bool Sort::isReal() const -{ - // CHECK: valid sort s? - return d_type->isReal(); -} +bool Sort::isReal() const { return d_type->isReal(); } -bool Sort::isString() const -{ - // CHECK: valid sort s? - return d_type->isString(); -} +bool Sort::isString() const { return d_type->isString(); } -bool Sort::isRegExp() const -{ - // CHECK: valid sort s? - return d_type->isRegExp(); -} +bool Sort::isRegExp() const { return d_type->isRegExp(); } -bool Sort::isRoundingMode() const -{ - // CHECK: valid sort s? - return d_type->isRoundingMode(); -} +bool Sort::isRoundingMode() const { return d_type->isRoundingMode(); } -bool Sort::isBitVector() const -{ - // CHECK: valid sort s? - return d_type->isBitVector(); -} +bool Sort::isBitVector() const { return d_type->isBitVector(); } -bool Sort::isFloatingPoint() const -{ - // CHECK: valid sort s? - return d_type->isFloatingPoint(); -} +bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); } -bool Sort::isDatatype() const -{ - // CHECK: valid sort s? - return d_type->isDatatype(); -} +bool Sort::isDatatype() const { return d_type->isDatatype(); } -bool Sort::isFunction() const -{ - // CHECK: valid sort s? - return d_type->isFunction(); -} +bool Sort::isFunction() const { return d_type->isFunction(); } -bool Sort::isPredicate() const -{ - // CHECK: valid sort s? - return d_type->isPredicate(); -} +bool Sort::isPredicate() const { return d_type->isPredicate(); } -bool Sort::isTuple() const -{ - // CHECK: valid sort s? - return d_type->isTuple(); -} +bool Sort::isTuple() const { return d_type->isTuple(); } -bool Sort::isRecord() const -{ - // CHECK: valid sort s? - return d_type->isRecord(); -} +bool Sort::isRecord() const { return d_type->isRecord(); } -bool Sort::isArray() const -{ - // CHECK: valid sort s? - return d_type->isArray(); -} +bool Sort::isArray() const { return d_type->isArray(); } -bool Sort::isSet() const -{ - // CHECK: valid sort s? - return d_type->isSet(); -} +bool Sort::isSet() const { return d_type->isSet(); } -bool Sort::isUninterpretedSort() const -{ - // CHECK: valid sort s? - return d_type->isSort(); -} +bool Sort::isUninterpretedSort() const { return d_type->isSort(); } -bool Sort::isSortConstructor() const -{ - // CHECK: valid sort s? - return d_type->isSortConstructor(); -} +bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); } Datatype Sort::getDatatype() const { @@ -855,11 +798,7 @@ Sort Sort::instantiate(const std::vector& params) const return static_cast(d_type.get())->instantiate(tparams); } -std::string Sort::toString() const -{ - // CHECK: valid sort s? - return d_type->toString(); -} +std::string Sort::toString() const { return d_type->toString(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! @@ -888,7 +827,6 @@ Term::~Term() {} Term& Term::operator=(const Term& t) { - // CHECK: expr managers must match if (this != &t) { *d_expr = *t.d_expr; @@ -896,17 +834,9 @@ Term& Term::operator=(const Term& t) return *this; } -bool Term::operator==(const Term& t) const -{ - // CHECK: expr managers must match - return *d_expr == *t.d_expr; -} +bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } -bool Term::operator!=(const Term& t) const -{ - // CHECK: expr managers must match - return *d_expr != *t.d_expr; -} +bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } Kind Term::getKind() const { return intToExtKind(d_expr->getKind()); } @@ -1069,7 +999,6 @@ OpTerm::~OpTerm() {} OpTerm& OpTerm::operator=(const OpTerm& t) { - // CHECK: expr managers must match if (this != &t) { *d_expr = *t.d_expr; @@ -1077,17 +1006,9 @@ OpTerm& OpTerm::operator=(const OpTerm& t) return *this; } -bool OpTerm::operator==(const OpTerm& t) const -{ - // CHECK: expr managers must match - return *d_expr == *t.d_expr; -} +bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; } -bool OpTerm::operator!=(const OpTerm& t) const -{ - // CHECK: expr managers must match - return *d_expr != *t.d_expr; -} +bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; } Kind OpTerm::getKind() const { return intToExtKind(d_expr->getKind()); } @@ -1535,7 +1456,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { - Options* o = opts == nullptr ? new Options() : opts; + Options* o = opts == nullptr ? new Options() : opts; d_exprMgr.reset(new ExprManager(*o)); d_smtEngine.reset(new SmtEngine(d_exprMgr.get())); d_rng.reset(new Random((*o)[options::seed])); @@ -1566,8 +1487,6 @@ Sort Solver::getRoundingmodeSort(void) const Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const { - // CHECK: indexSort exists - // CHECK: elemSort exists return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type); } @@ -1585,8 +1504,6 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const Sort Solver::mkFunctionSort(Sort domain, Sort range) const { - // CHECK: domain exists - // CHECK: range exists // CHECK: // domain.isFirstClass() // else "can not create function type for domain type that is not @@ -1603,8 +1520,6 @@ Sort Solver::mkFunctionSort(Sort domain, Sort range) const Sort Solver::mkFunctionSort(const std::vector& argSorts, Sort range) const { - // CHECK: for all s in argSorts, s exists - // CHECK: range exists // CHECK: argSorts.size() >= 1 // CHECK: // for (unsigned i = 0; i < argSorts.size(); ++ i) @@ -1629,7 +1544,6 @@ Sort Solver::mkParamSort(const std::string& symbol) const Sort Solver::mkPredicateSort(const std::vector& sorts) const { - // CHECK: for all s in sorts, s exists // CHECK: sorts.size() >= 1 // CHECK: // for (unsigned i = 0; i < sorts.size(); ++ i) @@ -1663,7 +1577,6 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const Sort Solver::mkTupleSort(const std::vector& sorts) const { - // CHECK: for all s in sorts, s exists // CHECK: // for (unsigned i = 0; i < sorts.size(); ++ i) // !sorts[i].isFunctionLike() @@ -1849,7 +1762,6 @@ Term Solver::mkBitVector(std::string& s, uint32_t base) const Term Solver::mkConst(RoundingMode rm) const { - // CHECK: valid rm? return d_exprMgr->mkConst(s_rmodes.at(rm)); } @@ -2007,9 +1919,12 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const { - // CHECK: arg 3 is bit-vector constant CVC4_API_KIND_CHECK_EXPECTED( kind == CONST_FLOATINGPOINT, kind, "CONST_FLOATINGPOINT"); + CVC4_API_ARG_CHECK_EXPECTED( + arg3.getSort().isBitVector() && arg3.d_expr->isConst(), + arg3, + "bit-vector constant"); return d_exprMgr->mkConst( CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst())); } @@ -2019,31 +1934,77 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const Term Solver::mkVar(const std::string& symbol, Sort sort) const { - // CHECK: sort exists? return d_exprMgr->mkVar(symbol, *sort.d_type); } -Term Solver::mkVar(Sort sort) const -{ - // CHECK: sort exists? - return d_exprMgr->mkVar(*sort.d_type); -} +Term Solver::mkVar(Sort sort) const { return d_exprMgr->mkVar(*sort.d_type); } Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const { - // CHECK: sort exists? return d_exprMgr->mkBoundVar(symbol, *sort.d_type); } Term Solver::mkBoundVar(Sort sort) const { - // CHECK: sort exists? return d_exprMgr->mkBoundVar(*sort.d_type); } /* Create terms */ /* -------------------------------------------------------------------------- */ +void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const +{ + CVC4_API_KIND_CHECK(kind); + Assert(isDefinedIntKind(extToIntKind(kind))); + const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind)); + CVC4_API_KIND_CHECK_EXPECTED( + mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, + kind, + "Only operator-style terms are created with mkTerm(), " + "to create variables and constants see mkVar(), mkBoundVar(), " + "and mkConst()."); + if (nchildren) + { + const uint32_t n = + nchildren - (mk == CVC4::kind::metakind::PARAMETERIZED ? 1 : 0); + CVC4_API_KIND_CHECK_EXPECTED( + n >= minArity(kind) && n <= maxArity(kind), + kind, + "Terms with kind " << kindToString(kind) << " must have at least " + << minArity(kind) << " children and at most " + << maxArity(kind) + << " children (the one under construction has " << n + << ")"); + } +} + +void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const +{ + const Kind kind = opTerm.getKind(); + Assert(isDefinedIntKind(extToIntKind(kind))); + const CVC4::Kind int_kind = extToIntKind(kind); + const CVC4::Kind int_op_kind = + NodeManager::operatorToKind(opTerm.d_expr->getNode()); + CVC4_API_ARG_CHECK_EXPECTED( + int_kind == kind::BUILTIN + || CVC4::kind::metaKindOf(int_op_kind) + == kind::metakind::PARAMETERIZED, + opTerm, + "This term constructor is for parameterized kinds only"); + if (nchildren) + { + uint32_t min_arity = ExprManager::minArity(int_op_kind); + uint32_t max_arity = ExprManager::maxArity(int_op_kind); + CVC4_API_KIND_CHECK_EXPECTED( + nchildren >= min_arity && nchildren <= max_arity, + kind, + "Terms with kind " << kindToString(kind) << " must have at least " + << min_arity << " children and at most " << max_arity + << " children (the one under construction has " + << nchildren << ")"); + } +} + Term Solver::mkTerm(Kind kind) const { CVC4_API_KIND_CHECK_EXPECTED( @@ -2069,71 +2030,19 @@ Term Solver::mkTerm(Kind kind, Sort sort) const Term Solver::mkTerm(Kind kind, Term child) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child.getExprManager()) - // CHECK: - // const Metakind mk = kind::metaKindOf(kind); - // mk != kind::metakind::PARAMETERIZED && mk != kind::metakind::OPERATOR - // else "Only operator-style expressions are made with mkExpr(); " - // "to make variables and constants, see mkVar(), mkBoundVar(), " - // "and mkConst()." - // CHECK: - // const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" - CVC4_API_KIND_CHECK(kind); - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - return d_exprMgr->mkExpr(k, *child.d_expr); + checkMkTerm(kind, 1); + return d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); } Term Solver::mkTerm(Kind kind, Term child1, Term child2) const { - CVC4_API_KIND_CHECK(kind); - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child1.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child2.getExprManager()) - // CHECK: - // const Metakind mk = kind::metaKindOf(kind); - // mk != kind::metakind::PARAMETERIZED && mk != kind::metakind::OPERATOR - // else "Only operator-style expressions are made with mkExpr(); " - // "to make variables and constants, see mkVar(), mkBoundVar(), " - // "and mkConst()." - // CHECK: - // const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - return d_exprMgr->mkExpr(k, *child1.d_expr, *child2.d_expr); + checkMkTerm(kind, 2); + return d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); } Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child1.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child2.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child3.getExprManager()) - // CHECK: - // const Metakind mk = kind::metaKindOf(kind); - // mk != kind::metakind::PARAMETERIZED && mk != kind::metakind::OPERATOR - // else "Only operator-style expressions are made with mkExpr(); " - // "to make variables and constants, see mkVar(), mkBoundVar(), " - // "and mkConst()." - // CHECK: - // const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" - CVC4_API_KIND_CHECK(kind); + checkMkTerm(kind, 3); std::vector echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; CVC4::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); @@ -2143,22 +2052,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const Term Solver::mkTerm(Kind kind, const std::vector& children) const { - // CHECK: - // for c in children: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(c.getExprManager()) - // CHECK: - // const Metakind mk = kind::metaKindOf(kind); - // mk != kind::metakind::PARAMETERIZED && mk != kind::metakind::OPERATOR - // else "Only operator-style expressions are made with mkExpr(); " - // "to make variables and constants, see mkVar(), mkBoundVar(), " - // "and mkConst()." - // CHECK: - // const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? - // 1 : 0); n < minArity(kind) || n > maxArity(kind) else "Exprs with kind %s - // must have at least %u children and " - // "at most %u children (the one under construction has %u)" - CVC4_API_KIND_CHECK(kind); + checkMkTerm(kind, children.size()); std::vector echildren = termVectorToExprs(children); CVC4::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); @@ -2168,102 +2062,32 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const Term Solver::mkTerm(OpTerm opTerm) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(opExpr.getExprManager()) - // CHECK: - // const Kind kind = NodeManager::opToKind(opExpr.getNode()); - // opExpr.getKind() != kind::BUILTIN - // && kind::metaKindOf(kind) != kind::metakind::PARAMETERIZED - // else "This Expr constructor is for parameterized kinds only" + checkMkOpTerm(opTerm, 0); return d_exprMgr->mkExpr(*opTerm.d_expr); } Term Solver::mkTerm(OpTerm opTerm, Term child) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(opExpr.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child.getExprManager()) - // CHECK: - // const Kind kind = NodeManager::opToKind(opExpr.getNode()); - // opExpr.getKind() != kind::BUILTIN - // && kind::metaKindOf(kind) != kind::metakind::PARAMETERIZED - // else "This Expr constructor is for parameterized kinds only" - // CHECK: - // const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" + checkMkOpTerm(opTerm, 1); return d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr); } Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(opExpr.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child1.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child2.getExprManager()) - // CHECK: - // const Kind kind = NodeManager::opToKind(opExpr.getNode()); - // opExpr.getKind() != kind::BUILTIN - // && kind::metaKindOf(kind) != kind::metakind::PARAMETERIZED - // else "This Expr constructor is for parameterized kinds only" - // CHECK: - // const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" + checkMkOpTerm(opTerm, 2); return d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr); } Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(opExpr.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child1.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child2.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(child3.getExprManager()) - // CHECK: - // const Kind kind = NodeManager::opToKind(opExpr.getNode()); - // opExpr.getKind() != kind::BUILTIN - // && kind::metaKindOf(kind) != kind::metakind::PARAMETERIZED - // else "This Expr constructor is for parameterized kinds only" - // CHECK: - // const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - // n < minArity(kind) || n > maxArity(kind) - // else "Exprs with kind %s must have at least %u children and " - // "at most %u children (the one under construction has %u)" + checkMkOpTerm(opTerm, 3); return d_exprMgr->mkExpr( *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); } Term Solver::mkTerm(OpTerm opTerm, const std::vector& children) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(opExpr.getExprManager()) - // for c in children: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(c.getExprManager()) - // CHECK: - // const Kind kind = NodeManager::opToKind(opExpr.getNode()); - // opExpr.getKind() != kind::BUILTIN - // && kind::metaKindOf(kind) != kind::metakind::PARAMETERIZED - // else "This Expr constructor is for parameterized kinds only" - // CHECK: - // const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? - // 1 : 0); n < minArity(kind) || n > maxArity(kind) else "Exprs with kind %s - // must have at least %u children and " - // "at most %u children (the one under construction has %u)" + checkMkOpTerm(opTerm, children.size()); std::vector echildren = termVectorToExprs(children); return d_exprMgr->mkExpr(*opTerm.d_expr, echildren); } @@ -2336,9 +2160,10 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg)); break; default: - // CHECK: kind valid? - Assert(!res.isNull()); + CVC4_API_KIND_CHECK_EXPECTED( + false, kind, "operator kind with uint32_t argument"); } + Assert(!res.isNull()); return res; } @@ -2374,9 +2199,10 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2)); break; default: - // CHECK: kind valid? - Assert(!res.isNull()); + CVC4_API_KIND_CHECK_EXPECTED( + false, kind, "operator kind with two uint32_t arguments"); } + Assert(!res.isNull()); return res; } @@ -2466,7 +2292,6 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const */ Term Solver::declareConst(const std::string& symbol, Sort sort) const { - // CHECK: sort exists return d_exprMgr->mkVar(symbol, *sort.d_type); } @@ -2490,7 +2315,6 @@ Sort Solver::declareDatatype( */ Term Solver::declareFun(const std::string& symbol, Sort sort) const { - // CHECK: sort exists // CHECK: // sort.isFirstClass() // else "can not create function type for range type that is not first class" @@ -2511,8 +2335,6 @@ Term Solver::declareFun(const std::string& symbol, const std::vector& sorts, Sort sort) const { - // CHECK: for all s in sorts, s exists - // CHECK: sort exists // CHECK: // for (unsigned i = 0; i < sorts.size(); ++ i) // sorts[i].isFirstClass() @@ -2563,7 +2385,6 @@ Term Solver::defineFun(const std::string& symbol, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: sort exists // CHECK: not recursive // CHECK: // sort.isFirstClass() @@ -2627,7 +2448,6 @@ Term Solver::defineFunRec(const std::string& symbol, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: sort exists // CHECK: // sort.isFirstClass() // else "can not create function type for range type that is not first class" diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index a701eb472..3481fd953 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -55,6 +55,7 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception CVC4ApiException(const std::string& str) : d_msg(str) {} CVC4ApiException(const std::stringstream& stream) :d_msg(stream.str()) {} std::string getMessage() const { return d_msg; } + const char* what() const noexcept override { return d_msg.c_str(); } private: std::string d_msg; }; @@ -2427,6 +2428,10 @@ class CVC4_PUBLIC Solver std::vector sortVectorToTypes(const std::vector& vector) const; /* Helper to convert a vector of sorts to internal types. */ std::vector termVectorToExprs(const std::vector& vector) const; + /* Helper to check for API misuse in mkTerm functions. */ + void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const; + /* Helper to check for API misuse in mkOpTerm functions. */ + void checkMkTerm(Kind kind, uint32_t nchildren) const; /* The expression manager of this solver. */ std::unique_ptr d_exprMgr; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 7cecdebbd..afa08068f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -60,6 +60,10 @@ class Type; class TypeCheckingException; class TypeCheckingExceptionPrivate; +namespace api { +class Solver; +} + namespace expr { namespace pickle { class Pickler; @@ -208,6 +212,16 @@ struct ExprHashFunction { * expressions. */ class CVC4_PUBLIC Expr { + friend class ExprManager; + friend class NodeManager; + friend class SmtEngine; + friend class TypeCheckingException; + friend class api::Solver; + friend class expr::ExportPrivate; + friend class expr::pickle::Pickler; + friend class prop::TheoryProxy; + friend class smt::SmtEnginePrivate; + friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); /** The internal expression representation */ NodeTemplate* d_node; @@ -592,17 +606,6 @@ private: * @return the internal node */ NodeTemplate getTNode() const; - - // Friend to access the actual internal expr information and private methods - friend class SmtEngine; - friend class smt::SmtEnginePrivate; - friend class ExprManager; - friend class NodeManager; - friend class TypeCheckingException; - friend class expr::pickle::Pickler; - friend class prop::TheoryProxy; - friend class expr::ExportPrivate; - friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template friend class NodeTemplate; };/* class Expr */