feat: change bv_decide to an elaborated config

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

@@ -170,8 +170,8 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
   match out? with
   | .timeout =>
     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."
+    err := err ++ "Consider increasing the timeout with the `timeout` config option.\n"
+    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option."
     throwError err
   | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
     if exitCode == 255 then

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

@@ -6,6 +6,7 @@ Authors: Kim Morrison, Henrik Böving
 prelude
 import Lean.Util.Trace
 import Lean.Elab.Tactic.Simp
+import Std.Tactic.BVDecide.Syntax
 
 /-!
 Provides environment extensions around the `bv_decide` tactic frontends.
@@ -32,30 +33,7 @@ register_builtin_option sat.solver : String := {
         to use the one that ships with Lean."
 }
 
-register_builtin_option sat.timeout : Nat := {
-  defValue := 10
-  descr := "the number of seconds that the sat solver is run before aborting"
-}
-
-register_builtin_option sat.trimProofs : Bool := {
-  defValue := true
-  descr := "Whether to run the trimming algorithm on LRAT proofs"
-}
-
-register_builtin_option sat.binaryProofs : Bool := {
-  defValue := true
-  descr := "Whether to use the binary LRAT proof format. Currently set to false and ignored on Windows due to a bug in CaDiCal."
-}
-
-register_builtin_option debug.bv.graphviz : Bool := {
-  defValue := false
-  descr := "Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process."
-}
-
-register_builtin_option bv.ac_nf : Bool := {
-  defValue := false
-  descr := "Canonicalize with respect to associativity and commutativitiy."
-}
+declare_config_elab elabBVDecideConfig Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig
 
 builtin_initialize bvNormalizeExt : Meta.SimpExtension ←
   Meta.registerSimpAttr `bv_normalize "simp theorems used by bv_normalize"

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

@@ -28,22 +28,22 @@ def getSrcDir : TermElabM System.FilePath := do
     | throwError "cannot compute parent directory of '{srcPath}'"
   return srcDir
 
-def mkContext (lratPath : System.FilePath) : TermElabM TacticContext := do
+def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM TacticContext := do
   let lratPath := (← getSrcDir) / lratPath
-  TacticContext.new lratPath
+  TacticContext.new lratPath cfg
 
 /--
 Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
 -/
-def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
-  let cert ← LratCert.ofFile cfg.lratPath cfg.trimProofs
-  cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
+  let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs
+  cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
-def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
+def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
   let unsatProver : UnsatProver := fun _ reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker cfg reflectionResult.bvExpr
+      let proof ← lratChecker ctx reflectionResult.bvExpr
       return .ok ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()
@@ -52,14 +52,15 @@ def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
 open Lean.Meta.Tactic in
 @[builtin_tactic Lean.Parser.Tactic.bvCheck]
 def evalBvCheck : Tactic := fun
-  | `(tactic| bv_check%$tk $path:str) => do
-    let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString
+  | `(tactic| bv_check%$tk $cfgStx:optConfig $path:str) => do
+    let cfg ← elabBVDecideConfig cfgStx
+    let ctx ← BVDecide.Frontend.BVCheck.mkContext path.getString cfg
     liftMetaFinishingTactic fun g => do
-      let g'? ← Normalize.bvNormalize g
+      let g'? ← Normalize.bvNormalize g cfg
       match g'? with
-      | some g' => bvCheck g' cfg
+      | some g' => bvCheck g' ctx
       | none =>
-        let bvNormalizeStx ← `(tactic| bv_normalize)
+        let bvNormalizeStx ← `(tactic| bv_normalize $cfgStx)
         logWarning m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around."
         TryThis.addSuggestion tk bvNormalizeStx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax

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

@@ -186,7 +186,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     err := err ++ m!"Consider the following assignment:\n"
     return err
 
-def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
+def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
@@ -197,7 +197,7 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
   let aigSize := entry.aig.decls.size
   trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
-  if cfg.graphviz then
+  if ctx.config.graphviz then
     IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry
 
   let (cnf, map) ←
@@ -211,12 +211,12 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
 
   let res ←
     withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
-      runExternal cnf cfg.solver cfg.lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs
+      runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
 
   match res with
   | .ok cert =>
     trace[Meta.Tactic.sat] "SAT solver found a proof."
-    let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
     return .ok ⟨proof, cert⟩
   | .error assignment =>
     trace[Meta.Tactic.sat] "SAT solver found a counter example."
@@ -267,10 +267,10 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
       return .ok cert
     | .error counterExample => return .error counterExample
 
-def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
+def bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
   let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
-      lratBitblaster g cfg reflectionResult atomsAssignment
+      lratBitblaster g ctx reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
 /--
@@ -287,18 +287,18 @@ structure Result where
 Try to close `g` using a bitblaster. Return either a `CounterExample` if one is found or a `Result`
 if `g` is proven.
 -/
-def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
-  let g? ← Normalize.bvNormalize g
+def bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result) := do
+  let g? ← Normalize.bvNormalize g ctx.config
   let some g := g? | return .ok ⟨none⟩
-  match ← bvUnsat g cfg with
+  match ← bvUnsat g ctx with
   | .ok lratCert => return .ok ⟨some lratCert⟩
   | .error counterExample => return .error counterExample
 
 /--
 Call `bvDecide'` and throw a pretty error if a counter example ends up being produced.
 -/
