projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce1b2f2) | patch
Add bag inferences for operators: intersection, duplicate_removal, and empty bags...
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Fri, 29 Jan 2021 21:44:28 +0000 (15:44 -0600)
committerGitHub <noreply@github.com>
Fri, 29 Jan 2021 21:44:28 +0000 (15:44 -0600)
commit50c3dee5c8a4855023df826e1a733ea3c6076774
tree3dd574a7e6153c9225c6abcde9085d06de057f6ftree
parentce1b2f2fb06150599c231bf0d59b52a07e74c3f5commit | diff
Add bag inferences for operators: intersection, duplicate_removal, and empty bags (#5832)

This PR adds inferences for operators: intersection, duplicate_removal, and empty bags during post check.
It also fixes a bug in SolverState::getElements
14 files changed:
src/theory/bags/bag_solver.cpp diff | blob | history
src/theory/bags/bag_solver.h diff | blob | history
src/theory/bags/infer_info.cpp diff | blob | history
src/theory/bags/inference_generator.cpp diff | blob | history
src/theory/bags/inference_generator.h diff | blob | history
src/theory/bags/solver_state.cpp diff | blob | history
src/theory/bags/solver_state.h diff | blob | history
src/theory/bags/theory_bags.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/bags/duplicate_removal1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/duplicate_removal2.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/emptybag1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/intersection_min1.smt2 [new file with mode: 0644] blob
test/regress/regress1/bags/intersection_min2.smt2 [new file with mode: 0644] blob