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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 12 Dec 2019 20:38:42 +0000 (14:38 -0600)
committer	GitHub <noreply@github.com>
	Thu, 12 Dec 2019 20:38:42 +0000 (14:38 -0600)
commit	e6d20229cf21a3614ac546514f42bd06002d52b8
tree	d47a2d716ab17151ae3e622a9e372b15cbdf605f	tree
parent	7fa164c306dbfe9aad68110cf3fd9cedd3d2e004	commit \| diff

Use the node-level datatypes API (#3556)

45 files changed:

src/expr/datatype.cpp		diff \| blob \| history
src/expr/expr_manager_template.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/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.h		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.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/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.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/term_database_sygus.h		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/sets/rels_utils.h		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history

RSS Atom