projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e91077d) | patch
Add operator MakeBagOp for constructing bags (#5209)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 21 Oct 2020 13:19:55 +0000 (08:19 -0500)
committerGitHub <noreply@github.com>
Wed, 21 Oct 2020 13:19:55 +0000 (08:19 -0500)
commit098cee0ea412e24e24caa79307e2950a640279af
treee0936bddb8700206d9d0691150b0b4af9dd23dc4tree
parente91077d81183c6c54ff0fdad5c6eb160f16c4205commit | diff
Add operator MakeBagOp for constructing bags (#5209)

This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp
16 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/theory/bags/bags_rewriter.cpp diff | blob | history
src/theory/bags/kinds diff | blob | history
src/theory/bags/make_bag_op.cpp [new file with mode: 0644] blob
src/theory/bags/make_bag_op.h [new file with mode: 0644] blob
src/theory/bags/theory_bags_type_enumerator.cpp diff | blob | history
src/theory/bags/theory_bags_type_rules.h diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_bags_rewriter_black.h [deleted file] blob | history
test/unit/theory/theory_bags_rewriter_white.h [new file with mode: 0644] blob
test/unit/theory/theory_bags_type_rules_black.h [deleted file] blob | history
test/unit/theory/theory_bags_type_rules_white.h [new file with mode: 0644] blob