diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 39 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 13 | ||||
| -rw-r--r-- | test/unit/api/op_black.h | 4 |
3 files changed, 54 insertions, 2 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; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 326a8fb70..8c9bdc10c 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1890,10 +1890,21 @@ class CVC4_PUBLIC Solver const std::vector<Term>& terms) const; /* .................................................................... */ - /* Create Operator Terms */ + /* Create Operators */ /* .................................................................... */ /** + * Create an operator for a builtin Kind + * The Kind may not be the Kind for an indexed operator + * (e.g. BITVECTOR_EXTRACT) + * Note: in this case, the Op simply wraps the Kind. + * The Kind can be used in mkTerm directly without + * creating an op first. + * @param kind the kind to wrap + */ + Op mkOp(Kind kind) const; + + /** * Create operator of kind: * - CHAIN * See enum Kind for a description of the parameters. diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h index 3bf9b93c3..dcad8b649 100644 --- a/test/unit/api/op_black.h +++ b/test/unit/api/op_black.h @@ -66,6 +66,10 @@ void OpBlack::testOpFromKind() Op plus(PLUS); TS_ASSERT(!plus.isIndexed()); TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&); + + TS_ASSERT_THROWS_NOTHING(d_solver.mkOp(PLUS)); + TS_ASSERT_EQUALS(plus, d_solver.mkOp(PLUS)); + TS_ASSERT_THROWS(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException&); } void OpBlack::testGetIndicesString() |