projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b5dec96) | patch
Add inference rules for table.group (#8819)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 23 Jun 2022 21:21:56 +0000 (16:21 -0500)
committerGitHub <noreply@github.com>
Thu, 23 Jun 2022 21:21:56 +0000 (21:21 +0000)
commit3f63a768eb2405b246a35e1386ca742f87691585
treef5683c821794dc2a1eda771feeeb9c539802eed0tree
parentb5dec96e8e65591e7686c460a30a5c62d5becdcfcommit | diff
Add inference rules for table.group (#8819)
16 files changed:
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/bags/bag_solver.cpp diff | blob | history
src/theory/bags/bag_solver.h diff | blob | history
src/theory/bags/bags_utils.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/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/bags/table_group2.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/bags/table_group3.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/bags/table_group4.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/bags/table_group5.smt2 [new file with mode: 0644] blob