From 207de293b26cf7771814d3cf421e64fc6116434e Mon Sep 17 00:00:00 2001 From: makaimann Date: Mon, 2 Dec 2019 13:36:19 -0800 Subject: [PATCH] OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (#3355) * Treat uninterpreted functions as a child in Term iteration * Remove unnecessary const_iterator constructor * Add parameter comments to const_iterator constructor * Use operator[] instead of storing a vector of Expr children * Switch pos member variable from int to uint32_t * Add comment about how UFs are treated in iteration * Allow OpTerm to contain a single Kind, update OpTerm construction * Update mkTerm to use only an OpTerm (and not also a Kind) * Remove unnecessary function checkMkOpTerm * Update mkOpTerm comments to not use _OP Kinds * Update examples to use new mkTerm * First pass on fixing unit test * Override kind for Constructor and Selector Terms * More fixes to unit tests * Updates to parser * Remove old assert (for Kind, OpTerm pattern which was removed) * Remove *_OP kinds from public API * Add hasOpTerm and getOpTerm methods to Term * Add test for UF iteration * Add unit test for getOpTerm * Move OpTerm implementation above Term implemenation to match header file Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than forward declaring within the same file that it's declared. * Fix mkTerm in datatypes-new.cpp example * Use helper function for creating term from Kind to avoid nested API calls * Rename: OpTerm->Op in API * Update OpTerm->Op in examples/tests/parser * Add case for APPLY_TESTER * operator term -> operator * Update src/api/cvc4cpp.h Co-Authored-By: Aina Niemetz * Comment comment suggestion Co-Authored-By: Aina Niemetz * Add not-null checks and implement Op from a single Kind constructor * Undo sed mistake for OpTerm replacement * Add 'd_' prefix to member vars * Fix comment and remove old commented-out code * Formatting * Revert "Formatting" This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9. * More fixes for sed mistakes * Minor formatting * Undo changes in CVC parser * Add isIndexed and prefix with d_ * Create helper function for isIndexed to avoid calling API functions in other API functions --- examples/api/bitvectors-new.cpp | 4 +- examples/api/datatypes-new.cpp | 14 +- examples/api/extract-new.cpp | 16 +- src/api/cvc4cpp.cpp | 969 ++++++++++++++----------- src/api/cvc4cpp.h | 386 +++++----- src/api/cvc4cppkind.h | 371 +++++----- src/parser/smt2/smt2.cpp | 51 +- src/parser/smt2/smt2.h | 10 +- src/preprocessing/passes/ackermann.cpp | 4 +- src/preprocessing/passes/ackermann.h | 4 +- src/smt/smt_engine.cpp | 7 +- src/theory/arith/arith_rewriter.cpp | 8 +- test/unit/api/opterm_black.h | 106 +-- test/unit/api/solver_black.h | 234 +++--- test/unit/api/term_black.h | 6 +- 15 files changed, 1172 insertions(+), 1018 deletions(-) diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 58912a1bb..4578da733 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -114,8 +114,8 @@ int main() 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; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index efbd33645..9ff05ac0d 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -36,11 +36,9 @@ void test(Solver& slv, Sort& consListSort) // 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 " @@ -53,8 +51,7 @@ void test(Solver& slv, Sort& consListSort) // 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 @@ -118,8 +115,7 @@ void test(Solver& slv, Sort& consListSort) 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 " diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 0cb885b2c..0f0f8243a 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -30,17 +30,17 @@ int main() 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; diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4bb772e9d..4fd3c4276 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -77,7 +77,6 @@ const static std::unordered_map s_kinds{ {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}, @@ -118,7 +117,6 @@ const static std::unordered_map s_kinds{ {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}, @@ -166,19 +164,12 @@ const static std::unordered_map s_kinds{ {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 ------------------------------------------------------------------ */ @@ -209,34 +200,17 @@ const static std::unordered_map s_kinds{ {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}, @@ -249,9 +223,7 @@ const static std::unordered_map s_kinds{ {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}, @@ -323,7 +295,7 @@ const static std::unordered_map {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}, @@ -364,7 +336,7 @@ const static std::unordered_map {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}, @@ -412,19 +384,19 @@ const static std::unordered_map {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 -------------------------------------------------------------- */ @@ -456,35 +428,33 @@ const static std::unordered_map {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}, @@ -497,9 +467,9 @@ const static std::unordered_map {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}, @@ -1022,6 +992,240 @@ size_t SortHashFunction::operator()(const Sort& s) const 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().k; + i = _int.toString(); + } + else if (k == RECORD_UPDATE) + { + i = d_expr->getConst().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().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().repeatAmount; + break; + case BITVECTOR_ZERO_EXTEND: + i = d_expr->getConst().zeroExtendAmount; + break; + case BITVECTOR_SIGN_EXTEND: + i = d_expr->getConst().signExtendAmount; + break; + case BITVECTOR_ROTATE_LEFT: + i = d_expr->getConst().rotateLeftAmount; + break; + case BITVECTOR_ROTATE_RIGHT: + i = d_expr->getConst().rotateRightAmount; + break; + case INT_TO_BITVECTOR: i = d_expr->getConst().size; break; + case FLOATINGPOINT_TO_UBV: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_UBV_TOTAL: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_SBV: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_SBV_TOTAL: + i = d_expr->getConst().bvs.size; + break; + case TUPLE_UPDATE: i = d_expr->getConst().getIndex(); break; + default: + CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" + << " kind " << kindToString(k); + } + return i; +} + +template <> +std::pair 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 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(); + indices = std::make_pair(ext.high, ext.low); + } + else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + { + CVC4::FloatingPointToFPIEEEBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + { + CVC4::FloatingPointToFPFloatingPoint ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_REAL) + { + CVC4::FloatingPointToFPReal ext = d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPSignedBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPUnsignedBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_GENERIC) + { + CVC4::FloatingPointToFPGeneric ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else + { + CVC4_API_CHECK(false) << "Can't get pair 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 */ /* -------------------------------------------------------------------------- */ @@ -1054,6 +1258,39 @@ Sort Term::getSort() const 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 @@ -1176,41 +1413,38 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) 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& 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(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(d_iterator); - d_iterator = new CVC4::Expr::const_iterator( - *static_cast(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(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(d_iterator) - == *static_cast(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 @@ -1220,33 +1454,53 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const Term::const_iterator& Term::const_iterator::operator++() { - Assert(d_iterator != nullptr); - ++*static_cast(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(d_iterator); + ++d_pos; return it; } Term Term::const_iterator::operator*() const { - Assert(d_iterator != nullptr); - return Term(**static_cast(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 @@ -1300,188 +1554,6 @@ size_t TermHashFunction::operator()(const Term& t) const 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().k; - i = _int.toString(); - } - else if (k == RECORD_UPDATE_OP) - { - i = d_expr->getConst().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().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().repeatAmount; - break; - case BITVECTOR_ZERO_EXTEND_OP: - i = d_expr->getConst().zeroExtendAmount; - break; - case BITVECTOR_SIGN_EXTEND_OP: - i = d_expr->getConst().signExtendAmount; - break; - case BITVECTOR_ROTATE_LEFT_OP: - i = d_expr->getConst().rotateLeftAmount; - break; - case BITVECTOR_ROTATE_RIGHT_OP: - i = d_expr->getConst().rotateRightAmount; - break; - case INT_TO_BITVECTOR_OP: - i = d_expr->getConst().size; - break; - case FLOATINGPOINT_TO_UBV_OP: - i = d_expr->getConst().bvs.size; - break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - i = d_expr->getConst().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_OP: - i = d_expr->getConst().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - i = d_expr->getConst().bvs.size; - break; - case TUPLE_UPDATE_OP: i = d_expr->getConst().getIndex(); break; - default: - CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" - << " kind " << kindToString(k); - } - return i; -} - -template <> -std::pair OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - std::pair 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(); - indices = std::make_pair(ext.high, ext.low); - } - else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP) - { - CVC4::FloatingPointToFPIEEEBitVector ext = - d_expr->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP) - { - CVC4::FloatingPointToFPFloatingPoint ext = - d_expr->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_REAL_OP) - { - CVC4::FloatingPointToFPReal ext = d_expr->getConst(); - 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(); - 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(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP) - { - CVC4::FloatingPointToFPGeneric ext = - d_expr->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else - { - CVC4_API_CHECK(false) << "Can't get pair 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 */ @@ -1635,10 +1707,11 @@ DatatypeSelector::~DatatypeSelector() {} 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 @@ -1675,10 +1748,11 @@ DatatypeConstructor::~DatatypeConstructor() {} 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 @@ -1695,11 +1769,12 @@ DatatypeSelector DatatypeConstructor::getSelector(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 @@ -1824,11 +1899,12 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) 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 @@ -2032,6 +2108,31 @@ Term Solver::mkBVFromStrHelper(uint32_t size, return mkValHelper(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()); + } + 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. */ /* .......................................................................... */ @@ -2079,36 +2180,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " 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 */ /* -------------------------------------------------------------------------- */ @@ -2758,25 +2829,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const 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()); - } - 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; } @@ -2849,69 +2902,99 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const 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& children) const +Term Solver::mkTerm(Op op, const std::vector& children) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) @@ -2920,11 +3003,19 @@ Term Solver::mkTerm(Kind kind, !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 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; @@ -2954,30 +3045,33 @@ Term Solver::mkTuple(const std::vector& sorts, 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(extToIntKind(k))).d_expr.get(); + return Op( + kind, + *mkValHelper(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(arg)).d_expr.get(); + res = Op( + kind, + *mkValHelper(CVC4::RecordUpdate(arg)).d_expr.get()); } else { @@ -2986,76 +3080,90 @@ OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const * as invalid. */ CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg) << "a string representing an integer, real or rational value."; - res = *mkValHelper(CVC4::Divisible(CVC4::Integer(arg))) - .d_expr.get(); + res = Op(kind, + *mkValHelper(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(arg)).d_expr.get(); + case DIVISIBLE: + res = + Op(kind, + *mkValHelper(CVC4::Divisible(arg)).d_expr.get()); break; - case BITVECTOR_REPEAT_OP: - res = *mkValHelper(CVC4::BitVectorRepeat(arg)) - .d_expr.get(); + case BITVECTOR_REPEAT: + res = Op(kind, + *mkValHelper(CVC4::BitVectorRepeat(arg)) + .d_expr.get()); break; - case BITVECTOR_ZERO_EXTEND_OP: - res = *mkValHelper( - CVC4::BitVectorZeroExtend(arg)) - .d_expr.get(); + case BITVECTOR_ZERO_EXTEND: + res = Op(kind, + *mkValHelper( + CVC4::BitVectorZeroExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_SIGN_EXTEND_OP: - res = *mkValHelper( - CVC4::BitVectorSignExtend(arg)) - .d_expr.get(); + case BITVECTOR_SIGN_EXTEND: + res = Op(kind, + *mkValHelper( + CVC4::BitVectorSignExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_LEFT_OP: - res = *mkValHelper( - CVC4::BitVectorRotateLeft(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_LEFT: + res = Op(kind, + *mkValHelper( + CVC4::BitVectorRotateLeft(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_RIGHT_OP: - res = *mkValHelper( - CVC4::BitVectorRotateRight(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_RIGHT: + res = Op(kind, + *mkValHelper( + CVC4::BitVectorRotateRight(arg)) + .d_expr.get()); break; - case INT_TO_BITVECTOR_OP: - res = *mkValHelper(CVC4::IntToBitVector(arg)) - .d_expr.get(); + case INT_TO_BITVECTOR: + res = Op(kind, + *mkValHelper(CVC4::IntToBitVector(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_OP: - res = + case FLOATINGPOINT_TO_UBV: + res = Op( + kind, *mkValHelper(CVC4::FloatingPointToUBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - res = *mkValHelper( - CVC4::FloatingPointToUBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_UBV_TOTAL: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToUBVTotal(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_OP: - res = + case FLOATINGPOINT_TO_SBV: + res = Op( + kind, *mkValHelper(CVC4::FloatingPointToSBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - res = *mkValHelper( - CVC4::FloatingPointToSBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_SBV_TOTAL: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToSBVTotal(arg)) + .d_expr.get()); break; - case TUPLE_UPDATE_OP: - res = - *mkValHelper(CVC4::TupleUpdate(arg)).d_expr.get(); + case TUPLE_UPDATE: + res = Op( + kind, + *mkValHelper(CVC4::TupleUpdate(arg)).d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -3067,48 +3175,55 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const 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(arg1, arg2)) - .d_expr.get(); + case BITVECTOR_EXTRACT: + res = Op(kind, + *mkValHelper( + CVC4::BitVectorExtract(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_REAL_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPReal(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_REAL: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPReal(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_GENERIC_OP: - res = *mkValHelper( - CVC4::FloatingPointToFPGeneric(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_GENERIC: + res = Op(kind, + *mkValHelper( + CVC4::FloatingPointToFPGeneric(arg1, arg2)) + .d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index ad923f866..d73fbfdbd 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -177,7 +177,7 @@ class CVC4_PUBLIC Sort friend class DatatypeConstructorDecl; friend class DatatypeDecl; friend class DatatypeSelectorDecl; - friend class OpTerm; + friend class Op; friend class Solver; friend struct SortHashFunction; friend class Term; @@ -523,6 +523,130 @@ struct CVC4_PUBLIC SortHashFunction 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 + * Check the Op Kind with getKind() to determine which argument to use. + * @return the indices used to create this Op + */ + template + 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 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 */ /* -------------------------------------------------------------------------- */ @@ -590,6 +714,17 @@ class CVC4_PUBLIC 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 */ @@ -668,6 +803,9 @@ class CVC4_PUBLIC 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 { @@ -675,19 +813,21 @@ class CVC4_PUBLIC 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& e, uint32_t p); /** - * Destructor. + * Copy constructor. */ - ~const_iterator(); + const_iterator(const const_iterator& it); /** * Assignment operator. @@ -729,10 +869,10 @@ class CVC4_PUBLIC Term 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 d_orig_expr; + /* Keeps track of the iteration position */ + uint32_t d_pos; }; /** @@ -827,119 +967,20 @@ std::ostream& operator<<(std::ostream& out, const std::unordered_map& 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 - * Check the OpTerm Kind with getKind() to determine which argument to use. - * @return the indices used to create this OpTerm - */ - template - 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 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; }; /* -------------------------------------------------------------------------- */ @@ -1143,7 +1184,7 @@ class CVC4_PUBLIC DatatypeSelector * 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 @@ -1200,7 +1241,7 @@ class CVC4_PUBLIC DatatypeConstructor * 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. @@ -1219,7 +1260,7 @@ class CVC4_PUBLIC DatatypeConstructor * @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 @@ -1366,7 +1407,7 @@ class CVC4_PUBLIC Datatype * 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; @@ -1773,59 +1814,52 @@ class CVC4_PUBLIC Solver Term mkTerm(Kind kind, const std::vector& 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& children) const; + Term mkTerm(Op op, const std::vector& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -1842,59 +1876,59 @@ class CVC4_PUBLIC Solver /* .................................................................... */ /** - * 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 */ @@ -2537,9 +2571,7 @@ class CVC4_PUBLIC Solver std::vector sortVectorToTypes(const std::vector& vector) const; /* Helper to convert a vector of sorts to internal types. */ std::vector termVectorToExprs(const std::vector& 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 @@ -2555,6 +2587,8 @@ class CVC4_PUBLIC Solver 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 diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 1f2a36676..bb2700706 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -143,26 +143,24 @@ enum CVC4_PUBLIC Kind : int32_t */ 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& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector& 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 --------------------------------------------------------------- */ @@ -381,16 +379,6 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) - */ - DIVISIBLE, /** * Arithmetic power. * Parameters: 2 @@ -517,9 +505,17 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) */ - DIVISIBLE_OP, + DIVISIBLE, /** * Multiple-precision rational constant. * Parameters: @@ -973,9 +969,6 @@ enum CVC4_PUBLIC Kind : int32_t /* 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'). @@ -983,125 +976,115 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& 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& 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& 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& 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& 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& 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& 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& 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ INT_TO_BITVECTOR, /** @@ -1371,17 +1354,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /** @@ -1390,17 +1371,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_FLOATINGPOINT, /** @@ -1409,17 +1388,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_REAL, /* @@ -1428,17 +1405,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /** @@ -1447,17 +1422,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /** @@ -1466,17 +1439,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_FP_GENERIC, /** @@ -1484,17 +1455,15 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_UBV, /** @@ -1502,18 +1471,16 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_UBV_TOTAL, /** @@ -1521,17 +1488,15 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_SBV, /** @@ -1539,18 +1504,16 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_SBV_TOTAL, /** @@ -1578,8 +1541,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Term of array sort * -[2]: Selection index * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector& children) */ SELECT, /** @@ -1589,8 +1552,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[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& children) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector& children) */ STORE, /** @@ -1599,8 +1562,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Array sort * -[2]: Term representing a constant * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector& children) * * Note: We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant @@ -1623,32 +1586,32 @@ enum CVC4_PUBLIC Kind : int32_t /** * 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& 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& 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, /** @@ -1674,18 +1637,16 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector& children) */ TUPLE_UPDATE, /** @@ -1693,18 +1654,16 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op,, const std::vector& children) */ RECORD_UPDATE, #if 0 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6dc29b8fe..c7e70495e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -123,23 +123,18 @@ void Smt2::addBitvectorOperators() { 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() @@ -234,29 +229,29 @@ void Smt2::addFloatingPointOperators() { 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"); } } @@ -311,7 +306,7 @@ void Smt2::addTheory(Theory theory) { 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: @@ -549,8 +544,8 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, return api::Term(); } -api::OpTerm Smt2::mkIndexedOp(const std::string& name, - const std::vector& numerals) +api::Op Smt2::mkIndexedOp(const std::string& name, + const std::vector& numerals) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) @@ -558,16 +553,16 @@ api::OpTerm Smt2::mkIndexedOp(const std::string& name, 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( diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ec7e2071a..215f565cd 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -75,7 +75,7 @@ class Smt2 : public Parser std::unordered_map operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to - * BITVECTOR_EXTRACT_OP). + * BITVECTOR_EXTRACT). */ std::unordered_map d_indexedOpKindMap; std::pair d_lastNamedTerm; @@ -106,7 +106,7 @@ class Smt2 : public Parser * 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, @@ -141,8 +141,8 @@ class Smt2 : public Parser * @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& numerals); + api::Op mkIndexedOp(const std::string& name, + const std::vector& numerals); /** * Returns the expression that name should be interpreted as. @@ -214,7 +214,7 @@ class Smt2 : public Parser const std::vector& guards, const std::vector& heads, Expr body); - + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 4b5873e80..87c7fa2ce 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -35,8 +35,7 @@ namespace passes { /* -------------------------------------------------------------------------- */ -namespace -{ +namespace { void addLemmaForPair(TNode args1, TNode args2, @@ -219,7 +218,6 @@ PreprocessingPassResult Ackermann::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } - /* -------------------------------------------------------------------------- */ } // namespace passes diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 8f27cab25..410dde8b9 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -55,8 +55,8 @@ class Ackermann : public PreprocessingPass * 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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index eb10f580a..c47506510 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2283,9 +2283,10 @@ void SmtEngine::setDefaults() { << 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()) { diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 13ab03b45..a1264c612 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -746,7 +746,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ ? 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().isIntegral()); Assert(n.getConst().isIntegral()); Assert(!d.getConst().isZero()); @@ -759,7 +761,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Node resultNode = mkRationalNode(Rational(result)); return RewriteResponse(REWRITE_DONE, resultNode); - }else{ + } + else + { return RewriteResponse(REWRITE_DONE, t); } } diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h index 150cebcbf..0dd7587ff 100644 --- a/test/unit/api/opterm_black.h +++ b/test/unit/api/opterm_black.h @@ -18,7 +18,7 @@ using namespace CVC4::api; -class OpTermBlack : public CxxTest::TestSuite +class OpBlack : public CxxTest::TestSuite { public: void setUp() override {} @@ -27,6 +27,7 @@ class OpTermBlack : public CxxTest::TestSuite void testGetKind(); void testGetSort(); void testIsNull(); + void testOpTermFromKind(); void testGetIndicesString(); void testGetIndicesKind(); void testGetIndicesUint(); @@ -36,168 +37,173 @@ class OpTermBlack : public CxxTest::TestSuite 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(), CVC4ApiException&); +} + +void OpBlack::testGetIndicesString() +{ + Op x; TS_ASSERT_THROWS(x.getIndices(), 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(); 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(); TS_ASSERT(record_update_idx == "test"); TS_ASSERT_THROWS(record_update_ot.getIndices(), 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(); 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(); TS_ASSERT(bitvector_repeat_idx == 5); TS_ASSERT_THROWS( (bitvector_repeat_ot.getIndices>()), 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(); 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(); 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(); 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(); 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(); 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(); 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(); 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(); 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(); 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(); TS_ASSERT(tuple_update_idx == 5); TS_ASSERT_THROWS(tuple_update_ot.getIndices(), 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 bitvector_extract_indices = bitvector_extract_ot.getIndices>(); TS_ASSERT((bitvector_extract_indices == std::pair{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 floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot .getIndices>(); TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices == std::pair{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 floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot .getIndices>(); TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices == std::pair{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 floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices>(); TS_ASSERT((floatingpoint_to_fp_real_indices == std::pair{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 floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot .getIndices>(); TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices == std::pair{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 floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot .getIndices>(); TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices == std::pair{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 floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot .getIndices>(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 374a3ff2a..92313ac3c 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -40,7 +40,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkFloatingPointSort(); void testMkDatatypeSort(); void testMkFunctionSort(); - void testMkOpTerm(); + void testMkOp(); void testMkParamSort(); void testMkPredicateSort(); void testMkRecordSort(); @@ -70,7 +70,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkSepNil(); void testMkString(); void testMkTerm(); - void testMkTermFromOpTerm(); + void testMkTermFromOp(); void testMkTrue(); void testMkTuple(); void testMkUninterpretedConst(); @@ -85,6 +85,9 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunRec(); void testDefineFunsRec(); + void testUFIteration(); + void testGetOp(); + void testPush1(); void testPush2(); void testPop1(); @@ -453,29 +456,27 @@ void SolverBlack::testMkPosZero() } } -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()); } @@ -611,7 +612,7 @@ void SolverBlack::testMkTerm() 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"); @@ -620,9 +621,9 @@ void SolverBlack::testMkTermFromOpTerm() std::vector v2 = {d_solver->mkReal(1), Term()}; std::vector 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"); @@ -641,80 +642,60 @@ void SolverBlack::testMkTermFromOpTerm() 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& 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& 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() @@ -916,6 +897,73 @@ void SolverBlack::testDefineFunsRec() 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"); @@ -1026,14 +1074,12 @@ void SolverBlack::testSimplify() 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"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index c5300dbfe..0d5400f5f 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -207,7 +207,7 @@ void TermBlack::testAndTerm() 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&); @@ -471,7 +471,7 @@ void TermBlack::testImpTerm() 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&); @@ -538,7 +538,7 @@ void TermBlack::testIteTerm() 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)); -- 2.30.2