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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Fri, 3 Jun 2022 22:24:39 +0000 (17:24 -0500)
committer	GitHub <noreply@github.com>
	Fri, 3 Jun 2022 22:24:39 +0000 (22:24 +0000)
commit	2abc3c3015d2ef0adb027f233f6558afd9b1091b
tree	ca3b0d75b8d3c8253979c3c3a3a0fa844ad1919e	tree
parent	846189ff975b206326edc1540578c3f8df72138c	commit \| diff

Add inference rules for set.map operator (#8849)

17 files changed:

src/expr/skolem_manager.cpp		diff \| blob \| history
src/expr/skolem_manager.h		diff \| blob \| history
src/theory/incomplete_id.cpp		diff \| blob \| history
src/theory/incomplete_id.h		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/sets/solver_state.cpp		diff \| blob \| history
src/theory/sets/solver_state.h		diff \| blob \| history
src/theory/sets/term_registry.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
test/regress/cli/CMakeLists.txt		diff \| blob \| history
test/regress/cli/regress1/sets/set_map_card_incomplete.smt2	[new file with mode: 0644]	blob
test/regress/cli/regress1/sets/set_map_negative_members.smt2	[new file with mode: 0644]	blob
test/regress/cli/regress1/sets/set_map_positive_members.smt2	[new file with mode: 0644]	blob
test/regress/cli/regress1/sets/set_map_unsat1.smt2	[new file with mode: 0644]	blob