diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 47 | ||||
| -rw-r--r-- | src/api/cpp/cvc5.h | 5 |
2 files changed, 52 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aafc5331a..9fb008bfd 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -428,6 +428,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::TO_INTEGER, TO_INTEGER}, {cvc5::Kind::TO_REAL, TO_REAL}, {cvc5::Kind::PI, PI}, + {cvc5::Kind::IAND_OP, IAND}, /* BV -------------------------------------------------------------- */ {cvc5::Kind::CONST_BITVECTOR, CONST_BITVECTOR}, {cvc5::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT}, @@ -1842,6 +1843,52 @@ bool Op::isIndexed() const CVC5_API_TRY_CATCH_END; } +size_t Op::getNumIndices() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + if (!isIndexedHelper()) + { + return 0; + } + + Kind k = intToExtKind(d_node->getKind()); + size_t size = 0; + switch (k) + { + case DIVISIBLE: size = 1; break; + case RECORD_UPDATE: size = 1; break; + case BITVECTOR_REPEAT: size = 1; break; + case BITVECTOR_ZERO_EXTEND: size = 1; break; + case BITVECTOR_SIGN_EXTEND: size = 1; break; + case BITVECTOR_ROTATE_LEFT: size = 1; break; + case BITVECTOR_ROTATE_RIGHT: size = 1; break; + case INT_TO_BITVECTOR: size = 1; break; + case IAND: size = 1; break; + case FLOATINGPOINT_TO_UBV: size = 1; break; + case FLOATINGPOINT_TO_SBV: size = 1; break; + case TUPLE_UPDATE: size = 1; break; + case REGEXP_REPEAT: size = 1; break; + case BITVECTOR_EXTRACT: size = 2; break; + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break; + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: size = 2; break; + case FLOATINGPOINT_TO_FP_REAL: size = 2; break; + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: size = 2; break; + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: size = 2; break; + case FLOATINGPOINT_TO_FP_GENERIC: size = 2; break; + case REGEXP_LOOP: size = 2; break; + case TUPLE_PROJECT: + size = d_node->getConst<TupleProjectOp>().getIndices().size(); + break; + default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k); + } + + //////// all checks before this line + return size; + //////// + CVC5_API_TRY_CATCH_END; +} + template <> std::string Op::getIndices() const { diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index aaf19c30b..c8f1b8d4a 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -819,6 +819,11 @@ class CVC4_EXPORT Op bool isIndexed() const; /** + * @return the number of indices of this op + */ + size_t getNumIndices() const; + + /** * Get the indices used to create this Op. * Supports the following template arguments: * - string |