From adfbc56f9100257da410e9c36f6f90ca203b6eeb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 14 Oct 2024 23:23:18 +0200
Subject: [PATCH] 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   |  5 +++--
 .../Elab/Tactic/BVDecide/Frontend/Attr.lean   |  2 +-
 src/Std/Tactic/BVDecide/Syntax.lean           |  4 ++++
 tests/lean/run/bv_decide_rewriter.lean        | 21 +++++++++++++------
 tests/lean/run/bv_errors.lean                 |  3 ++-
 5 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean
index 6f498afc86..2b58e2de4f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/External.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
index d5139298be..ce770dd5d5 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
+++ b/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."
 }
 
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index 68c4a6a6c5..aeedb45f04 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/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
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 81cf3a1e34..0d4c7c2a07 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/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
diff --git a/tests/lean/run/bv_errors.lean b/tests/lean/run/bv_errors.lean
index caa39cb26f..29023911f9 100644
--- a/tests/lean/run/bv_errors.lean
+++ b/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