From 42c15c764e354046ab511e165caa31e001d14f88 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 18 Sep 2018 17:22:30 -0700 Subject: [PATCH] New C++ API: Introduce new macro and exception for API checks. (#2486) --- src/api/cvc4cpp.cpp | 351 +++++++++++++++++++++----------------------- src/api/cvc4cpp.h | 15 ++ 2 files changed, 179 insertions(+), 187 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 013e2165f..a3b951dd2 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -17,6 +17,7 @@ #include "api/cvc4cpp.h" #include "base/cvc4_assert.h" +#include "base/cvc4_check.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/kind.h" @@ -34,77 +35,6 @@ namespace CVC4 { namespace api { -/* -------------------------------------------------------------------------- */ -/* Result */ -/* -------------------------------------------------------------------------- */ - -Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {} - -bool Result::isSat(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::SAT; -} - -bool Result::isUnsat(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::UNSAT; -} - -bool Result::isSatUnknown(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::SAT_UNKNOWN; -} - -bool Result::isValid(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALID; -} - -bool Result::isInvalid(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::INVALID; -} - -bool Result::isValidUnknown(void) const -{ - return d_result->getType() == CVC4::Result::TYPE_VALIDITY - && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN; -} - -bool Result::operator==(const Result& r) const -{ - return *d_result == *r.d_result; -} - -bool Result::operator!=(const Result& r) const -{ - return *d_result != *r.d_result; -} - -std::string Result::getUnknownExplanation(void) const -{ - std::stringstream ss; - ss << d_result->whyUnknown(); - return ss.str(); -} - -std::string Result::toString(void) const { return d_result->toString(); } - -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::Result Result::getResult(void) const { return *d_result; } - -std::ostream& operator<<(std::ostream& out, const Result& r) -{ - out << r.toString(); - return out; -} - /* -------------------------------------------------------------------------- */ /* Kind */ /* -------------------------------------------------------------------------- */ @@ -656,6 +586,118 @@ std::ostream& operator<<(std::ostream& out, Kind k) size_t KindHashFunction::operator()(Kind k) const { return k; } +/* -------------------------------------------------------------------------- */ +/* API guard helpers */ +/* -------------------------------------------------------------------------- */ + +namespace { + +class CVC4ApiExceptionStream +{ + public: + CVC4ApiExceptionStream() {} + /* Note: This needs to be explicitly set to 'noexcept(false)' since it is + * a destructor that throws an exception and in C++11 all destructors + * default to noexcept(true) (else this triggers a call to std::terminate). */ + ~CVC4ApiExceptionStream() noexcept(false) + { + if (!std::uncaught_exception()) + { + throw CVC4ApiException(d_stream.str()); + } + } + + std::ostream& ostream() { return d_stream; } + + private: + std::stringstream d_stream; +}; + +#define CVC4_API_CHECK(cond) \ + CVC4_PREDICT_FALSE(cond) \ + ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() + +#define CVC4_API_KIND_CHECK(kind) \ + CVC4_API_CHECK(isDefinedKind(kind)) \ + << "Invalid kind '" << kindToString(kind) << "'"; + +#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind, expected_kind_str) \ + CVC4_API_CHECK(cond) << "Invalid kind '" << kindToString(kind) \ + << "', expected " << expected_kind_str; + +} // namespace + +/* -------------------------------------------------------------------------- */ +/* Result */ +/* -------------------------------------------------------------------------- */ + +Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {} + +bool Result::isSat(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_SAT + && d_result->isSat() == CVC4::Result::SAT; +} + +bool Result::isUnsat(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_SAT + && d_result->isSat() == CVC4::Result::UNSAT; +} + +bool Result::isSatUnknown(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_SAT + && d_result->isSat() == CVC4::Result::SAT_UNKNOWN; +} + +bool Result::isValid(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_VALIDITY + && d_result->isValid() == CVC4::Result::VALID; +} + +bool Result::isInvalid(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_VALIDITY + && d_result->isValid() == CVC4::Result::INVALID; +} + +bool Result::isValidUnknown(void) const +{ + return d_result->getType() == CVC4::Result::TYPE_VALIDITY + && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN; +} + +bool Result::operator==(const Result& r) const +{ + return *d_result == *r.d_result; +} + +bool Result::operator!=(const Result& r) const +{ + return *d_result != *r.d_result; +} + +std::string Result::getUnknownExplanation(void) const +{ + std::stringstream ss; + ss << d_result->whyUnknown(); + return ss.str(); +} + +std::string Result::toString(void) const { return d_result->toString(); } + +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Result Result::getResult(void) const { return *d_result; } + +std::ostream& operator<<(std::ostream& out, const Result& r) +{ + out << r.toString(); + return out; +} + /* -------------------------------------------------------------------------- */ /* Sort */ /* -------------------------------------------------------------------------- */ @@ -1813,57 +1855,42 @@ Term Solver::mkConst(RoundingMode rm) const Term Solver::mkConst(Kind kind, Sort arg) const { - PrettyCheckArgument(kind == EMPTYSET, - kind, - "Invalid kind '%s', expected EMPTY_SET", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET, kind, "EMPTY_SET"); return d_exprMgr->mkConst(CVC4::EmptySet(*arg.d_type)); } Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const { - PrettyCheckArgument(kind == UNINTERPRETED_CONSTANT, - kind, - "Invalid kind '%s', expected UNINTERPRETED_CONSTANT", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == UNINTERPRETED_CONSTANT, kind, "UNINTERPRETED_CONSTANT"); return d_exprMgr->mkConst(CVC4::UninterpretedConstant(*arg1.d_type, arg2)); } Term Solver::mkConst(Kind kind, bool arg) const { - PrettyCheckArgument(kind == CONST_BOOLEAN, - kind, - "Invalid kind '%s', expected CONST_BOOLEAN", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BOOLEAN, kind, "CONST_BOOLEAN"); return d_exprMgr->mkConst(arg); } Term Solver::mkConst(Kind kind, const char* arg) const { - PrettyCheckArgument(kind == CONST_STRING, - kind, - "Invalid kind '%s', expected CONST_STRING", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind, "CONST_STRING"); return d_exprMgr->mkConst(CVC4::String(arg)); } Term Solver::mkConst(Kind kind, const std::string& arg) const { - PrettyCheckArgument(kind == CONST_STRING, - kind, - "Invalid kind '%s', expected CONST_STRING", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind, "CONST_STRING"); return d_exprMgr->mkConst(CVC4::String(arg)); } Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const { - PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or " - "CONST_RATIONAL or CONST_BITVECTOR", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == ABSTRACT_VALUE || kind == CONST_RATIONAL + || kind == CONST_BITVECTOR, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2))); @@ -1877,12 +1904,11 @@ Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const { - PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or " - "CONST_RATIONAL or CONST_BITVECTOR", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == ABSTRACT_VALUE || kind == CONST_RATIONAL + || kind == CONST_BITVECTOR, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2))); @@ -1896,12 +1922,11 @@ Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const Term Solver::mkConst(Kind kind, uint32_t arg) const { - PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or " - "CONST_RATIONAL or CONST_BITVECTOR", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == ABSTRACT_VALUE || kind == CONST_RATIONAL + || kind == CONST_BITVECTOR, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1915,11 +1940,9 @@ Term Solver::mkConst(Kind kind, uint32_t arg) const Term Solver::mkConst(Kind kind, int32_t arg) const { - PrettyCheckArgument( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1929,11 +1952,9 @@ Term Solver::mkConst(Kind kind, int32_t arg) const Term Solver::mkConst(Kind kind, int64_t arg) const { - PrettyCheckArgument( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1943,11 +1964,9 @@ Term Solver::mkConst(Kind kind, int64_t arg) const Term Solver::mkConst(Kind kind, uint64_t arg) const { - PrettyCheckArgument( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, + kind, + "ABSTRACT_VALUE or CONST_RATIONAL"); if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1957,56 +1976,40 @@ Term Solver::mkConst(Kind kind, uint64_t arg) const Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const { - PrettyCheckArgument(kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2)); } Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const { - PrettyCheckArgument(kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2)); } Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const { - PrettyCheckArgument(kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2)); } Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const { - PrettyCheckArgument(kind == CONST_RATIONAL, - kind, - "Invalid kind '%s', expected CONST_RATIONAL", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2)); } Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const { - PrettyCheckArgument(kind == CONST_BITVECTOR, - kind, - "Invalid kind '%s', expected CONST_BITVECTOR", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == CONST_BITVECTOR, kind, "CONST_BITVECTOR"); return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2)); } Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const { // CHECK: arg 3 is bit-vector constant - PrettyCheckArgument(kind == CONST_FLOATINGPOINT, - kind, - "Invalid kind '%s', expected CONST_FLOATINGPOINT", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == CONST_FLOATINGPOINT, kind, "CONST_FLOATINGPOINT"); return d_exprMgr->mkConst( CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst())); } @@ -2043,11 +2046,10 @@ Term Solver::mkBoundVar(Sort sort) const Term Solver::mkTerm(Kind kind) const { - PrettyCheckArgument( + CVC4_API_KIND_CHECK_EXPECTED( kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind, - "Invalid kind '%s', expected PI or REGEXP_EMPTY or REGEXP_SIGMA", - kindToString(kind).c_str()); + "PI or REGEXP_EMPTY or REGEXP_SIGMA"); if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { CVC4::Kind k = extToIntKind(kind); @@ -2060,10 +2062,8 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, Sort sort) const { - PrettyCheckArgument(kind == SEP_NIL || kind == UNIVERSE_SET, - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == SEP_NIL || kind == UNIVERSE_SET, kind, "SEP_NIL or UNIVERSE_SET"); return d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind)); } @@ -2083,10 +2083,7 @@ Term Solver::mkTerm(Kind kind, Term child) const // 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)" - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); CVC4::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); return d_exprMgr->mkExpr(k, *child.d_expr); @@ -2094,10 +2091,7 @@ Term Solver::mkTerm(Kind kind, Term child) const Term Solver::mkTerm(Kind kind, Term child1, Term child2) const { - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); // CHECK: // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(child1.getExprManager()) @@ -2139,10 +2133,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const // 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)" - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); std::vector echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; CVC4::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); @@ -2167,10 +2158,7 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const // 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)" - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); std::vector echildren = termVectorToExprs(children); CVC4::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); @@ -2296,28 +2284,20 @@ std::vector Solver::termVectorToExprs( OpTerm Solver::mkOpTerm(Kind kind, Kind k) { - PrettyCheckArgument(kind == CHAIN_OP, - kind, - "Invalid kind '%s', expected CHAIN_OP", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind, "CHAIN_OP"); return d_exprMgr->mkConst(CVC4::Chain(extToIntKind(k))); } OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) { - PrettyCheckArgument(kind == RECORD_UPDATE_OP, - kind, - "Invalid kind '%s', expected RECORD_UPDATE_OP", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK_EXPECTED( + kind == RECORD_UPDATE_OP, kind, "RECORD_UPDATE_OP"); return d_exprMgr->mkConst(CVC4::RecordUpdate(arg)); } OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) { - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); OpTerm res; switch (kind) { @@ -2364,10 +2344,7 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) { - PrettyCheckArgument(isDefinedKind(kind), - kind, - "Invalid kind '%s'", - kindToString(kind).c_str()); + CVC4_API_KIND_CHECK(kind); OpTerm res; switch (kind) { diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index b1a1e2abd..a701eb472 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -25,6 +25,7 @@ #include #include #include +#include #include #include #include @@ -44,6 +45,20 @@ class Result; namespace api { +/* -------------------------------------------------------------------------- */ +/* Exception */ +/* -------------------------------------------------------------------------- */ + +class CVC4_PUBLIC CVC4ApiException : public std::exception +{ + public: + CVC4ApiException(const std::string& str) : d_msg(str) {} + CVC4ApiException(const std::stringstream& stream) :d_msg(stream.str()) {} + std::string getMessage() const { return d_msg; } + private: + std::string d_msg; +}; + /* -------------------------------------------------------------------------- */ /* Result */ /* -------------------------------------------------------------------------- */ -- 2.30.2