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/cvc4cppkind.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/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 3fb16abcb..b2413486e 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1715,6 +1715,22 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ DT_SIZE, + /** + * Operator for tuple projection indices + * Parameters: 1 + * -[1]: The tuple projection indices + * Create with: + * mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) + * + * constructs a new tuple from an existing one using the elements at the + * given indices + * Parameters: 1 + * -[1]: a term of tuple sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) + */ + TUPLE_PROJECT, #if 0 /* datatypes height bound */ DT_HEIGHT_BOUND, |