diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 620 |
1 files changed, 427 insertions, 193 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c626b7275..c8248d803 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -637,14 +637,35 @@ class CVC4ApiExceptionStream 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; - -#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; - +#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \ + CVC4_PREDICT_FALSE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid kind '" << kindToString(kind) << "', expected " + +#define CVC4_API_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_FALSE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + +#define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_FALSE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid size of argument '" << #arg << "', expected " + +#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ + CVC4_PREDICT_FALSE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiExceptionStream().ostream() \ + << "Invalid " << what << "'" << arg << "' at index" << idx \ + << ", expected " } // namespace /* -------------------------------------------------------------------------- */ @@ -757,6 +778,13 @@ bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); } bool Sort::isDatatype() const { return d_type->isDatatype(); } +bool Sort::isParametricDatatype() const +{ + if (!d_type->isDatatype()) return false; + DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); + return type->isParametric(); +} + bool Sort::isFunction() const { return d_type->isFunction(); } bool Sort::isPredicate() const { return d_type->isPredicate(); } @@ -773,16 +801,21 @@ bool Sort::isUninterpretedSort() const { return d_type->isSort(); } bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); } +bool Sort::isFirstClass() const { return d_type->isFirstClass(); } + +bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); } + Datatype Sort::getDatatype() const { - // CHECK: is this a datatype sort? + CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); return type->getDatatype(); } Sort Sort::instantiate(const std::vector<Sort>& params) const { - // CHECK: Is this a datatype/sort constructor sort? + CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) + << "Expected parametric datatype or sort constructor sort."; std::vector<Type> tparams; for (const Sort& s : params) { @@ -790,7 +823,6 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const } if (d_type->isDatatype()) { - // CHECK: is parametric? DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); return type->instantiate(tparams); } @@ -804,6 +836,155 @@ std::string Sort::toString() const { return d_type->toString(); } // to the new API. !!! CVC4::Type Sort::getType(void) const { return *d_type; } +/* Function sort ------------------------------------------------------- */ + +size_t Sort::getFunctionArity() const +{ + CVC4_API_CHECK(isFunction()) << "Not a function sort."; + return static_cast<FunctionType*>(d_type.get())->getArity(); +} + +std::vector<Sort> Sort::getFunctionDomainSorts() const +{ + CVC4_API_CHECK(isFunction()) << "Not a function sort."; + std::vector<CVC4::Type> types = + static_cast<FunctionType*>(d_type.get())->getArgTypes(); + return typeVectorToSorts(types); +} + +Sort Sort::getFunctionCodomainSort() const +{ + CVC4_API_CHECK(isFunction()) << "Not a function sort."; + return static_cast<FunctionType*>(d_type.get())->getRangeType(); +} + +/* Array sort ---------------------------------------------------------- */ + +Sort Sort::getArrayIndexSort() const +{ + CVC4_API_CHECK(isArray()) << "Not an array sort."; + return static_cast<ArrayType*>(d_type.get())->getIndexType(); +} + +Sort Sort::getArrayElementSort() const +{ + CVC4_API_CHECK(isArray()) << "Not an array sort."; + return static_cast<ArrayType*>(d_type.get())->getConstituentType(); +} + +/* Set sort ------------------------------------------------------------ */ + +Sort Sort::getSetElementSort() const +{ + CVC4_API_CHECK(isSet()) << "Not a set sort."; + return static_cast<SetType*>(d_type.get())->getElementType(); +} + +/* Uninterpreted sort -------------------------------------------------- */ + +std::string Sort::getUninterpretedSortName() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + return static_cast<SortType*>(d_type.get())->getName(); +} + +bool Sort::isUninterpretedSortParameterized() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + return static_cast<SortType*>(d_type.get())->isParameterized(); +} + +std::vector<Sort> Sort::getUninterpretedSortParamSorts() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + std::vector<CVC4::Type> types = + static_cast<SortType*>(d_type.get())->getParamTypes(); + return typeVectorToSorts(types); +} + +/* Sort constructor sort ----------------------------------------------- */ + +std::string Sort::getSortConstructorName() const +{ + CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + return static_cast<SortConstructorType*>(d_type.get())->getName(); +} + +size_t Sort::getSortConstructorArity() const +{ + CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + return static_cast<SortConstructorType*>(d_type.get())->getArity(); +} + +/* Bit-vector sort ----------------------------------------------------- */ + +uint32_t Sort::getBVSize() const +{ + CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort."; + return static_cast<BitVectorType*>(d_type.get())->getSize(); +} + +/* Floating-point sort ------------------------------------------------- */ + +uint32_t Sort::getFPExponentSize() const +{ + CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + return static_cast<FloatingPointType*>(d_type.get())->getExponentSize(); +} + +uint32_t Sort::getFPSignificandSize() const +{ + CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + return static_cast<FloatingPointType*>(d_type.get())->getSignificandSize(); +} + +/* Datatype sort ------------------------------------------------------- */ + +std::vector<Sort> Sort::getDatatypeParamSorts() const +{ + CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; + std::vector<CVC4::Type> types = + static_cast<DatatypeType*>(d_type.get())->getParamTypes(); + return typeVectorToSorts(types); +} + +size_t Sort::getDatatypeArity() const +{ + CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; + return static_cast<DatatypeType*>(d_type.get())->getArity(); +} + +/* Tuple sort ---------------------------------------------------------- */ + +size_t Sort::getTupleLength() const +{ + CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; + return static_cast<DatatypeType*>(d_type.get())->getTupleLength(); +} + +std::vector<Sort> Sort::getTupleSorts() const +{ + CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; + std::vector<CVC4::Type> types = + static_cast<DatatypeType*>(d_type.get())->getTupleTypes(); + return typeVectorToSorts(types); +} + +/* --------------------------------------------------------------------- */ + +std::vector<Sort> Sort::typeVectorToSorts( + const std::vector<CVC4::Type>& types) const +{ + std::vector<Sort> res; + for (const CVC4::Type& t : types) + { + res.push_back(Sort(t)); + } + return res; +} + +/* --------------------------------------------------------------------- */ + std::ostream& operator<<(std::ostream& out, const Sort& s) { out << s.toString(); @@ -1140,6 +1321,13 @@ void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) d_dtype->addConstructor(*ctor.d_ctor); } +size_t DatatypeDecl::getNumConstructors() const +{ + return d_dtype->getNumConstructors(); +} + +bool DatatypeDecl::isParametric() const { return d_dtype->isParametric(); } + std::string DatatypeDecl::toString() const { std::stringstream ss; @@ -1344,6 +1532,13 @@ Term Datatype::getConstructorTerm(const std::string& name) const return d_dtype->getConstructor(name); } +size_t Datatype::getNumConstructors() const +{ + return d_dtype->getNumConstructors(); +} + +bool Datatype::isParametric() const { return d_dtype->isParametric(); } + Datatype::const_iterator Datatype::begin() const { return Datatype::const_iterator(*d_dtype, true); @@ -1492,49 +1687,49 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const Sort Solver::mkBitVectorSort(uint32_t size) const { - // CHECK: size > 0 + CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; return d_exprMgr->mkBitVectorType(size); } +Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const +{ + CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; + CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; + return d_exprMgr->mkFloatingPointType(exp, sig); +} + Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const { - // CHECK: num constructors > 0 + CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl) + << "a datatype declaration with at least one constructor"; return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype); } -Sort Solver::mkFunctionSort(Sort domain, Sort range) const +Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { - // CHECK: - // domain.isFirstClass() - // else "can not create function type for domain type that is not - // first class" - // CHECK: - // range.isFirstClass() - // else "can not create function type for range type that is not - // first class" - // CHECK: - // !range.isFunction() - // else "must flatten function types" - return d_exprMgr->mkFunctionType(*domain.d_type, *range.d_type); + 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. */ + return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type); } -Sort Solver::mkFunctionSort(const std::vector<Sort>& argSorts, Sort range) const +Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const { - // CHECK: argSorts.size() >= 1 - // CHECK: - // for (unsigned i = 0; i < argSorts.size(); ++ i) - // argSorts[i].isFirstClass() - // else "can not create function type for argument type that is not - // first class" - // CHECK: - // range.isFirstClass() - // else "can not create function type for range type that is not - // first class" - // CHECK: - // !range.isFunction() - // else "must flatten function types" - std::vector<Type> argTypes = sortVectorToTypes(argSorts); - return d_exprMgr->mkFunctionType(argTypes, *range.d_type); + 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].isFirstClass(), "parameter sort", sorts[i], i) + << "first-class sort as parameter 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. */ + std::vector<Type> argTypes = sortVectorToTypes(sorts); + return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type); } Sort Solver::mkParamSort(const std::string& symbol) const @@ -1544,12 +1739,14 @@ Sort Solver::mkParamSort(const std::string& symbol) const Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const { - // CHECK: sorts.size() >= 1 - // CHECK: - // for (unsigned i = 0; i < sorts.size(); ++ i) - // sorts[i].isFirstClass() - // else "can not create predicate type for argument type that is not - // first class" + 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].isFirstClass(), "parameter sort", sorts[i], i) + << "first-class sort as parameter sort for predicate sort"; + } std::vector<Type> types = sortVectorToTypes(sorts); return d_exprMgr->mkPredicateType(types); } @@ -1575,12 +1772,20 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const return d_exprMgr->mkSort(symbol); } +Sort Solver::mkSortConstructorSort(const std::string& symbol, + size_t arity) const +{ + return d_exprMgr->mkSortConstructor(symbol, arity); +} + Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const { - // CHECK: - // for (unsigned i = 0; i < sorts.size(); ++ i) - // !sorts[i].isFunctionLike() - // else "function-like types in tuples not allowed" + for (size_t i = 0, size = sorts.size(); i < size; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) + << "non-function-like sort as parameter sort for tuple sort"; + } std::vector<Type> types = sortVectorToTypes(sorts); return d_exprMgr->mkTupleType(types); } @@ -1767,42 +1972,41 @@ Term Solver::mkConst(RoundingMode rm) const Term Solver::mkConst(Kind kind, Sort arg) const { - CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET, kind, "EMPTY_SET"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED( - kind == UNINTERPRETED_CONSTANT, kind, "UNINTERPRETED_CONSTANT"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BOOLEAN, kind, "CONST_BOOLEAN"); + CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BOOLEAN, kind) << "CONST_BOOLEAN"; return d_exprMgr->mkConst<bool>(arg); } Term Solver::mkConst(Kind kind, const char* arg) const { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind, "CONST_STRING"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind, "CONST_STRING"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); + 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))); @@ -1816,11 +2020,10 @@ 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 { - CVC4_API_KIND_CHECK_EXPECTED( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); + 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))); @@ -1834,11 +2037,10 @@ Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const Term Solver::mkConst(Kind kind, uint32_t arg) const { - CVC4_API_KIND_CHECK_EXPECTED( - kind == ABSTRACT_VALUE || kind == CONST_RATIONAL - || kind == CONST_BITVECTOR, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR"); + 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))); @@ -1853,8 +2055,8 @@ Term Solver::mkConst(Kind kind, uint32_t arg) const Term Solver::mkConst(Kind kind, int32_t arg) const { CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL"); + kind) + << "ABSTRACT_VALUE or CONST_RATIONAL"; if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1865,8 +2067,8 @@ Term Solver::mkConst(Kind kind, int32_t arg) const Term Solver::mkConst(Kind kind, int64_t arg) const { CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL"); + kind) + << "ABSTRACT_VALUE or CONST_RATIONAL"; if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1877,8 +2079,8 @@ Term Solver::mkConst(Kind kind, int64_t arg) const Term Solver::mkConst(Kind kind, uint64_t arg) const { CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL, - kind, - "ABSTRACT_VALUE or CONST_RATIONAL"); + kind) + << "ABSTRACT_VALUE or CONST_RATIONAL"; if (kind == ABSTRACT_VALUE) { return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg))); @@ -1888,43 +2090,46 @@ Term Solver::mkConst(Kind kind, uint64_t arg) const Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind, "CONST_RATIONAL"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED( - kind == CONST_BITVECTOR, kind, "CONST_BITVECTOR"); + 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 { - CVC4_API_KIND_CHECK_EXPECTED( - kind == CONST_FLOATINGPOINT, kind, "CONST_FLOATINGPOINT"); + 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"); + arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3) + << "bit-vector constant"; return d_exprMgr->mkConst( CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>())); } @@ -1959,22 +2164,19 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const 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()."); + 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 - << ")"); + 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 << ")"; } } @@ -1985,32 +2187,28 @@ void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const 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"); + 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 << ")"); + 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( - kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, - kind, - "PI or REGEXP_EMPTY or REGEXP_SIGMA"); + kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) + << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { CVC4::Kind k = extToIntKind(kind); @@ -2023,8 +2221,8 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, Sort sort) const { - CVC4_API_KIND_CHECK_EXPECTED( - kind == SEP_NIL || kind == UNIVERSE_SET, kind, "SEP_NIL or UNIVERSE_SET"); + 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)); } @@ -2108,14 +2306,14 @@ std::vector<Expr> Solver::termVectorToExprs( OpTerm Solver::mkOpTerm(Kind kind, Kind k) { - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind, "CHAIN_OP"); + 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) { - CVC4_API_KIND_CHECK_EXPECTED( - kind == RECORD_UPDATE_OP, kind, "RECORD_UPDATE_OP"); + CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind) + << "RECORD_UPDATE_OP"; return d_exprMgr->mkConst(CVC4::RecordUpdate(arg)); } @@ -2160,8 +2358,8 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg)); break; default: - CVC4_API_KIND_CHECK_EXPECTED( - false, kind, "operator kind with uint32_t argument"); + CVC4_API_KIND_CHECK_EXPECTED(false, kind) + << "operator kind with uint32_t argument"; } Assert(!res.isNull()); return res; @@ -2199,8 +2397,8 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2)); break; default: - CVC4_API_KIND_CHECK_EXPECTED( - false, kind, "operator kind with two uint32_t arguments"); + CVC4_API_KIND_CHECK_EXPECTED(false, kind) + << "operator kind with two uint32_t arguments"; } Assert(!res.isNull()); return res; @@ -2315,16 +2513,7 @@ Sort Solver::declareDatatype( */ Term Solver::declareFun(const std::string& symbol, Sort sort) const { - // CHECK: - // sort.isFirstClass() - // else "can not create function type for range type that is not first class" - // CHECK: - // !sort.isFunction() - // else "must flatten function types" Type type = *sort.d_type; - // CHECK: - // !t.isFunction() || THEORY_UF not enabled - // else "Functions (of non-zero arity) cannot be declared in logic" return d_exprMgr->mkVar(symbol, type); } @@ -2335,26 +2524,21 @@ Term Solver::declareFun(const std::string& symbol, const std::vector<Sort>& sorts, Sort sort) const { - // CHECK: - // for (unsigned i = 0; i < sorts.size(); ++ i) - // sorts[i].isFirstClass() - // else "can not create function type for argument type that is not - // first class" - // CHECK: - // sort.isFirstClass() - // else "can not create function type for range type that is not first class" - // CHECK: - // !sort.isFunction() - // else "must flatten function types" + for (size_t i = 0, size = sorts.size(); i < size; ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + sorts[i].isFirstClass(), "parameter sort", sorts[i], 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"; + Assert(!sort.isFunction()); /* A function sort is not first-class. */ Type type = *sort.d_type; if (!sorts.empty()) { std::vector<Type> types = sortVectorToTypes(sorts); type = d_exprMgr->mkFunctionType(types, type); } - // CHECK: - // !t.isFunction() || THEORY_UF not enabled - // else "Functions (of non-zero arity) cannot be declared in logic" return d_exprMgr->mkVar(symbol, type); } @@ -2363,10 +2547,6 @@ Term Solver::declareFun(const std::string& symbol, */ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const { - // CHECK: - // - logic set? - // - !THEORY_UF && !THEORY_ARRAYS && !THEORY_DATATYPES && !THEORY_SETS - // else "Free sort symbols not allowed in logic" if (arity == 0) return d_exprMgr->mkSort(symbol); return d_exprMgr->mkSortConstructor(symbol, arity); } @@ -2386,27 +2566,26 @@ Term Solver::defineFun(const std::string& symbol, // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) // CHECK: not recursive - // CHECK: - // sort.isFirstClass() - // else "can not create function type for range type that is not first class" - // !sort.isFunction() - // else "must flatten function types" + CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) + << "first-class sort as codomain sort for function sort"; // CHECK: // for v in bound_vars: is bound var - std::vector<Type> types; - for (const Term& v : bound_vars) + std::vector<Type> domain_types; + for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { - types.push_back(v.d_expr->getType()); + CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + t.isFirstClass(), "sort of parameter", bound_vars[i], i) + << "first-class sort of parameter of defined function"; + domain_types.push_back(t); } - // CHECK: - // for (unsigned i = 0; i < types.size(); ++ i) - // sorts[i].isFirstClass() - // else "can not create function type for argument type that is not - // first class" + CVC4_API_CHECK(sort == term.getSort()) + << "Invalid sort of function body '" << term << "', expected '" << sort + << "'"; Type type = *sort.d_type; - if (!types.empty()) + if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(types, type); + type = d_exprMgr->mkFunctionType(domain_types, type); } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); @@ -2423,9 +2602,25 @@ Term Solver::defineFun(Term fun, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: - // - bound_vars matches sort of fun - // - expr matches sort of fun + CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; + 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( + domain_sorts[i] == bound_vars[i].getSort(), + "sort of parameter", + bound_vars[i], + i) + << "'" << domain_sorts[i] << "'"; + } + Sort codomain = fun.getSort().getFunctionCodomainSort(); + CVC4_API_CHECK(codomain == term.getSort()) + << "Invalid sort of function body '" << term << "', expected '" + << codomain << "'"; + // CHECK: not recursive // CHECK: // for v in bound_vars: is bound var @@ -2448,27 +2643,27 @@ Term Solver::defineFunRec(const std::string& symbol, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: - // sort.isFirstClass() - // else "can not create function type for range type that is not first class" - // !sort.isFunction() - // else "must flatten function types" + 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. */ // CHECK: // for v in bound_vars: is bound var - std::vector<Type> types; - for (const Term& v : bound_vars) + std::vector<Type> domain_types; + for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { - types.push_back(v.d_expr->getType()); + CVC4::Type t = bound_vars[i].d_expr->getType(); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + t.isFirstClass(), "sort of parameter", bound_vars[i], i) + << "first-class sort of parameter of defined function"; + domain_types.push_back(t); } - // CHECK: - // for (unsigned i = 0; i < types.size(); ++ i) - // sorts[i].isFirstClass() - // else "can not create function type for argument type that is not - // first class" + CVC4_API_CHECK(sort == term.getSort()) + << "Invalid sort of function body '" << term << "', expected '" << sort + << "'"; Type type = *sort.d_type; - if (!types.empty()) + if (!domain_types.empty()) { - type = d_exprMgr->mkFunctionType(types, type); + type = d_exprMgr->mkFunctionType(domain_types, type); } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); @@ -2486,9 +2681,24 @@ Term Solver::defineFunRec(Term fun, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: - // - bound_vars matches sort of fun - // - expr matches sort of fun + CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; + 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( + domain_sorts[i] == bound_vars[i].getSort(), + "sort of parameter", + bound_vars[i], + i) + << "'" << domain_sorts[i] << "'"; + } + Sort codomain = fun.getSort().getFunctionCodomainSort(); + CVC4_API_CHECK(codomain == term.getSort()) + << "Invalid sort of function body '" << term << "', expected '" + << codomain << "'"; // CHECK: // for v in bound_vars: is bound var std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); @@ -2512,10 +2722,34 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, // == NodeManager::fromExprManager(bv.getExprManager()) // NodeManager::fromExprManager(d_exprMgr) // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: - // - bound_vars matches sort of funs - // - exprs matches sort of funs - // CHECK: + size_t funs_size = funs.size(); + CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars) + << "'" << funs_size << "'"; + for (size_t j = 0; j < funs_size; ++j) + { + const Term& fun = funs[j]; + const std::vector<Term>& bvars = bound_vars[j]; + const Term& term = terms[j]; + + CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; + 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) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + domain_sorts[i] == bvars[i].getSort(), + "sort of parameter", + bvars[i], + i) + << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j << "]"; + } + Sort codomain = fun.getSort().getFunctionCodomainSort(); + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + codomain == term.getSort(), "sort of function body", term, j) + << "'" << codomain << "'"; + } // CHECK: // for bv in bound_vars (for v in bv): is bound var std::vector<Expr> efuns = termVectorToExprs(funs); |