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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Sun, 4 Oct 2020 20:10:24 +0000 (15:10 -0500)
committer	GitHub <noreply@github.com>
	Sun, 4 Oct 2020 20:10:24 +0000 (15:10 -0500)
commit	13cf41801f8f2bac538cb45d53ae7427916041a7
tree	78e82b56e92004991890943ba5da863e6af3538f	tree
parent	d662d3321a46aac61973f7a90341ea870c0b1171	commit \| diff

Remove subtyping for sets theory (#5179)

This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:

Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON

31 files changed:

examples/api/python/sets.py		diff \| blob \| history
examples/api/sets.cpp		diff \| blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cpp.h		diff \| blob \| history
src/api/python/cvc4.pxd		diff \| blob \| history
src/api/python/cvc4.pxi		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/kinds		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/singleton_op.cpp	[new file with mode: 0644]	blob
src/theory/sets/singleton_op.h	[new file with mode: 0644]	blob
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_enumerator.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
test/regress/regress0/sets/sets-poly-int-real.smt2		diff \| blob \| history
test/unit/theory/CMakeLists.txt		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_black.h		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.h	[new file with mode: 0644]	blob

RSS Atom