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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 15 May 2022 16:30:26 +0000 (11:30 -0500)
committer	GitHub <noreply@github.com>
	Sun, 15 May 2022 16:30:26 +0000 (16:30 +0000)
commit	e3bec47e98e76ad6e4a11259af096abb20f7de57
tree	5d3e12897c5604d04f4ff96204dda17ea4a330e6	tree
parent	c8b193f93369e042bf768d8ba567d6dc4ba01e7e	commit \| diff

Eliminate ops for parameterized type constructors (#8761)

We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences.

44 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/expr/node_manager_template.h		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.cpp		diff \| blob \| history
src/theory/bags/bag_make_op.cpp	[deleted file]	blob \| history
src/theory/bags/bag_make_op.h	[deleted file]	blob \| history
src/theory/bags/bag_reduction.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/bags_utils.cpp		diff \| blob \| history
src/theory/bags/kinds		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_rules.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/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	[deleted file]	blob \| history
src/theory/sets/singleton_op.h	[deleted file]	blob \| history
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.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history
src/theory/strings/seq_unit_op.cpp	[deleted file]	blob \| history
src/theory/strings/seq_unit_op.h	[deleted file]	blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_normal_form_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.cpp		diff \| blob \| history

RSS Atom