projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 45b367a) | patch
Remove redundant projection operators (#8889)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Sat, 18 Jun 2022 17:31:08 +0000 (12:31 -0500)
committerGitHub <noreply@github.com>
Sat, 18 Jun 2022 17:31:08 +0000 (10:31 -0700)
commit72fe8a98d6f794a03727c6ec24af53cf75204275
treeacb97f766209538e092bcdc143a4d0ab2c2e3d4ftree
parent45b367a0261e3d18661e046fed8add898c6d512ccommit | diff
Remove redundant projection operators (#8889)

This removes all projection operators for tuples and tables except a generic one `ProjectOp`.
It also updates the number of indices and other issues in cvc5.cpp
17 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bags/bag_reduction.cpp diff | blob | history
src/theory/bags/bags_utils.cpp diff | blob | history
src/theory/bags/inference_generator.cpp diff | blob | history
src/theory/bags/kinds diff | blob | history
src/theory/bags/table_project_op.cpp [deleted file] blob | history
src/theory/bags/table_project_op.h [deleted file] blob | history
src/theory/bags/theory_bags_type_rules.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/project_op.cpp [new file with mode: 0644] blob
src/theory/datatypes/project_op.h [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes_type_rules.cpp diff | blob | history
src/theory/datatypes/tuple_project_op.cpp [deleted file] blob | history
src/theory/datatypes/tuple_project_op.h [deleted file] blob | history