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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 18 May 2022 06:01:20 +0000 (01:01 -0500)
committer	GitHub <noreply@github.com>
	Wed, 18 May 2022 06:01:20 +0000 (06:01 +0000)
commit	6d886ae8bb345dae281b95ec152aee2106137831
tree	1580d6b043ea86aa91334449cfbd570846592d2c	tree
parent	0a8938d9c2774a2db4da7354d57251f262c0987f	commit \| diff

Eliminate subtypes (#8783)

61 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/expr/match_trie.cpp		diff \| blob \| history
src/expr/nary_match_trie.cpp		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/subs.cpp		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.cpp		diff \| blob \| history
src/theory/bags/bags_utils.cpp		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/bags/solver_state.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_macros.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_eval_cache.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/term_pools.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/eager_solver.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/function_const.cpp		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.cpp		diff \| blob \| history
test/unit/node/type_node_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history

RSS Atom