diff options
| author | makaimann <makaim@stanford.edu> | 2019-12-04 18:59:44 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-12-04 18:59:44 -0800 |
| commit | 2c68fa6fea5f98d6e5078961156d8c746bbd13c3 (patch) | |
| tree | 7ba9d6bc5d024363321a30db3292e9d93ef3a8f9 /src/api/cvc4cpp.cpp | |
| parent | ae789c1d976b21bac4217a83f5ad9615b8f5e0f5 (diff) | |
Add mkOp for a single Kind (#3522)
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 39 |
1 files changed, 38 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 651ed60e4..7a3577e0d 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -527,6 +527,30 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::LAST_KIND, LAST_KIND}, }; +/* Set of kinds for indexed operators */ +const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds( + {CHAIN, + RECORD_UPDATE, + 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, + 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}); + namespace { bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } @@ -1025,7 +1049,11 @@ 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()) + if (d_expr->isNull() && t.d_expr->isNull()) + { + return (d_kind == t.d_kind); + } + else if (d_expr->isNull() || t.d_expr->isNull()) { return false; } @@ -3064,6 +3092,15 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, /* Create operators */ /* -------------------------------------------------------------------------- */ +Op Solver::mkOp(Kind kind) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end()) + << "Expected a kind for a non-indexed operator."; + return Op(kind); + CVC4_API_SOLVER_TRY_CATCH_END +} + Op Solver::mkOp(Kind kind, Kind k) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; |