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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Mon, 25 Oct 2021 16:36:35 +0000 (11:36 -0500)
committer	GitHub <noreply@github.com>
	Mon, 25 Oct 2021 16:36:35 +0000 (16:36 +0000)
commit	0e28a3a86f45e012e59751b0091760f5e2baebd6
tree	800cd7d21917b78fcef67ba7b19b14666083a27f	tree
parent	ec0b33514ffe0b8be065da424348cc1b1d06ecb6	commit \| diff

Add inference for count map (#7264)

19 files changed:

src/expr/skolem_manager.cpp		diff \| blob \| history
src/expr/skolem_manager.h		diff \| blob \| history
src/smt/set_defaults.cpp		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_rewriter.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/normal_form.cpp		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/bags/fuzzy1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bags/fuzzy2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bags/map.smt2	[deleted file]	blob \| history
test/regress/regress1/bags/map1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bags/map2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bags/map3.smt2	[new file with mode: 0644]	blob