projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 80d9eab) | patch
Add tuple projection operator (#5904)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 3 Mar 2021 08:16:32 +0000 (02:16 -0600)
committerGitHub <noreply@github.com>
Wed, 3 Mar 2021 08:16:32 +0000 (08:16 +0000)
commitc4709cb01356dd73fdd767d19af85b36ffd566c4
tree9ad44e16486ec4cbb2d4c6776c1d80a179cc6894tree
parent80d9eab67e60ae8750165ce18ecd4eebcdc06b44commit | 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.
16 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cpp.h diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bags/make_bag_op.h diff | blob | history
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/datatypes/tuple_project_op.cpp [new file with mode: 0644] blob
src/theory/datatypes/tuple_project_op.h [new file with mode: 0644] blob
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/datatypes/tuple_projection.smt2 [new file with mode: 0644] blob
test/unit/api/solver_black.cpp diff | blob | history