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
/* -------------------------------------------------------------------------- */
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(); }
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)
{
}
if (d_type->isDatatype())
{
- // CHECK: is parametric?
DatatypeType* type = static_cast<DatatypeType*>(d_type.get());
return type->instantiate(tparams);
}
// 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();
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;
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);
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
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);
}
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);
}
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)));
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)));
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)));
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)));
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)));
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)));
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>()));
}
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 << ")";
}
}
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);
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));
}
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));
}
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;
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;
*/
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);
}
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);
}
*/
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);
}
// 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);
// == 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
// == 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);
// == 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);
// == 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);
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#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<Sort>{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<Sort>{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&);
+}
projects / cvc5.git / commitdiff