[unsat-cores] Improving new unsat cores (#6356)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 14 Apr 2021 17:50:10 +0000 (14:50 -0300)
committerGitHub <noreply@github.com>
Wed, 14 Apr 2021 17:50:10 +0000 (17:50 +0000)
commitb6db4446a28d498af8fb4e629392985dfe2a976c
treeb283483ce265b25bfdd8e769f2026dd414510ac3
parentf74bdbd182d95a8e6395aaaf348ca0e41baa3bf4
[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
18 files changed:
src/api/cpp/cvc5.cpp
src/options/smt_options.toml
src/preprocessing/assertion_pipeline.cpp
src/preprocessing/passes/ite_removal.cpp
src/preprocessing/passes/quantifier_macros.cpp
src/prop/minisat/core/Solver.cc
src/prop/proof_cnf_stream.cpp
src/prop/proof_cnf_stream.h
src/prop/prop_engine.cpp
src/prop/theory_proxy.cpp
src/smt/assertions.cpp
src/smt/proof_manager.cpp
src/smt/proof_manager.h
src/smt/set_defaults.cpp
src/smt/smt_engine.cpp
src/smt/smt_solver.cpp
src/smt/smt_solver.h
src/theory/theory_engine.cpp