Term p = slv.mkVar("p", intPred);
// Constants
- Term zero = slv.mkInteger(0);
- Term one = slv.mkInteger(1);
+ Term zero = slv.mkReal(0);
+ Term one = slv.mkReal(1);
// Terms
Term f_x = slv.mkTerm(APPLY_UF, f, x);
Term t = slv.mkTerm(
APPLY_CONSTRUCTOR,
consList.getConstructorTerm("cons"),
- slv.mkInteger(0),
+ slv.mkReal(0),
slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
std::cout << "t is " << t << std::endl
<< "sort of cons is "
<< paramConsList.getConstructorTerm("cons").getSort() << std::endl
<< std::endl;
- Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50));
+ Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50));
std::cout << "Assert " << assertion << std::endl;
slv.assertFormula(assertion);
std::cout << "Expect sat." << std::endl;
Term y = slv.mkVar("y", real);
// Constants
- Term three = slv.mkInteger(3);
- Term neg2 = slv.mkInteger(-2);
+ Term three = slv.mkReal(3);
+ Term neg2 = slv.mkReal(-2);
Term two_thirds = slv.mkReal(2, 3);
// Terms
// Find me an element in {1, 2} intersection {2, 3}, if there is one.
{
- Term one = slv.mkInteger(1);
- Term two = slv.mkInteger(2);
- Term three = slv.mkInteger(3);
+ Term one = slv.mkReal(1);
+ Term two = slv.mkReal(2);
+ Term three = slv.mkReal(3);
Term singleton_one = slv.mkTerm(SINGLETON, one);
Term singleton_two = slv.mkTerm(SINGLETON, two);
// Length of y: |y|
Term leny = slv.mkTerm(STRING_LENGTH, y);
// |y| >= 0
- Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
+ Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0));
// Regular expression: (ab[c-e]*f)|g|h
Term r = slv.mkTerm(REGEXP_UNION,
#include "util/result.h"
#include "util/utility.h"
+#include <cstring>
#include <sstream>
namespace CVC4 {
CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \
<< "', expected non-null object";
+#define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
+ CVC4_API_CHECK(arg != nullptr) \
+ << "Invalid null argument for '" << #arg << "'";
+
#define CVC4_API_KIND_CHECK(kind) \
CVC4_API_CHECK(isDefinedKind(kind)) \
<< "Invalid kind '" << kindToString(kind) << "'";
& 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 \
+#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
Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
+Sort::Sort() : d_type(new CVC4::Type()) {}
+
Sort::~Sort() {}
bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
+bool Sort::isNull() const { return d_type->isNull(); }
+
bool Sort::isBoolean() const { return d_type->isBoolean(); }
bool Sort::isInteger() const { return d_type->isInteger(); }
Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
{
+ CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort)
+ << "non-null index sort";
+ CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
+ << "non-null element sort";
return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
}
Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
{
+ CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
+ << "non-null codomain sort";
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)
<< "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].isNull(), "parameter sort", sorts[i], i)
+ << "non-null sort";
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.isNull(), codomain)
+ << "non-null codomain 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. */
<< "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].isNull(), "parameter sort", sorts[i], i)
+ << "non-null sort";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
<< "first-class sort as parameter sort for predicate sort";
const std::vector<std::pair<std::string, Sort>>& fields) const
{
std::vector<std::pair<std::string, Type>> f;
+ size_t i = 0;
for (const auto& p : fields)
{
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !p.second.isNull(), "parameter sort", p.second, i)
+ << "non-null sort";
+ i += 1;
f.emplace_back(p.first, *p.second.d_type);
}
return d_exprMgr->mkRecordType(Record(f));
Sort Solver::mkSetSort(Sort elemSort) const
{
+ CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
+ << "non-null element sort";
return d_exprMgr->mkSetType(*elemSort.d_type);
}
{
for (size_t i = 0, size = sorts.size(); i < size; ++i)
{
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !sorts[i].isNull(), "parameter sort", sorts[i], i)
+ << "non-null sort";
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";
Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); }
-Term Solver::mkInteger(const char* s, uint32_t base) const
-{
- return d_exprMgr->mkConst(Rational(s, base));
-}
-
-Term Solver::mkInteger(const std::string& s, uint32_t base) const
-{
- return d_exprMgr->mkConst(Rational(s, base));
-}
-
-Term Solver::mkInteger(int32_t val) const
-{
- return d_exprMgr->mkConst(Rational(val));
-}
-
-Term Solver::mkInteger(uint32_t val) const
-{
- return d_exprMgr->mkConst(Rational(val));
-}
-
-Term Solver::mkInteger(int64_t val) const
+Term Solver::mkPi() const
{
- return d_exprMgr->mkConst(Rational(val));
+ return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
}
-Term Solver::mkInteger(uint64_t val) const
+template <typename T>
+Term Solver::mkConstHelper(T t) const
{
- return d_exprMgr->mkConst(Rational(val));
+ try
+ {
+ Term res = d_exprMgr->mkConst(t);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (CVC4::TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
-Term Solver::mkPi() const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkRealFromStrHelper(std::string s) const
{
- return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+ try
+ {
+ /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+ * throws an std::invalid_argument exception. For consistency, we treat it
+ * as invalid. */
+ CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+ << "a string representing an integer, real or rational value.";
+ CVC4::Rational r = s.find('/') != std::string::npos
+ ? CVC4::Rational(s)
+ : CVC4::Rational::fromDecimal(s);
+ return mkConstHelper<CVC4::Rational>(r);
+ }
+ catch (std::invalid_argument& e)
+ {
+ throw CVC4ApiException(e.what());
+ }
}
-Term Solver::mkReal(const char* s, uint32_t base) const
+Term Solver::mkReal(const char* s) const
{
- return d_exprMgr->mkConst(Rational(s, base));
+ CVC4_API_ARG_CHECK_NOT_NULL(s);
+ return mkRealFromStrHelper(std::string(s));
}
-Term Solver::mkReal(const std::string& s, uint32_t base) const
+Term Solver::mkReal(const std::string& s) const
{
- return d_exprMgr->mkConst(Rational(s, base));
+ return mkRealFromStrHelper(s);
}
Term Solver::mkReal(int32_t val) const
{
- return d_exprMgr->mkConst(Rational(val));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
}
Term Solver::mkReal(int64_t val) const
{
- return d_exprMgr->mkConst(Rational(val));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
}
Term Solver::mkReal(uint32_t val) const
{
- return d_exprMgr->mkConst(Rational(val));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
}
Term Solver::mkReal(uint64_t val) const
{
- return d_exprMgr->mkConst(Rational(val));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
}
Term Solver::mkReal(int32_t num, int32_t den) const
{
- return d_exprMgr->mkConst(Rational(num, den));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
Term Solver::mkReal(int64_t num, int64_t den) const
{
- return d_exprMgr->mkConst(Rational(num, den));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
Term Solver::mkReal(uint32_t num, uint32_t den) const
{
- return d_exprMgr->mkConst(Rational(num, den));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
Term Solver::mkReal(uint64_t num, uint64_t den) const
{
- return d_exprMgr->mkConst(Rational(num, den));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
}
Term Solver::mkRegexpEmpty() const
{
- return d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<Expr>());
+ try
+ {
+ Term res =
+ d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkRegexpSigma() const
{
- return d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<Expr>());
+ try
+ {
+ Term res =
+ d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkEmptySet(Sort s) const
{
- return d_exprMgr->mkConst(EmptySet(*s.d_type));
+ CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
+ << "null sort or set sort";
+ return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
}
Term Solver::mkSepNil(Sort sort) const
{
- return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkString(const char* s) const
{
- return d_exprMgr->mkConst(String(s));
+ return mkConstHelper<CVC4::String>(CVC4::String(s));
}
Term Solver::mkString(const std::string& s) const
{
- return d_exprMgr->mkConst(String(s));
+ return mkConstHelper<CVC4::String>(CVC4::String(s));
}
Term Solver::mkString(const unsigned char c) const
{
- return d_exprMgr->mkConst(String(std::string(1, c)));
+ return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
}
Term Solver::mkString(const std::vector<unsigned>& s) const
{
- return d_exprMgr->mkConst(String(s));
+ return mkConstHelper<CVC4::String>(CVC4::String(s));
}
Term Solver::mkUniverseSet(Sort sort) const
{
- return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res =
+ d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
-Term Solver::mkBitVector(uint32_t size) const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
{
- return d_exprMgr->mkConst(BitVector(size));
+ CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
+ return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
}
-Term Solver::mkBitVector(uint32_t size, uint32_t val) const
+Term Solver::mkBitVector(uint32_t size, uint64_t val) const
{
- return d_exprMgr->mkConst(BitVector(size, val));
+ return mkBVFromIntHelper(size, val);
}
-Term Solver::mkBitVector(uint32_t size, uint64_t val) const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
{
- return d_exprMgr->mkConst(BitVector(size, val));
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+ CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 16, s) << "base 2 or 16";
+ return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+ }
+ catch (std::invalid_argument& e)
+ {
+ throw CVC4ApiException(e.what());
+ }
}
Term Solver::mkBitVector(const char* s, uint32_t base) const
{
- return d_exprMgr->mkConst(BitVector(s, base));
+ CVC4_API_ARG_CHECK_NOT_NULL(s);
+ return mkBVFromStrHelper(std::string(s), base);
}
-Term Solver::mkBitVector(std::string& s, uint32_t base) const
+Term Solver::mkBitVector(const std::string& s, uint32_t base) const
{
- return d_exprMgr->mkConst(BitVector(s, base));
+ return mkBVFromStrHelper(s, base);
}
Term Solver::mkConst(RoundingMode rm) const
{
- return d_exprMgr->mkConst(s_rmodes.at(rm));
+ try
+ {
+ return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+ }
+ catch (std::invalid_argument& e)
+ {
+ throw CVC4ApiException(e.what());
+ }
}
Term Solver::mkConst(Kind kind, Sort arg) const
{
- CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET, kind) << "EMPTY_SET";
- return d_exprMgr->mkConst(CVC4::EmptySet(*arg.d_type));
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(
+ (kind == EMPTYSET && arg.isNull()) || arg.isSet(), arg)
+ << "null sort or set sort";
+ CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET || kind == UNIVERSE_SET, kind)
+ << "EMPTY_SET or UNIVERSE_SET";
+ if (kind == EMPTYSET)
+ {
+ return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*arg.d_type));
+ }
+ else
+ {
+ Term res = d_exprMgr->mkNullaryOperator(*arg.d_type, extToIntKind(kind));
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const
{
+ CVC4_API_ARG_CHECK_EXPECTED(!arg1.isNull(), arg1) << "non-null sort";
CVC4_API_KIND_CHECK_EXPECTED(kind == UNINTERPRETED_CONSTANT, kind)
<< "UNINTERPRETED_CONSTANT";
- return d_exprMgr->mkConst(CVC4::UninterpretedConstant(*arg1.d_type, arg2));
+ return mkConstHelper<CVC4::UninterpretedConstant>(
+ 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";
- return d_exprMgr->mkConst<bool>(arg);
+ return mkConstHelper<bool>(arg);
+}
+
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const
+{
+ CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+ CVC4_API_KIND_CHECK_EXPECTED(
+ kind == ABSTRACT_VALUE || kind == CONST_RATIONAL || kind == CONST_STRING,
+ kind)
+ << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_STRING";
+ if (kind == ABSTRACT_VALUE)
+ {
+ try
+ {
+ return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(s, 10)));
+ // do not call getType(), for abstract values, type can not be computed
+ // until it is substituted away
+ }
+ catch (std::invalid_argument& e)
+ {
+ throw CVC4ApiException(e.what());
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+ }
+ else if (kind == CONST_RATIONAL)
+ {
+ return mkRealFromStrHelper(s);
+ }
+ return mkConstHelper<CVC4::String>(CVC4::String(s));
}
Term Solver::mkConst(Kind kind, const char* arg) const
{
- CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind) << "CONST_STRING";
- return d_exprMgr->mkConst(CVC4::String(arg));
+ CVC4_API_ARG_CHECK_NOT_NULL(arg);
+ return mkConstFromStrHelper(kind, std::string(arg));
}
Term Solver::mkConst(Kind kind, const std::string& arg) const
{
- CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind) << "CONST_STRING";
- return d_exprMgr->mkConst(CVC4::String(arg));
+ return mkConstFromStrHelper(kind, arg);
+}
+
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const
+{
+ CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+ CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind)
+ << "CONST_BITVECTOR";
+ return mkBVFromStrHelper(s, a);
}
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";
- if (kind == ABSTRACT_VALUE)
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
- }
- if (kind == CONST_RATIONAL)
- {
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
- }
- return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+ CVC4_API_ARG_CHECK_NOT_NULL(arg1);
+ return mkConstFromStrHelper(kind, std::string(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";
- if (kind == ABSTRACT_VALUE)
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
- }
- if (kind == CONST_RATIONAL)
- {
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
- }
- return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+ return mkConstFromStrHelper(kind, arg1, arg2);
}
-Term Solver::mkConst(Kind kind, uint32_t arg) const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+template <typename T>
+Term Solver::mkConstFromIntHelper(Kind kind, T a) const
{
- CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
- || kind == CONST_BITVECTOR,
+ CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
kind)
- << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR";
+ << "ABSTRACT_VALUE or CONST_RATIONAL";
if (kind == ABSTRACT_VALUE)
{
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
- }
- if (kind == CONST_RATIONAL)
- {
- return d_exprMgr->mkConst(CVC4::Rational(arg));
+ try
+ {
+ return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(a)));
+ // do not call getType(), for abstract values, type can not be computed
+ // until it is substituted away
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
- return d_exprMgr->mkConst(CVC4::BitVector(arg));
+ return mkConstHelper<CVC4::Rational>(CVC4::Rational(a));
}
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";
- if (kind == ABSTRACT_VALUE)
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
- }
- return d_exprMgr->mkConst(CVC4::Rational(arg));
+ return mkConstFromIntHelper<int64_t>(kind, static_cast<int64_t>(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";
- if (kind == ABSTRACT_VALUE)
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
- }
- return d_exprMgr->mkConst(CVC4::Rational(arg));
+ return mkConstFromIntHelper<int64_t>(kind, arg);
+}
+
+Term Solver::mkConst(Kind kind, uint32_t arg) const
+{
+ return mkConstFromIntHelper<uint64_t>(kind, static_cast<uint64_t>(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";
- if (kind == ABSTRACT_VALUE)
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
- }
- return d_exprMgr->mkConst(CVC4::Rational(arg));
+ return mkConstFromIntHelper<uint64_t>(kind, arg);
}
Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
{
- CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
- << "CONST_RATIONAL";
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+ CVC4_API_KIND_CHECK_EXPECTED(
+ kind == CONST_BITVECTOR || kind == CONST_RATIONAL, kind)
+ << "CONST_BITVECTOR or CONST_RATIONAL";
+ if (kind == CONST_BITVECTOR)
+ {
+ return mkBVFromIntHelper(arg1, arg2);
+ }
+ return mkConstHelper<CVC4::Rational>(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";
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+ return mkConstHelper<CVC4::Rational>(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";
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+ return mkConstHelper<CVC4::Rational>(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";
- return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+ return mkConstHelper<CVC4::Rational>(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";
- return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+ return mkBVFromIntHelper(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_ARG_CHECK_EXPECTED(arg1 > 0, arg1) << "a value > 0";
+ CVC4_API_ARG_CHECK_EXPECTED(arg2 > 0, arg2) << "a value > 0";
+ uint32_t bw = arg1 + arg2;
+ CVC4_API_ARG_CHECK_EXPECTED(bw == arg3.getSort().getBVSize(), arg3)
+ << "a bit-vector constant with bit-width '" << bw << "'";
+ CVC4_API_ARG_CHECK_EXPECTED(!arg3.isNull(), arg3) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(
arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3)
<< "bit-vector constant";
- return d_exprMgr->mkConst(
+ return mkConstHelper<CVC4::FloatingPoint>(
CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
}
Term Solver::mkVar(const std::string& symbol, Sort sort) const
{
- return d_exprMgr->mkVar(symbol, *sort.d_type);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
-Term Solver::mkVar(Sort sort) const { return d_exprMgr->mkVar(*sort.d_type); }
+Term Solver::mkVar(Sort sort) const
+{
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res = d_exprMgr->mkVar(*sort.d_type);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const
{
- return d_exprMgr->mkBoundVar(symbol, *sort.d_type);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkBoundVar(Sort sort) const
{
- return d_exprMgr->mkBoundVar(*sort.d_type);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ Term res = d_exprMgr->mkBoundVar(*sort.d_type);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
/* Create terms */
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";
- if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+ try
{
- CVC4::Kind k = extToIntKind(kind);
- Assert(isDefinedIntKind(k));
- return d_exprMgr->mkExpr(k, std::vector<Expr>());
+ CVC4_API_KIND_CHECK_EXPECTED(
+ kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+ << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+ Term res;
+ if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+ {
+ CVC4::Kind k = extToIntKind(kind);
+ Assert(isDefinedIntKind(k));
+ res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+ }
+ else
+ {
+ Assert(kind == PI);
+ res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+ }
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
}
- Assert(kind == PI);
- return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
}
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";
- return d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
+ try
+ {
+ CVC4_API_KIND_CHECK_EXPECTED(kind == SEP_NIL, kind) << "SEP_NIL";
+ Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(Kind kind, Term child) const
{
- checkMkTerm(kind, 1);
- return d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+ checkMkTerm(kind, 1);
+ Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
{
- checkMkTerm(kind, 2);
- return d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ checkMkTerm(kind, 2);
+ Term res =
+ d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
{
- checkMkTerm(kind, 3);
- std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
- CVC4::Kind k = extToIntKind(kind);
- Assert(isDefinedIntKind(k));
- return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
- : d_exprMgr->mkExpr(k, echildren);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+ checkMkTerm(kind, 3);
+ std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
+ CVC4::Kind k = extToIntKind(kind);
+ Assert(isDefinedIntKind(k));
+ Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
+ : d_exprMgr->mkExpr(k, echildren);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
{
- checkMkTerm(kind, children.size());
- std::vector<Expr> echildren = termVectorToExprs(children);
- CVC4::Kind k = extToIntKind(kind);
- Assert(isDefinedIntKind(k));
- return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
- : d_exprMgr->mkExpr(k, echildren);
-}
-
-Term Solver::mkTerm(OpTerm opTerm) const
-{
- checkMkOpTerm(opTerm, 0);
- return d_exprMgr->mkExpr(*opTerm.d_expr);
+ try
+ {
+ for (size_t i = 0, size = children.size(); i < size; ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !children[i].isNull(), "parameter term", children[i], i)
+ << "non-null term";
+ }
+ checkMkTerm(kind, children.size());
+ std::vector<Expr> echildren = termVectorToExprs(children);
+ CVC4::Kind k = extToIntKind(kind);
+ Assert(isDefinedIntKind(k));
+ Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
+ : d_exprMgr->mkExpr(k, echildren);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(OpTerm opTerm, Term child) const
{
- checkMkOpTerm(opTerm, 1);
- return d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+ checkMkOpTerm(opTerm, 1);
+ Term res = d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
{
- checkMkOpTerm(opTerm, 2);
- return d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ checkMkOpTerm(opTerm, 2);
+ Term res =
+ d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
{
- checkMkOpTerm(opTerm, 3);
- return d_exprMgr->mkExpr(
- *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ try
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+ checkMkOpTerm(opTerm, 3);
+ Term res = d_exprMgr->mkExpr(
+ *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
{
- checkMkOpTerm(opTerm, children.size());
- std::vector<Expr> echildren = termVectorToExprs(children);
- return d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+ try
+ {
+ for (size_t i = 0, size = children.size(); i < size; ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ !children[i].isNull(), "parameter term", children[i], i)
+ << "non-null term";
+ }
+ checkMkOpTerm(opTerm, children.size());
+ std::vector<Expr> echildren = termVectorToExprs(children);
+ Term res = d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
std::vector<Expr> Solver::termVectorToExprs(
OpTerm Solver::mkOpTerm(Kind kind, Kind k)
{
CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
- return d_exprMgr->mkConst(CVC4::Chain(extToIntKind(k)));
+ return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
}
OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
{
CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
<< "RECORD_UPDATE_OP";
- return d_exprMgr->mkConst(CVC4::RecordUpdate(arg));
+ return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
+ .d_expr.get();
}
OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
OpTerm res;
switch (kind)
{
- case DIVISIBLE_OP: res = d_exprMgr->mkConst(CVC4::Divisible(arg)); break;
+ case DIVISIBLE_OP:
+ res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+ break;
case BITVECTOR_REPEAT_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorRepeat(arg));
+ res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+ .d_expr.get();
break;
case BITVECTOR_ZERO_EXTEND_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorZeroExtend(arg));
+ res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+ CVC4::BitVectorZeroExtend(arg))
+ .d_expr.get();
break;
case BITVECTOR_SIGN_EXTEND_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorSignExtend(arg));
+ res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+ CVC4::BitVectorSignExtend(arg))
+ .d_expr.get();
break;
case BITVECTOR_ROTATE_LEFT_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorRotateLeft(arg));
+ res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+ CVC4::BitVectorRotateLeft(arg))
+ .d_expr.get();
break;
case BITVECTOR_ROTATE_RIGHT_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorRotateRight(arg));
+ res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+ CVC4::BitVectorRotateRight(arg))
+ .d_expr.get();
break;
case INT_TO_BITVECTOR_OP:
- res = d_exprMgr->mkConst(CVC4::IntToBitVector(arg));
+ res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_UBV_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToUBV(arg));
+ res = *mkConstHelper<CVC4::FloatingPointToUBV>(
+ CVC4::FloatingPointToUBV(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_UBV_TOTAL_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToUBVTotal(arg));
+ res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+ CVC4::FloatingPointToUBVTotal(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_SBV_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToSBV(arg));
+ res = *mkConstHelper<CVC4::FloatingPointToSBV>(
+ CVC4::FloatingPointToSBV(arg))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_SBV_TOTAL_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToSBVTotal(arg));
+ res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+ CVC4::FloatingPointToSBVTotal(arg))
+ .d_expr.get();
break;
case TUPLE_UPDATE_OP:
- res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg));
+ res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
+ .d_expr.get();
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
switch (kind)
{
case BITVECTOR_EXTRACT_OP:
- res = d_exprMgr->mkConst(CVC4::BitVectorExtract(arg1, arg2));
+ res = *mkConstHelper<CVC4::BitVectorExtract>(
+ CVC4::BitVectorExtract(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
- res =
- d_exprMgr->mkConst(CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+ CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
- res =
- d_exprMgr->mkConst(CVC4::FloatingPointToFPFloatingPoint(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+ CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_REAL_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToFPReal(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+ CVC4::FloatingPointToFPReal(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
- res = d_exprMgr->mkConst(
- CVC4::FloatingPointToFPSignedBitVector(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+ CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
- res = d_exprMgr->mkConst(
- CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+ CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
+ .d_expr.get();
break;
case FLOATINGPOINT_TO_FP_GENERIC_OP:
- res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2));
+ res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+ CVC4::FloatingPointToFPGeneric(arg1, arg2))
+ .d_expr.get();
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
*/
Sort(const CVC4::Type& t);
+ /**
+ * Constructor.
+ */
+ Sort();
+
/**
* Destructor.
*/
*/
bool operator!=(const Sort& s) const;
+ /**
+ * @return true if this Sort is a null sort.
+ */
+ bool isNull() const;
+
/**
* Is this a Boolean sort?
* @return true if the sort is a Boolean sort
*/
Term mkTerm(Kind kind, const std::vector<Term>& children) const;
- /**
- * Create term with no children from a given operator term.
- * Create operator terms with mkOpTerm().
- * @param the operator term
- * @return the Term
- */
- Term mkTerm(OpTerm opTerm) const;
-
/**
* Create unary term from a given operator term.
* Create operator terms with mkOpTerm().
*/
Term mkBoolean(bool val) const;
- /**
- * Create an Integer constant.
- * @param s the string represetntation of the constant
- * @param base the base of the string representation
- * @return the Integer constant
- */
- Term mkInteger(const char* s, uint32_t base = 10) const;
-
- /**
- * Create an Integer constant.
- * @param s the string represetntation of the constant
- * @param base the base of the string representation
- * @return the Integer constant
- */
- Term mkInteger(const std::string& s, uint32_t base = 10) const;
-
- /**
- * Create an Integer constant.
- * @param val the value of the constant
- * @return the Integer constant
- */
- Term mkInteger(int32_t val) const;
-
- /**
- * Create an Integer constant.
- * @param val the value of the constant
- * @return the Integer constant
- */
- Term mkInteger(uint32_t val) const;
-
- /**
- * Create an Integer constant.
- * @param val the value of the constant
- * @return the Integer constant
- */
- Term mkInteger(int64_t val) const;
-
- /**
- * Create an Integer constant.
- * @param val the value of the constant
- * @return the Integer constant
- */
- Term mkInteger(uint64_t val) const;
-
/**
* Create a constant representing the number Pi.
* @return a constant representing Pi
Term mkPi() const;
/**
- * Create an Real constant.
- * @param s the string represetntation of the constant
- * @param base the base of the string representation
- * @return the Real constant
+ * Create a real constant.
+ * @param s the string representation of the constant, may represent an
+ * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
+ * @return a constant of sort Real or Integer (if 's' represents an integer)
*/
- Term mkReal(const char* s, uint32_t base = 10) const;
+ Term mkReal(const char* s) const;
/**
- * Create an Real constant.
- * @param s the string represetntation of the constant
- * @param base the base of the string representation
- * @return the Real constant
+ * Create a real constant.
+ * @param s the string representation of the constant, may represent an
+ * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
+ * @return a constant of sort Real or Integer (if 's' represents an integer)
*/
- Term mkReal(const std::string& s, uint32_t base = 10) const;
+ Term mkReal(const std::string& s) const;
/**
- * Create an Real constant.
+ * Create a real constant from an integer.
* @param val the value of the constant
- * @return the Real constant
+ * @return a constant of sort Integer
*/
Term mkReal(int32_t val) const;
/**
- * Create an Real constant.
+ * Create a real constant from an integer.
* @param val the value of the constant
- * @return the Real constant
+ * @return a constant of sort Integer
*/
Term mkReal(int64_t val) const;
/**
- * Create an Real constant.
+ * Create a real constant from an unsigned integer.
* @param val the value of the constant
- * @return the Real constant
+ * @return a constant of sort Integer
*/
Term mkReal(uint32_t val) const;
/**
- * Create an Real constant.
+ * Create a real constant from an unsigned integer.
* @param val the value of the constant
- * @return the Real constant
+ * @return a constant of sort Integer
*/
Term mkReal(uint64_t val) const;
/**
- * Create an Rational constant.
+ * Create a real constant from a rational.
* @param num the value of the numerator
* @param den the value of the denominator
- * @return the Rational constant
+ * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
*/
Term mkReal(int32_t num, int32_t den) const;
/**
- * Create an Rational constant.
+ * Create a real constant from a rational.
* @param num the value of the numerator
* @param den the value of the denominator
- * @return the Rational constant
+ * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
*/
Term mkReal(int64_t num, int64_t den) const;
/**
- * Create an Rational constant.
+ * Create a real constant from a rational.
* @param num the value of the numerator
* @param den the value of the denominator
- * @return the Rational constant
+ * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
*/
Term mkReal(uint32_t num, uint32_t den) const;
/**
- * Create an Rational constant.
+ * Create a real constant from a rational.
* @param num the value of the numerator
* @param den the value of the denominator
- * @return the Rational constant
+ * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
*/
Term mkReal(uint64_t num, uint64_t den) const;
*/
Term mkUniverseSet(Sort sort) const;
- /**
- * Create a bit-vector constant of given size with value 0.
- * @param size the bit-width of the bit-vector sort
- * @return the bit-vector constant
- */
- Term mkBitVector(uint32_t size) const;
-
- /**
- * Create a bit-vector constant of given size and value.
- * @param size the bit-width of the bit-vector sort
- * @param val the value of the constant
- * @return the bit-vector constant
- */
- Term mkBitVector(uint32_t size, uint32_t val) const;
-
/**
* Create a bit-vector constant of given size and value.
* @param size the bit-width of the bit-vector sort
* @param base the base of the string representation
* @return the bit-vector constant
*/
- Term mkBitVector(std::string& s, uint32_t base = 2) const;
+ Term mkBitVector(const std::string& s, uint32_t base = 2) const;
/**
* Create constant of kind:
/**
* Create constant of kind:
+ * - ABSTRACT_VALUE
+ * - CONST_RATIONAL (for integers, reals)
* - CONST_STRING
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
/**
* Create constant of kind:
+ * - ABSTRACT_VALUE
+ * - CONST_RATIONAL (for integers, reals)
* - CONST_STRING
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
/**
* Create constant of kind:
- * - ABSTRACT_VALUE
- * - CONST_RATIONAL (for integers, reals)
* - CONST_BITVECTOR
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
* @param arg1 the first argument to this kind
* @param arg2 the second argument to this kind
*/
- Term mkConst(Kind kind, const char* arg1, uint32_t arg2 = 10) const;
+ Term mkConst(Kind kind, const char* arg1, uint32_t arg2) const;
/**
* Create constant of kind:
- * - ABSTRACT_VALUE
- * - CONST_RATIONAL (for integers, reals)
* - CONST_BITVECTOR
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
* @param arg1 the first argument to this kind
* @param arg2 the second argument to this kind
*/
- Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2 = 10) const;
+ Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const;
/**
* Create constant of kind:
* - ABSTRACT_VALUE
* - CONST_RATIONAL (for integers, reals)
- * - CONST_BITVECTOR
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
* @param arg the argument to this kind
/**
* Create constant of kind:
* - CONST_RATIONAL (for rationals)
+ * - CONST_BITVECTOR
* See enum Kind for a description of the parameters.
* @param kind the kind of the constant
* @param arg1 the first argument to this kind
void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const;
/* Helper to check for API misuse in mkOpTerm functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
+ /* Helper for mk-functions that call d_exprMgr->mkConst(). */
+ template <typename T> Term mkConstHelper(T t) const;
+ /* Helper for mkReal functions that take a string as argument. */
+ Term mkRealFromStrHelper(std::string s) const;
+ /* Helper for mkBitVector functions that take a string as argument. */
+ Term mkBVFromStrHelper(std::string s, uint32_t base) const;
+ /* Helper for mkBitVector functions that take an integer as argument. */
+ Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
+ /* Helper for mkConst functions that take a string as argument. */
+ Term mkConstFromStrHelper(Kind kind, std::string s) const;
+ Term mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const;
+ /* Helper for mkConst functions that take an integer as argument. */
+ template <typename T>
+ Term mkConstFromIntHelper(Kind kind, T a) const;
/* The expression manager of this solver. */
std::unique_ptr<ExprManager> d_exprMgr;
* Parameters: 1
* -[1]: Index of the abstract value
* Create with:
- * mkConst(Kind kind, const char* s, uint32_t base = 10)
- * mkConst(Kind kind, const std::string& s, uint32_t base = 10)
+ * mkConst(Kind kind, const char* arg)
+ * mkConst(Kind kind, const std::string& arg)
* mkConst(Kind kind, uint32_t arg)
* mkConst(Kind kind, int32_t arg)
* mkConst(Kind kind, int64_t arg)
* Parameters:
* See mkBitVector().
* Create with:
- * mkBitVector(uint32_t size)
- * mkBitVector(uint32_t size, uint32_t val)
* mkBitVector(uint32_t size, uint64_t val)
* mkBitVector(const char* s, uint32_t base = 2)
* mkBitVector(std::string& s, uint32_t base = 2)
* mkConst(Kind kind, const char* s, uint32_t base = 10)
* mkConst(Kind kind, const std::string& s, uint32_t base = 10)
- * mkConst(Kind kind, uint32_t arg)
* mkConst(Kind kind, uint32_t arg1, uint64_t arg2)
*/
CONST_BITVECTOR,
* All set variables must be interpreted as subsets of it.
* Create with:
* mkUniverseSet(Sort sort)
- * mkTerm(Kind kind, Sort sort)
+ * mkConst(Kind kind, Sort sort)
*/
UNIVERSE_SET,
/**
void testMkFloatingPointSort();
void testMkDatatypeSort();
void testMkFunctionSort();
+ void testMkOpTerm();
void testMkParamSort();
void testMkPredicateSort();
void testMkRecordSort();
void testMkSetSort();
void testMkSortConstructorSort();
- void testMkUninterpretedSort();
void testMkTupleSort();
+ void testMkUninterpretedSort();
+
+ void testMkBitVector();
+ void testMkBoundVar();
+ void testMkBoolean();
+ void testMkConst();
+ void testMkEmptySet();
+ void testMkFalse();
+ void testMkPi();
+ void testMkReal();
+ void testMkRegexpEmpty();
+ void testMkRegexpSigma();
+ void testMkSepNil();
+ void testMkString();
+ void testMkUniverseSet();
+ void testMkTerm();
+ void testMkTrue();
+ void testMkVar();
void testDeclareFun();
void testDefineFun();
void testDefineFunRec();
void testDefineFunsRec();
- void testMkRegexpEmpty();
- void testMkRegexpSigma();
-
private:
Solver d_solver;
};
CVC4ApiException&);
}
+void SolverBlack::testMkBitVector()
+{
+ uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
+ uint64_t val2 = 2;
+ TS_ASSERT_THROWS(d_solver.mkBitVector(size0, val1), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkBitVector(size0, val2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkBitVector("", 2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkBitVector("10", 3), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkBitVector("20", 2), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector(size1, val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector(size2, val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 16));
+}
+
+void SolverBlack::testMkBoundVar()
+{
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort intSort = d_solver.getIntegerSort();
+ Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+ TS_ASSERT_THROWS(d_solver.mkBoundVar(Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(boolSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(funSort));
+ TS_ASSERT_THROWS(d_solver.mkBoundVar("a", Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(std::string("b"), boolSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar("", funSort));
+}
+
+void SolverBlack::testMkBoolean()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(true));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(false));
+}
+
+void SolverBlack::testMkConst()
+{
+ // mkConst(RoundingMode rm) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(RoundingMode::ROUND_TOWARD_ZERO));
+
+ // mkConst(Kind kind, Sort arg) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(EMPTYSET, Sort()));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort())));
+ TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(UNIVERSE_SET, Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(APPLY, d_solver.getBooleanSort()),
+ CVC4ApiException&);
+
+ // mkConst(Kind kind, Sort arg1, int32_t arg2) const
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkConst(UNINTERPRETED_CONSTANT, d_solver.getBooleanSort(), 1));
+ TS_ASSERT_THROWS(d_solver.mkConst(UNINTERPRETED_CONSTANT, Sort(), 1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort(), 1),
+ CVC4ApiException&);
+
+ // mkConst(Kind kind, bool arg) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_BOOLEAN, true));
+ TS_ASSERT_THROWS(d_solver.mkConst(UNINTERPRETED_CONSTANT, true),
+ CVC4ApiException&);
+
+ // mkConst(Kind kind, const char* arg) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, std::string("1")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_STRING, "asdf"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1/2"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1.2"));
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, nullptr), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, ""), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, std::string("1.2")),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, "1/2"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, "asdf"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, "1..2"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, "asdf"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(BITVECTOR_ULT, "asdf"), CVC4ApiException&);
+
+ // mkConst(Kind kind, const std::string& arg) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_STRING, std::string("asdf")));
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkConst(CONST_RATIONAL, std::string("1/2")));
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkConst(CONST_RATIONAL, std::string("1.2")));
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, nullptr), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, std::string("")),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, std::string("asdf")),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(BITVECTOR_ULT, std::string("asdf")),
+ CVC4ApiException&);
+
+ // mkConst(Kind kind, const char* arg1, uint32_t arg2) const
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 2));
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkConst(CONST_BITVECTOR, std::string("10a"), 16));
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, nullptr, 1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("")),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("101", 6)),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("102", 16)),
+ CVC4ApiException&);
+
+ // mkConst(Kind kind, int32_t arg) const
+ // mkConst(Kind kind, uint32_t arg) const
+ // mkConst(Kind kind, int64_t arg) const
+ // mkConst(Kind kind, uint64_t arg) const
+ int32_t val1 = 2;
+ uint32_t val2 = 2;
+ int64_t val3 = 2;
+ uint64_t val4 = 2;
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val4));
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val1), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val3), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val4), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val4));
+
+ // mkConst(Kind kind, int32_t arg1, int32_t arg2) const
+ // mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
+ // mkConst(Kind kind, int64_t arg1, int64_t arg2) const
+ // mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val1, val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val2, val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val3, val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val4, val4));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_BITVECTOR, val2, val2));
+
+ // mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
+#ifdef CVC4_USE_SYMFPU
+ Term t1 = d_solver.mkBitVector(8);
+ Term t2 = d_solver.mkBitVector(4);
+ Term t3 = d_solver.mkReal(2);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1));
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, t1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 0, t1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t2),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t2),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, 3, 5, t1),
+ CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testMkEmptySet()
+{
+ TS_ASSERT_THROWS(d_solver.mkEmptySet(d_solver.getBooleanSort()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkEmptySet(Sort()));
+}
+
+void SolverBlack::testMkFalse()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse());
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse());
+}
+
+void SolverBlack::testMkOpTerm()
+{
+ // mkOpTerm(Kind kind, Kind k)
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(CHAIN_OP, EQUAL));
+ TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL),
+ CVC4ApiException&);
+
+ // mkOpTerm(Kind kind, const std::string& arg)
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(RECORD_UPDATE_OP, "asdf"));
+ TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
+ CVC4ApiException&);
+
+ // mkOpTerm(Kind kind, uint32_t arg)
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(DIVISIBLE_OP, 1));
+ TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1),
+ CVC4ApiException&);
+
+ // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1));
+ TS_ASSERT_THROWS(d_solver.mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&);
+}
+
+void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver.mkPi()); }
+
+void SolverBlack::testMkReal()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("123"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("1.23"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("1/23"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("12/3"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(".2"));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal("2."));
+ TS_ASSERT_THROWS(d_solver.mkReal(nullptr), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(""), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("asdf"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("1.2/3"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("."), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("/"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("2/"), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal("/2"), CVC4ApiException&);
+
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("123")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("1.23")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("1/23")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("12/3")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string(".2")));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(std::string("2.")));
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("asdf")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string(".")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("/")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("2/")), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkReal(std::string("/2")), CVC4ApiException&);
+
+ int32_t val1 = 1;
+ int64_t val2 = -1;
+ uint32_t val3 = 1;
+ uint64_t val4 = -1;
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val1, val1));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val2, val2));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val3, val3));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkReal(val4, val4));
+}
+
+void SolverBlack::testMkRegexpEmpty()
+{
+ Sort strSort = d_solver.getStringSort();
+ Term s = d_solver.mkVar("s", strSort);
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+}
+
+void SolverBlack::testMkRegexpSigma()
+{
+ Sort strSort = d_solver.getStringSort();
+ Term s = d_solver.mkVar("s", strSort);
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+}
+
+void SolverBlack::testMkSepNil()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkSepNil(d_solver.getBooleanSort()));
+ TS_ASSERT_THROWS(d_solver.mkSepNil(Sort()), CVC4ApiException&);
+}
+
+void SolverBlack::testMkString()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkString(""));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkString("asdfasdf"));
+}
+
+void SolverBlack::testMkTerm()
+{
+ Sort bv32 = d_solver.mkBitVectorSort(32);
+ Term a = d_solver.mkVar("a", bv32);
+ Term b = d_solver.mkVar("b", bv32);
+ std::vector<Term> v1 = {a, b};
+ std::vector<Term> v2 = {a, Term()};
+ std::vector<Term> v3 = {a, d_solver.mkTrue()};
+ std::vector<Term> v4 = {d_solver.mkReal(1), d_solver.mkReal(2)};
+ std::vector<Term> v5 = {d_solver.mkReal(1), Term()};
+ OpTerm opterm1 = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
+ OpTerm opterm2 = d_solver.mkOpTerm(DIVISIBLE_OP, 1);
+ OpTerm opterm3 = d_solver.mkOpTerm(CHAIN_OP, EQUAL);
+
+ // mkTerm(Kind kind) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(PI));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(REGEXP_EMPTY));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(REGEXP_SIGMA));
+ TS_ASSERT_THROWS(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException&);
+
+ // mkTerm(Kind kind, Sort sort) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(SEP_NIL, d_solver.getBooleanSort()));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(SEP_NIL, Sort()));
+
+ // mkTerm(Kind kind, Term child) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(NOT, d_solver.mkTrue()));
+ TS_ASSERT_THROWS(d_solver.mkTerm(NOT, Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(NOT, a), CVC4ApiException&);
+
+ // mkTerm(Kind kind, Term child1, Term child2) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(EQUAL, a, b));
+ TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()),
+ CVC4ApiException&);
+
+ // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(
+ ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
+ TS_ASSERT_THROWS(
+ d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b),
+ CVC4ApiException&);
+
+ // mkTerm(Kind kind, const std::vector<Term>& children) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(EQUAL, v1));
+ TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, v2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(EQUAL, v3), CVC4ApiException&);
+
+ // mkTerm(OpTerm opTerm, Term child) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm1, a));
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm2, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, Term()), CVC4ApiException&);
+
+ // mkTerm(OpTerm opTerm, Term child1, Term child2) const
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(2)));
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, d_solver.mkReal(1), Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, Term(), d_solver.mkReal(1)),
+ CVC4ApiException&);
+
+ // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(
+ opterm3, d_solver.mkReal(1), d_solver.mkReal(1), d_solver.mkReal(2)));
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(1), Term()),
+ CVC4ApiException&);
+
+ // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm3, v4));
+ TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, v5), CVC4ApiException&);
+}
+
+void SolverBlack::testMkTrue()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue());
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue());
+}
+
+void SolverBlack::testMkUniverseSet()
+{
+ TS_ASSERT_THROWS(d_solver.mkUniverseSet(Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException&);
+}
+
+void SolverBlack::testMkVar()
+{
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort intSort = d_solver.getIntegerSort();
+ Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+ TS_ASSERT_THROWS(d_solver.mkVar(Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(boolSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(funSort));
+ TS_ASSERT_THROWS(d_solver.mkVar("a", Sort()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(std::string("b"), boolSort));
+ TS_ASSERT_THROWS_NOTHING(d_solver.mkVar("", funSort));
+}
+
void SolverBlack::testDeclareFun()
{
Sort bvSort = d_solver.mkBitVectorSort(32);
d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
CVC4ApiException&);
}
-
-void SolverBlack::testMkRegexpEmpty()
-{
- Sort strSort = d_solver.getStringSort();
- Term s = d_solver.mkVar("s", strSort);
- TS_ASSERT_THROWS_NOTHING(
- d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
-}
-
-void SolverBlack::testMkRegexpSigma()
-{
- Sort strSort = d_solver.getStringSort();
- Term s = d_solver.mkVar("s", strSort);
- TS_ASSERT_THROWS_NOTHING(
- d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
-}
Term p = d_solver.mkVar("p", funSort2);
TS_ASSERT_THROWS_NOTHING(p.getKind());
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS_NOTHING(zero.getKind());
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
TS_ASSERT_THROWS_NOTHING(p.getSort());
TS_ASSERT(p.getSort() == funSort2);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS_NOTHING(zero.getSort());
TS_ASSERT(zero.getSort() == intSort);
TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
Term p = d_solver.mkVar("p", funSort2);
TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
Term p = d_solver.mkVar("p", funSort2);
TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
- Term zero = d_solver.mkInteger(0);
+ Term zero = d_solver.mkReal(0);
TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
projects / cvc5.git / commitdiff