Add option --proof-alethe-experimental (cvc5#10539)

This option is now required to use Alethe proofs on main.
HanielB · Mar 25, 2024 · a40d28f · a40d28f
1 parent 2cf2797
commit a40d28f
Show file tree

Hide file tree

Showing 7 changed files with 37 additions and 18 deletions.
diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst
@@ -1,13 +1,14 @@
 Proof format: Alethe
 ====================
 
+**WARNING: This format is experimental on the main branch of cvc5. To use this format, the option --proof-alethe-experimental must be used, or otherwise an execption is thrown.**
+
 Using the flag :ref:`proof-format-mode=alethe <lbl-option-proof-format-mode>`,
 cvc5 outputs proofs in the `Alethe proof format
 <https://verit.loria.fr/documentation/alethe-spec.pdf>`_. Additonally, the
 following additional flags are currently required: :ref:`simplification=none
-<lbl-option-simplification>`, :ref:`dag-thresh=0 <lbl-option-dag-thresh>`,
-:ref:`proof-granularity=theory-rewrite <lbl-option-proof-granularity>`. These requirements are due to not yet
-supporting printing proofs with term sharing and proofs with non-detailed steps.
+<lbl-option-simplification>`, and :ref:`proof-alethe-experimental`.
+The first requirement is due to not yet supporting proofs with non-detailed steps.
 
 The Alethe proof format is a flexible proof format for SMT solvers based on
 SMT-LIB.  It includes both coarse- and fine-grained steps and was first
@@ -23,4 +24,4 @@ cvc5's Alethe proofs.
 
 A simple example of cvc5 producing a proof in the Alethe proof format:
 
-.. run-command:: bin/cvc5 --dump-proofs --proof-format-mode=alethe --simplification=none --dag-thresh=0 --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
+.. run-command:: bin/cvc5 --dump-proofs --proof-format-mode=alethe --simplification=none --proof-alethe-experimental ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
@@ -25,6 +25,14 @@ name   = "Proof"
   name       = "alf"
   help       = "Output AletheLF proof"
 
+[[option]]
+  name       = "proofAletheExperimental"
+  category   = "expert"
+  long       = "proof-alethe-experimental"
+  type       = "bool"
+  default    = "false"
+  help       = "Enable the use of Alethe proofs (experimental)"
+
 [[option]]
   name       = "proofPrintConclusion"
   category   = "expert"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
@@ -181,14 +181,24 @@ void SetDefaults::setDefaultsPre(Options& opts)
     // note that this test assumes that granularity modes are ordered and
     // THEORY_REWRITE is gonna be, in the enum, after the lower granularity
     // levels
-    if (opts.proof.proofFormatMode == options::ProofFormatMode::ALETHE
-        && opts.proof.proofGranularityMode
-               < options::ProofGranularityMode::THEORY_REWRITE)
+    if (opts.proof.proofFormatMode == options::ProofFormatMode::ALETHE)
     {
-      SET_AND_NOTIFY(Proof,
-                     proofGranularityMode,
-                     options::ProofGranularityMode::THEORY_REWRITE,
-                     "Alethe requires granularity at least theory-rewrite");
+      if (!opts.proof.proofAletheExperimental)
+      {
+        std::stringstream ss;
+        ss << "proof-format=alethe is experimental in this version. If "
+              "you know what you are doing, you can try "
+              "--proof-alethe-experimental";
+        throw OptionException(ss.str());
+      }
+      if (opts.proof.proofGranularityMode
+          < options::ProofGranularityMode::THEORY_REWRITE)
+      {
+        SET_AND_NOTIFY(Proof,
+                       proofGranularityMode,
+                       options::ProofGranularityMode::THEORY_REWRITE,
+                       "Alethe requires granularity at least theory-rewrite");
+      }
     }
   }
   if (!opts.smt.produceProofs)

diff --git a/test/regress/cli/regress0/proofs/alethe-res-need-or-step.smt2 b/test/regress/cli/regress0/proofs/alethe-res-need-or-step.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite --no-proof-alethe-res-pivots
+; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite --no-proof-alethe-res-pivots --proof-alethe-experimental
 ; EXIT: 0
 ; SCRUBBER: grep -v -E '.*'
 (set-logic QF_UF)
@@ -8,4 +8,4 @@
 (declare-fun e0 () I)
 (assert (or (= e0 (o e0 e0)) (= e (o e0 e))))
 (assert (and (not (= e0 (o e0 e0))) (not (= e (o e0 e)))))
-(check-sat)
+(check-sat)
diff --git a/test/regress/cli/regress0/proofs/issue9393-optResReconstruction-alethebug.smt2 b/test/regress/cli/regress0/proofs/issue9393-optResReconstruction-alethebug.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite --proof-alethe-res-pivots
+; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite --proof-alethe-res-pivots  --proof-alethe-experimental
 ; EXIT: 0
 ; SCRUBBER: grep -v -E '.*'
 (set-logic QF_UF)
@@ -10,4 +10,4 @@
 (assert (and (or (= e4 (o e4 e)) (= e4 (o e4 e4)) (= e4 (o e4 e2))) (or (= (o e4 e4) (o (o e4 e2) e2)) (= (o e4 e) (o (o e4 e2) e2))) (or (= e2 (o e4 e)) (= e2 (o e4 e4)) (= e2 (o e4 (o (o e4 e2) e2)))) (= (o e4 e2) (o e (o (o e4 e2) e2))) (or (= e4 (o (o (o e4 e2) e2) (o e4 e2))) (= e4 (o e (o (o e4 e2) e2))) (= e4 (o (o e4 e2) e))) (or (= e (o e4 e4)) (= e2 (o e4 e2)))))
 (assert (and (not (= (o e4 e4) (o (o e4 e2) e4))) (not (= (o e2 e4) (o (o e4 e2) e4)))))
 (assert (and (= (o e4 e2) (o e4 (o e4 e2))) (= (o e4 e2) (o (o (o e4 e2) e2) (o e4 e2)))))
-(check-sat)
+(check-sat)
diff --git a/test/regress/cli/regress0/proofs/issue9531-alethe-resolution.smt2 b/test/regress/cli/regress0/proofs/issue9531-alethe-resolution.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --proof-granularity=theory-rewrite
+; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --proof-granularity=theory-rewrite --proof-alethe-experimental
 ; EXIT: 0
 ; SCRUBBER: grep -v -E '.*'
 (set-logic QF_UF)
@@ -13,4 +13,4 @@
 (assert (= (o e e) (o u u)))
 (assert (or (= (o u (o u u)) (o (o e e) (o (o e e) (o u (o u u))))) (not (= (o u (o u u)) (o (o (o e e) (o u (o u u))) (o e e))))))
 (assert (not (= (o u (o u u)) (o (o u u) (o (o e e) (o u (o u u)))))))
-(check-sat)
+(check-sat)
diff --git a/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite
+; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite --proof-alethe-experimental
 ; EXIT: 0
 ; SCRUBBER: grep -v -E '.*'
 (set-logic AUFLIA)