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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 16 Dec 2021 22:16:03 +0000 (16:16 -0600)
committer	GitHub <noreply@github.com>
	Thu, 16 Dec 2021 22:16:03 +0000 (16:16 -0600)
commit	03cb06e30a13bdb9e6a3c6c3d54bfe7411f27ec8
tree	9ef6a18dd4efb1f8bb1cf5010556f9c35bffeb2b	tree
parent	0c21537af09a451e57cb6251ebba2c20c69cf612	commit \| diff

Eliminate most static calls to rewrite in quantifiers (#7823)

36 files changed:

src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.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/enum_stream_substitution.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_val_generator.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_basic.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		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_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_random_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_random_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.h		diff \| blob \| history

RSS Atom