From e4e8d99ec19598c77144d3ffde2b5792db4430d3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Jan 2019 20:07:43 -0800 Subject: New C++ API: Add tests for mk-functions in solver object. (#2764) --- examples/api/combination-new.cpp | 4 +- examples/api/datatypes-new.cpp | 4 +- examples/api/linear_arith-new.cpp | 4 +- examples/api/sets-new.cpp | 6 +- examples/api/strings-new.cpp | 2 +- src/api/cvc4cpp.cpp | 755 +++++++++++++++++++++++++++----------- src/api/cvc4cpp.h | 159 +++----- src/api/cvc4cppkind.h | 9 +- test/unit/api/solver_black.h | 416 ++++++++++++++++++++- test/unit/api/term_black.h | 18 +- 10 files changed, 1019 insertions(+), 358 deletions(-) diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp index 2956d76e6..8c968c95e 100644 --- a/examples/api/combination-new.cpp +++ b/examples/api/combination-new.cpp @@ -59,8 +59,8 @@ int main() 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); diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index b6a816db4..48560e894 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort) 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 @@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort) << "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; diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp index ef8faade9..d643b85bc 100644 --- a/examples/api/linear_arith-new.cpp +++ b/examples/api/linear_arith-new.cpp @@ -40,8 +40,8 @@ int main() 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 diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp index be35bcc21..2dcfbbc02 100644 --- a/examples/api/sets-new.cpp +++ b/examples/api/sets-new.cpp @@ -70,9 +70,9 @@ int main() // 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); diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp index 2010c6909..c88ccc9c0 100644 --- a/examples/api/strings-new.cpp +++ b/examples/api/strings-new.cpp @@ -57,7 +57,7 @@ int main() // 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, diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index cd604a25c..8a583a671 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -32,6 +32,7 @@ #include "util/result.h" #include "util/utility.h" +#include #include namespace CVC4 { @@ -639,6 +640,10 @@ class CVC4ApiExceptionStream 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) << "'"; @@ -665,12 +670,12 @@ class CVC4ApiExceptionStream & 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 @@ -751,12 +756,16 @@ std::ostream& operator<<(std::ostream& out, const Result& r) 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(); } @@ -1744,6 +1753,10 @@ Sort Solver::getRoundingmodeSort(void) const 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); } @@ -1769,6 +1782,8 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const 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) @@ -1783,10 +1798,15 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const << "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. */ @@ -1805,6 +1825,9 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const << "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"; @@ -1817,8 +1840,13 @@ Sort Solver::mkRecordSort( const std::vector>& fields) const { std::vector> 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)); @@ -1826,6 +1854,8 @@ Sort Solver::mkRecordSort( 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); } @@ -1845,6 +1875,9 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const { 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"; @@ -1873,327 +1906,437 @@ Term Solver::mkFalse(void) const { return d_exprMgr->mkConst(false); } Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst(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 +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(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(val)); } Term Solver::mkReal(int64_t val) const { - return d_exprMgr->mkConst(Rational(val)); + return mkConstHelper(CVC4::Rational(val)); } Term Solver::mkReal(uint32_t val) const { - return d_exprMgr->mkConst(Rational(val)); + return mkConstHelper(CVC4::Rational(val)); } Term Solver::mkReal(uint64_t val) const { - return d_exprMgr->mkConst(Rational(val)); + return mkConstHelper(CVC4::Rational(val)); } Term Solver::mkReal(int32_t num, int32_t den) const { - return d_exprMgr->mkConst(Rational(num, den)); + return mkConstHelper(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(num, den)); } Term Solver::mkReal(uint32_t num, uint32_t den) const { - return d_exprMgr->mkConst(Rational(num, den)); + return mkConstHelper(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(num, den)); } Term Solver::mkRegexpEmpty() const { - return d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector()); + try + { + Term res = + d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector()); + (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()); + try + { + Term res = + d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector()); + (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(*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(s)); } Term Solver::mkString(const std::string& s) const { - return d_exprMgr->mkConst(String(s)); + return mkConstHelper(CVC4::String(s)); } Term Solver::mkString(const unsigned char c) const { - return d_exprMgr->mkConst(String(std::string(1, c))); + return mkConstHelper(CVC4::String(std::string(1, c))); } Term Solver::mkString(const std::vector& s) const { - return d_exprMgr->mkConst(String(s)); + return mkConstHelper(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(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(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(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(*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(*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(arg); + return mkConstHelper(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(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 +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(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(kind, static_cast(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(kind, arg); +} + +Term Solver::mkConst(Kind kind, uint32_t arg) const +{ + return mkConstFromIntHelper(kind, static_cast(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(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(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(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(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(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(arg1, arg2, arg3.d_expr->getConst())); } @@ -2202,19 +2345,62 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const 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 */ @@ -2269,88 +2455,201 @@ void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const 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()); + 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()); + } + 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 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 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& children) const { - checkMkTerm(kind, children.size()); - std::vector 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 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& children) const { - checkMkOpTerm(opTerm, children.size()); - std::vector 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 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 Solver::termVectorToExprs( @@ -2370,14 +2669,15 @@ std::vector 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(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(arg)) + .d_expr.get(); } OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) @@ -2386,39 +2686,60 @@ 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(arg)).d_expr.get(); + break; case BITVECTOR_REPEAT_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorRepeat(arg)); + res = *mkConstHelper(CVC4::BitVectorRepeat(arg)) + .d_expr.get(); break; case BITVECTOR_ZERO_EXTEND_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorZeroExtend(arg)); + res = *mkConstHelper( + CVC4::BitVectorZeroExtend(arg)) + .d_expr.get(); break; case BITVECTOR_SIGN_EXTEND_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorSignExtend(arg)); + res = *mkConstHelper( + CVC4::BitVectorSignExtend(arg)) + .d_expr.get(); break; case BITVECTOR_ROTATE_LEFT_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorRotateLeft(arg)); + res = *mkConstHelper( + CVC4::BitVectorRotateLeft(arg)) + .d_expr.get(); break; case BITVECTOR_ROTATE_RIGHT_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorRotateRight(arg)); + res = *mkConstHelper( + CVC4::BitVectorRotateRight(arg)) + .d_expr.get(); break; case INT_TO_BITVECTOR_OP: - res = d_exprMgr->mkConst(CVC4::IntToBitVector(arg)); + res = *mkConstHelper(CVC4::IntToBitVector(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_UBV_OP: - res = d_exprMgr->mkConst(CVC4::FloatingPointToUBV(arg)); + res = *mkConstHelper( + CVC4::FloatingPointToUBV(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_UBV_TOTAL_OP: - res = d_exprMgr->mkConst(CVC4::FloatingPointToUBVTotal(arg)); + res = *mkConstHelper( + CVC4::FloatingPointToUBVTotal(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_SBV_OP: - res = d_exprMgr->mkConst(CVC4::FloatingPointToSBV(arg)); + res = *mkConstHelper( + CVC4::FloatingPointToSBV(arg)) + .d_expr.get(); break; case FLOATINGPOINT_TO_SBV_TOTAL_OP: - res = d_exprMgr->mkConst(CVC4::FloatingPointToSBVTotal(arg)); + res = *mkConstHelper( + CVC4::FloatingPointToSBVTotal(arg)) + .d_expr.get(); break; case TUPLE_UPDATE_OP: - res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg)); + res = *mkConstHelper(CVC4::TupleUpdate(arg)) + .d_expr.get(); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -2435,29 +2756,39 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) switch (kind) { case BITVECTOR_EXTRACT_OP: - res = d_exprMgr->mkConst(CVC4::BitVectorExtract(arg1, arg2)); + res = *mkConstHelper( + 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(arg1, arg2)) + .d_expr.get(); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - res = - d_exprMgr->mkConst(CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)); + res = *mkConstHelper( + 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(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(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(arg1, arg2)) + .d_expr.get(); break; case FLOATINGPOINT_TO_FP_GENERIC_OP: - res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2)); + res = *mkConstHelper( + CVC4::FloatingPointToFPGeneric(arg1, arg2)) + .d_expr.get(); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index d06955a05..e18e3ac6b 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -191,6 +191,11 @@ class CVC4_PUBLIC Sort */ Sort(const CVC4::Type& t); + /** + * Constructor. + */ + Sort(); + /** * Destructor. */ @@ -210,6 +215,11 @@ class CVC4_PUBLIC Sort */ 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 @@ -1690,14 +1700,6 @@ class CVC4_PUBLIC Solver */ Term mkTerm(Kind kind, const std::vector& 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(). @@ -1818,50 +1820,6 @@ class CVC4_PUBLIC Solver */ 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 @@ -1869,78 +1827,78 @@ class CVC4_PUBLIC Solver 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; @@ -2005,21 +1963,6 @@ class CVC4_PUBLIC Solver */ 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 @@ -2042,7 +1985,7 @@ class CVC4_PUBLIC Solver * @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: @@ -2081,6 +2024,8 @@ class CVC4_PUBLIC Solver /** * 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 @@ -2090,6 +2035,8 @@ class CVC4_PUBLIC Solver /** * 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 @@ -2099,33 +2046,28 @@ class CVC4_PUBLIC Solver /** * 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 @@ -2185,6 +2127,7 @@ class CVC4_PUBLIC Solver /** * 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 @@ -2581,6 +2524,20 @@ class CVC4_PUBLIC Solver 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 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 + Term mkConstFromIntHelper(Kind kind, T a) const; /* The expression manager of this solver. */ std::unique_ptr d_exprMgr; diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index f91f934f9..a940dbefa 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -70,8 +70,8 @@ enum CVC4_PUBLIC Kind : int32_t * 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) @@ -658,14 +658,11 @@ enum CVC4_PUBLIC Kind : int32_t * 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, @@ -1922,7 +1919,7 @@ enum CVC4_PUBLIC Kind : int32_t * 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, /** diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index b0249b8a0..29e57ef63 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -38,22 +38,37 @@ class SolverBlack : public CxxTest::TestSuite 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; }; @@ -219,6 +234,383 @@ void SolverBlack::testMkTupleSort() 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 v1 = {a, b}; + std::vector v2 = {a, Term()}; + std::vector v3 = {a, d_solver.mkTrue()}; + std::vector v4 = {d_solver.mkReal(1), d_solver.mkReal(2)}; + std::vector 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& 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& 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); @@ -329,19 +721,3 @@ void SolverBlack::testDefineFunsRec() 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())); -} diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index ae1dfe7ba..a7f735651 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -77,7 +77,7 @@ void TermBlack::testGetKind() 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); @@ -116,7 +116,7 @@ void TermBlack::testGetSort() 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); @@ -161,7 +161,7 @@ void TermBlack::testNotTerm() 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&); @@ -195,7 +195,7 @@ void TermBlack::testAndTerm() 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&); @@ -259,7 +259,7 @@ void TermBlack::testOrTerm() 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&); @@ -323,7 +323,7 @@ void TermBlack::testXorTerm() 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&); @@ -387,7 +387,7 @@ void TermBlack::testEqTerm() 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&); @@ -451,7 +451,7 @@ void TermBlack::testImpTerm() 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&); @@ -515,7 +515,7 @@ void TermBlack::testIteTerm() 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); -- cgit v1.2.3