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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 5 Nov 2021 16:54:30 +0000 (11:54 -0500)
committer	GitHub <noreply@github.com>
	Fri, 5 Nov 2021 16:54:30 +0000 (11:54 -0500)
commit	a82b7fb2760e705aba57516fc32041214e701559
tree	4b1bf5b14898dd6a4ae06c5934cb32f34ed660ac	tree
parent	71cab467df779fc1a52e8a5f981132f49d9d3182	commit \| diff

Remove many static calls to rewrite (#7580)

This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.

It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).

67 files changed:

src/smt/model_blocker.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/branch_and_bound.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/inference_manager.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.h		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/pow2_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.h		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/pp_rewrite_eq.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/decision_strategy.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/first_order_model_fmc.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/ho_term_database.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.h		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.h		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.h		diff \| blob \| history
src/theory/sets/theory_sets_type_enumerator.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history

RSS Atom