Reconciling proofs and unsat cores (#6405)

This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:

the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.

1 files changed, 25 insertions, 16 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 83b83f3be..bb5cc1abe 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -201,27 +201,36 @@ header = "options/smt_options.h"
   help       = "turn on unsat core generation"
 
 [[option]]
-  name       = "checkUnsatCores"
-  category   = "regular"
-  long       = "check-unsat-cores"
-  type       = "bool"
-  help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
-
-# Temporary option until old unsat cores are removed and this becomes the standard
-[[option]]
-  name       = "unsatCoresNew"
+  name       = "unsatCoresMode"
+  smt_name   = "unsat-cores-mode"
   category   = "regular"
-  long       = "produce-unsat-cores-new"
-  type       = "bool"
-  help       = "turn on unsat core generation using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs."
+  long       = "unsat-cores-mode=MODE"
+  type       = "UnsatCoresMode"
+  default    = "OFF"
+  help       = "choose unsat core mode, see --unsat-cores-mode=help"
+  help_mode  = "unsat cores modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not produce unsat cores."
+[[option.mode.OLD_PROOF]]
+  name = "old-proof"
+  help = "Produce unsat cores from old proof infrastructure."
+[[option.mode.SAT_PROOF]]
+  name = "sat-proof"
+  help = "Produce unsat cores from SAT and preprocessing proofs."
+[[option.mode.FULL_PROOF]]
+  name = "full-proof"
+  help = "Produce unsat cores from full proofs."
+[[option.mode.ASSUMPTIONS]]
+  name = "assumptions"
+  help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
 
-# Temporary option until old unsat cores are removed and this becomes the standard
 [[option]]
-  name       = "checkUnsatCoresNew"
+  name       = "checkUnsatCores"
   category   = "regular"
-  long       = "check-unsat-cores-new"
+  long       = "check-unsat-cores"
   type       = "bool"
-  help       = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs."
+  help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
 
 [[option]]
   name       = "dumpUnsatCores"