Removes old proof code (#4964)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 1 Sep 2020 22:08:23 +0000 (19:08 -0300)
committerGitHub <noreply@github.com>
Tue, 1 Sep 2020 22:08:23 +0000 (19:08 -0300)
commit8ad308b23c705e73507a42d2425289e999d47f86
tree29e3ac78844bc57171e0d122d758a8371a292a93
parent62ec0666dd4d409ee85603ae94d7ab1a2b4c9dcc
Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
157 files changed:
src/CMakeLists.txt
src/options/bv_options.toml
src/options/options.h
src/options/options_public_functions.cpp
src/options/proof_options.toml
src/options/smt_options.toml
src/preprocessing/assertion_pipeline.cpp
src/preprocessing/passes/ite_simp.cpp
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/non_clausal_simp.cpp
src/preprocessing/passes/quantifier_macros.cpp
src/proof/arith_proof.cpp [deleted file]
src/proof/arith_proof.h [deleted file]
src/proof/arith_proof_recorder.cpp [deleted file]
src/proof/arith_proof_recorder.h [deleted file]
src/proof/array_proof.cpp [deleted file]
src/proof/array_proof.h [deleted file]
src/proof/bitvector_proof.cpp [deleted file]
src/proof/bitvector_proof.h [deleted file]
src/proof/clausal_bitvector_proof.cpp [deleted file]
src/proof/clausal_bitvector_proof.h [deleted file]
src/proof/clause_id.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/dimacs.cpp [deleted file]
src/proof/dimacs.h [deleted file]
src/proof/drat/drat_proof.cpp [deleted file]
src/proof/drat/drat_proof.h [deleted file]
src/proof/er/er_proof.cpp [deleted file]
src/proof/er/er_proof.h [deleted file]
src/proof/lemma_proof.cpp [deleted file]
src/proof/lemma_proof.h [deleted file]
src/proof/lfsc_proof_printer.cpp [deleted file]
src/proof/lfsc_proof_printer.h [deleted file]
src/proof/lrat/lrat_proof.cpp [deleted file]
src/proof/lrat/lrat_proof.h [deleted file]
src/proof/proof.h [deleted file]
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/proof_output_channel.cpp [deleted file]
src/proof/proof_output_channel.h [deleted file]
src/proof/proof_utils.cpp [deleted file]
src/proof/proof_utils.h [deleted file]
src/proof/resolution_bitvector_proof.cpp [deleted file]
src/proof/resolution_bitvector_proof.h [deleted file]
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/simplify_boolean_node.cpp [deleted file]
src/proof/simplify_boolean_node.h [deleted file]
src/proof/skolemization_manager.cpp [deleted file]
src/proof/skolemization_manager.h [deleted file]
src/proof/theory_proof.cpp [deleted file]
src/proof/theory_proof.h [deleted file]
src/proof/uf_proof.cpp [deleted file]
src/proof/uf_proof.h [deleted file]
src/prop/bvminisat/bvminisat.cpp
src/prop/bvminisat/bvminisat.h
src/prop/bvminisat/core/Solver.cc
src/prop/bvminisat/core/Solver.h
src/prop/bvminisat/core/SolverTypes.h
src/prop/bvminisat/simp/SimpSolver.cc
src/prop/cadical.cpp
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/cryptominisat.cpp
src/prop/cryptominisat.h
src/prop/kissat.cpp
src/prop/minisat/core/Solver.cc
src/prop/minisat/core/Solver.h
src/prop/minisat/core/SolverTypes.h
src/prop/minisat/minisat.cpp
src/prop/minisat/simp/SimpSolver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/sat_solver.h
src/prop/theory_proxy.cpp
src/smt/assertions.cpp
src/smt/assertions.h
src/smt/command.cpp
src/smt/command.h
src/smt/process_assertions.cpp
src/smt/set_defaults.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_scope.cpp
src/smt/smt_engine_stats.cpp
src/smt/smt_engine_stats.h
src/smt/smt_solver.cpp
src/smt/term_formula_removal.cpp
src/theory/arith/callbacks.cpp
src/theory/arith/constraint.cpp
src/theory/arith/constraint.h
src/theory/arith/linear_equality.cpp
src/theory/arith/nl/nl_model.cpp
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arrays/array_proof_reconstruction.cpp [deleted file]
src/theory/arrays/array_proof_reconstruction.h [deleted file]
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bv/bitblast/aig_bitblaster.h
src/theory/bv/bitblast/bitblaster.h
src/theory/bv/bitblast/eager_bitblaster.cpp
src/theory/bv/bitblast/eager_bitblaster.h
src/theory/bv/bitblast/lazy_bitblaster.cpp
src/theory/bv/bitblast/lazy_bitblaster.h
src/theory/bv/bv_eager_solver.cpp
src/theory/bv/bv_eager_solver.h
src/theory/bv/bv_subtheory.h
src/theory/bv/bv_subtheory_bitblast.cpp
src/theory/bv/bv_subtheory_bitblast.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/combination_engine.cpp
src/theory/engine_output_channel.cpp
src/theory/engine_output_channel.h
src/theory/ext_theory.h
src/theory/output_channel.cpp
src/theory/output_channel.h
src/theory/quantifiers/fun_def_process.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/instantiate.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sort_inference.cpp
src/theory/strings/theory_strings_preprocess.cpp
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_test_utils.h
src/theory/uf/eq_proof.cpp
src/theory/uf/eq_proof.h
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/equality_engine_types.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
src/util/CMakeLists.txt
src/util/proof.h [deleted file]
test/regress/CMakeLists.txt
test/regress/regress0/bug217.smt2
test/regress/regress0/options/invalid_option_inc_proofs.smt2 [deleted file]
test/regress/regress1/bv/bench_38.delta.smt2
test/regress/regress1/non-fatal-errors.smt2
test/regress/regress1/quantifiers/dump-inst-proof.smt2
test/unit/CMakeLists.txt
test/unit/proof/CMakeLists.txt [deleted file]
test/unit/proof/drat_proof_black.h [deleted file]
test/unit/proof/er_proof_black.h [deleted file]
test/unit/proof/lfsc_proof_printer_black.h [deleted file]
test/unit/proof/lrat_proof_black.h [deleted file]
test/unit/proof/utils.h [deleted file]
test/unit/prop/cnf_stream_white.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h