From: Aina Niemetz Date: Thu, 4 Oct 2018 23:47:43 +0000 (-0700) Subject: New C++ API: Add checks for Sorts. (#2519) X-Git-Tag: cvc5-1.0.0~4456 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=682a9ad81e7819a391b6eac49ea989d75c9774cc;p=cvc5.git New C++ API: Add checks for Sorts. (#2519) --- diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 596d0b515..cd34a5130 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -50,10 +50,8 @@ int main() // Creating a bit-vector type of width 32 Sort bitvector32 = slv.mkBitVectorSort(32); - std::cout << "bitvector32 " << bitvector32 << std::endl; // Variables Term x = slv.mkVar("x", bitvector32); - std::cout << "bitvector32 " << bitvector32 << std::endl; Term a = slv.mkVar("a", bitvector32); Term b = slv.mkVar("b", bitvector32); 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(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(d_type.get()); return type->getDatatype(); } Sort Sort::instantiate(const std::vector& params) const { - // CHECK: Is this a datatype/sort constructor sort? + CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) + << "Expected parametric datatype or sort constructor sort."; std::vector tparams; for (const Sort& s : params) { @@ -790,7 +823,6 @@ Sort Sort::instantiate(const std::vector& params) const } if (d_type->isDatatype()) { - // CHECK: is parametric? DatatypeType* type = static_cast(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(d_type.get())->getArity(); +} + +std::vector Sort::getFunctionDomainSorts() const +{ + CVC4_API_CHECK(isFunction()) << "Not a function sort."; + std::vector types = + static_cast(d_type.get())->getArgTypes(); + return typeVectorToSorts(types); +} + +Sort Sort::getFunctionCodomainSort() const +{ + CVC4_API_CHECK(isFunction()) << "Not a function sort."; + return static_cast(d_type.get())->getRangeType(); +} + +/* Array sort ---------------------------------------------------------- */ + +Sort Sort::getArrayIndexSort() const +{ + CVC4_API_CHECK(isArray()) << "Not an array sort."; + return static_cast(d_type.get())->getIndexType(); +} + +Sort Sort::getArrayElementSort() const +{ + CVC4_API_CHECK(isArray()) << "Not an array sort."; + return static_cast(d_type.get())->getConstituentType(); +} + +/* Set sort ------------------------------------------------------------ */ + +Sort Sort::getSetElementSort() const +{ + CVC4_API_CHECK(isSet()) << "Not a set sort."; + return static_cast(d_type.get())->getElementType(); +} + +/* Uninterpreted sort -------------------------------------------------- */ + +std::string Sort::getUninterpretedSortName() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + return static_cast(d_type.get())->getName(); +} + +bool Sort::isUninterpretedSortParameterized() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + return static_cast(d_type.get())->isParameterized(); +} + +std::vector Sort::getUninterpretedSortParamSorts() const +{ + CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; + std::vector types = + static_cast(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(d_type.get())->getName(); +} + +size_t Sort::getSortConstructorArity() const +{ + CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + return static_cast(d_type.get())->getArity(); +} + +/* Bit-vector sort ----------------------------------------------------- */ + +uint32_t Sort::getBVSize() const +{ + CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort."; + return static_cast(d_type.get())->getSize(); +} + +/* Floating-point sort ------------------------------------------------- */ + +uint32_t Sort::getFPExponentSize() const +{ + CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + return static_cast(d_type.get())->getExponentSize(); +} + +uint32_t Sort::getFPSignificandSize() const +{ + CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + return static_cast(d_type.get())->getSignificandSize(); +} + +/* Datatype sort ------------------------------------------------------- */ + +std::vector Sort::getDatatypeParamSorts() const +{ + CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; + std::vector types = + static_cast(d_type.get())->getParamTypes(); + return typeVectorToSorts(types); +} + +size_t Sort::getDatatypeArity() const +{ + CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; + return static_cast(d_type.get())->getArity(); +} + +/* Tuple sort ---------------------------------------------------------- */ + +size_t Sort::getTupleLength() const +{ + CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; + return static_cast(d_type.get())->getTupleLength(); +} + +std::vector Sort::getTupleSorts() const +{ + CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; + std::vector types = + static_cast(d_type.get())->getTupleTypes(); + return typeVectorToSorts(types); +} + +/* --------------------------------------------------------------------- */ + +std::vector Sort::typeVectorToSorts( + const std::vector& types) const +{ + std::vector 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& argSorts, Sort range) const +Sort Solver::mkFunctionSort(const std::vector& 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 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 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& 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 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& 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 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(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())); } @@ -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 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& 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 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 types; - for (const Term& v : bound_vars) + std::vector 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 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 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 types; - for (const Term& v : bound_vars) + std::vector 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 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 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 ebound_vars = termVectorToExprs(bound_vars); @@ -2512,10 +2722,34 @@ void Solver::defineFunsRec(const std::vector& 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& bvars = bound_vars[j]; + const Term& term = terms[j]; + + CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; + std::vector 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 efuns = termVectorToExprs(funs); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 3481fd953..fc07a1cd7 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -271,6 +271,12 @@ class CVC4_PUBLIC Sort */ bool isDatatype() const; + /** + * Is this a parametric datatype sort? + * @return true if the sort is a parametric datatype sort + */ + bool isParametricDatatype() const; + /** * Is this a function sort? * @return true if the sort is a function sort @@ -321,6 +327,34 @@ class CVC4_PUBLIC Sort */ bool isSortConstructor() const; + /** + * Is this a first-class sort? + * First-class sorts are sorts for which: + * (1) we handle equalities between terms of that type, and + * (2) they are allowed to be parameters of parametric sorts (e.g. index or + * element sorts of arrays). + * + * Examples of sorts that are not first-class include sort constructor sorts + * and regular expression sorts. + * + * @return true if this is a first-class sort + */ + bool isFirstClass() const; + + /** + * Is this a function-LIKE sort? + * + * Anything function-like except arrays (e.g., datatype selectors) is + * considered a function here. Function-like terms can not be the argument + * or return value for any term that is function-like. + * This is mainly to avoid higher order. + * + * Note that arrays are explicitly not considered function-like here. + * + * @return true if this is a function-like sort + */ + bool isFunctionLike() const; + /** * @return the underlying datatype of a datatype sort */ @@ -348,7 +382,118 @@ class CVC4_PUBLIC Sort // to the new API. !!! CVC4::Type getType(void) const; + /* Function sort ------------------------------------------------------- */ + + /** + * @return the arity of a function sort + */ + size_t getFunctionArity() const; + + /** + * @return the domain sorts of a function sort + */ + std::vector getFunctionDomainSorts() const; + + /** + * @return the codomain sort of a function sort + */ + Sort getFunctionCodomainSort() const; + + /* Array sort ---------------------------------------------------------- */ + + /** + * @return the array index sort of an array sort + */ + Sort getArrayIndexSort() const; + + /** + * @return the array element sort of an array element sort + */ + Sort getArrayElementSort() const; + + /* Set sort ------------------------------------------------------------ */ + + /** + * @return the element sort of a set sort + */ + Sort getSetElementSort() const; + + /* Uninterpreted sort -------------------------------------------------- */ + + /** + * @return the name of an uninterpreted sort + */ + std::string getUninterpretedSortName() const; + + /** + * @return true if an uninterpreted sort is parameterezied + */ + bool isUninterpretedSortParameterized() const; + + /** + * @return the parameter sorts of an uninterpreted sort + */ + std::vector getUninterpretedSortParamSorts() const; + + /* Sort constructor sort ----------------------------------------------- */ + + /** + * @return the name of a sort constructor sort + */ + std::string getSortConstructorName() const; + + /** + * @return the arity of a sort constructor sort + */ + size_t getSortConstructorArity() const; + + /* Bit-vector sort ----------------------------------------------------- */ + + /** + * @return the bit-width of the bit-vector sort + */ + uint32_t getBVSize() const; + + /* Floating-point sort ------------------------------------------------- */ + + /** + * @return the bit-width of the exponent of the floating-point sort + */ + uint32_t getFPExponentSize() const; + + /** + * @return the width of the significand of the floating-point sort + */ + uint32_t getFPSignificandSize() const; + + /* Datatype sort ------------------------------------------------------- */ + + /** + * @return the parameter sorts of a datatype sort + */ + std::vector getDatatypeParamSorts() const; + + /** + * @return the arity of a datatype sort + */ + size_t getDatatypeArity() const; + + /* Tuple sort ---------------------------------------------------------- */ + + /** + * @return the length of a tuple sort + */ + size_t getTupleLength() const; + + /** + * @return the element sorts of a tuple sort + */ + std::vector getTupleSorts() const; + private: + /* Helper to convert a vector of sorts into a vector of internal types. */ + std::vector typeVectorToSorts( + const std::vector& vector) const; /** * The interal type wrapped by this sort. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -914,6 +1059,12 @@ class CVC4_PUBLIC DatatypeDecl */ void addConstructor(const DatatypeConstructorDecl& ctor); + /** Get the number of constructors (so far) for this Datatype declaration. */ + size_t getNumConstructors() const; + + /** Is this Datatype declaration parametric? */ + bool isParametric() const; + /** * @return a string representation of this datatype declaration */ @@ -1165,6 +1316,12 @@ class CVC4_PUBLIC Datatype */ Term getConstructorTerm(const std::string& name) const; + /** Get the number of constructors for this Datatype. */ + size_t getNumConstructors() const; + + /** Is this Datatype parametric? */ + bool isParametric() const; + /** * @return a string representation of this datatype */ @@ -1421,6 +1578,13 @@ class CVC4_PUBLIC Solver */ Sort mkBitVectorSort(uint32_t size) const; + /** + * Create a floating-point sort. + * @param exp the bit-width of the exponent of the floating-point sort. + * @param sig the bit-width of the significand of the floating-point sort. + */ + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const; + /** * Create a datatype sort. * @param dtypedecl the datatype declaration from which the sort is created @@ -1431,18 +1595,18 @@ class CVC4_PUBLIC Solver /** * Create function sort. * @param domain the sort of the fuction argument - * @param range the sort of the function return value + * @param codomain the sort of the function return value * @return the function sort */ - Sort mkFunctionSort(Sort domain, Sort range) const; + Sort mkFunctionSort(Sort domain, Sort codomain) const; /** * Create function sort. - * @param argSorts the sort of the function arguments - * @param range the sort of the function return value + * @param sorts the sort of the function arguments + * @param codomain the sort of the function return value * @return the function sort */ - Sort mkFunctionSort(const std::vector& argSorts, Sort range) const; + Sort mkFunctionSort(const std::vector& sorts, Sort codomain) const; /** * Create a sort parameter. @@ -1480,6 +1644,14 @@ class CVC4_PUBLIC Solver */ Sort mkUninterpretedSort(const std::string& symbol) const; + /** + * Create a sort constructor sort. + * @param symbol the symbol of the sort + * @param arity the arity of the sort + * @return the sort constructor sort + */ + Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const; + /** * Create a tuple sort. * @param sorts of the elements of the tuple diff --git a/src/expr/type.cpp b/src/expr/type.cpp index a3e35e91f..fe8cc097b 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -72,6 +72,18 @@ bool Type::isWellFounded() const { return d_typeNode->isWellFounded(); } +bool Type::isFirstClass() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFirstClass(); +} + +bool Type::isFunctionLike() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFunctionLike(); +} + Expr Type::mkGroundTerm() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->mkGroundTerm().toExpr(); diff --git a/src/expr/type.h b/src/expr/type.h index b2ec1b024..4d22f1538 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -144,6 +144,33 @@ protected: */ bool isWellFounded() const; + /** + * Is this a first-class type? + * + * First-class types are types for which: + * (1) we handle equalities between terms of that type, and + * (2) they are allowed to be parameters of parametric types (e.g. index or + * element types of arrays). + * + * Examples of types that are not first-class include constructor types, + * selector types, tester types, regular expressions and SExprs. + */ + bool isFirstClass() const; + + /** + * Is this a function-LIKE type? + * + * Anything function-like except arrays (e.g., datatype selectors) is + * considered a function here. Function-like terms can not be the argument + * or return value for any term that is function-like. + * This is mainly to avoid higher order. + * + * Note that arrays are explicitly not considered function-like here. + * + * @return true if this is a function-like type + */ + bool isFunctionLike() const; + /** * Construct and return a ground term for this Type. Throws an * exception if this type is not well-founded. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b54290612..fd65f96b9 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -20,6 +20,7 @@ #include "expr/node_manager_attributes.h" #include "expr/type_properties.h" #include "options/base_options.h" +#include "options/bv_options.h" #include "options/expr_options.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" @@ -222,6 +223,7 @@ bool TypeNode::isClosedEnumerable() } bool TypeNode::isFirstClass() const { + (void)options::bitblastMode(); return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE && diff --git a/src/options/options.h b/src/options/options.h index 474fe3a4b..1b61994c5 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -33,12 +33,16 @@ namespace CVC4 { +namespace api { +class Solver; +} namespace options { struct OptionsHolder; class OptionsHandler; }/* CVC4::options namespace */ class CVC4_PUBLIC Options { + friend api::Solver; /** The struct that holds all option values. */ options::OptionsHolder* d_holder; diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index aa9248e6c..7c8e3d766 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -81,6 +81,7 @@ macro(cvc4_add_unit_test_white name output_dir) cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() +add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) add_subdirectory(expr) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt new file mode 100644 index 000000000..90d34f7c6 --- /dev/null +++ b/test/unit/api/CMakeLists.txt @@ -0,0 +1,4 @@ +#-----------------------------------------------------------------------------# +# Add unit tests + +cvc4_add_unit_test_black(api_guards_black api) diff --git a/test/unit/api/api_guards_black.h b/test/unit/api/api_guards_black.h new file mode 100644 index 000000000..777ce81f1 --- /dev/null +++ b/test/unit/api/api_guards_black.h @@ -0,0 +1,473 @@ +/********************* */ +/*! \file api_guards_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the guards of the C++ API functions. + ** + ** Black box testing of the guards of the C++ API functions. + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class ApiGuardsBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testSolverMkBitVectorSort(); + void testSolverMkFloatingPointSort(); + void testSolverMkDatatypeSort(); + void testSolverMkFunctionSort(); + void testSolverMkPredicateSort(); + void testSolverMkTupleSort(); + void testSortGetDatatype(); + void testSortInstantiate(); + void testSortGetFunctionArity(); + void testSortGetFunctionDomainSorts(); + void testSortGetFunctionCodomainSort(); + void testSortGetArrayIndexSort(); + void testSortGetArrayElementSort(); + void testSortGetSetElementSort(); + void testSortGetUninterpretedSortName(); + void testSortIsUninterpretedSortParameterized(); + void testSortGetUninterpretedSortParamSorts(); + void testSortGetUninterpretedSortConstructorName(); + void testSortGetUninterpretedSortConstructorArity(); + void testSortGetBVSize(); + void testSortGetFPExponentSize(); + void testSortGetFPSignificandSize(); + void testSortGetDatatypeParamSorts(); + void testSortGetDatatypeArity(); + void testSortGetTupleLength(); + void testSortGetTupleSorts(); + void testSolverDeclareFun(); + void testSolverDefineFun(); + void testSolverDefineFunRec(); + void testSolverDefineFunsRec(); + + private: + Solver d_solver; +}; + +void ApiGuardsBlack::setUp() {} + +void ApiGuardsBlack::tearDown() {} + +void ApiGuardsBlack::testSolverMkBitVectorSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); + TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverMkFloatingPointSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverMkDatatypeSort() +{ + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); + DatatypeDecl throwsDtypeSpec("list"); + TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverMkFunctionSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, + d_solver.getIntegerSort())); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, + d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), + d_solver.mkUninterpretedSort("u")}, + funSort2), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverMkPredicateSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver.mkPredicateSort({d_solver.getIntegerSort()})); + TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverMkTupleSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetDatatype() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortInstantiate() +{ + // instantiate parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING( + paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()})); + // instantiate non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS( + dtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetFunctionArity() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetFunctionDomainSorts() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetFunctionCodomainSort() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetArrayIndexSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort()); + TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetArrayElementSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort()); + TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetSetElementSort() +{ + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetUninterpretedSortName() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortIsUninterpretedSortParameterized() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetUninterpretedSortParamSorts() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetUninterpretedSortConstructorName() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetUninterpretedSortConstructorArity() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetBVSize() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetFPExponentSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetFPSignificandSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetDatatypeParamSorts() +{ + // create parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); + // create non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetDatatypeArity() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetTupleLength() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSortGetTupleSorts() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverDeclareFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort)); + TS_ASSERT_THROWS_NOTHING( + d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), + CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverDefineFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverDefineFunRec() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); +} + +void ApiGuardsBlack::testSolverDefineFunsRec() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term b4 = d_solver.mkBoundVar("b4", uSort); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term v4 = d_solver.mkVar("v4", uSort); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), + CVC4ApiException&); +}