[proof-new] Only use old proofs for unsat cores if no proof new (#5725)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Thu, 24 Dec 2020 04:15:40 +0000 (01:15 -0300)
committerGitHub <noreply@github.com>
Thu, 24 Dec 2020 04:15:40 +0000 (01:15 -0300)
commite0dfc0a343dfd330f9c8d2a5c1ebd21146366ca9
tree4602faa1f16a2548fe27ad1e7ea6a6a28bec4ee7
parenta539b63c369544ed08a1fa7fa4c8e3d437be3766
[proof-new] Only use old proofs for unsat cores if no proof new (#5725)

Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.

This also does some minor refactoring in some preprocessing. No behavior is changed.
17 files changed:
src/preprocessing/assertion_pipeline.cpp
src/preprocessing/passes/apply_substs.cpp
src/preprocessing/passes/ite_removal.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/prop/minisat/core/Solver.cc
src/prop/minisat/minisat.cpp
src/prop/minisat/simp/SimpSolver.cc
src/prop/prop_engine.cpp
src/prop/theory_proxy.cpp
src/smt/assertions.cpp
src/smt/process_assertions.cpp
src/smt/set_defaults.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/strings/theory_strings_preprocess.cpp