FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
}
-Term Solver::mkConst(RoundingMode rm) const
+Term Solver::mkRoundingMode(RoundingMode rm) const
{
return mkConstHelper<CVC4::RoundingMode>(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>(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>(
- 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<bool>(arg);
-}
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const
-{
- CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
- CVC4_API_KIND_CHECK_EXPECTED(
- kind == ABSTRACT_VALUE || kind == CONST_RATIONAL || kind == CONST_STRING,
- kind)
- << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_STRING";
- if (kind == ABSTRACT_VALUE)
- {
- try
- {
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(s, 10)));
- // do not call getType(), for abstract values, type can not be computed
- // until it is substituted away
- }
- catch (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>(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 <typename T>
-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>(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<int64_t>(kind, static_cast<int64_t>(arg));
-}
-
-Term Solver::mkConst(Kind kind, int64_t arg) const
-{
- return mkConstFromIntHelper<int64_t>(kind, arg);
-}
-
-Term Solver::mkConst(Kind kind, uint32_t arg) const
-{
- return mkConstFromIntHelper<uint64_t>(kind, static_cast<uint64_t>(arg));
-}
-
-Term Solver::mkConst(Kind kind, uint64_t arg) const
-{
- return mkConstFromIntHelper<uint64_t>(kind, arg);
-}
-
-Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
-{
- CVC4_API_KIND_CHECK_EXPECTED(
- kind == CONST_BITVECTOR || kind == CONST_RATIONAL, kind)
- << "CONST_BITVECTOR or CONST_RATIONAL";
- if (kind == CONST_BITVECTOR)
- {
- return mkBVFromIntHelper(arg1, arg2);
- }
- try
- {
- return mkConstHelper<CVC4::Rational>(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>(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>(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>(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>(
- CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
+ CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
}
/* Create variables */
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 */
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 <typename T>
- Term mkConstFromIntHelper(Kind kind, T a) const;
/**
* Helper function that ensures that a given term is of sort real (as opposed
* -[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,
/**
* 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
* mkTrue()
* mkFalse()
* mkBoolean(bool val)
- * mkConst(Kind kind, bool arg)
*/
CONST_BOOLEAN,
/* Logical not.
* 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,
/**
* 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,
/**
* -[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,
/**
* -[1]: Sort of the set elements
* Create with:
* mkEmptySet(Sort sort)
- * mkConst(Sort sort)
*/
EMPTYSET,
/**
* All set variables must be interpreted as subsets of it.
* Create with:
* mkUniverseSet(Sort sort)
- * mkConst(Kind kind, Sort sort)
*/
UNIVERSE_SET,
/**
* mkString(const std::string& s)
* mkString(const unsigned char c)
* mkString(const std::vector<unsigned>& s)
- * mkConst(Kind kind, const char* s)
- * mkConst(Kind kind, const std::string& s)
*/
CONST_STRING,
/**
}
// 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); }
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();
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()
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&);
}
}
projects / cvc5.git / commitdiff