projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d2f0f6d) | patch
Simplify reductions for set and bag choose (#8304)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Mar 2022 01:11:12 +0000 (20:11 -0500)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 01:11:12 +0000 (01:11 +0000)
commit85900254c193c7205afc6f67158459d0940b7426
treeec9df1bd2541cb2b61581bbd1fde008d493fd943tree
parentd2f0f6d468473cffee92d9835d9b4d0c88550253commit | diff
Simplify reductions for set and bag choose (#8304)

Ensures that the reductions are deterministic, thus fixes cvc5/cvc5-projects#493.

The reductions can be further simplified to not introduce UF. This will be addressed in a later PR.
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/skolem_lemma.cpp diff | blob | history
src/theory/skolem_lemma.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sets/proj-issue493-choose-det.smt2 [new file with mode: 0644] blob