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/parser/smt2/smt2.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/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 4d75a982b..049bf8b4d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1097,6 +1097,12 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } + else if (p.d_kind == api::TUPLE_PROJECT) + { + api::Term ret = d_solver->mkTerm(p.d_op, args[0]); + Debug("parser") << "applyParseOp: return projection " << ret << std::endl; + return ret; + } else if (p.d_kind != api::NULL_EXPR) { // it should not have an expression or type specified at this point |