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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 13 Dec 2019 15:53:02 +0000 (09:53 -0600)
committer	GitHub <noreply@github.com>
	Fri, 13 Dec 2019 15:53:02 +0000 (09:53 -0600)
commit	9acb8b8d0d529c4780191660f8ef2b51e4a92926
tree	1ee538fbc959102d4778cfc74047ee4df87a36c2	tree
parent	866f7fb6d4642a51893b0978114b432f990f4c9d	commit \| diff

Add support for set comprehension (#3312)

19 files changed:

src/expr/node.h		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/sets/kinds		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.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		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_type_rules.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/sets/comp-qf-error.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/comp-intersect.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/comp-odd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/comp-pos-member.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/comp-positive.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/set-comp-sat.smt2	[new file with mode: 0644]	blob