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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 9 Jul 2022 03:42:48 +0000 (22:42 -0500)
committer	GitHub <noreply@github.com>
	Sat, 9 Jul 2022 03:42:48 +0000 (03:42 +0000)
commit	2812687446f7f967b62f3e8410012a96e2a87068
tree	5db83853a808519574d671addb23fec9646a35b2	tree
parent	5750f285aad69921acb1c68e9ab03307d4943369	commit \| diff

Eliminate static options access in proof utilities (#8927)

This requires changing many of the proof interfaces to pass Env instead of ProofNodeManager. This is also work towards simplifying the initialization of our proof infrastructure.

118 files changed:

src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/proof/alethe/alethe_post_processor.cpp		diff \| blob \| history
src/proof/alethe/alethe_post_processor.h		diff \| blob \| history
src/proof/buffered_proof_generator.cpp		diff \| blob \| history
src/proof/buffered_proof_generator.h		diff \| blob \| history
src/proof/conv_proof_generator.cpp		diff \| blob \| history
src/proof/conv_proof_generator.h		diff \| blob \| history
src/proof/eager_proof_generator.cpp		diff \| blob \| history
src/proof/eager_proof_generator.h		diff \| blob \| history
src/proof/lazy_proof.cpp		diff \| blob \| history
src/proof/lazy_proof.h		diff \| blob \| history
src/proof/lazy_proof_chain.cpp		diff \| blob \| history
src/proof/lazy_proof_chain.h		diff \| blob \| history
src/proof/lazy_tree_proof_generator.cpp		diff \| blob \| history
src/proof/lazy_tree_proof_generator.h		diff \| blob \| history
src/proof/lfsc/lfsc_post_processor.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_post_processor.h		diff \| blob \| history
src/proof/proof.cpp		diff \| blob \| history
src/proof/proof.h		diff \| blob \| history
src/proof/proof_ensure_closed.cpp		diff \| blob \| history
src/proof/proof_ensure_closed.h		diff \| blob \| history
src/proof/proof_node_updater.cpp		diff \| blob \| history
src/proof/proof_node_updater.h		diff \| blob \| history
src/proof/proof_set.h		diff \| blob \| history
src/proof/trust_node.cpp		diff \| blob \| history
src/proof/trust_node.h		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/proof_post_processor.cpp		diff \| blob \| history
src/prop/proof_post_processor.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/prop_proof_manager.h		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/zero_level_learner.cpp		diff \| blob \| history
src/smt/env.cpp		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/witness_form.cpp		diff \| blob \| history
src/theory/arith/branch_and_bound.cpp		diff \| blob \| history
src/theory/arith/branch_and_bound.h		diff \| blob \| history
src/theory/arith/linear/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/linear/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/proof_generator.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		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.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/operator_elim.h		diff \| blob \| history
src/theory/arith/pp_rewrite_eq.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arrays/inference_manager.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_proof_generator.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblast_proof_generator.h		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/combination_engine.cpp		diff \| blob \| history
src/theory/combination_engine.h		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/sets/term_registry.cpp		diff \| blob \| history
src/theory/sets/term_registry.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.h		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_engine_proof_generator.cpp		diff \| blob \| history
src/theory/theory_engine_proof_generator.h		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/trust_substitutions.cpp		diff \| blob \| history
src/theory/trust_substitutions.h		diff \| blob \| history
src/theory/uf/lambda_lift.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		diff \| blob \| history
test/unit/theory/theory_arith_coverings_white.cpp		diff \| blob \| history

RSS Atom