feat: add options to configure all of bv_decides preprocessing

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

@@ -308,22 +308,18 @@ def acNormalizePass : Pass where
 
     return newGoal
 
-/--
-The normalization passes used by `bv_normalize` and thus `bv_decide`.
--/
-def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
-  [
-    rewriteRulesPass cfg.maxSteps,
-    andFlatteningPass,
-    embeddedConstraintPass cfg.maxSteps
-  ]
-
 def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
-  let mut passPipeline := defaultPipeline cfg
+  let mut passPipeline := [rewriteRulesPass cfg.maxSteps]
 
   if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]
 
+  if cfg.andFlattening then
+    passPipeline := passPipeline ++ [andFlatteningPass]
+
+  if cfg.embeddedConstraintSubst then
+    passPipeline := passPipeline ++ [embeddedConstraintPass cfg.maxSteps]
+
   return passPipeline
 
 end Pass

src/Std/Tactic/BVDecide/Syntax.lean

@@ -29,6 +29,16 @@ structure BVDecideConfig where
   -/
   acNf : Bool := false
   /--
+  Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
+  This has synergy potential with embedded constraint substitution.
+  -/
+  andFlattening : Bool := true
+  /--
+  Look at all hypotheses of the form `h : x = true`, if `x` occurs in another hypothesis substitute
+  it with `true`.
+  -/
+  embeddedConstraintSubst : Bool := true
+  /--
   Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
   Lean process.
   -/