-def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
-  match ← bvDecide' g cfg with
+def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
+  match ← bvDecide' g ctx with
   | .ok result => return result
   | .error counterExample =>
     counterExample.goal.withContext do
@@ -309,9 +309,10 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun
-  | `(tactic| bv_decide) => do
+  | `(tactic| bv_decide $cfg:optConfig) => do
+    let cfg ← elabBVDecideConfig cfg
     IO.FS.withTempFile fun _ lratFile => do
-      let cfg ← BVDecide.Frontend.TacticContext.new lratFile
+      let cfg ← BVDecide.Frontend.TacticContext.new lratFile cfg
       liftMetaFinishingTactic fun g => do
         discard <| bvDecide g cfg
   | _ => throwUnsupportedSyntax

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

@@ -34,12 +34,13 @@ open Lean.Meta.Tactic in
 open Lean.Elab.Tactic.BVDecide.LRAT in
 @[builtin_tactic Lean.Parser.Tactic.bvTrace]
 def evalBvTrace : Tactic := fun
-  | `(tactic| bv_decide?%$tk) => do
+  | `(tactic| bv_decide?%$tk $cfgStx:optConfig) => do
+    let cfg := { (← elabBVDecideConfig cfgStx) with trimProofs := false }
     let lratFile : System.FilePath ← BVTrace.getLratFileName
-    let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false }
+    let ctx ← BVCheck.mkContext lratFile cfg
     let g ← getMainGoal
     let trace ← g.withContext do
-      bvDecide g cfg
+      bvDecide g ctx
     /-
     Ideally trace.lratCert would be the `ByteArray` version of the proof already and we just write
     it. This isn't yet possible so instead we do the following:
@@ -57,12 +58,12 @@ def evalBvTrace : Tactic := fun
       let normalizeStx ← `(tactic| bv_normalize)
       TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef)
     | some .. =>
-      if sat.trimProofs.get (← getOptions) then
+      if ctx.config.trimProofs then
         let lratPath := (← BVCheck.getSrcDir) / lratFile
         let proof ← loadLRATProof lratPath
         let trimmed ← IO.ofExcept <| trim proof
         dumpLRATProof lratPath trimmed cfg.binaryProofs
-      let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString))
+      let bvCheckStx ← `(tactic| bv_check $cfgStx:optConfig $(quote lratFile.toString))
       TryThis.addSuggestion tk bvCheckStx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 

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

@@ -30,37 +30,28 @@ structure TacticContext where
   reflectionDef : Name
   solver : System.FilePath
   lratPath : System.FilePath
-  graphviz : Bool
-  timeout : Nat
-  trimProofs : Bool
-  binaryProofs : Bool
+  config : BVDecideConfig
 
