projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89dfd27) | patch
expand bag.choose operator (#7481)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Mon, 8 Nov 2021 23:13:27 +0000 (17:13 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Nov 2021 23:13:27 +0000 (23:13 +0000)
commite398f79c61304378cc736828632a462c74ce39d2
tree7e06f2d70f4185337de34cb8edb73923193701b5tree
parent89dfd279d8786c54c35ff8f5e2802ec51a59a969commit | diff
expand bag.choose operator (#7481)

This PR expands bag.choose operator as a preprocessing step.
It also refactors the implementation of choose operator for sets
16 files changed:
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/bags/bags_rewriter.cpp diff | blob | history
src/theory/bags/inference_generator.cpp diff | blob | history
src/theory/bags/normal_form.cpp diff | blob | history
src/theory/bags/normal_form.h diff | blob | history
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/bags/theory_bags.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/bags/choose1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/choose2.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/choose3.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/choose4.smt2 [new file with mode: 0644] blob
test/unit/theory/theory_bags_normal_form_white.cpp diff | blob | history