diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-03-03 02:16:32 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-03 08:16:32 +0000 |
commit | c4709cb01356dd73fdd767d19af85b36ffd566c4 (patch) | |
tree | 9ad44e16486ec4cbb2d4c6776c1d80a179cc6894 /src/api/cvc4cpp.cpp | |
parent | 80d9eab67e60ae8750165ce18ecd4eebcdc06b44 (diff) |
Add tuple projection operator (#5904)
This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e1c64b750..c3490938b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -232,6 +232,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE}, {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE}, {DT_SIZE, CVC4::Kind::DT_SIZE}, + {TUPLE_PROJECT, CVC4::Kind::TUPLE_PROJECT}, /* Separation Logic ---------------------------------------------------- */ {SEP_NIL, CVC4::Kind::SEP_NIL}, {SEP_EMP, CVC4::Kind::SEP_EMP}, @@ -538,6 +539,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE}, {CVC4::Kind::DT_SIZE, DT_SIZE}, + {CVC4::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ {CVC4::Kind::SEP_NIL, SEP_NIL}, {CVC4::Kind::SEP_EMP, SEP_EMP}, @@ -4749,6 +4751,35 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const CVC4_API_SOLVER_TRY_CATCH_END; } +Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + + Op res; + switch (kind) + { + case TUPLE_PROJECT: + { + res = Op(this, + kind, + *mkValHelper<CVC4::TupleProjectOp>(CVC4::TupleProjectOp(args)) + .d_node); + } + break; + default: + { + std::string message = "operator kind with " + std::to_string(args.size()) + + " uint32_t arguments"; + CVC4_API_KIND_CHECK_EXPECTED(false, kind) << message; + } + } + Assert(!res.isNull()); + return res; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Non-SMT-LIB commands */ /* -------------------------------------------------------------------------- */ |