diff options
author | makaimann <makaim@stanford.edu> | 2019-12-02 13:36:19 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-02 13:36:19 -0800 |
commit | 207de293b26cf7771814d3cf421e64fc6116434e (patch) | |
tree | 3b8af6d5d4504c182bd80df06330829dbcab2516 /src | |
parent | dc99f1c45f616a93ee84b2a6ba877518206bdbaf (diff) |
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 <aina.niemetz@gmail.com>
* Comment comment suggestion
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* 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
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 969 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 386 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 371 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 51 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 10 | ||||
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/ackermann.h | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 8 |
9 files changed, 958 insertions, 852 deletions
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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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}, @@ -1023,6 +993,240 @@ size_t SortHashFunction::operator()(const Sort& s) const } /* -------------------------------------------------------------------------- */ +/* Op */ +/* -------------------------------------------------------------------------- */ + +Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} + +Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {} + +Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e)) +{ +} + +Op::~Op() {} + +/* Helpers */ +/* -------------------------------------------------------------------------- */ + +/* Split out to avoid nested API calls (problematic with API tracing). */ +/* .......................................................................... */ + +bool Op::isIndexedHelper() const { return !d_expr->isNull(); } + +/* Public methods */ +bool Op::operator==(const Op& t) const +{ + if (d_expr->isNull() || t.d_expr->isNull()) + { + return false; + } + return (d_kind == t.d_kind) && (*d_expr == *t.d_expr); +} + +bool Op::operator!=(const Op& t) const { return !(*this == t); } + +Kind Op::getKind() const +{ + CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind"; + return d_kind; +} + +Sort Op::getSort() const +{ + CVC4_API_CHECK_NOT_NULL; + return Sort(d_expr->getType()); +} + +bool Op::isNull() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); } + +bool Op::isIndexed() const { return isIndexedHelper(); } + +template <> +std::string Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + std::string i; + Kind k = intToExtKind(d_expr->getKind()); + + if (k == DIVISIBLE) + { + // DIVISIBLE returns a string index to support + // arbitrary precision integers + CVC4::Integer _int = d_expr->getConst<Divisible>().k; + i = _int.toString(); + } + else if (k == RECORD_UPDATE) + { + i = d_expr->getConst<RecordUpdate>().getField(); + } + else + { + CVC4_API_CHECK(false) << "Can't get string index from" + << " kind " << kindToString(k); + } + + return i; +} + +template <> +Kind Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + Kind kind = intToExtKind(d_expr->getKind()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN"; + return intToExtKind(d_expr->getConst<Chain>().getOperator()); +} + +template <> +uint32_t Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + uint32_t i = 0; + Kind k = intToExtKind(d_expr->getKind()); + switch (k) + { + case BITVECTOR_REPEAT: + i = d_expr->getConst<BitVectorRepeat>().repeatAmount; + break; + case BITVECTOR_ZERO_EXTEND: + i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount; + break; + case BITVECTOR_SIGN_EXTEND: + i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount; + break; + case BITVECTOR_ROTATE_LEFT: + i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount; + break; + case BITVECTOR_ROTATE_RIGHT: + i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount; + break; + case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break; + case FLOATINGPOINT_TO_UBV: + i = d_expr->getConst<FloatingPointToUBV>().bvs.size; + break; + case FLOATINGPOINT_TO_UBV_TOTAL: + i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size; + break; + case FLOATINGPOINT_TO_SBV: + i = d_expr->getConst<FloatingPointToSBV>().bvs.size; + break; + case FLOATINGPOINT_TO_SBV_TOTAL: + i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size; + break; + case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break; + default: + CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" + << " kind " << kindToString(k); + } + return i; +} + +template <> +std::pair<uint32_t, uint32_t> Op::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + + std::pair<uint32_t, uint32_t> indices; + Kind k = intToExtKind(d_expr->getKind()); + + // using if/else instead of case statement because want local variables + if (k == BITVECTOR_EXTRACT) + { + CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>(); + indices = std::make_pair(ext.high, ext.low); + } + else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + { + CVC4::FloatingPointToFPIEEEBitVector ext = + d_expr->getConst<FloatingPointToFPIEEEBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + { + CVC4::FloatingPointToFPFloatingPoint ext = + d_expr->getConst<FloatingPointToFPFloatingPoint>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_REAL) + { + CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPSignedBitVector ext = + d_expr->getConst<FloatingPointToFPSignedBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) + { + CVC4::FloatingPointToFPUnsignedBitVector ext = + d_expr->getConst<FloatingPointToFPUnsignedBitVector>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_GENERIC) + { + CVC4::FloatingPointToFPGeneric ext = + d_expr->getConst<FloatingPointToFPGeneric>(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else + { + CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from" + << " kind " << kindToString(k); + } + return indices; +} + +std::string Op::toString() const +{ + CVC4_API_CHECK_NOT_NULL; + if (d_expr->isNull()) + { + return kindToString(d_kind); + } + else + { + CVC4_API_CHECK(!d_expr->isNull()) + << "Expecting a non-null internal expression"; + return d_expr->toString(); + } +} + +// !!! This is only temporarily available until the parser is fully migrated +// to the new API. !!! +CVC4::Expr Op::getExpr(void) const { return *d_expr; } + +std::ostream& operator<<(std::ostream& out, const Op& t) +{ + out << t.toString(); + return out; +} + +size_t OpHashFunction::operator()(const Op& t) const +{ + if (t.isIndexedHelper()) + { + return ExprHashFunction()(*t.d_expr); + } + else + { + return KindHashFunction()(t.d_kind); + } +} + +/* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ @@ -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<CVC4::Expr>& e, + uint32_t p) + : d_orig_expr(e), d_pos(p) +{ +} Term::const_iterator::const_iterator(const const_iterator& it) - : d_iterator(nullptr) + : d_orig_expr(nullptr) { - if (it.d_iterator != nullptr) + if (it.d_orig_expr != nullptr) { - d_iterator = new CVC4::Expr::const_iterator( - *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + d_orig_expr = it.d_orig_expr; + d_pos = it.d_pos; } } Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) { - delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); - d_iterator = new CVC4::Expr::const_iterator( - *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + d_orig_expr = it.d_orig_expr; + d_pos = it.d_pos; return *this; } -Term::const_iterator::~const_iterator() -{ - delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); -} - bool Term::const_iterator::operator==(const const_iterator& it) const { - if (d_iterator == nullptr || it.d_iterator == nullptr) + if (d_orig_expr == nullptr || it.d_orig_expr == nullptr) { return false; } - return *static_cast<CVC4::Expr::const_iterator*>(d_iterator) - == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator); + return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos); } bool Term::const_iterator::operator!=(const const_iterator& it) const @@ -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<CVC4::Expr::const_iterator*>(d_iterator); + Assert(d_orig_expr != nullptr); + ++d_pos; return *this; } Term::const_iterator Term::const_iterator::operator++(int) { - Assert(d_iterator != nullptr); + Assert(d_orig_expr != nullptr); const_iterator it = *this; - ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator); + ++d_pos; return it; } Term Term::const_iterator::operator*() const { - Assert(d_iterator != nullptr); - return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator)); + Assert(d_orig_expr != nullptr); + if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)) + { + return Term(d_orig_expr->getOperator()); + } + else + { + uint32_t idx = d_pos; + if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF) + { + Assert(idx > 0); + --idx; + } + Assert(idx >= 0); + return Term((*d_orig_expr)[idx]); + } } Term::const_iterator Term::begin() const { - return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin())); + return Term::const_iterator(d_expr, 0); } Term::const_iterator Term::end() const { - return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end())); + int endpos = d_expr->getNumChildren(); + if (d_expr->getKind() == CVC4::Kind::APPLY_UF) + { + // one more child if this is a UF application (count the UF as a child) + ++endpos; + } + return Term::const_iterator(d_expr, endpos); } // !!! This is only temporarily available until the parser is fully migrated @@ -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<Divisible>().k; - i = _int.toString(); - } - else if (k == RECORD_UPDATE_OP) - { - i = d_expr->getConst<RecordUpdate>().getField(); - } - else - { - CVC4_API_CHECK(false) << "Can't get string index from" - << " kind " << kindToString(k); - } - - return i; -} - -template <> -Kind OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - Kind kind = intToExtKind(d_expr->getKind()); - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; - return intToExtKind(d_expr->getConst<Chain>().getOperator()); -} - -template <> -uint32_t OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - uint32_t i = 0; - Kind k = intToExtKind(d_expr->getKind()); - switch (k) - { - case BITVECTOR_REPEAT_OP: - i = d_expr->getConst<BitVectorRepeat>().repeatAmount; - break; - case BITVECTOR_ZERO_EXTEND_OP: - i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount; - break; - case BITVECTOR_SIGN_EXTEND_OP: - i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount; - break; - case BITVECTOR_ROTATE_LEFT_OP: - i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount; - break; - case BITVECTOR_ROTATE_RIGHT_OP: - i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount; - break; - case INT_TO_BITVECTOR_OP: - i = d_expr->getConst<IntToBitVector>().size; - break; - case FLOATINGPOINT_TO_UBV_OP: - i = d_expr->getConst<FloatingPointToUBV>().bvs.size; - break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_OP: - i = d_expr->getConst<FloatingPointToSBV>().bvs.size; - break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size; - break; - case TUPLE_UPDATE_OP: i = d_expr->getConst<TupleUpdate>().getIndex(); break; - default: - CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" - << " kind " << kindToString(k); - } - return i; -} - -template <> -std::pair<uint32_t, uint32_t> OpTerm::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - std::pair<uint32_t, uint32_t> indices; - Kind k = intToExtKind(d_expr->getKind()); - - // using if/else instead of case statement because want local variables - if (k == BITVECTOR_EXTRACT_OP) - { - CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>(); - indices = std::make_pair(ext.high, ext.low); - } - else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP) - { - CVC4::FloatingPointToFPIEEEBitVector ext = - d_expr->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP) - { - CVC4::FloatingPointToFPFloatingPoint ext = - d_expr->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_REAL_OP) - { - CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP) - { - CVC4::FloatingPointToFPSignedBitVector ext = - d_expr->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP) - { - CVC4::FloatingPointToFPUnsignedBitVector ext = - d_expr->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP) - { - CVC4::FloatingPointToFPGeneric ext = - d_expr->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); - } - else - { - CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from" - << " kind " << kindToString(k); - } - return indices; -} - -std::string OpTerm::toString() const { return d_expr->toString(); } - -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; } - -std::ostream& operator<<(std::ostream& out, const OpTerm& t) -{ - out << t.toString(); - return out; -} - -size_t OpTermHashFunction::operator()(const OpTerm& t) const -{ - return ExprHashFunction()(*t.d_expr); -} /* -------------------------------------------------------------------------- */ /* Datatypes */ @@ -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>(CVC4::BitVector(size, val)); } +Term Solver::mkTermFromKind(Kind kind) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK_EXPECTED( + kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) + << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; + + Term res; + if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) + { + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + res = d_exprMgr->mkExpr(k, std::vector<Expr>()); + } + else + { + Assert(kind == PI); + res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); + } + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Helpers for converting vectors. */ /* .......................................................................... */ @@ -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<Expr>()); - } - else - { - Assert(kind == PI); - res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); - } - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - + return mkTermFromKind(kind); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -2849,69 +2902,99 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& 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<Term>& children) const +Term Solver::mkTerm(Op op, const std::vector<Term>& children) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = children.size(); i < size; ++i) @@ -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<Expr> echildren = termVectorToExprs(children); - Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren); + Term res; + if (op.isIndexedHelper()) + { + res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren); + } + else + { + res = d_exprMgr->mkExpr(int_kind, echildren); + } + (void)res.d_expr->getType(true); /* kick off type checking */ return res; @@ -2954,30 +3045,33 @@ Term Solver::mkTuple(const std::vector<Sort>& 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>(CVC4::Chain(extToIntKind(k))).d_expr.get(); + return Op( + kind, + *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get()); CVC4_API_SOLVER_TRY_CATCH_END; } -OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const +Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED( - (kind == RECORD_UPDATE_OP) || (kind == DIVISIBLE_OP), kind) - << "RECORD_UPDATE_OP or DIVISIBLE_OP"; - OpTerm res; - if (kind == RECORD_UPDATE_OP) + CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE), + kind) + << "RECORD_UPDATE or DIVISIBLE"; + Op res; + if (kind == RECORD_UPDATE) { - res = - *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get(); + res = Op( + kind, + *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get()); } else { @@ -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::Divisible(CVC4::Integer(arg))) - .d_expr.get(); + res = Op(kind, + *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg))) + .d_expr.get()); } return res; CVC4_API_SOLVER_TRY_CATCH_END; } -OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const +Op Solver::mkOp(Kind kind, uint32_t arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_KIND_CHECK(kind); - OpTerm res; + Op res; switch (kind) { - case DIVISIBLE_OP: - res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get(); + case DIVISIBLE: + res = + Op(kind, + *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get()); break; - case BITVECTOR_REPEAT_OP: - res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) - .d_expr.get(); + case BITVECTOR_REPEAT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) + .d_expr.get()); break; - case BITVECTOR_ZERO_EXTEND_OP: - res = *mkValHelper<CVC4::BitVectorZeroExtend>( - CVC4::BitVectorZeroExtend(arg)) - .d_expr.get(); + case BITVECTOR_ZERO_EXTEND: + res = Op(kind, + *mkValHelper<CVC4::BitVectorZeroExtend>( + CVC4::BitVectorZeroExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_SIGN_EXTEND_OP: - res = *mkValHelper<CVC4::BitVectorSignExtend>( - CVC4::BitVectorSignExtend(arg)) - .d_expr.get(); + case BITVECTOR_SIGN_EXTEND: + res = Op(kind, + *mkValHelper<CVC4::BitVectorSignExtend>( + CVC4::BitVectorSignExtend(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_LEFT_OP: - res = *mkValHelper<CVC4::BitVectorRotateLeft>( - CVC4::BitVectorRotateLeft(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_LEFT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRotateLeft>( + CVC4::BitVectorRotateLeft(arg)) + .d_expr.get()); break; - case BITVECTOR_ROTATE_RIGHT_OP: - res = *mkValHelper<CVC4::BitVectorRotateRight>( - CVC4::BitVectorRotateRight(arg)) - .d_expr.get(); + case BITVECTOR_ROTATE_RIGHT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorRotateRight>( + CVC4::BitVectorRotateRight(arg)) + .d_expr.get()); break; - case INT_TO_BITVECTOR_OP: - res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) - .d_expr.get(); + case INT_TO_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_OP: - res = + case FLOATINGPOINT_TO_UBV: + res = Op( + kind, *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_TOTAL_OP: - res = *mkValHelper<CVC4::FloatingPointToUBVTotal>( - CVC4::FloatingPointToUBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_UBV_TOTAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToUBVTotal>( + CVC4::FloatingPointToUBVTotal(arg)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_OP: - res = + case FLOATINGPOINT_TO_SBV: + res = Op( + kind, *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) - .d_expr.get(); + .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_TOTAL_OP: - res = *mkValHelper<CVC4::FloatingPointToSBVTotal>( - CVC4::FloatingPointToSBVTotal(arg)) - .d_expr.get(); + case FLOATINGPOINT_TO_SBV_TOTAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToSBVTotal>( + CVC4::FloatingPointToSBVTotal(arg)) + .d_expr.get()); break; - case TUPLE_UPDATE_OP: - res = - *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get(); + case TUPLE_UPDATE: + res = Op( + kind, + *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -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>( - CVC4::BitVectorExtract(arg1, arg2)) - .d_expr.get(); + case BITVECTOR_EXTRACT: + res = Op(kind, + *mkValHelper<CVC4::BitVectorExtract>( + CVC4::BitVectorExtract(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( - CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( + CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( - CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( + CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_REAL_OP: - res = *mkValHelper<CVC4::FloatingPointToFPReal>( - CVC4::FloatingPointToFPReal(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_REAL: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPReal>( + CVC4::FloatingPointToFPReal(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( - CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( + CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: - res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( - CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( + CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) + .d_expr.get()); break; - case FLOATINGPOINT_TO_FP_GENERIC_OP: - res = *mkValHelper<CVC4::FloatingPointToFPGeneric>( - CVC4::FloatingPointToFPGeneric(arg1, arg2)) - .d_expr.get(); + case FLOATINGPOINT_TO_FP_GENERIC: + res = Op(kind, + *mkValHelper<CVC4::FloatingPointToFPGeneric>( + CVC4::FloatingPointToFPGeneric(arg1, arg2)) + .d_expr.get()); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) 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; @@ -524,6 +524,130 @@ struct CVC4_PUBLIC SortHashFunction }; /* -------------------------------------------------------------------------- */ +/* Op */ +/* -------------------------------------------------------------------------- */ + +/** + * A CVC4 operator. + * An operator is a term that represents certain operators, instantiated + * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. + */ +class CVC4_PUBLIC Op +{ + friend class Solver; + friend struct OpHashFunction; + + public: + /** + * Constructor. + */ + Op(); + + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor for a single kind (non-indexed operator). + * @param k the kind of this Op + */ + Op(const Kind k); + + // !!! This constructor is only temporarily public until the parser is fully + // migrated to the new API. !!! + /** + * Constructor. + * @param k the kind of this Op + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + Op(const Kind k, const CVC4::Expr& e); + + /** + * Destructor. + */ + ~Op(); + + /** + * Syntactic equality operator. + * Return true if both operators are syntactically identical. + * Both operators must belong to the same solver object. + * @param t the operator to compare to for equality + * @return true if the operators are equal + */ + bool operator==(const Op& t) const; + + /** + * Syntactic disequality operator. + * Return true if both operators differ syntactically. + * Both terms must belong to the same solver object. + * @param t the operator to compare to for disequality + * @return true if operators are disequal + */ + bool operator!=(const Op& t) const; + + /** + * @return the kind of this operator + */ + Kind getKind() const; + + /** + * @return the sort of this operator + */ + Sort getSort() const; + + /** + * @return true if this operator is a null term + */ + bool isNull() const; + + /** + * @return true iff this operator is indexed + */ + bool isIndexed() const; + + /** + * Get the indices used to create this Op. + * Supports the following template arguments: + * - string + * - Kind + * - uint32_t + * - pair<uint32_t, uint32_t> + * Check the Op Kind with getKind() to determine which argument to use. + * @return the indices used to create this Op + */ + template <typename T> + T getIndices() const; + + /** + * @return a string representation of this operator + */ + std::string toString() const; + + // !!! This is only temporarily available until the parser is fully migrated + // to the new API. !!! + CVC4::Expr getExpr(void) const; + + private: + /* The kind of this operator. */ + Kind d_kind; + + /** + * The internal expression wrapped by this operator. + * This is a shared_ptr rather than a unique_ptr to avoid overhead due to + * memory allocation (CVC4::Expr is already ref counted, so this could be + * a unique_ptr instead). + */ + std::shared_ptr<CVC4::Expr> d_expr; + + /** + * Note: An indexed operator has a non-null internal expr, d_expr + * Note 2: We use a helper method to avoid having API functions call + * other API functions (we need to call this internally) + * @return true iff this Op is indexed + */ + bool isIndexedHelper() const; +}; + +/* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ @@ -591,6 +715,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 */ bool isNull() const; @@ -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<std::input_iterator_tag, Term> { @@ -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<CVC4::Expr>& 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<CVC4::Expr> 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<Term, V, TermHashFunction>& unordered_map) CVC4_PUBLIC; -/* -------------------------------------------------------------------------- */ -/* OpTerm */ -/* -------------------------------------------------------------------------- */ - -/** - * A CVC4 operator term. - * An operator term is a term that represents certain operators, instantiated - * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. - */ -class CVC4_PUBLIC OpTerm -{ - friend class Solver; - friend struct OpTermHashFunction; - - public: - /** - * Constructor. - */ - OpTerm(); - - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param e the internal expression that is to be wrapped by this term - * @return the Term - */ - OpTerm(const CVC4::Expr& e); - - /** - * Destructor. - */ - ~OpTerm(); - - /** - * Syntactic equality operator. - * Return true if both operator terms are syntactically identical. - * Both operator terms must belong to the same solver object. - * @param t the operator term to compare to for equality - * @return true if the operator terms are equal - */ - bool operator==(const OpTerm& t) const; - - /** - * Syntactic disequality operator. - * Return true if both operator terms differ syntactically. - * Both terms must belong to the same solver object. - * @param t the operator term to compare to for disequality - * @return true if operator terms are disequal - */ - bool operator!=(const OpTerm& t) const; - - /** - * @return the kind of this operator term - */ - Kind getKind() const; - - /** - * @return the sort of this operator term - */ - Sort getSort() const; - - /** - * @return true if this operator term is a null term - */ - bool isNull() const; - - /** - * Get the indices used to create this OpTerm. - * Supports the following template arguments: - * - string - * - Kind - * - uint32_t - * - pair<uint32_t, uint32_t> - * Check the OpTerm Kind with getKind() to determine which argument to use. - * @return the indices used to create this OpTerm - */ - template <typename T> - T getIndices() const; - - /** - * @return a string representation of this operator term - */ - std::string toString() const; - - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - CVC4::Expr getExpr(void) const; - - private: - /** - * The internal expression wrapped by this operator term. - * This is a shared_ptr rather than a unique_ptr to avoid overhead due to - * memory allocation (CVC4::Expr is already ref counted, so this could be - * a unique_ptr instead). - */ - std::shared_ptr<CVC4::Expr> d_expr; -}; - /** - * Serialize an operator term to given stream. + * Serialize an operator to given stream. * @param out the output stream - * @param t the operator term to be serialized to the given output stream + * @param t the operator to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_PUBLIC; /** - * Hash function for OpTerms. + * Hash function for Ops. */ -struct CVC4_PUBLIC OpTermHashFunction +struct CVC4_PUBLIC OpHashFunction { - size_t operator()(const OpTerm& t) const; + size_t operator()(const Op& t) const; }; /* -------------------------------------------------------------------------- */ @@ -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<Term>& children) const; /** - * Create nullary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create nullary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm) const; + Term mkTerm(Op op) const; /** - * Create unary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create unary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child the child of the term * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm, Term child) const; + Term mkTerm(Op op, Term child) const; /** - * Create binary term of given kind from a given operator term. - * @param kind the kind of the term - * Create operator terms with mkOpTerm(). - * @param the operator term + * Create binary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child1 the first child of the term * @child2 the second child of the term * @return the Term */ - Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const; + Term mkTerm(Op op, Term child1, Term child2) const; /** - * Create ternary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). - * @param kind the kind of the term - * @param the operator term + * Create ternary term of given kind from a given operator. + * Create operators with mkOp(). + * @param the operator * @child1 the first child of the term * @child2 the second child of the term * @child3 the third child of the term * @return the Term */ - Term mkTerm( - Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const; + Term mkTerm(Op op, Term child1, Term child2, Term child3) const; /** - * Create n-ary term of given kind from a given operator term. - * Create operator terms with mkOpTerm(). + * Create n-ary term of given kind from a given operator. + * Create operators with mkOp(). * @param kind the kind of the term - * @param the operator term + * @param the operator * @children the children of the term * @return the Term */ - Term mkTerm(Kind kind, - OpTerm opTerm, - const std::vector<Term>& children) const; + Term mkTerm(Op op, const std::vector<Term>& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -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<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; /* Helper to convert a vector of sorts to internal types. */ std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const; - /* Helper to check for API misuse in mkTerm functions. */ - void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const; - /* Helper to check for API misuse in mkOpTerm functions. */ + /* Helper to check for API misuse in mkOp functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ template <typename T> @@ -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<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& children) * Turned into a conjunction of binary applications of the operator on * adjoining parameters. */ CHAIN, - /** - * Chained operator. - * Parameters: 1 - * -[1]: Kind of the binary operation - * Create with: - * mkOpTerm(Kind opkind, Kind kind) - */ - CHAIN_OP, /* Boolean --------------------------------------------------------------- */ @@ -382,16 +380,6 @@ enum CVC4_PUBLIC Kind : int32_t */ ABS, /** - * Divisibility-by-k predicate. - * Parameters: 2 - * -[1]: DIVISIBLE_OP Term - * -[2]: Integer Term - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) - */ - DIVISIBLE, - /** * Arithmetic power. * Parameters: 2 * -[1]..[2]: Terms of sort Integer, Real @@ -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<Term>& 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<Term>& children) */ - BITVECTOR_EXTRACT_OP, + BITVECTOR_EXTRACT, /** * Operator for bit-vector repeat. * Parameter 1: * -[1]: Number of times to repeat a given bit-vector * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector repeat. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_REPEAT + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_REPEAT_OP, + BITVECTOR_REPEAT, /** * Operator for bit-vector zero-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector zero-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_ZERO_EXTEND + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ZERO_EXTEND_OP, + BITVECTOR_ZERO_EXTEND, /** * Operator for bit-vector sign-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_SIGN_EXTEND_OP, - /** - * Operator for bit-vector rotate left. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be rotated + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector sign-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_SIGN_EXTEND + * -[2]: Term of bit-vector sort * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ROTATE_LEFT_OP, + BITVECTOR_SIGN_EXTEND, /** - * Operator for bit-vector rotate right. + * Operator for bit-vector rotate left. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be rotated * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_ROTATE_RIGHT_OP, -#if 0 - /* bit-vector boolean bit extract. - * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */ - BITVECTOR_BITOF, -#endif - /* Bit-vector extract. - * Parameters: 2 - * -[1]: BITVECTOR_EXTRACT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_EXTRACT, - /* Bit-vector repeat. - * Parameters: 2 - * -[1]: BITVECTOR_REPEAT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_REPEAT, - /* Bit-vector zero-extend. - * Parameters: 2 - * -[1]: BITVECTOR_ZERO_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_ZERO_EXTEND, - /* Bit-vector sign-extend. - * Parameters: 2 - * -[1]: BITVECTOR_SIGN_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_SIGN_EXTEND, - /* Bit-vector rotate left. + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate left. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_LEFT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_LEFT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_LEFT, /** - * Bit-vector rotate right. + * Operator for bit-vector rotate right. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be rotated + * Create with: + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate right. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_RIGHT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_RIGHT, +#if 0 + /* bit-vector boolean bit extract. */ + BITVECTOR_BITOF, +#endif /** * Operator for the conversion from Integer to bit-vector. * Parameter: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - INT_TO_BITVECTOR_OP, - /** - * Integer conversion to bit-vector. + * mkOp(Kind kind, uint32_t param). + * + * Apply integer conversion to bit-vector. * Parameters: 2 - * -[1]: INT_TO_BITVECTOR_OP Term + * -[1]: Op of kind INT_TO_BITVECTOR * -[2]: Integer term * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ INT_TO_BITVECTOR, /** @@ -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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) * * Note: We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant @@ -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<Term>& children) + * mkTerm(Kind kind, Op op) + * mkTerm(Kind kind, Op op, Term child) + * mkTerm(Kind kind, Op op, Term child1, Term child2) + * mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, Op op, const std::vector<Term>& children) */ APPLY_CONSTRUCTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (undefined if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (defined rigidly if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR_TOTAL, /** @@ -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<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& 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<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op,, const std::vector<Term>& 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<uint64_t>& numerals) +api::Op Smt2::mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) @@ -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<std::string, Kind> operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to - * BITVECTOR_EXTRACT_OP). + * BITVECTOR_EXTRACT). */ std::unordered_map<std::string, api::Kind> d_indexedOpKindMap; std::pair<Expr, std::string> d_lastNamedTerm; @@ -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<uint64_t>& numerals); + api::Op mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals); /** * Returns the expression that name should be interpreted as. @@ -214,7 +214,7 @@ class Smt2 : public Parser const std::vector<Expr>& guards, const std::vector<Expr>& heads, Expr body); - + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. 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<Rational>().isIntegral()); Assert(n.getConst<Rational>().isIntegral()); Assert(!d.getConst<Rational>().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); } } |