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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Fri, 6 Nov 2020 21:28:38 +0000 (15:28 -0600)
committer	GitHub <noreply@github.com>
	Fri, 6 Nov 2020 21:28:38 +0000 (15:28 -0600)
commit	63df35c477ee9e6c7bdeae677656dd374563de55
tree	1ab725ce9c6f8dafdeda032d572963363f181f7b	tree
parent	6476c8c75ed7fd584b5afa658dd2c8ba277c59e2	commit \| diff

Fix issue #5342 (#5349)

This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).

src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.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/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sets/issue5342.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/issue5342_difference_version.smt2	[new file with mode: 0644]	blob