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.h | |
| 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.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 60127d18b..d503a317e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2620,6 +2620,14 @@ class CVC4_PUBLIC Solver */ Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const; + /** + * Create operator of Kind: + * - TUPLE_PROJECT + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + */ + Op mkOp(Kind kind, const std::vector<uint32_t>& args) const; + /* .................................................................... */ /* Create Constants */ /* .................................................................... */ |