From 45b367a0261e3d18661e046fed8add898c6d512c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 17 Jun 2022 12:57:24 -0700 Subject: [PATCH] Add support for operators with same payload (#8886) This fixes an issue with supporting operators with the same payload. It changes the API to use the `mkConst()` overload that passes an explicit kind, which is required when the same payload is shared by multiple kinds. --- src/api/cpp/cvc5.cpp | 36 +++++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index baa94039a..92f791d51 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -743,6 +743,40 @@ const static std::unordered_set s_indexed_kinds( FLOATINGPOINT_TO_FP_FROM_SBV, FLOATINGPOINT_TO_FP_FROM_UBV}); +/** + * Mapping from external (API) kind to the corresponding internal operator kind. + */ +const static std::unordered_map s_op_kinds{ + {BITVECTOR_EXTRACT, internal::Kind::BITVECTOR_EXTRACT_OP}, + {BITVECTOR_REPEAT, internal::Kind::BITVECTOR_REPEAT_OP}, + {BITVECTOR_ROTATE_LEFT, internal::Kind::BITVECTOR_ROTATE_LEFT_OP}, + {BITVECTOR_ROTATE_RIGHT, internal::Kind::BITVECTOR_ROTATE_RIGHT_OP}, + {BITVECTOR_SIGN_EXTEND, internal::Kind::BITVECTOR_SIGN_EXTEND_OP}, + {BITVECTOR_ZERO_EXTEND, internal::Kind::BITVECTOR_ZERO_EXTEND_OP}, + {DIVISIBLE, internal::Kind::DIVISIBLE_OP}, + {FLOATINGPOINT_TO_SBV, internal::Kind::FLOATINGPOINT_TO_SBV_OP}, + {FLOATINGPOINT_TO_UBV, internal::Kind::FLOATINGPOINT_TO_UBV_OP}, + {FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + internal::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP}, + {FLOATINGPOINT_TO_FP_FROM_FP, + internal::Kind::FLOATINGPOINT_TO_FP_FROM_FP_OP}, + {FLOATINGPOINT_TO_FP_FROM_REAL, + internal::Kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP}, + {FLOATINGPOINT_TO_FP_FROM_SBV, + internal::Kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP}, + {FLOATINGPOINT_TO_FP_FROM_UBV, + internal::Kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP}, + {IAND, internal::Kind::IAND_OP}, + {INT_TO_BITVECTOR, internal::Kind::INT_TO_BITVECTOR_OP}, + {REGEXP_REPEAT, internal::Kind::REGEXP_REPEAT_OP}, + {REGEXP_LOOP, internal::Kind::REGEXP_LOOP_OP}, + {TUPLE_PROJECT, internal::Kind::TUPLE_PROJECT_OP}, + {TABLE_PROJECT, internal::Kind::TABLE_PROJECT_OP}, + {TABLE_AGGREGATE, internal::Kind::TABLE_AGGREGATE_OP}, + {TABLE_JOIN, internal::Kind::TABLE_JOIN_OP}, + {TABLE_GROUP, internal::Kind::TABLE_GROUP_OP}, +}; + /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ @@ -4888,7 +4922,7 @@ template Op Solver::mkOpHelper(Kind kind, const T& t) const { //////// all checks before this line - internal::Node res = getNodeManager()->mkConst(t); + internal::Node res = getNodeManager()->mkConst(s_op_kinds.at(kind), t); static_cast(res.getType(true)); /* kick off type checking */ return Op(this, kind, res); } -- 2.30.2