cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
// Assert that a is odd
- OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
- Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a);
+ Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+ Term lsb_of_a = slv.mkTerm(extract_op, a);
cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
cout << "Assert " << a_odd << endl;
// which is equivalent to consList["cons"].getConstructor(). Note that
// "nil" is a constructor too, so it needs to be applied with
// APPLY_CONSTRUCTOR, even though it has no arguments.
- Term t = slv.mkTerm(
- APPLY_CONSTRUCTOR,
- consList.getConstructorTerm("cons"),
- slv.mkReal(0),
- slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+ Term t = slv.mkTerm(consList.getConstructorTerm("cons"),
+ slv.mkReal(0),
+ slv.mkTerm(consList.getConstructorTerm("nil")));
std::cout << "t is " << t << std::endl
<< "sort of cons is "
// Here we first get the DatatypeConstructor for cons (with
// consList["cons"]) in order to get the "head" selector symbol
// to apply.
- Term t2 =
- slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
+ Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t);
std::cout << "t2 is " << t2 << std::endl
<< "simplify(t2) is " << slv.simplify(t2) << std::endl
Term a = slv.mkConst(paramConsIntListSort, "a");
std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
- Term head_a = slv.mkTerm(
- APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
+ Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a);
std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
<< std::endl
<< "sort of cons is "
Term x = slv.mkConst(bitvector32, "a");
- OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
- Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
+ Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1);
+ Term x_31_1 = slv.mkTerm(ext_31_1, x);
- OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0);
- Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x);
+ Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0);
+ Term x_30_0 = slv.mkTerm(ext_30_0, x);
- OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31);
- Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x);
+ Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31);
+ Term x_31_31 = slv.mkTerm(ext_31_31, x);
- OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
- Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x);
+ Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+ Term x_0_0 = slv.mkTerm(ext_0_0, x);
Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
cout << " Asserting: " << eq << endl;
{LAMBDA, CVC4::Kind::LAMBDA},
{CHOICE, CVC4::Kind::CHOICE},
{CHAIN, CVC4::Kind::CHAIN},
- {CHAIN_OP, CVC4::Kind::CHAIN_OP},
/* Boolean ------------------------------------------------------------- */
{CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
{NOT, CVC4::Kind::NOT},
{ARCSECANT, CVC4::Kind::ARCSECANT},
{ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
{SQRT, CVC4::Kind::SQRT},
- {DIVISIBLE_OP, CVC4::Kind::DIVISIBLE_OP},
{CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
{LT, CVC4::Kind::LT},
{LEQ, CVC4::Kind::LEQ},
{BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
{BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
{BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
- {BITVECTOR_EXTRACT_OP, CVC4::Kind::BITVECTOR_EXTRACT_OP},
- {BITVECTOR_REPEAT_OP, CVC4::Kind::BITVECTOR_REPEAT_OP},
- {BITVECTOR_ZERO_EXTEND_OP, CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP},
- {BITVECTOR_SIGN_EXTEND_OP, CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP},
- {BITVECTOR_ROTATE_LEFT_OP, CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP},
- {BITVECTOR_ROTATE_RIGHT_OP, CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP},
{BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
{BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
{BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
{BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
{BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
{BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
- {INT_TO_BITVECTOR_OP, CVC4::Kind::INT_TO_BITVECTOR_OP},
{INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
{BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
/* FP ------------------------------------------------------------------ */
{FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
{FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
{FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
- {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
- CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
- {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
- CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
- {FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
- CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
{FLOATINGPOINT_TO_FP_FLOATINGPOINT,
CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
- {FLOATINGPOINT_TO_FP_REAL_OP, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP},
{FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
- {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
- CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
{FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
- {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
- CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
{FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
- {FLOATINGPOINT_TO_FP_GENERIC_OP,
- CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP},
{FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
- {FLOATINGPOINT_TO_UBV_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_OP},
{FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
- {FLOATINGPOINT_TO_UBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP},
{FLOATINGPOINT_TO_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL},
- {FLOATINGPOINT_TO_SBV_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_OP},
{FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
- {FLOATINGPOINT_TO_SBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP},
{FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL},
{FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
{FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL},
{APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
{APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL},
{APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
- {TUPLE_UPDATE_OP, CVC4::Kind::TUPLE_UPDATE_OP},
{TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
- {RECORD_UPDATE_OP, CVC4::Kind::RECORD_UPDATE_OP},
{RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
/* Separation Logic ---------------------------------------------------- */
{SEP_NIL, CVC4::Kind::SEP_NIL},
{CVC4::Kind::LAMBDA, LAMBDA},
{CVC4::Kind::CHOICE, CHOICE},
{CVC4::Kind::CHAIN, CHAIN},
- {CVC4::Kind::CHAIN_OP, CHAIN_OP},
+ {CVC4::Kind::CHAIN_OP, CHAIN},
/* Boolean --------------------------------------------------------- */
{CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
{CVC4::Kind::NOT, NOT},
{CVC4::Kind::ARCSECANT, ARCSECANT},
{CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
{CVC4::Kind::SQRT, SQRT},
- {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE_OP},
+ {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE},
{CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
{CVC4::Kind::LT, LT},
{CVC4::Kind::LEQ, LEQ},
{CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
{CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
{CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
- {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT_OP},
- {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT_OP},
- {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND_OP},
- {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP},
- {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT_OP},
- {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT_OP},
+ {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT},
+ {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT},
+ {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND},
+ {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND},
+ {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT},
+ {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT},
{CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
{CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
{CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
{CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
{CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
{CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
- {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR_OP},
+ {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR},
{CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
{CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
/* FP -------------------------------------------------------------- */
{CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
{CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
{CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
- FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
+ FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
- FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
+ FLOATINGPOINT_TO_FP_FLOATINGPOINT},
{CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
FLOATINGPOINT_TO_FP_FLOATINGPOINT},
- {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL_OP},
+ {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL},
{CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
{CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
- FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
+ FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
- FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
+ FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
{CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
- FLOATINGPOINT_TO_FP_GENERIC_OP},
+ FLOATINGPOINT_TO_FP_GENERIC},
{CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
- {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV_OP},
+ {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV},
{CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
- {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP,
- FLOATINGPOINT_TO_UBV_TOTAL_OP},
+ {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, FLOATINGPOINT_TO_UBV_TOTAL},
{CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL},
- {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV_OP},
+ {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV},
{CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
- {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP,
- FLOATINGPOINT_TO_SBV_TOTAL_OP},
+ {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, FLOATINGPOINT_TO_SBV_TOTAL},
{CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL},
{CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
{CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, FLOATINGPOINT_TO_REAL_TOTAL},
{CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
{CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL},
{CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
- {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE_OP},
+ {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE},
{CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
- {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE_OP},
+ {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
{CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
/* Separation Logic ------------------------------------------------ */
{CVC4::Kind::SEP_NIL, SEP_NIL},
return TypeHashFunction()(*s.d_type);
}
+/* -------------------------------------------------------------------------- */
+/* Op */
+/* -------------------------------------------------------------------------- */
+
+Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
+
+Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {}
+
+Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e))
+{
+}
+
+Op::~Op() {}
+
+/* Helpers */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing). */
+/* .......................................................................... */
+
+bool Op::isIndexedHelper() const { return !d_expr->isNull(); }
+
+/* Public methods */
+bool Op::operator==(const Op& t) const
+{
+ if (d_expr->isNull() || t.d_expr->isNull())
+ {
+ return false;
+ }
+ return (d_kind == t.d_kind) && (*d_expr == *t.d_expr);
+}
+
+bool Op::operator!=(const Op& t) const { return !(*this == t); }
+
+Kind Op::getKind() const
+{
+ CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind";
+ return d_kind;
+}
+
+Sort Op::getSort() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ return Sort(d_expr->getType());
+}
+
+bool Op::isNull() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); }
+
+bool Op::isIndexed() const { return isIndexedHelper(); }
+
+template <>
+std::string Op::getIndices() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ CVC4_API_CHECK(!d_expr->isNull())
+ << "Expecting a non-null internal expression. This Op is not indexed.";
+
+ std::string i;
+ Kind k = intToExtKind(d_expr->getKind());
+
+ if (k == DIVISIBLE)
+ {
+ // DIVISIBLE returns a string index to support
+ // arbitrary precision integers
+ CVC4::Integer _int = d_expr->getConst<Divisible>().k;
+ i = _int.toString();
+ }
+ else if (k == RECORD_UPDATE)
+ {
+ i = d_expr->getConst<RecordUpdate>().getField();
+ }
+ else
+ {
+ CVC4_API_CHECK(false) << "Can't get string index from"
+ << " kind " << kindToString(k);
+ }
+
+ return i;
+}
+
+template <>
+Kind Op::getIndices() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ CVC4_API_CHECK(!d_expr->isNull())
+ << "Expecting a non-null internal expression. This Op is not indexed.";
+ Kind kind = intToExtKind(d_expr->getKind());
+ CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
+ return intToExtKind(d_expr->getConst<Chain>().getOperator());
+}
+
+template <>
+uint32_t Op::getIndices() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ CVC4_API_CHECK(!d_expr->isNull())
+ << "Expecting a non-null internal expression. This Op is not indexed.";
+
+ uint32_t i = 0;
+ Kind k = intToExtKind(d_expr->getKind());
+ switch (k)
+ {
+ case BITVECTOR_REPEAT:
+ i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
+ break;
+ case BITVECTOR_ZERO_EXTEND:
+ i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
+ break;
+ case BITVECTOR_SIGN_EXTEND:
+ i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
+ break;
+ case BITVECTOR_ROTATE_LEFT:
+ i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
+ break;
+ case BITVECTOR_ROTATE_RIGHT:
+ i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
+ break;
+ case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break;
+ case FLOATINGPOINT_TO_UBV:
+ i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
+ break;
+ case FLOATINGPOINT_TO_UBV_TOTAL:
+ i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size;
+ break;
+ case FLOATINGPOINT_TO_SBV:
+ i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
+ break;
+ case FLOATINGPOINT_TO_SBV_TOTAL:
+ i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size;
+ break;
+ case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
+ default:
+ CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
+ << " kind " << kindToString(k);
+ }
+ return i;
+}
+
+template <>
+std::pair<uint32_t, uint32_t> Op::getIndices() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ CVC4_API_CHECK(!d_expr->isNull())
+ << "Expecting a non-null internal expression. This Op is not indexed.";
+
+ std::pair<uint32_t, uint32_t> indices;
+ Kind k = intToExtKind(d_expr->getKind());
+
+ // using if/else instead of case statement because want local variables
+ if (k == BITVECTOR_EXTRACT)
+ {
+ CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
+ indices = std::make_pair(ext.high, ext.low);
+ }
+ else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
+ {
+ CVC4::FloatingPointToFPIEEEBitVector ext =
+ d_expr->getConst<FloatingPointToFPIEEEBitVector>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
+ {
+ CVC4::FloatingPointToFPFloatingPoint ext =
+ d_expr->getConst<FloatingPointToFPFloatingPoint>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else if (k == FLOATINGPOINT_TO_FP_REAL)
+ {
+ CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
+ {
+ CVC4::FloatingPointToFPSignedBitVector ext =
+ d_expr->getConst<FloatingPointToFPSignedBitVector>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
+ {
+ CVC4::FloatingPointToFPUnsignedBitVector ext =
+ d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else if (k == FLOATINGPOINT_TO_FP_GENERIC)
+ {
+ CVC4::FloatingPointToFPGeneric ext =
+ d_expr->getConst<FloatingPointToFPGeneric>();
+ indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+ }
+ else
+ {
+ CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
+ << " kind " << kindToString(k);
+ }
+ return indices;
+}
+
+std::string Op::toString() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ if (d_expr->isNull())
+ {
+ return kindToString(d_kind);
+ }
+ else
+ {
+ CVC4_API_CHECK(!d_expr->isNull())
+ << "Expecting a non-null internal expression";
+ return d_expr->toString();
+ }
+}
+
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr Op::getExpr(void) const { return *d_expr; }
+
+std::ostream& operator<<(std::ostream& out, const Op& t)
+{
+ out << t.toString();
+ return out;
+}
+
+size_t OpHashFunction::operator()(const Op& t) const
+{
+ if (t.isIndexedHelper())
+ {
+ return ExprHashFunction()(*t.d_expr);
+ }
+ else
+ {
+ return KindHashFunction()(t.d_kind);
+ }
+}
+
/* -------------------------------------------------------------------------- */
/* Term */
/* -------------------------------------------------------------------------- */
return Sort(d_expr->getType());
}
+bool Term::hasOp() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ return d_expr->hasOperator();
+}
+
+Op Term::getOp() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ CVC4_API_CHECK(d_expr->hasOperator())
+ << "Expecting Term to have an Op when calling getOp()";
+ CVC4::Expr op = d_expr->getOperator();
+ CVC4::Type t = op.getType();
+
+ // special cases for Datatype operators
+ if (t.isSelector())
+ {
+ return Op(APPLY_SELECTOR, op);
+ }
+ else if (t.isConstructor())
+ {
+ return Op(APPLY_CONSTRUCTOR, op);
+ }
+ else if (t.isTester())
+ {
+ return Op(APPLY_TESTER, op);
+ }
+ else
+ {
+ return Op(intToExtKind(op.getKind()), op);
+ }
+}
+
bool Term::isNull() const { return d_expr->isNull(); }
bool Term::isParameterized() const
std::string Term::toString() const { return d_expr->toString(); }
-Term::const_iterator::const_iterator() : d_iterator(nullptr) {}
+Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {}
-Term::const_iterator::const_iterator(void* it) : d_iterator(it) {}
+Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e,
+ uint32_t p)
+ : d_orig_expr(e), d_pos(p)
+{
+}
Term::const_iterator::const_iterator(const const_iterator& it)
- : d_iterator(nullptr)
+ : d_orig_expr(nullptr)
{
- if (it.d_iterator != nullptr)
+ if (it.d_orig_expr != nullptr)
{
- d_iterator = new CVC4::Expr::const_iterator(
- *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+ d_orig_expr = it.d_orig_expr;
+ d_pos = it.d_pos;
}
}
Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
{
- delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
- d_iterator = new CVC4::Expr::const_iterator(
- *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+ d_orig_expr = it.d_orig_expr;
+ d_pos = it.d_pos;
return *this;
}
-Term::const_iterator::~const_iterator()
-{
- delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
-}
-
bool Term::const_iterator::operator==(const const_iterator& it) const
{
- if (d_iterator == nullptr || it.d_iterator == nullptr)
+ if (d_orig_expr == nullptr || it.d_orig_expr == nullptr)
{
return false;
}
- return *static_cast<CVC4::Expr::const_iterator*>(d_iterator)
- == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator);
+ return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos);
}
bool Term::const_iterator::operator!=(const const_iterator& it) const
Term::const_iterator& Term::const_iterator::operator++()
{
- Assert(d_iterator != nullptr);
- ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+ Assert(d_orig_expr != nullptr);
+ ++d_pos;
return *this;
}
Term::const_iterator Term::const_iterator::operator++(int)
{
- Assert(d_iterator != nullptr);
+ Assert(d_orig_expr != nullptr);
const_iterator it = *this;
- ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+ ++d_pos;
return it;
}
Term Term::const_iterator::operator*() const
{
- Assert(d_iterator != nullptr);
- return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator));
+ Assert(d_orig_expr != nullptr);
+ if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF))
+ {
+ return Term(d_orig_expr->getOperator());
+ }
+ else
+ {
+ uint32_t idx = d_pos;
+ if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)
+ {
+ Assert(idx > 0);
+ --idx;
+ }
+ Assert(idx >= 0);
+ return Term((*d_orig_expr)[idx]);
+ }
}
Term::const_iterator Term::begin() const
{
- return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin()));
+ return Term::const_iterator(d_expr, 0);
}
Term::const_iterator Term::end() const
{
- return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
+ int endpos = d_expr->getNumChildren();
+ if (d_expr->getKind() == CVC4::Kind::APPLY_UF)
+ {
+ // one more child if this is a UF application (count the UF as a child)
+ ++endpos;
+ }
+ return Term::const_iterator(d_expr, endpos);
}
// !!! This is only temporarily available until the parser is fully migrated
return ExprHashFunction()(*t.d_expr);
}
-/* -------------------------------------------------------------------------- */
-/* OpTerm */
-/* -------------------------------------------------------------------------- */
-
-OpTerm::OpTerm() : d_expr(new CVC4::Expr()) {}
-
-OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
-
-OpTerm::~OpTerm() {}
-
-bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
-
-bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
-
-Kind OpTerm::getKind() const
-{
- CVC4_API_CHECK_NOT_NULL;
- return intToExtKind(d_expr->getKind());
-}
-
-Sort OpTerm::getSort() const
-{
- CVC4_API_CHECK_NOT_NULL;
- return Sort(d_expr->getType());
-}
-
-bool OpTerm::isNull() const { return d_expr->isNull(); }
-
-template <>
-std::string OpTerm::getIndices() const
-{
- CVC4_API_CHECK_NOT_NULL;
- std::string i;
- Kind k = intToExtKind(d_expr->getKind());
-
- if (k == DIVISIBLE_OP)
- {
- // DIVISIBLE_OP returns a string index to support
- // arbitrary precision integers
- CVC4::Integer _int = d_expr->getConst<Divisible>().k;
- i = _int.toString();
- }
- else if (k == RECORD_UPDATE_OP)
- {
- i = d_expr->getConst<RecordUpdate>().getField();
- }
- else
- {
- CVC4_API_CHECK(false) << "Can't get string index from"
- << " kind " << kindToString(k);
- }
-
- return i;
-}
-
-template <>
-Kind OpTerm::getIndices() const
-{
- CVC4_API_CHECK_NOT_NULL;
- Kind kind = intToExtKind(d_expr->getKind());
- CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
- return intToExtKind(d_expr->getConst<Chain>().getOperator());
-}
-
-template <>
-uint32_t OpTerm::getIndices() const
-{
- CVC4_API_CHECK_NOT_NULL;
- uint32_t i = 0;
- Kind k = intToExtKind(d_expr->getKind());
- switch (k)
- {
- case BITVECTOR_REPEAT_OP:
- i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
- break;
- case BITVECTOR_ZERO_EXTEND_OP:
- i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
- break;
- case BITVECTOR_SIGN_EXTEND_OP:
- i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
- break;
- case BITVECTOR_ROTATE_LEFT_OP:
- i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
- break;
- case BITVECTOR_ROTATE_RIGHT_OP:
- i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
- break;
- case INT_TO_BITVECTOR_OP:
- i = d_expr->getConst<IntToBitVector>().size;
- break;
- case FLOATINGPOINT_TO_UBV_OP:
- i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
- break;
- case FLOATINGPOINT_TO_UBV_TOTAL_OP:
- i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size;
- break;
- case FLOATINGPOINT_TO_SBV_OP:
- i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
- break;
- case FLOATINGPOINT_TO_SBV_TOTAL_OP:
- i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size;
- break;
- case TUPLE_UPDATE_OP: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
- default:
- CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
- << " kind " << kindToString(k);
- }
- return i;
-}
-
-template <>
-std::pair<uint32_t, uint32_t> OpTerm::getIndices() const
-{
- CVC4_API_CHECK_NOT_NULL;
- std::pair<uint32_t, uint32_t> indices;
- Kind k = intToExtKind(d_expr->getKind());
-
- // using if/else instead of case statement because want local variables
- if (k == BITVECTOR_EXTRACT_OP)
- {
- CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
- indices = std::make_pair(ext.high, ext.low);
- }
- else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP)
- {
- CVC4::FloatingPointToFPIEEEBitVector ext =
- d_expr->getConst<FloatingPointToFPIEEEBitVector>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP)
- {
- CVC4::FloatingPointToFPFloatingPoint ext =
- d_expr->getConst<FloatingPointToFPFloatingPoint>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else if (k == FLOATINGPOINT_TO_FP_REAL_OP)
- {
- CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP)
- {
- CVC4::FloatingPointToFPSignedBitVector ext =
- d_expr->getConst<FloatingPointToFPSignedBitVector>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP)
- {
- CVC4::FloatingPointToFPUnsignedBitVector ext =
- d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP)
- {
- CVC4::FloatingPointToFPGeneric ext =
- d_expr->getConst<FloatingPointToFPGeneric>();
- indices = std::make_pair(ext.t.exponent(), ext.t.significand());
- }
- else
- {
- CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
- << " kind " << kindToString(k);
- }
- return indices;
-}
-
-std::string OpTerm::toString() const { return d_expr->toString(); }
-
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; }
-
-std::ostream& operator<<(std::ostream& out, const OpTerm& t)
-{
- out << t.toString();
- return out;
-}
-
-size_t OpTermHashFunction::operator()(const OpTerm& t) const
-{
- return ExprHashFunction()(*t.d_expr);
-}
/* -------------------------------------------------------------------------- */
/* Datatypes */
bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
-OpTerm DatatypeSelector::getSelectorTerm() const
+Op DatatypeSelector::getSelectorTerm() const
{
CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
- return d_stor->getSelector();
+ CVC4::Expr sel = d_stor->getSelector();
+ return Op(APPLY_SELECTOR, sel);
}
std::string DatatypeSelector::toString() const
bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
-OpTerm DatatypeConstructor::getConstructorTerm() const
+Op DatatypeConstructor::getConstructorTerm() const
{
CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
- return OpTerm(d_ctor->getConstructor());
+ CVC4::Expr ctor = d_ctor->getConstructor();
+ return Op(APPLY_CONSTRUCTOR, ctor);
}
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
return (*d_ctor)[name];
}
-OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const
+Op DatatypeConstructor::getSelectorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
- return d_ctor->getSelector(name);
+ CVC4::Expr sel = d_ctor->getSelector(name);
+ return Op(APPLY_SELECTOR, sel);
}
DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
return (*d_dtype)[name];
}
-OpTerm Datatype::getConstructorTerm(const std::string& name) const
+Op Datatype::getConstructorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
- return d_dtype->getConstructor(name);
+ CVC4::Expr ctor = d_dtype->getConstructor(name);
+ return Op(APPLY_CONSTRUCTOR, ctor);
}
size_t Datatype::getNumConstructors() const
return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
}
+Term Solver::mkTermFromKind(Kind kind) const
+{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_KIND_CHECK_EXPECTED(
+ kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+ << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+
+ Term res;
+ if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+ {
+ CVC4::Kind k = extToIntKind(kind);
+ Assert(isDefinedIntKind(k));
+ res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+ }
+ else
+ {
+ Assert(kind == PI);
+ res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+ }
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
/* Helpers for converting vectors. */
/* .......................................................................... */
<< " children (the one under construction has " << nchildren << ")";
}
-void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
-{
- Assert(isDefinedIntKind(extToIntKind(kind)));
- const CVC4::Kind int_kind = extToIntKind(kind);
- const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
- const CVC4::Kind int_op_to_kind =
- NodeManager::operatorToKind(opTerm.d_expr->getNode());
- CVC4_API_ARG_CHECK_EXPECTED(
- int_kind == int_op_to_kind
- || (kind == APPLY_CONSTRUCTOR
- && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
- || (kind == APPLY_SELECTOR
- && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
- || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
- kind)
- << "kind that matches kind associated with given operator term";
- CVC4_API_ARG_CHECK_EXPECTED(
- int_op_kind == CVC4::kind::BUILTIN
- || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
- opTerm)
- << "This term constructor is for parameterized kinds only";
- uint32_t min_arity = ExprManager::minArity(int_kind);
- uint32_t max_arity = ExprManager::maxArity(int_kind);
- CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
- kind)
- << "Terms with kind " << kindToString(kind) << " must have at least "
- << min_arity << " children and at most " << max_arity
- << " children (the one under construction has " << nchildren << ")";
-}
-
/* Sorts Handling */
/* -------------------------------------------------------------------------- */
Term Solver::mkTerm(Kind kind) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_KIND_CHECK_EXPECTED(
- kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
- << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
-
- Term res;
- if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
- {
- CVC4::Kind k = extToIntKind(kind);
- Assert(isDefinedIntKind(k));
- res = d_exprMgr->mkExpr(k, std::vector<Expr>());
- }
- else
- {
- Assert(kind == PI);
- res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
- }
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
-
+ return mkTermFromKind(kind);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
+Term Solver::mkTerm(Op op) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- checkMkOpTerm(kind, opTerm, 0);
- const CVC4::Kind int_kind = extToIntKind(kind);
- Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
+ Term res;
+ if (op.isIndexedHelper())
+ {
+ const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+ res = d_exprMgr->mkExpr(int_kind, *op.d_expr);
+ }
+ else
+ {
+ res = mkTermFromKind(op.d_kind);
+ }
+
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
+Term Solver::mkTerm(Op op, Term child) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
- checkMkOpTerm(kind, opTerm, 1);
- const CVC4::Kind int_kind = extToIntKind(kind);
- Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
+ const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+ Term res;
+ if (op.isIndexedHelper())
+ {
+ res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
+ }
+ else
+ {
+ res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
+ }
+
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
+Term Solver::mkTerm(Op op, Term child1, Term child2) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
- checkMkOpTerm(kind, opTerm, 2);
- const CVC4::Kind int_kind = extToIntKind(kind);
- Term res = d_exprMgr->mkExpr(
- int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+ const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+ Term res;
+ if (op.isIndexedHelper())
+ {
+ res =
+ d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr);
+ }
+ else
+ {
+ res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
+ }
+
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Term Solver::mkTerm(
- Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const
+Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
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(kind, opTerm, 3);
- const CVC4::Kind int_kind = extToIntKind(kind);
- Term res = d_exprMgr->mkExpr(
- int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+ Term res;
+ if (op.isIndexedHelper())
+ {
+ res = d_exprMgr->mkExpr(
+ int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ }
+ else
+ {
+ res = d_exprMgr->mkExpr(
+ int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ }
+
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-Term Solver::mkTerm(Kind kind,
- OpTerm opTerm,
- const std::vector<Term>& children) const
+Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
for (size_t i = 0, size = children.size(); i < size; ++i)
!children[i].isNull(), "parameter term", children[i], i)
<< "non-null term";
}
- checkMkOpTerm(kind, opTerm, children.size());
- const CVC4::Kind int_kind = extToIntKind(kind);
+ const CVC4::Kind int_kind = extToIntKind(op.d_kind);
std::vector<Expr> echildren = termVectorToExprs(children);
- Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
+ Term res;
+ if (op.isIndexedHelper())
+ {
+ res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
+ }
+ else
+ {
+ res = d_exprMgr->mkExpr(int_kind, echildren);
+ }
+
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-/* Create operator terms */
+/* Create operators */
/* -------------------------------------------------------------------------- */
-OpTerm Solver::mkOpTerm(Kind kind, Kind k) const
+Op Solver::mkOp(Kind kind, Kind k) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
+ CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
- return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+ return Op(
+ kind,
+ *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get());
CVC4_API_SOLVER_TRY_CATCH_END;
}
-OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const
+Op Solver::mkOp(Kind kind, const std::string& arg) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_KIND_CHECK_EXPECTED(
- (kind == RECORD_UPDATE_OP) || (kind == DIVISIBLE_OP), kind)
- << "RECORD_UPDATE_OP or DIVISIBLE_OP";
- OpTerm res;
- if (kind == RECORD_UPDATE_OP)
+ CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE),
+ kind)
+ << "RECORD_UPDATE or DIVISIBLE";
+ Op res;
+ if (kind == RECORD_UPDATE)
{
- res =
- *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
+ res = Op(
+ kind,
+ *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
}
else
{
* as invalid. */
CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
<< "a string representing an integer, real or rational value.";
- res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
- .d_expr.get();
+ res = Op(kind,
+ *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
+ .d_expr.get());
}
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
-OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const
+Op Solver::mkOp(Kind kind, uint32_t arg) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK(kind);
- OpTerm res;
+ Op res;
switch (kind)
{
- case DIVISIBLE_OP:
- res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+ case DIVISIBLE:
+ res =
+ Op(kind,
+ *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
break;
- case BITVECTOR_REPEAT_OP:
- res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
- .d_expr.get();
+ case BITVECTOR_REPEAT:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+ .d_expr.get());
break;
- case BITVECTOR_ZERO_EXTEND_OP:
- res = *mkValHelper<CVC4::BitVectorZeroExtend>(
- CVC4::BitVectorZeroExtend(arg))
- .d_expr.get();
+ case BITVECTOR_ZERO_EXTEND:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorZeroExtend>(
+ CVC4::BitVectorZeroExtend(arg))
+ .d_expr.get());
break;
- case BITVECTOR_SIGN_EXTEND_OP:
- res = *mkValHelper<CVC4::BitVectorSignExtend>(
- CVC4::BitVectorSignExtend(arg))
- .d_expr.get();
+ case BITVECTOR_SIGN_EXTEND:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorSignExtend>(
+ CVC4::BitVectorSignExtend(arg))
+ .d_expr.get());
break;
- case BITVECTOR_ROTATE_LEFT_OP:
- res = *mkValHelper<CVC4::BitVectorRotateLeft>(
- CVC4::BitVectorRotateLeft(arg))
- .d_expr.get();
+ case BITVECTOR_ROTATE_LEFT:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorRotateLeft>(
+ CVC4::BitVectorRotateLeft(arg))
+ .d_expr.get());
break;
- case BITVECTOR_ROTATE_RIGHT_OP:
- res = *mkValHelper<CVC4::BitVectorRotateRight>(
- CVC4::BitVectorRotateRight(arg))
- .d_expr.get();
+ case BITVECTOR_ROTATE_RIGHT:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorRotateRight>(
+ CVC4::BitVectorRotateRight(arg))
+ .d_expr.get());
break;
- case INT_TO_BITVECTOR_OP:
- res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
- .d_expr.get();
+ case INT_TO_BITVECTOR:
+ res = Op(kind,
+ *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_UBV_OP:
- res =
+ case FLOATINGPOINT_TO_UBV:
+ res = Op(
+ kind,
*mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
- .d_expr.get();
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_UBV_TOTAL_OP:
- res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
- CVC4::FloatingPointToUBVTotal(arg))
- .d_expr.get();
+ case FLOATINGPOINT_TO_UBV_TOTAL:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToUBVTotal>(
+ CVC4::FloatingPointToUBVTotal(arg))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_SBV_OP:
- res =
+ case FLOATINGPOINT_TO_SBV:
+ res = Op(
+ kind,
*mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
- .d_expr.get();
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_SBV_TOTAL_OP:
- res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
- CVC4::FloatingPointToSBVTotal(arg))
- .d_expr.get();
+ case FLOATINGPOINT_TO_SBV_TOTAL:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToSBVTotal>(
+ CVC4::FloatingPointToSBVTotal(arg))
+ .d_expr.get());
break;
- case TUPLE_UPDATE_OP:
- res =
- *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
+ case TUPLE_UPDATE:
+ res = Op(
+ kind,
+ *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
CVC4_API_SOLVER_TRY_CATCH_END;
}
-OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const
+Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_KIND_CHECK(kind);
- OpTerm res;
+ Op res;
switch (kind)
{
- case BITVECTOR_EXTRACT_OP:
- res = *mkValHelper<CVC4::BitVectorExtract>(
- CVC4::BitVectorExtract(arg1, arg2))
- .d_expr.get();
+ case BITVECTOR_EXTRACT:
+ res = Op(kind,
+ *mkValHelper<CVC4::BitVectorExtract>(
+ CVC4::BitVectorExtract(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
- CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+ CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
- CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
+ CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_REAL_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPReal>(
- CVC4::FloatingPointToFPReal(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_REAL:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPReal>(
+ CVC4::FloatingPointToFPReal(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
- CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
+ CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
- CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+ CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
+ .d_expr.get());
break;
- case FLOATINGPOINT_TO_FP_GENERIC_OP:
- res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
- CVC4::FloatingPointToFPGeneric(arg1, arg2))
- .d_expr.get();
+ case FLOATINGPOINT_TO_FP_GENERIC:
+ res = Op(kind,
+ *mkValHelper<CVC4::FloatingPointToFPGeneric>(
+ CVC4::FloatingPointToFPGeneric(arg1, arg2))
+ .d_expr.get());
break;
default:
CVC4_API_KIND_CHECK_EXPECTED(false, kind)
friend class DatatypeConstructorDecl;
friend class DatatypeDecl;
friend class DatatypeSelectorDecl;
- friend class OpTerm;
+ friend class Op;
friend class Solver;
friend struct SortHashFunction;
friend class Term;
size_t operator()(const Sort& s) const;
};
+/* -------------------------------------------------------------------------- */
+/* Op */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * A CVC4 operator.
+ * An operator is a term that represents certain operators, instantiated
+ * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
+ */
+class CVC4_PUBLIC Op
+{
+ friend class Solver;
+ friend struct OpHashFunction;
+
+ public:
+ /**
+ * Constructor.
+ */
+ Op();
+
+ // !!! This constructor is only temporarily public until the parser is fully
+ // migrated to the new API. !!!
+ /**
+ * Constructor for a single kind (non-indexed operator).
+ * @param k the kind of this Op
+ */
+ Op(const Kind k);
+
+ // !!! This constructor is only temporarily public until the parser is fully
+ // migrated to the new API. !!!
+ /**
+ * Constructor.
+ * @param k the kind of this Op
+ * @param e the internal expression that is to be wrapped by this term
+ * @return the Term
+ */
+ Op(const Kind k, const CVC4::Expr& e);
+
+ /**
+ * Destructor.
+ */
+ ~Op();
+
+ /**
+ * Syntactic equality operator.
+ * Return true if both operators are syntactically identical.
+ * Both operators must belong to the same solver object.
+ * @param t the operator to compare to for equality
+ * @return true if the operators are equal
+ */
+ bool operator==(const Op& t) const;
+
+ /**
+ * Syntactic disequality operator.
+ * Return true if both operators differ syntactically.
+ * Both terms must belong to the same solver object.
+ * @param t the operator to compare to for disequality
+ * @return true if operators are disequal
+ */
+ bool operator!=(const Op& t) const;
+
+ /**
+ * @return the kind of this operator
+ */
+ Kind getKind() const;
+
+ /**
+ * @return the sort of this operator
+ */
+ Sort getSort() const;
+
+ /**
+ * @return true if this operator is a null term
+ */
+ bool isNull() const;
+
+ /**
+ * @return true iff this operator is indexed
+ */
+ bool isIndexed() const;
+
+ /**
+ * Get the indices used to create this Op.
+ * Supports the following template arguments:
+ * - string
+ * - Kind
+ * - uint32_t
+ * - pair<uint32_t, uint32_t>
+ * Check the Op Kind with getKind() to determine which argument to use.
+ * @return the indices used to create this Op
+ */
+ template <typename T>
+ T getIndices() const;
+
+ /**
+ * @return a string representation of this operator
+ */
+ std::string toString() const;
+
+ // !!! This is only temporarily available until the parser is fully migrated
+ // to the new API. !!!
+ CVC4::Expr getExpr(void) const;
+
+ private:
+ /* The kind of this operator. */
+ Kind d_kind;
+
+ /**
+ * The internal expression wrapped by this operator.
+ * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
+ * memory allocation (CVC4::Expr is already ref counted, so this could be
+ * a unique_ptr instead).
+ */
+ std::shared_ptr<CVC4::Expr> d_expr;
+
+ /**
+ * Note: An indexed operator has a non-null internal expr, d_expr
+ * Note 2: We use a helper method to avoid having API functions call
+ * other API functions (we need to call this internally)
+ * @return true iff this Op is indexed
+ */
+ bool isIndexedHelper() const;
+};
+
/* -------------------------------------------------------------------------- */
/* Term */
/* -------------------------------------------------------------------------- */
*/
Sort getSort() const;
+ /**
+ * @return true iff this term has an operator
+ */
+ bool hasOp() const;
+
+ /**
+ * @return the Op used to create this term
+ * Note: This is safe to call when hasOp() returns true.
+ */
+ Op getOp() const;
+
/**
* @return true if this Term is a null term
*/
/**
* Iterator for the children of a Term.
+ * Note: This treats uninterpreted functions as Term just like any other term
+ * for example, the term f(x, y) will have Kind APPLY_UF and three
+ * children: f, x, and y
*/
class const_iterator : public std::iterator<std::input_iterator_tag, Term>
{
public:
/**
- * Constructor.
+ * Null Constructor.
*/
const_iterator();
/**
- * Copy constructor.
+ * Constructor
+ * @param e a shared pointer to the expression that we're iterating over
+ * @param p the position of the iterator (e.g. which child it's on)
*/
- const_iterator(const const_iterator& it);
+ const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p);
/**
- * Destructor.
+ * Copy constructor.
*/
- ~const_iterator();
+ const_iterator(const const_iterator& it);
/**
* Assignment operator.
Term operator*() const;
private:
- /* The internal expression iterator wrapped by this iterator. */
- void* d_iterator;
- /* Constructor. */
- explicit const_iterator(void*);
+ /* The original expression to be iteratoed over */
+ std::shared_ptr<CVC4::Expr> d_orig_expr;
+ /* Keeps track of the iteration position */
+ uint32_t d_pos;
};
/**
const std::unordered_map<Term, V, TermHashFunction>&
unordered_map) CVC4_PUBLIC;
-/* -------------------------------------------------------------------------- */
-/* OpTerm */
-/* -------------------------------------------------------------------------- */
-
-/**
- * A CVC4 operator term.
- * An operator term is a term that represents certain operators, instantiated
- * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
- */
-class CVC4_PUBLIC OpTerm
-{
- friend class Solver;
- friend struct OpTermHashFunction;
-
- public:
- /**
- * Constructor.
- */
- OpTerm();
-
- // !!! This constructor is only temporarily public until the parser is fully
- // migrated to the new API. !!!
- /**
- * Constructor.
- * @param e the internal expression that is to be wrapped by this term
- * @return the Term
- */
- OpTerm(const CVC4::Expr& e);
-
- /**
- * Destructor.
- */
- ~OpTerm();
-
- /**
- * Syntactic equality operator.
- * Return true if both operator terms are syntactically identical.
- * Both operator terms must belong to the same solver object.
- * @param t the operator term to compare to for equality
- * @return true if the operator terms are equal
- */
- bool operator==(const OpTerm& t) const;
-
- /**
- * Syntactic disequality operator.
- * Return true if both operator terms differ syntactically.
- * Both terms must belong to the same solver object.
- * @param t the operator term to compare to for disequality
- * @return true if operator terms are disequal
- */
- bool operator!=(const OpTerm& t) const;
-
- /**
- * @return the kind of this operator term
- */
- Kind getKind() const;
-
- /**
- * @return the sort of this operator term
- */
- Sort getSort() const;
-
- /**
- * @return true if this operator term is a null term
- */
- bool isNull() const;
-
- /**
- * Get the indices used to create this OpTerm.
- * Supports the following template arguments:
- * - string
- * - Kind
- * - uint32_t
- * - pair<uint32_t, uint32_t>
- * Check the OpTerm Kind with getKind() to determine which argument to use.
- * @return the indices used to create this OpTerm
- */
- template <typename T>
- T getIndices() const;
-
- /**
- * @return a string representation of this operator term
- */
- std::string toString() const;
-
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- CVC4::Expr getExpr(void) const;
-
- private:
- /**
- * The internal expression wrapped by this operator term.
- * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
- * memory allocation (CVC4::Expr is already ref counted, so this could be
- * a unique_ptr instead).
- */
- std::shared_ptr<CVC4::Expr> d_expr;
-};
-
/**
- * Serialize an operator term to given stream.
+ * Serialize an operator to given stream.
* @param out the output stream
- * @param t the operator term to be serialized to the given output stream
+ * @param t the operator to be serialized to the given output stream
* @return the output stream
*/
-std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_PUBLIC;
/**
- * Hash function for OpTerms.
+ * Hash function for Ops.
*/
-struct CVC4_PUBLIC OpTermHashFunction
+struct CVC4_PUBLIC OpHashFunction
{
- size_t operator()(const OpTerm& t) const;
+ size_t operator()(const Op& t) const;
};
/* -------------------------------------------------------------------------- */
* Get the selector operator of this datatype selector.
* @return the selector operator
*/
- OpTerm getSelectorTerm() const;
+ Op getSelectorTerm() const;
/**
* @return a string representation of this datatype selector
* Get the constructor operator of this datatype constructor.
* @return the constructor operator
*/
- OpTerm getConstructorTerm() const;
+ Op getConstructorTerm() const;
/**
* Get the datatype selector with the given name.
* @param name the name of the datatype selector
* @return a term representing the datatype selector with the given name
*/
- OpTerm getSelectorTerm(const std::string& name) const;
+ Op getSelectorTerm(const std::string& name) const;
/**
* @return a string representation of this datatype constructor
* similarly-named constructors, the
* first is returned.
*/
- OpTerm getConstructorTerm(const std::string& name) const;
+ Op getConstructorTerm(const std::string& name) const;
/** Get the number of constructors for this Datatype. */
size_t getNumConstructors() const;
Term mkTerm(Kind kind, const std::vector<Term>& children) const;
/**
- * Create nullary term of given kind from a given operator term.
- * Create operator terms with mkOpTerm().
- * @param kind the kind of the term
- * @param the operator term
+ * Create nullary term of given kind from a given operator.
+ * Create operators with mkOp().
+ * @param the operator
* @return the Term
*/
- Term mkTerm(Kind kind, OpTerm opTerm) const;
+ Term mkTerm(Op op) const;
/**
- * Create unary term of given kind from a given operator term.
- * Create operator terms with mkOpTerm().
- * @param kind the kind of the term
- * @param the operator term
+ * Create unary term of given kind from a given operator.
+ * Create operators with mkOp().
+ * @param the operator
* @child the child of the term
* @return the Term
*/
- Term mkTerm(Kind kind, OpTerm opTerm, Term child) const;
+ Term mkTerm(Op op, Term child) const;
/**
- * Create binary term of given kind from a given operator term.
- * @param kind the kind of the term
- * Create operator terms with mkOpTerm().
- * @param the operator term
+ * Create binary term of given kind from a given operator.
+ * Create operators with mkOp().
+ * @param the operator
* @child1 the first child of the term
* @child2 the second child of the term
* @return the Term
*/
- Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const;
+ Term mkTerm(Op op, Term child1, Term child2) const;
/**
- * Create ternary term of given kind from a given operator term.
- * Create operator terms with mkOpTerm().
- * @param kind the kind of the term
- * @param the operator term
+ * Create ternary term of given kind from a given operator.
+ * Create operators with mkOp().
+ * @param the operator
* @child1 the first child of the term
* @child2 the second child of the term
* @child3 the third child of the term
* @return the Term
*/
- Term mkTerm(
- Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const;
+ Term mkTerm(Op op, Term child1, Term child2, Term child3) const;
/**
- * Create n-ary term of given kind from a given operator term.
- * Create operator terms with mkOpTerm().
+ * Create n-ary term of given kind from a given operator.
+ * Create operators with mkOp().
* @param kind the kind of the term
- * @param the operator term
+ * @param the operator
* @children the children of the term
* @return the Term
*/
- Term mkTerm(Kind kind,
- OpTerm opTerm,
- const std::vector<Term>& children) const;
+ Term mkTerm(Op op, const std::vector<Term>& children) const;
/**
* Create a tuple term. Terms are automatically converted if sorts are
/* .................................................................... */
/**
- * Create operator term of kind:
- * - CHAIN_OP
+ * Create operator of kind:
+ * - CHAIN
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param k the kind argument to this operator
*/
- OpTerm mkOpTerm(Kind kind, Kind k) const;
+ Op mkOp(Kind kind, Kind k) const;
/**
* Create operator of kind:
- * - RECORD_UPDATE_OP
- * - DIVISIBLE_OP (to support arbitrary precision integers)
+ * - RECORD_UPDATE
+ * - DIVISIBLE (to support arbitrary precision integers)
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param arg the string argument to this operator
*/
- OpTerm mkOpTerm(Kind kind, const std::string& arg) const;
+ Op mkOp(Kind kind, const std::string& arg) const;
/**
* Create operator of kind:
- * - DIVISIBLE_OP
- * - BITVECTOR_REPEAT_OP
- * - BITVECTOR_ZERO_EXTEND_OP
- * - BITVECTOR_SIGN_EXTEND_OP
- * - BITVECTOR_ROTATE_LEFT_OP
- * - BITVECTOR_ROTATE_RIGHT_OP
- * - INT_TO_BITVECTOR_OP
- * - FLOATINGPOINT_TO_UBV_OP
- * - FLOATINGPOINT_TO_UBV_TOTAL_OP
- * - FLOATINGPOINT_TO_SBV_OP
- * - FLOATINGPOINT_TO_SBV_TOTAL_OP
- * - TUPLE_UPDATE_OP
+ * - DIVISIBLE
+ * - BITVECTOR_REPEAT
+ * - BITVECTOR_ZERO_EXTEND
+ * - BITVECTOR_SIGN_EXTEND
+ * - BITVECTOR_ROTATE_LEFT
+ * - BITVECTOR_ROTATE_RIGHT
+ * - INT_TO_BITVECTOR
+ * - FLOATINGPOINT_TO_UBV
+ * - FLOATINGPOINT_TO_UBV_TOTAL
+ * - FLOATINGPOINT_TO_SBV
+ * - FLOATINGPOINT_TO_SBV_TOTAL
+ * - TUPLE_UPDATE
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param arg the uint32_t argument to this operator
*/
- OpTerm mkOpTerm(Kind kind, uint32_t arg) const;
+ Op mkOp(Kind kind, uint32_t arg) const;
/**
* Create operator of Kind:
- * - BITVECTOR_EXTRACT_OP
- * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
- * - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
- * - FLOATINGPOINT_TO_FP_REAL_OP
- * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
- * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
- * - FLOATINGPOINT_TO_FP_GENERIC_OP
+ * - BITVECTOR_EXTRACT
+ * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
+ * - FLOATINGPOINT_TO_FP_FLOATINGPOINT
+ * - FLOATINGPOINT_TO_FP_REAL
+ * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
+ * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
+ * - FLOATINGPOINT_TO_FP_GENERIC
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param arg1 the first uint32_t argument to this operator
* @param arg2 the second uint32_t argument to this operator
*/
- OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const;
+ Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
/* .................................................................... */
/* Create Constants */
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
/* Helper to convert a vector of sorts to internal types. */
std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
- /* Helper to check for API misuse in mkTerm functions. */
- void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const;
- /* Helper to check for API misuse in mkOpTerm functions. */
+ /* Helper to check for API misuse in mkOp functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/* Helper for mk-functions that call d_exprMgr->mkConst(). */
template <typename T>
Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
/* Helper for setLogic. */
void setLogicHelper(const std::string& logic) const;
+ /* Helper for mkTerm functions that create Term from a Kind */
+ Term mkTermFromKind(Kind kind) const;
/**
* Helper function that ensures that a given term is of sort real (as opposed
*/
CHOICE,
/**
- * Chained operation.
+ * Chained operator.
+ * Parameters: 1
+ * -[1]: Kind of the binary operation
+ * Create with:
+ * mkOp(Kind opkind, Kind kind)
+
+ * Apply chained operation.
* Parameters: n > 1
- * -[1]: Term of kind CHAIN_OP (represents a binary op)
+ * -[1]: Op of kind CHAIN (represents a binary op)
* -[2]..[n]: Arguments to that operator
* Create with:
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, Term child1, Term child2, Term child3)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op, Term child1, Term child2, Term child3)
+ * mkTerm(Op op, const std::vector<Term>& children)
* Turned into a conjunction of binary applications of the operator on
* adjoining parameters.
*/
CHAIN,
- /**
- * Chained operator.
- * Parameters: 1
- * -[1]: Kind of the binary operation
- * Create with:
- * mkOpTerm(Kind opkind, Kind kind)
- */
- CHAIN_OP,
/* Boolean --------------------------------------------------------------- */
* mkTerm(Kind kind, Term child)
*/
ABS,
- /**
- * Divisibility-by-k predicate.
- * Parameters: 2
- * -[1]: DIVISIBLE_OP Term
- * -[2]: Integer Term
- * Create with:
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, const std::vector<Term>& children)
- */
- DIVISIBLE,
/**
* Arithmetic power.
* Parameters: 2
* Parameter: 1
* -[1]: The k to divide by (sort Integer)
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
+ * mkOp(Kind kind, uint32_t param)
+ *
+ * Apply divisibility-by-k predicate.
+ * Parameters: 2
+ * -[1]: Op of kind DIVISIBLE
+ * -[2]: Integer Term
+ * Create with:
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
- DIVISIBLE_OP,
+ DIVISIBLE,
/**
* Multiple-precision rational constant.
* Parameters:
/* term to be treated as a variable. used for eager bit-blasting Ackermann
* expansion of bvurem (internal-only symbol) */
BITVECTOR_ACKERMANIZE_UREM,
- /* operator for the bit-vector boolean bit extract.
- * One parameter, parameter is the index of the bit to extract */
- BITVECTOR_BITOF_OP,
#endif
/**
* Operator for bit-vector extract (from index 'high' to 'low').
* -[1]: The 'high' index
* -[2]: The 'low' index
* Create with:
- * mkOpTerm(Kind kind, uint32_t param, uint32_t param)
+ * mkOp(Kind kind, uint32_t param, uint32_t param)
+ *
+ * Apply bit-vector extract.
+ * Parameters: 2
+ * -[1]: Op of kind BITVECTOR_EXTRACT
+ * -[2]: Term of bit-vector sort
+ * Create with:
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
- BITVECTOR_EXTRACT_OP,
+ BITVECTOR_EXTRACT,
/**
* Operator for bit-vector repeat.
* Parameter 1:
* -[1]: Number of times to repeat a given bit-vector
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply bit-vector repeat.
+ * Parameters: 2
+ * -[1]: Op of kind BITVECTOR_REPEAT
+ * -[2]: Term of bit-vector sort
+ * Create with:
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
- BITVECTOR_REPEAT_OP,
+ BITVECTOR_REPEAT,
/**
* Operator for bit-vector zero-extend.
* Parameter 1:
* -[1]: Number of bits by which a given bit-vector is to be extended
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply bit-vector zero-extend.
+ * Parameters: 2
+ * -[1]: Op of kind BITVECTOR_ZERO_EXTEND
+ * -[2]: Term of bit-vector sort
+ * Create with:
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
- BITVECTOR_ZERO_EXTEND_OP,
+ BITVECTOR_ZERO_EXTEND,
/**
* Operator for bit-vector sign-extend.
* Parameter 1:
* -[1]: Number of bits by which a given bit-vector is to be extended
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
- */
- BITVECTOR_SIGN_EXTEND_OP,
- /**
- * Operator for bit-vector rotate left.
- * Parameter 1:
- * -[1]: Number of bits by which a given bit-vector is to be rotated
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply bit-vector sign-extend.
+ * Parameters: 2
+ * -[1]: Op of kind BITVECTOR_SIGN_EXTEND
+ * -[2]: Term of bit-vector sort
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
- BITVECTOR_ROTATE_LEFT_OP,
+ BITVECTOR_SIGN_EXTEND,
/**
- * Operator for bit-vector rotate right.
+ * Operator for bit-vector rotate left.
* Parameter 1:
* -[1]: Number of bits by which a given bit-vector is to be rotated
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
- */
- BITVECTOR_ROTATE_RIGHT_OP,
-#if 0
- /* bit-vector boolean bit extract.
- * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */
- BITVECTOR_BITOF,
-#endif
- /* Bit-vector extract.
- * Parameters: 2
- * -[1]: BITVECTOR_EXTRACT_OP Term
- * -[2]: Term of bit-vector sort
- * Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
- */
- BITVECTOR_EXTRACT,
- /* Bit-vector repeat.
- * Parameters: 2
- * -[1]: BITVECTOR_REPEAT_OP Term
- * -[2]: Term of bit-vector sort
- * Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
- */
- BITVECTOR_REPEAT,
- /* Bit-vector zero-extend.
- * Parameters: 2
- * -[1]: BITVECTOR_ZERO_EXTEND_OP Term
- * -[2]: Term of bit-vector sort
- * Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
- */
- BITVECTOR_ZERO_EXTEND,
- /* Bit-vector sign-extend.
- * Parameters: 2
- * -[1]: BITVECTOR_SIGN_EXTEND_OP Term
- * -[2]: Term of bit-vector sort
- * Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
- */
- BITVECTOR_SIGN_EXTEND,
- /* Bit-vector rotate left.
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply bit-vector rotate left.
* Parameters: 2
- * -[1]: BITVECTOR_ROTATE_LEFT_OP Term
+ * -[1]: Op of kind BITVECTOR_ROTATE_LEFT
* -[2]: Term of bit-vector sort
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
BITVECTOR_ROTATE_LEFT,
/**
- * Bit-vector rotate right.
+ * Operator for bit-vector rotate right.
+ * Parameter 1:
+ * -[1]: Number of bits by which a given bit-vector is to be rotated
+ * Create with:
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply bit-vector rotate right.
* Parameters: 2
- * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term
+ * -[1]: Op of kind BITVECTOR_ROTATE_RIGHT
* -[2]: Term of bit-vector sort
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
BITVECTOR_ROTATE_RIGHT,
+#if 0
+ /* bit-vector boolean bit extract. */
+ BITVECTOR_BITOF,
+#endif
/**
* Operator for the conversion from Integer to bit-vector.
* Parameter: 1
* -[1]: Size of the bit-vector to convert to
* Create with:
- * mkOpTerm(Kind kind, uint32_t param).
- */
- INT_TO_BITVECTOR_OP,
- /**
- * Integer conversion to bit-vector.
+ * mkOp(Kind kind, uint32_t param).
+ *
+ * Apply integer conversion to bit-vector.
* Parameters: 2
- * -[1]: INT_TO_BITVECTOR_OP Term
+ * -[1]: Op of kind INT_TO_BITVECTOR
* -[2]: Integer term
* Create with:
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
INT_TO_BITVECTOR,
/**
* -[1]: Exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
- /**
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
* Conversion from an IEEE-754 bit vector to floating-point.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
/**
* -[1]: Exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
- /**
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
* Conversion between floating-point sorts.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_FLOATINGPOINT,
/**
* -[1]: Exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_REAL_OP,
- /**
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
* Conversion from a real to floating-point.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_REAL
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_REAL,
/*
* -[1]: Exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
- /**
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
* Conversion from a signed bit vector to floating-point.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
/**
* -[1]: Exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
- /**
- * Operator for converting an unsigned bit vector to floating-point.
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
+ * Converting an unsigned bit vector to floating-point.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
/**
* -[1]: exponent size
* -[2]: Significand size
* Create with:
- * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
- */
- FLOATINGPOINT_TO_FP_GENERIC_OP,
- /**
+ * mkOp(Kind kind, uint32_t param1, uint32_t param2)
+ *
* Generic conversion to floating-point, used in parsing only.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_GENERIC
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_FP_GENERIC,
/**
* Parameters: 1
* -[1]: Size of the bit-vector to convert to
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
- */
- FLOATINGPOINT_TO_UBV_OP,
- /**
+ * mkOp(Kind kind, uint32_t param)
+ *
* Conversion from a floating-point value to an unsigned bit vector.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_UBV,
/**
* Parameters: 1
* -[1]: Size of the bit-vector to convert to
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
- */
- FLOATINGPOINT_TO_UBV_TOTAL_OP,
- /**
+ * mkOp(Kind kind, uint32_t param)
+ *
* Conversion from a floating-point value to an unsigned bit vector
* (defined for all inputs).
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV_TOTAL
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_UBV_TOTAL,
/**
* Parameters: 1
* -[1]: Size of the bit-vector to convert to
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
- */
- FLOATINGPOINT_TO_SBV_OP,
- /**
+ * mkOp(Kind kind, uint32_t param)
+ *
* Conversion from a floating-point value to a signed bit vector.
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_SBV,
/**
* Parameters: 1
* -[1]: Size of the bit-vector to convert to
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
- */
- FLOATINGPOINT_TO_SBV_TOTAL_OP,
- /**
+ * mkOp(Kind kind, uint32_t param)
+ *
* Conversion from a floating-point value to a signed bit vector
* (defined for all inputs).
* Parameters: 2
- * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term
+ * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV_TOTAL
* -[2]: Term of sort FloatingPoint
* Create with:
- * mkTerm(Term opTerm, Term child)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
FLOATINGPOINT_TO_SBV_TOTAL,
/**
* -[1]: Term of array sort
* -[2]: Selection index
* Create with:
- * mkTerm(Term opTerm, Term child1, Term child2)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
SELECT,
/**
* -[2]: Store index
* -[3]: Term to store at the index
* Create with:
- * mkTerm(Term opTerm, Term child1, Term child2, Term child3)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2, Term child3)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
STORE,
/**
* -[1]: Array sort
* -[2]: Term representing a constant
* Create with:
- * mkTerm(Term opTerm, Term child1, Term child2)
- * mkTerm(Term opTerm, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op, const std::vector<Term>& children)
*
* Note: We currently support the creation of constant arrays, but under some
* conditions when there is a chain of equalities connecting two constant
/**
* Constructor application.
* Paramters: n > 0
- * -[1]: Constructor (operator term)
+ * -[1]: Constructor (operator)
* -[2]..[n]: Parameters to the constructor
* Create with:
- * mkTerm(Kind kind, OpTerm opTerm)
- * mkTerm(Kind kind, OpTerm opTerm, Term child)
- * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2)
- * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
- * mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children)
+ * mkTerm(Kind kind, Op op)
+ * mkTerm(Kind kind, Op op, Term child)
+ * mkTerm(Kind kind, Op op, Term child1, Term child2)
+ * mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
+ * mkTerm(Kind kind, Op op, const std::vector<Term>& children)
*/
APPLY_CONSTRUCTOR,
/**
* Datatype selector application.
* Parameters: 1
- * -[1]: Selector (operator term)
+ * -[1]: Selector (operator)
* -[2]: Datatype term (undefined if mis-applied)
* Create with:
- * mkTerm(Kind kind, OpTerm opTerm, Term child)
+ * mkTerm(Kind kind, Op op, Term child)
*/
APPLY_SELECTOR,
/**
* Datatype selector application.
* Parameters: 1
- * -[1]: Selector (operator term)
+ * -[1]: Selector (operator)
* -[2]: Datatype term (defined rigidly if mis-applied)
* Create with:
- * mkTerm(Kind kind, OpTerm opTerm, Term child)
+ * mkTerm(Kind kind, Op op, Term child)
*/
APPLY_SELECTOR_TOTAL,
/**
* Parameters: 1
* -[1]: Index of the tuple to be updated
* Create with:
- * mkOpTerm(Kind kind, uint32_t param)
- */
- TUPLE_UPDATE_OP,
- /**
- * Tuple update.
+ * mkOp(Kind kind, uint32_t param)
+ *
+ * Apply tuple update.
* Parameters: 3
- * -[1]: TUPLE_UPDATE_OP (which references an index)
+ * -[1]: Op of kind TUPLE_UPDATE (which references an index)
* -[2]: Tuple
* -[3]: Element to store in the tuple at the given index
* Create with:
- * mkTerm(Kind kind, Term child1, Term child2, Term child3)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op, const std::vector<Term>& children)
*/
TUPLE_UPDATE,
/**
* Parameters: 1
* -[1]: Name of the field to be updated
* Create with:
- * mkOpTerm(Kind kind, const std::string& param)
- */
- RECORD_UPDATE_OP,
- /**
+ * mkOp(Kind kind, const std::string& param)
+ *
* Record update.
* Parameters: 3
- * -[1]: RECORD_UPDATE_OP Term (which references a field)
+ * -[1]: Op of kind RECORD_UPDATE (which references a field)
* -[2]: Record term to update
* -[3]: Element to store in the record in the given field
* Create with:
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkTerm(Op op, Term child1, Term child2)
+ * mkTerm(Op op,, const std::vector<Term>& children)
*/
RECORD_UPDATE,
#if 0
addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
addIndexedOperator(
- kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
+ kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
+ addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
addIndexedOperator(
- kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat");
- addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND,
- api::BITVECTOR_ZERO_EXTEND_OP,
- "zero_extend");
- addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND,
- api::BITVECTOR_SIGN_EXTEND_OP,
- "sign_extend");
- addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT,
- api::BITVECTOR_ROTATE_LEFT_OP,
- "rotate_left");
+ kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
+ addIndexedOperator(
+ kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
+ addIndexedOperator(
+ kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
- api::BITVECTOR_ROTATE_RIGHT_OP,
+ api::BITVECTOR_ROTATE_RIGHT,
"rotate_right");
- addIndexedOperator(
- kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
+ addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
}
void Smt2::addDatatypesOperators()
addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
- api::FLOATINGPOINT_TO_FP_GENERIC_OP,
+ api::FLOATINGPOINT_TO_FP_GENERIC,
"to_fp");
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+ api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
"to_fp_unsigned");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
+ kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
addIndexedOperator(
- kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
+ kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
if (!strictModeEnabled())
{
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+ api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
"to_fp_bv");
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
- api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+ api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
"to_fp_fp");
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
- api::FLOATINGPOINT_TO_FP_REAL_OP,
+ api::FLOATINGPOINT_TO_FP_REAL,
"to_fp_real");
addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
- api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+ api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
"to_fp_signed");
}
}
addOperator(kind::INTS_DIVISION, "div");
addOperator(kind::INTS_MODULUS, "mod");
addOperator(kind::ABS, "abs");
- addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
+ addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
break;
case THEORY_REALS:
return api::Term();
}
-api::OpTerm Smt2::mkIndexedOp(const std::string& name,
- const std::vector<uint64_t>& numerals)
+api::Op Smt2::mkIndexedOp(const std::string& name,
+ const std::vector<uint64_t>& numerals)
{
const auto& kIt = d_indexedOpKindMap.find(name);
if (kIt != d_indexedOpKindMap.end())
api::Kind k = (*kIt).second;
if (numerals.size() == 1)
{
- return d_solver->mkOpTerm(k, numerals[0]);
+ return d_solver->mkOp(k, numerals[0]);
}
else if (numerals.size() == 2)
{
- return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
+ return d_solver->mkOp(k, numerals[0], numerals[1]);
}
}
parseError(std::string("Unknown indexed function `") + name + "'");
- return api::OpTerm();
+ return api::Op();
}
Expr Smt2::mkDefineFunRec(
std::unordered_map<std::string, Kind> operatorKindMap;
/**
* Maps indexed symbols to the kind of the operator (e.g. "extract" to
- * BITVECTOR_EXTRACT_OP).
+ * BITVECTOR_EXTRACT).
*/
std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
std::pair<Expr, std::string> d_lastNamedTerm;
* BITVECTOR_EXTRACT). NOTE: this is an internal kind for now
* because that is what we use to create expressions. Eventually
* it will be an api::Kind.
- * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT_OP)
+ * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT)
* @param name The name of the symbol (e.g. "extract")
*/
void addIndexedOperator(Kind tKind,
* @return The operator term corresponding to the indexed operator or a parse
* error if the name is not valid.
*/
- api::OpTerm mkIndexedOp(const std::string& name,
- const std::vector<uint64_t>& numerals);
+ api::Op mkIndexedOp(const std::string& name,
+ const std::vector<uint64_t>& numerals);
/**
* Returns the expression that name should be interpreted as.
const std::vector<Expr>& guards,
const std::vector<Expr>& heads,
Expr body);
-
+
/**
* Class for creating instances of `SynthFunCommand`s. Creating an instance
* of this class pushes the scope, destroying it pops the scope.
/* -------------------------------------------------------------------------- */
-namespace
-{
+namespace {
void addLemmaForPair(TNode args1,
TNode args2,
return PreprocessingPassResult::NO_CONFLICT;
}
-
/* -------------------------------------------------------------------------- */
} // namespace passes
* occurring in the input formula, add the following lemma:
* (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
*/
- PreprocessingPassResult applyInternal(
- AssertionPipeline* assertionsToPreprocess) override;
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
private:
/* Map each function to a set of terms associated with it */
<< endl;
setOption("incremental", SExpr("false"));
}
- if (d_logic > LogicInfo("QF_AUFBVLRA")) {
- throw OptionException(
- "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
+ if (d_logic > LogicInfo("QF_AUFBVLRA"))
+ {
+ throw OptionException(
+ "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
}
if (options::bitvectorAlgebraicSolver())
{
? nm->mkNode(kind::UMINUS, nn)
: nn;
return RewriteResponse(REWRITE_AGAIN, ret);
- }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){
+ }
+ else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL)
+ {
Assert(d.getConst<Rational>().isIntegral());
Assert(n.getConst<Rational>().isIntegral());
Assert(!d.getConst<Rational>().isZero());
Node resultNode = mkRationalNode(Rational(result));
return RewriteResponse(REWRITE_DONE, resultNode);
- }else{
+ }
+ else
+ {
return RewriteResponse(REWRITE_DONE, t);
}
}
using namespace CVC4::api;
-class OpTermBlack : public CxxTest::TestSuite
+class OpBlack : public CxxTest::TestSuite
{
public:
void setUp() override {}
void testGetKind();
void testGetSort();
void testIsNull();
+ void testOpTermFromKind();
void testGetIndicesString();
void testGetIndicesKind();
void testGetIndicesUint();
Solver d_solver;
};
-void OpTermBlack::testGetKind()
+void OpBlack::testGetKind()
{
- OpTerm x;
+ Op x;
TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
- x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
TS_ASSERT_THROWS_NOTHING(x.getKind());
}
-void OpTermBlack::testGetSort()
+void OpBlack::testGetSort()
{
- OpTerm x;
+ Op x;
TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
- x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
TS_ASSERT_THROWS_NOTHING(x.getSort());
}
-void OpTermBlack::testIsNull()
+void OpBlack::testIsNull()
{
- OpTerm x;
+ Op x;
TS_ASSERT(x.isNull());
- x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+ x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
TS_ASSERT(!x.isNull());
}
-void OpTermBlack::testGetIndicesString()
+void OpBlack::testOpTermFromKind()
{
- OpTerm x;
+ Op plus(PLUS);
+ TS_ASSERT(!plus.isIndexed());
+ TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
+}
+
+void OpBlack::testGetIndicesString()
+{
+ Op x;
TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&);
- OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4);
+ Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
+ TS_ASSERT(divisible_ot.isIndexed());
std::string divisible_idx = divisible_ot.getIndices<std::string>();
TS_ASSERT(divisible_idx == "4");
- OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "test");
+ Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
std::string record_update_idx = record_update_ot.getIndices<std::string>();
TS_ASSERT(record_update_idx == "test");
TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&);
}
-void OpTermBlack::testGetIndicesKind()
+void OpBlack::testGetIndicesKind()
{
- OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND);
+ Op chain_ot = d_solver.mkOp(CHAIN, AND);
+ TS_ASSERT(chain_ot.isIndexed());
Kind chain_idx = chain_ot.getIndices<Kind>();
TS_ASSERT(chain_idx == AND);
}
-void OpTermBlack::testGetIndicesUint()
+void OpBlack::testGetIndicesUint()
{
- OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5);
+ Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+ TS_ASSERT(bitvector_repeat_ot.isIndexed());
uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
TS_ASSERT(bitvector_repeat_idx == 5);
TS_ASSERT_THROWS(
(bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
CVC4ApiException&);
- OpTerm bitvector_zero_extend_ot =
- d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6);
+ Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
uint32_t bitvector_zero_extend_idx =
bitvector_zero_extend_ot.getIndices<uint32_t>();
TS_ASSERT(bitvector_zero_extend_idx == 6);
- OpTerm bitvector_sign_extend_ot =
- d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7);
+ Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
uint32_t bitvector_sign_extend_idx =
bitvector_sign_extend_ot.getIndices<uint32_t>();
TS_ASSERT(bitvector_sign_extend_idx == 7);
- OpTerm bitvector_rotate_left_ot =
- d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8);
+ Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
uint32_t bitvector_rotate_left_idx =
bitvector_rotate_left_ot.getIndices<uint32_t>();
TS_ASSERT(bitvector_rotate_left_idx == 8);
- OpTerm bitvector_rotate_right_ot =
- d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9);
+ Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
uint32_t bitvector_rotate_right_idx =
bitvector_rotate_right_ot.getIndices<uint32_t>();
TS_ASSERT(bitvector_rotate_right_idx == 9);
- OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10);
+ Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
TS_ASSERT(int_to_bitvector_idx == 10);
- OpTerm floatingpoint_to_ubv_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11);
+ Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
uint32_t floatingpoint_to_ubv_idx =
floatingpoint_to_ubv_ot.getIndices<uint32_t>();
TS_ASSERT(floatingpoint_to_ubv_idx == 11);
- OpTerm floatingpoint_to_ubv_total_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12);
+ Op floatingpoint_to_ubv_total_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_UBV_TOTAL, 12);
uint32_t floatingpoint_to_ubv_total_idx =
floatingpoint_to_ubv_total_ot.getIndices<uint32_t>();
TS_ASSERT(floatingpoint_to_ubv_total_idx == 12);
- OpTerm floatingpoint_to_sbv_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13);
+ Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
uint32_t floatingpoint_to_sbv_idx =
floatingpoint_to_sbv_ot.getIndices<uint32_t>();
TS_ASSERT(floatingpoint_to_sbv_idx == 13);
- OpTerm floatingpoint_to_sbv_total_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14);
+ Op floatingpoint_to_sbv_total_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_SBV_TOTAL, 14);
uint32_t floatingpoint_to_sbv_total_idx =
floatingpoint_to_sbv_total_ot.getIndices<uint32_t>();
TS_ASSERT(floatingpoint_to_sbv_total_idx == 14);
- OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 5);
+ Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
TS_ASSERT(tuple_update_idx == 5);
TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(),
CVC4ApiException&);
}
-void OpTermBlack::testGetIndicesPairUint()
+void OpBlack::testGetIndicesPairUint()
{
- OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0);
+ Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+ TS_ASSERT(bitvector_extract_ot.isIndexed());
std::pair<uint32_t, uint32_t> bitvector_extract_indices =
bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
- OpTerm floatingpoint_to_fp_ieee_bitvector_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 4, 25);
+ Op floatingpoint_to_fp_ieee_bitvector_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
floatingpoint_to_fp_ieee_bitvector_ot
.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices
== std::pair<uint32_t, uint32_t>{4, 25}));
- OpTerm floatingpoint_to_fp_floatingpoint_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 4, 25);
+ Op floatingpoint_to_fp_floatingpoint_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
floatingpoint_to_fp_floatingpoint_ot
.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices
== std::pair<uint32_t, uint32_t>{4, 25}));
- OpTerm floatingpoint_to_fp_real_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 4, 25);
+ Op floatingpoint_to_fp_real_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((floatingpoint_to_fp_real_indices
== std::pair<uint32_t, uint32_t>{4, 25}));
- OpTerm floatingpoint_to_fp_signed_bitvector_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 4, 25);
+ Op floatingpoint_to_fp_signed_bitvector_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
floatingpoint_to_fp_signed_bitvector_ot
.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices
== std::pair<uint32_t, uint32_t>{4, 25}));
- OpTerm floatingpoint_to_fp_unsigned_bitvector_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 4, 25);
+ Op floatingpoint_to_fp_unsigned_bitvector_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
floatingpoint_to_fp_unsigned_bitvector_ot
.getIndices<std::pair<uint32_t, uint32_t>>();
TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices
== std::pair<uint32_t, uint32_t>{4, 25}));
- OpTerm floatingpoint_to_fp_generic_ot =
- d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 4, 25);
+ Op floatingpoint_to_fp_generic_ot =
+ d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
floatingpoint_to_fp_generic_ot
.getIndices<std::pair<uint32_t, uint32_t>>();
void testMkFloatingPointSort();
void testMkDatatypeSort();
void testMkFunctionSort();
- void testMkOpTerm();
+ void testMkOp();
void testMkParamSort();
void testMkPredicateSort();
void testMkRecordSort();
void testMkSepNil();
void testMkString();
void testMkTerm();
- void testMkTermFromOpTerm();
+ void testMkTermFromOp();
void testMkTrue();
void testMkTuple();
void testMkUninterpretedConst();
void testDefineFunRec();
void testDefineFunsRec();
+ void testUFIteration();
+ void testGetOp();
+
void testPush1();
void testPush2();
void testPop1();
}
}
-void SolverBlack::testMkOpTerm()
+void SolverBlack::testMkOp()
{
- // 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&);
+ // mkOp(Kind kind, Kind k)
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(CHAIN, EQUAL));
+ TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&);
- // mkOpTerm(Kind kind, const std::string& arg)
- TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf"));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, "2147483648"));
- TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
+ // mkOp(Kind kind, const std::string& arg)
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(RECORD_UPDATE, "asdf"));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, "2147483648"));
+ TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, "asdf"),
CVC4ApiException&);
- // mkOpTerm(Kind kind, uint32_t arg)
- TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1));
- TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1),
- CVC4ApiException&);
+ // mkOp(Kind kind, uint32_t arg)
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, 1));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_LEFT, 1));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_RIGHT, 1));
+ TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, 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&);
+ // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_EXTRACT, 1, 1));
+ TS_ASSERT_THROWS(d_solver->mkOp(DIVISIBLE, 1, 2), CVC4ApiException&);
}
void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&);
}
-void SolverBlack::testMkTermFromOpTerm()
+void SolverBlack::testMkTermFromOp()
{
Sort bv32 = d_solver->mkBitVectorSort(32);
Term a = d_solver->mkConst(bv32, "a");
std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
std::vector<Term> v3 = {};
// simple operator terms
- 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);
+ Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
+ Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
+ Op opterm3 = d_solver->mkOp(CHAIN, EQUAL);
// list datatype
Sort sort = d_solver->mkParamSort("T");
Term c = d_solver->mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
// list datatype constructor and selector operator terms
- OpTerm consTerm1 = list.getConstructorTerm("cons");
- OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm();
- OpTerm nilTerm1 = list.getConstructorTerm("nil");
- OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm();
- OpTerm headTerm1 = list["cons"].getSelectorTerm("head");
- OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
- OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail");
- OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm();
-
- // mkTerm(Kind kind, OpTerm opTerm) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
- TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1),
+ Op consTerm1 = list.getConstructorTerm("cons");
+ Op consTerm2 = list.getConstructor("cons").getConstructorTerm();
+ Op nilTerm1 = list.getConstructorTerm("nil");
+ Op nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+ Op headTerm1 = list["cons"].getSelectorTerm("head");
+ Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+ Op tailTerm1 = list["cons"].getSelectorTerm("tail");
+ Op tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+ // mkTerm(Kind kind, Op op) const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2));
+ TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+
+ // mkTerm(Kind kind, Op op, Term child) const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c));
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)),
CVC4ApiException&);
- // mkTerm(Kind kind, OpTerm opTerm, Term child) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a));
+ // mkTerm(Kind kind, Op op, Term child1, Term child2) const
TS_ASSERT_THROWS_NOTHING(
- d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1)));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
- TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()),
- CVC4ApiException&);
- TS_ASSERT_THROWS(
- d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
- CVC4ApiException&);
-
- // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
+ d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
- CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
- TS_ASSERT_THROWS_NOTHING(
- d_solver->mkTerm(APPLY_CONSTRUCTOR,
- consTerm1,
- d_solver->mkReal(0),
- d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
- TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b),
+ consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1)));
+ 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&);
- TS_ASSERT_THROWS(
- d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()),
- CVC4ApiException&);
- TS_ASSERT_THROWS(
- d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)),
- CVC4ApiException&);
- // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+ // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
// const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN,
- opterm3,
- d_solver->mkReal(1),
- d_solver->mkReal(1),
- d_solver->mkReal(2)));
- TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a),
- CVC4ApiException&);
+ 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(
- CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+ opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
CVC4ApiException&);
- // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1));
- TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&);
+ // mkTerm(Op op, const std::vector<Term>& children) const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v1));
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v3), CVC4ApiException&);
}
void SolverBlack::testMkTrue()
CVC4ApiException&);
}
+void SolverBlack::testUFIteration()
+{
+ Sort intSort = d_solver->getIntegerSort();
+ Sort funSort = d_solver->mkFunctionSort({intSort, intSort}, intSort);
+ Term x = d_solver->mkConst(intSort, "x");
+ Term y = d_solver->mkConst(intSort, "y");
+ Term f = d_solver->mkConst(funSort, "f");
+ Term fxy = d_solver->mkTerm(APPLY_UF, f, x, y);
+
+ // Expecting the uninterpreted function to be one of the children
+ Term expected_children[3] = {f, x, y};
+ uint32_t idx = 0;
+ for (auto c : fxy)
+ {
+ TS_ASSERT(idx < 3);
+ TS_ASSERT(c == expected_children[idx]);
+ idx++;
+ }
+}
+
+void SolverBlack::testGetOp()
+{
+ Sort bv32 = d_solver->mkBitVectorSort(32);
+ Term a = d_solver->mkConst(bv32, "a");
+ Op ext = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
+ Term exta = d_solver->mkTerm(ext, a);
+
+ TS_ASSERT(!a.hasOp());
+ TS_ASSERT_THROWS(a.getOp(), CVC4ApiException&);
+ TS_ASSERT(exta.hasOp());
+ TS_ASSERT_EQUALS(exta.getOp(), ext);
+
+ // Test Datatypes -- more complicated
+ DatatypeDecl consListSpec("list");
+ DatatypeConstructorDecl cons("cons");
+ DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
+ DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+ cons.addSelector(head);
+ cons.addSelector(tail);
+ consListSpec.addConstructor(cons);
+ DatatypeConstructorDecl nil("nil");
+ consListSpec.addConstructor(nil);
+ Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
+ Datatype consList = consListSort.getDatatype();
+
+ Op consTerm = consList.getConstructorTerm("cons");
+ Op nilTerm = consList.getConstructorTerm("nil");
+ Op headTerm = consList["cons"].getSelectorTerm("head");
+
+ TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR);
+ TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR);
+ TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR);
+
+ Term listnil = d_solver->mkTerm(nilTerm);
+ Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil);
+ Term listhead = d_solver->mkTerm(headTerm, listcons1);
+
+ TS_ASSERT(listnil.hasOp());
+ TS_ASSERT_EQUALS(listnil.getOp(), nilTerm);
+
+ TS_ASSERT(listcons1.hasOp());
+ TS_ASSERT_EQUALS(listcons1.getOp(), consTerm);
+
+ TS_ASSERT(listhead.hasOp());
+ TS_ASSERT_EQUALS(listhead.getOp(), headTerm);
+}
+
void SolverBlack::testPush1()
{
d_solver->setOption("incremental", "true");
TS_ASSERT(i1 == d_solver->simplify(i3));
Datatype consList = consListSort.getDatatype();
- Term dt1 = d_solver->mkTerm(
- APPLY_CONSTRUCTOR,
- consList.getConstructorTerm("cons"),
- d_solver->mkReal(0),
- d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+ Term dt1 =
+ d_solver->mkTerm(consList.getConstructorTerm("cons"),
+ d_solver->mkReal(0),
+ d_solver->mkTerm(consList.getConstructorTerm("nil")));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
- Term dt2 = d_solver->mkTerm(
- APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
+ Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1);
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
Term b1 = d_solver->mkVar(bvSort, "b1");
Term b = d_solver.mkTrue();
TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&);
- TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
Term b = d_solver.mkTrue();
TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&);
- TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
Term b = d_solver.mkTrue();
TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&);
TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&);
- TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
projects / cvc5.git / commitdiff