# HG changeset patch
# User blanchet
# Date 1686750447 -7200
# Node ID d3122089b67c917bd740ca91c28818e0dd15ef91
# Parent  b7b777fc916cf641ef2c9ccf85a6d384a08ae840
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice

diff -r b7b777fc916c -r d3122089b67c NEWS
--- a/NEWS	Wed Jun 07 17:09:17 2023 +0200
+++ b/NEWS	Wed Jun 14 15:47:27 2023 +0200
@@ -64,11 +64,11 @@
 
 * Sledgehammer:
   - Added an inconsistency check mode to find likely unprovable
-    conjectures. It is enabled by default in addition to the usual
-    proving mode and can be controlled using the 'falsify' option.
+    conjectures. It is disabled by default and can be controlled using
+    the 'falsify' option.
   - Added an abduction mode to find likely missing hypotheses to
-    conjectures. It currently works only with the E prover. It is
-    enabled by default and can be controlled using the 'abduce' option.
+    conjectures. It works only with the E prover. It is disabled by
+    default and can be controlled using the 'abduce' option.
 
 * Metis:
   - Made clausifier more robust in the face of nested lambdas.
diff -r b7b777fc916c -r d3122089b67c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jun 07 17:09:17 2023 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jun 14 15:47:27 2023 +0200
@@ -264,29 +264,29 @@
 readable and also faster than \textit{metis} or \textit{smt} one-line
 proofs. This feature is experimental.
 
-For goals that are inconsistent with the background theory (and hence unprovable
-unless the theory is itself inconsistent), such as
-
-\prew
-\textbf{lemma} ``$\mathit{length}\; (\mathit{zip}\; \mathit{xs}\; \mathit{ys}) = \mathit{length}\; \mathit{xs}$'' \\
-\textbf{sledgehammer}
-\postw
-
-Sledgehammer's output might look as follows:
-
-\prew
-\slshape
-vampire found a falsification\ldots \\
-vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
-\postw
-
-Sometimes Sledgehammer will helpfully suggest a missing assumption:
-
-\prew
-\slshape
-e: Candidate missing assumption: \\
-length ys = length xs
-\postw
+%For goals that are inconsistent with the background theory (and hence unprovable
+%unless the theory is itself inconsistent), such as
+%
+%\prew
+%\textbf{lemma} ``$\mathit{length}\; (\mathit{zip}\; \mathit{xs}\; \mathit{ys}) = \mathit{length}\; \mathit{xs}$'' \\
+%\textbf{sledgehammer}
+%\postw
+%
+%Sledgehammer's output might look as follows:
+%
+%\prew
+%\slshape
+%vampire found a falsification\ldots \\
+%vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
+%\postw
+%
+%Sometimes Sledgehammer will helpfully suggest a missing assumption:
+%
+%\prew
+%\slshape
+%e: Candidate missing assumption: \\
+%length ys = length xs
+%\postw
 
 \section{Hints}
 \label{hints}
@@ -640,6 +640,7 @@
 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmartfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -818,7 +819,7 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opsmartx{falsify}{dont\_falsify}
+\opsmartfalse{falsify}{dont\_falsify}
 Specifies whether Sledgehammer should look for falsifications or for proofs. By
 default, it looks for both.
 
@@ -828,7 +829,7 @@
 only the background theory; this might happen, for example, if a flawed axiom is
 used or if a flawed lemma was introduced with \textbf{sorry}.
 
-\opdefault{abduce}{smart\_int}{smart}
+\opdefault{abduce}{smart\_int}{0}
 Specifies the maximum number of candidate missing assumptions that may be
 displayed. These hypotheses are discovered heuristically by a process called
 abduction (which stands in contrast to deduction)---that is, they are guessed
diff -r b7b777fc916c -r d3122089b67c src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 07 17:09:17 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 14 15:47:27 2023 +0200
@@ -53,8 +53,8 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("spy", "false"),
-   ("abduce", "smart"),
-   ("falsify", "smart"),
+   ("abduce", "0"),
+   ("falsify", "false"),
    ("type_enc", "smart"),
    ("strict", "false"),
    ("lam_trans", "smart"),