From 51cb061609e10ff68fb9db053d23ea9dd72ddea2 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 10 Jan 2019 10:47:53 -0800 Subject: [PATCH] New C++ API: Get rid of mkConst functions (simplify API). (#2783) --- src/api/cvc4cpp.cpp | 238 +++++------------------------------ src/api/cvc4cpp.h | 187 +++------------------------ src/api/cvc4cppkind.h | 40 ++---- src/parser/smt2/Smt2.g | 20 +-- test/unit/api/solver_black.h | 205 +++++++++++++----------------- 5 files changed, 155 insertions(+), 535 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f9dfaa143..5321a90ec 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2303,254 +2303,74 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); } -Term Solver::mkConst(RoundingMode rm) const +Term Solver::mkRoundingMode(RoundingMode rm) const { return mkConstHelper(s_rmodes.at(rm)); } -Term Solver::mkConst(Kind kind, Sort arg) const +Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const { - 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 (const CVC4::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"; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; 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 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 (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } - catch (const CVC4::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_ARG_CHECK_NOT_NULL(arg); - return mkConstFromStrHelper(kind, std::string(arg)); -} - -Term Solver::mkConst(Kind kind, const std::string& arg) const -{ - return mkConstFromStrHelper(kind, arg); + CVC4::UninterpretedConstant(*sort.d_type, index)); } -/* 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_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 +Term Solver::mkAbstractValue(const std::string& index) const { - return mkConstFromStrHelper(kind, arg1, arg2); -} - -/* 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) - << "ABSTRACT_VALUE or CONST_RATIONAL"; - if (kind == ABSTRACT_VALUE) - { - 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 (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } - catch (const CVC4::TypeCheckingException& e) - { - throw CVC4ApiException(e.getMessage()); - } - } + CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; try { - return mkConstHelper(CVC4::Rational(a)); + CVC4::Integer idx(index, 10); + CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) + << "a string representing an integer > 0"; + return d_exprMgr->mkConst(CVC4::AbstractValue(idx)); + // do not call getType(), for abstract values, type can not be computed + // until it is substituted away } catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } -} - -Term Solver::mkConst(Kind kind, int32_t arg) const -{ - return mkConstFromIntHelper(kind, static_cast(arg)); -} - -Term Solver::mkConst(Kind kind, int64_t arg) const -{ - 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 -{ - return mkConstFromIntHelper(kind, arg); -} - -Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const -{ - 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); - } - try - { - return mkConstHelper(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } -} - -Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; - try - { - return mkConstHelper(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) + catch (const CVC4::TypeCheckingException& e) { - throw CVC4ApiException(e.what()); + throw CVC4ApiException(e.getMessage()); } } -Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const +Term Solver::mkAbstractValue(uint64_t index) const { - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; try { - return mkConstHelper(CVC4::Rational(arg1, arg2)); + CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; + return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))); + // do not call getType(), for abstract values, type can not be computed + // until it is substituted away } catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } -} - -Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) - << "CONST_RATIONAL"; - try - { - return mkConstHelper(CVC4::Rational(arg1, arg2)); - } - catch (const std::invalid_argument& e) + catch (const CVC4::TypeCheckingException& e) { - throw CVC4ApiException(e.what()); + throw CVC4ApiException(e.getMessage()); } } -Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const -{ - CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind) - << "CONST_BITVECTOR"; - return mkBVFromIntHelper(arg1, arg2); -} - -Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const +Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; - 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) + CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; + CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; + uint32_t bw = exp + sig; + CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) << "a bit-vector constant with bit-width '" << bw << "'"; - CVC4_API_ARG_CHECK_EXPECTED(!arg3.isNull(), arg3) << "non-null term"; + CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED( - arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3) + val.getSort().isBitVector() && val.d_expr->isConst(), val) << "bit-vector constant"; return mkConstHelper( - CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst())); + CVC4::FloatingPoint(exp, sig, val.d_expr->getConst())); } /* Create variables */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index ef82a9174..1d98f127d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2088,183 +2088,38 @@ class CVC4_PUBLIC Solver Term mkNegZero(uint32_t exp, uint32_t sig) const; /** - * Create constant of kind: - * - CONST_ROUNDINGMODE + * Create a roundingmode constant. * @param rm the floating point rounding mode this constant represents */ - Term mkConst(RoundingMode rm) const; - - /* - * Create constant of kind: - * - EMPTYSET - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, Sort arg) const; - - /** - * Create constant of kind: - * - UNINTERPRETED_CONSTANT - * 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, Sort arg1, int32_t arg2) const; - - /** - * Create constant of kind: - * - BOOLEAN - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, bool arg) const; - - /** - * 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 - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, const char* arg) const; - - /** - * 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 - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, const std::string& arg) const; - - /** - * Create constant of kind: - * - 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) const; + Term mkRoundingMode(RoundingMode rm) const; /** - * Create constant of kind: - * - 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 + * Create uninterpreted constant. + * @param arg1 Sort of the constant + * @param arg2 Index of the constant */ - Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const; + Term mkUninterpretedConst(Sort sort, int32_t index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind + * Create an abstract value constant. + * @param index Index of the abstract value */ - Term mkConst(Kind kind, uint32_t arg) const; + Term mkAbstractValue(const std::string& index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind + * Create an abstract value constant. + * @param index Index of the abstract value */ - Term mkConst(Kind kind, int32_t arg) const; + Term mkAbstractValue(uint64_t index) const; /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, int64_t arg) const; - - /** - * Create constant of kind: - * - ABSTRACT_VALUE - * - CONST_RATIONAL (for integers, reals) - * See enum Kind for a description of the parameters. - * @param kind the kind of the constant - * @param arg the argument to this kind - */ - Term mkConst(Kind kind, uint64_t arg) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * 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, int32_t arg1, int32_t arg2) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * 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, int64_t arg1, int64_t arg2) const; - - /** - * 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 - * @param arg2 the second argument to this kind - */ - Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const; - - /** - * Create constant of kind: - * - CONST_RATIONAL (for rationals) - * 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, uint64_t arg1, uint64_t arg2) const; - - /** - * Create constant of kind: - * - 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, uint32_t arg1, uint64_t arg2) const; - - /** - * Create constant of kind: - * - CONST_FLOATINGPOINT (requires CVC4 to be compiled with symFPU support) - * 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 - * @param arg3 the third argument to this kind + * Create a floating-point constant (requires CVC4 to be compiled with symFPU + * support). + * @param exp Size of the exponent + * @param sig Size of the significand + * @param val Value of the floating-point constant as a bit-vector term */ - Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const; + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const; /* .................................................................... */ /* Create Variables */ @@ -2644,12 +2499,6 @@ class CVC4_PUBLIC Solver Term mkBVFromStrHelper(uint32_t size, 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; /** * Helper function that ensures that a given term is of sort real (as opposed diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index a940dbefa..a7f6926bb 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -62,7 +62,7 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Sort of the constant * -[2]: Index of the constant * Create with: - * mkConst(Kind, Sort, int32_t) + * mkUninterpretedConst(Sort sort, int32_t index) */ UNINTERPRETED_CONSTANT, /** @@ -70,12 +70,8 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Index of the abstract value * Create with: - * 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) - * mkConst(Kind kind, uint64_t arg) + * mkAbstractValue(const std::string& index); + * mkAbstractValue(uint64_t index); */ ABSTRACT_VALUE, #if 0 @@ -204,7 +200,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTrue() * mkFalse() * mkBoolean(bool val) - * mkConst(Kind kind, bool arg) */ CONST_BOOLEAN, /* Logical not. @@ -568,20 +563,10 @@ enum CVC4_PUBLIC Kind : int32_t * mkReal(int64_t val) * mkReal(uint32_t val) * mkReal(uint64_t val) - * mkRational(int32_t num, int32_t den) - * mkRational(int64_t num, int64_t den) - * mkRational(uint32_t num, uint32_t den) - * mkRational(uint64_t num, uint64_t den) - * 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, int64_t arg) - * mkConst(Kind kind, uint64_t arg) - * mkConst(Kind kind, int32_t arg) - * mkConst(Kind kind, int32_t arg1, int32_t arg2) - * mkConst(Kind kind, int64_t arg1, int64_t arg2) - * mkConst(Kind kind, uint32_t arg1, uint32_t arg2) - * mkConst(Kind kind, uint64_t arg1, uint64_t arg2) + * mkReal(int32_t num, int32_t den) + * mkReal(int64_t num, int64_t den) + * mkReal(uint32_t num, uint32_t den) + * mkReal(uint64_t num, uint64_t den) */ CONST_RATIONAL, /** @@ -661,9 +646,6 @@ enum CVC4_PUBLIC Kind : int32_t * 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 arg1, uint64_t arg2) */ CONST_BITVECTOR, /** @@ -1166,13 +1148,13 @@ enum CVC4_PUBLIC Kind : int32_t * -[2]: Size of the significand * -[3]: Value of the floating-point constant as a bit-vector term * Create with: - * mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) + * mkFloatingPoint(uint32_t sig, uint32_t exp, Term val) */ CONST_FLOATINGPOINT, /** * Floating-point rounding mode term. * Create with: - * mkConst(RoundingMode rm) + * mkRoundingMode(RoundingMode rm) */ CONST_ROUNDINGMODE, /** @@ -1830,7 +1812,6 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Sort of the set elements * Create with: * mkEmptySet(Sort sort) - * mkConst(Sort sort) */ EMPTYSET, /** @@ -1919,7 +1900,6 @@ enum CVC4_PUBLIC Kind : int32_t * All set variables must be interpreted as subsets of it. * Create with: * mkUniverseSet(Sort sort) - * mkConst(Kind kind, Sort sort) */ UNIVERSE_SET, /** @@ -2122,8 +2102,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkString(const std::string& s) * mkString(const unsigned char c) * mkString(const std::vector& s) - * mkConst(Kind kind, const char* s) - * mkConst(Kind kind, const std::string& s) */ CONST_STRING, /** diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e33ab7a70..c72a4f99b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2330,16 +2330,16 @@ termAtomic[CVC4::api::Term& atomTerm] } // Floating-point rounding mode constants - | FP_RNE_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } - | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } + | FP_RNE_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } + | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } // String constant | str[s,false] { atomTerm = SOLVER->mkString(s, true); } diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 5c2c7a8f5..3bfb51200 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -49,22 +49,29 @@ class SolverBlack : public CxxTest::TestSuite void testMkTupleSort(); void testMkUninterpretedSort(); + void testMkAbstractValue(); void testMkBitVector(); void testMkBoolean(); void testMkBoundVar(); - void testMkConst(); void testMkEmptySet(); void testMkFalse(); void testMkFloatingPoint(); + void testMkNaN(); + void testMkNegInf(); + void testMkNegZero(); void testMkPi(); + void testMkPosInf(); + void testMkPosZero(); void testMkReal(); void testMkRegexpEmpty(); void testMkRegexpSigma(); + void testMkRoundingMode(); void testMkSepNil(); void testMkString(); void testMkTerm(); void testMkTrue(); void testMkTuple(); + void testMkUninterpretedConst(); void testMkUniverseSet(); void testMkVar(); @@ -281,132 +288,58 @@ void SolverBlack::testMkBoolean() TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(false)); } -void SolverBlack::testMkConst() +void SolverBlack::testMkRoundingMode() { - // 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&); + d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); +} - // 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"))); +void SolverBlack::testMkUninterpretedConst() +{ 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&); + d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); + TS_ASSERT_THROWS(d_solver.mkUninterpretedConst(Sort(), 1), 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), +void SolverBlack::testMkAbstractValue() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue(std::string("1"))); + TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("")), + TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("-1")), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 6), + TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("1.2")), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkAbstractValue("1/2"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkAbstractValue("asdf"), 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 + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint32_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint64_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)-1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)-1)); + TS_ASSERT_THROWS(d_solver.mkAbstractValue(0), CVC4ApiException&); +} + +void SolverBlack::testMkFloatingPoint() +{ Term t1 = d_solver.mkBitVector(8); Term t2 = d_solver.mkBitVector(4); Term t3 = d_solver.mkReal(2); if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPoint(3, 5, t1)); } else { - TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1), - CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException&); } - 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&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&); } void SolverBlack::testMkEmptySet() @@ -422,23 +355,63 @@ void SolverBlack::testMkFalse() TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse()); } -void SolverBlack::testMkFloatingPoint() +void SolverBlack::testMkNaN() { if (CVC4::Configuration::isBuiltWithSymFPU()) { - TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5)); TS_ASSERT_THROWS_NOTHING(d_solver.mkNaN(3, 5)); - TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + } + else + { + TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&); + } +} + +void SolverBlack::testMkNegZero() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5)); } else { - TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&); + } +} + +void SolverBlack::testMkNegInf() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5)); + } + else + { TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&); + } +} + +void SolverBlack::testMkPosInf() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + } + else + { TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&); + } +} + +void SolverBlack::testMkPosZero() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosZero(3, 5)); + } + else + { + TS_ASSERT_THROWS(d_solver.mkPosZero(3, 5), CVC4ApiException&); } } -- 2.30.2