-def TacticContext.new (lratPath : System.FilePath) : Lean.Elab.TermElabM TacticContext := do
+def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
+    Lean.Elab.TermElabM TacticContext := do
+  -- Account for: https://github.com/arminbiere/cadical/issues/112
+  let config :=
+    if System.Platform.isWindows then
+      { config with binaryProofs := false }
+    else
+      config
   let exprDef ← Lean.Elab.Term.mkAuxName `_expr_def
   let certDef ← Lean.Elab.Term.mkAuxName `_cert_def
   let reflectionDef ← Lean.Elab.Term.mkAuxName `_reflection_def
-  let opts ← getOptions
   let solver ← determineSolver
   trace[Meta.Tactic.sat] m!"Using SAT solver at '{solver}'"
-  let timeout := sat.timeout.get opts
-  let graphviz := debug.bv.graphviz.get opts
-  let trimProofs := sat.trimProofs.get opts
-  let binaryProofs :=
-    -- Account for: https://github.com/arminbiere/cadical/issues/112
-    if System.Platform.isWindows then
-      false
-    else
-      sat.binaryProofs.get opts
   return {
     exprDef,
     certDef,
     reflectionDef,
     solver,
     lratPath,
-    graphviz,
-    timeout,
-    trimProofs,
-    binaryProofs
+    config
   }
 where
   determineSolver : Lean.Elab.TermElabM System.FilePath := do

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

@@ -157,14 +157,14 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
 /--
 Responsible for applying the Bitwuzla style rewrite rules.
 -/
-def rewriteRulesPass : Pass := fun goal => do
+def rewriteRulesPass (maxSteps : Nat) : Pass := fun goal => do
   let bvThms ← bvNormalizeExt.getTheorems
   let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
   let sevalThms ← getSEvalTheorems
   let sevalSimprocs ← Simp.getSEvalSimprocs
 
   let simpCtx : Simp.Context := {
-    config := { failIfUnchanged := false, zetaDelta := true }
+    config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
     simpTheorems := #[bvThms, sevalThms]
     congrTheorems := (← getSimpCongrTheorems)
   }
@@ -181,7 +181,7 @@ def rewriteRulesPass : Pass := fun goal => do
 Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
 them to substitute occurences of `x` within other hypotheses
 -/
-def embeddedConstraintPass : Pass := fun goal =>
+def embeddedConstraintPass (maxSteps : Nat) : Pass := fun goal =>
   goal.withContext do
     let hyps ← goal.getNondepPropHyps
     let relevanceFilter acc hyp := do
@@ -195,7 +195,7 @@ def embeddedConstraintPass : Pass := fun goal =>
     let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
 
     let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false }
+      config := { failIfUnchanged := false, maxSteps }
       simpTheorems := relevantHyps
       congrTheorems := (← getSimpCongrTheorems)
     }
@@ -222,32 +222,35 @@ def acNormalizePass : Pass := fun goal => do
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
+def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
+  [
+    rewriteRulesPass cfg.maxSteps,
+    embeddedConstraintPass cfg.maxSteps
+  ]
 
-def passPipeline : MetaM (List Pass) := do
-  let opts ← getOptions
+def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
+  let mut passPipeline := defaultPipeline cfg
 
-  let mut passPipeline := defaultPipeline
-
-  if bv.ac_nf.get opts then
+  if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]
 
   return passPipeline
 
 end Pass
 
-def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
+def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do
   withTraceNode `bv (fun _ => return "Normalizing goal") do
     -- Contradiction proof
     let some g ← g.falseOrByContra | return none
     trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
-    Pass.fixpointPipeline (← Pass.passPipeline) g
+    Pass.fixpointPipeline (Pass.passPipeline cfg) g
 
 @[builtin_tactic Lean.Parser.Tactic.bvNormalize]
 def evalBVNormalize : Tactic := fun
-  | `(tactic| bv_normalize) => do
+  | `(tactic| bv_normalize $cfg:optConfig) => do
+    let cfg ← elabBVDecideConfig cfg
     let g ← getMainGoal
-    match ← bvNormalize g with
+    match ← bvNormalize g cfg with
     | some newGoal => replaceMainGoal [newGoal]
     | none => replaceMainGoal []
   | _ => throwUnsupportedSyntax