diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst index b5cf4bdf283..6f00e2c95e4 100644 --- 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 `, cvc5 outputs proofs in the `Alethe proof format `_. Additonally, the following additional flags are currently required: :ref:`simplification=none -`, :ref:`dag-thresh=0 `, -:ref:`proof-granularity=theory-rewrite `. These requirements are due to not yet -supporting printing proofs with term sharing and proofs with non-detailed steps. +`, 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 index 01412a24052..0bc89de7fe4 100644 --- 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 index f4b42c0315e..06069bfe5c9 100644 --- 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 index 8cd64fddf15..fc45d544b48 100644 --- 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) \ No newline at end of file +(check-sat) diff --git a/test/regress/cli/regress0/proofs/issue9393-optResReconstruction-alethebug.smt2 b/test/regress/cli/regress0/proofs/issue9393-optResReconstruction-alethebug.smt2 index eca4ab0b33b..9b88f10a9cc 100644 --- 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) \ No newline at end of file +(check-sat) diff --git a/test/regress/cli/regress0/proofs/issue9531-alethe-resolution.smt2 b/test/regress/cli/regress0/proofs/issue9531-alethe-resolution.smt2 index 9238fa0c498..f86d7b9265e 100644 --- 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) \ No newline at end of file +(check-sat) diff --git a/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 index ae03cb50bdc..f0f10397aa5 100644 --- 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)