projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2117152) | patch
Implement bags rewriter (#5132)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Mon, 28 Sep 2020 13:53:07 +0000 (08:53 -0500)
committerGitHub <noreply@github.com>
Mon, 28 Sep 2020 13:53:07 +0000 (08:53 -0500)
commit0f77646dfc0944f1f17f121ffb3112bf8b244f76
treec47327731f05c19232f9c756f43da878f83d4ec9tree
parent2117152db35fe1e8cee1632303789dceda311d1acommit | diff
Implement bags rewriter (#5132)

This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes.
Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).
18 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/bags/bags_rewriter.cpp [new file with mode: 0644] blob
src/theory/bags/bags_rewriter.h [new file with mode: 0644] blob
src/theory/bags/bags_statistics.cpp [new file with mode: 0644] blob
src/theory/bags/bags_statistics.h [new file with mode: 0644] blob
src/theory/bags/kinds diff | blob | history
src/theory/bags/normal_form.cpp diff | blob | history
src/theory/bags/normal_form.h diff | blob | history
src/theory/bags/rewrites.cpp [new file with mode: 0644] blob
src/theory/bags/rewrites.h [new file with mode: 0644] blob
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/bags/theory_bags.h diff | blob | history
src/theory/bags/theory_bags_rewriter.cpp [deleted file] blob | history
src/theory/bags/theory_bags_rewriter.h [deleted file] blob | history
src/theory/bags/theory_bags_type_enumerator.h 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 [new file with mode: 0644] blob