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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 3 Feb 2022 19:19:31 +0000 (13:19 -0600)
committer	GitHub <noreply@github.com>
	Thu, 3 Feb 2022 19:19:31 +0000 (11:19 -0800)
commit	a09a4a300d52cdb4026bbba0184da152e0a65296
tree	79dfed212ce8d6d02b3b6de29d1d7382c98c7bc8	tree
parent	3eb47718f6e24cc719094732b639e1d8b73012a4	commit \| diff

Eliminate more static uses of rewrite (#8040)

20 files changed:

src/expr/subs.cpp		diff \| blob \| history
src/expr/subs.h		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.h		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/relational_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/relational_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history