git.libre-soc.org Git - cvc5.git/commit

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Tue, 15 Mar 2022 19:28:41 +0000 (14:28 -0500)
committer	GitHub <noreply@github.com>
	Tue, 15 Mar 2022 19:28:41 +0000 (19:28 +0000)
commit	e5e9ca94a9171914694bcf009cb2968af93af624
tree	cd59143d5b5df1ec5f9ab7be8d81035b728f6808	tree
parent	030cea7270b61225d24c0768613dd73317b8e21d	commit \| diff

Add skolem lemmas for bags card terms (#7995)

This PR refactors the way skolem lemmas are generated for bags, count terms, and card terms.
As a side effect, this refactoring fixed cvc5/cvc5-projects#481

22 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/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/card_solver.cpp		diff \| blob \| history
src/theory/bags/card_solver.h		diff \| blob \| history
src/theory/bags/infer_info.cpp		diff \| blob \| history
src/theory/bags/infer_info.h		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
src/theory/bags/theory_bags.h		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/bags/murxla5.smt2	[new file with mode: 0644]	blob
test/unit/theory/theory_bags_rewriter_white.cpp		diff \| blob \| history

RSS Atom