chore: disable ac_nf by default (#5673)

We trust that the users read the error messages or tactic docs to
discover the option.
AWS problems have shown that this can be too eager of an operation to
do.
Given that we have the luxury of interactivity let's go for an approach
where the users
can optionally enable it.

src/Lean/Elab/Tactic/BVDecide/External.lean

@@ -169,8 +169,9 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
   let out? ← runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
   match out? with
   | .timeout =>
-    let mut err := "The SAT solver timed out while solving the problem."
-    err := err ++ "\nConsider increasing the timeout with `set_option sat.timeout <sec>`"
+    let mut err := "The SAT solver timed out while solving the problem.\n"
+    err := err ++ "Consider increasing the timeout with `set_option sat.timeout <sec>`.\n"
+    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option."
     throwError err
   | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
     if exitCode == 255 then

src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean

@@ -53,7 +53,7 @@ register_builtin_option debug.bv.graphviz : Bool := {
 }
 
 register_builtin_option bv.ac_nf : Bool := {
-  defValue := true
+  defValue := false
   descr := "Canonicalize with respect to associativity and commutativitiy."
 }
 

src/Std/Tactic/BVDecide/Syntax.lean

@@ -46,6 +46,10 @@ terms that were considered as variables.
 
 In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.
 
+If solving your problem relies inherently on using associativity or commutativity, consider enabling
+the `bv.ac_nf` option.
+
+
 Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
 -/
 syntax (name := bvDecide) "bv_decide" : tactic

tests/lean/run/bv_decide_rewriter.lean

@@ -17,12 +17,6 @@ example :
 example (x y z : BitVec 8) (h1 : x = z → False) (h2 : x = y) (h3 : y = z) : False := by
   bv_decide
 
-example (x y : BitVec 256) : x * y = y * x := by
-  bv_decide
-
-example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by
-  bv_decide
-
 def mem_subset (a1 a2 b1 b2 : BitVec 64) : Bool :=
   (b2 - b1 = BitVec.ofNat 64 (2^64 - 1)) ||
   ((a2 - b1 <= b2 - b1 && a1 - b1 <= a2 - b1))
@@ -84,3 +78,18 @@ example {x : BitVec 16} : (10 + x) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : (x + 10) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
+
+
+
+
+section
+
+set_option bv.ac_nf true
+
+example (x y : BitVec 256) : x * y = y * x := by
+  bv_decide
+
+example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by
+  bv_decide
+
+end

tests/lean/run/bv_errors.lean

@@ -6,7 +6,8 @@ set_option bv.ac_nf false
 
 /--
 error: The SAT solver timed out while solving the problem.
-Consider increasing the timeout with `set_option sat.timeout <sec>`
+Consider increasing the timeout with `set_option sat.timeout <sec>`.
+If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option.
 -/
 #guard_msgs in
 set_option sat.timeout 1 in