[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.

1 files changed, 18 insertions, 0 deletions

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 0345991d2..253dbecaf 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -38,6 +38,24 @@ class ProofPostproccess;
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
  * well as setting up the global proof checker and proof node manager.
+ *
+ * The proof production of an SmtEngine is directly impacted by whether, and
+ * how, we are producing unsat cores:
+ *
+ * - If we are producing unsat cores using the old proof infrastructure, then
+ *   SmtEngine will not have proofs in the sense of this proof manager.
+ *
+ * - If we are producing unsat cores using this proof infrastructure, then the
+ *   SmtEngine will have proofs using this proof manager (if --produce-proofs
+ *   was not passed by the user it will be activated), but these proofs will
+ *   only cover preprocessing and the prop engine, i.e., the theory engine will
+ *   not have proofs.
+ *
+ * - If we are not producing unsat cores then the SmtEngine will have proofs as
+ *   long as --produce-proofs was given.
+ *
+ * - If SmtEngine has been configured in a way that is incompatible with proofs
+ *   then unsat core production will be disabled.
  */
 class PfManager
 {