inductive Lean.Elab.Tactic.BVDecide.SolverMode : Type

The various kinds of configurations offered for the SAT solver.

• proof : SolverMode

  Set SAT solver options to improve proof search.

• counterexample : SolverMode

  Set SAT solver options to improve counterexample search.

• default : SolverMode

  Don't set additional SAT solver flags.

structure Lean.Elab.Tactic.BVDecide.BVDecideConfig : Type

The configuration options for bv_decide.

• timeout : Nat

  The number of seconds that the SAT solver is run before aborting.

• trimProofs : Bool

  Whether to run the trimming algorithm on LRAT proofs.

• binaryProofs : Bool

  Whether to use the binary LRAT proof format.

• acNf : Bool

  Canonicalize with respect to associativity and commutativity.

• andFlattening : Bool

  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. Because embedded constraint substitution is the only use case for this feature it is automatically disabled whenever embedded constraint substitution is disabled.

• embeddedConstraintSubst : Bool

  Look at all hypotheses of the form h : x = true, if x occurs in another hypothesis substitute it with true.

• structures : Bool

  Split up local declarations of structures that are collections of other supported types into their individual parts automatically.

• fixedInt : Bool

  Enable preprocessing with the int_toBitVec simp set to reduce UIntX/IntX to BitVec and thus make them accessible for bv_decide.

• enums : Bool

  Handle equality on enum inductives by turning them into BitVec.

• graphviz : Bool

  Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process.

• maxSteps : Nat

  The maximum number of subexpressions to visit when performing simplification.

• shortCircuit : Bool

  Short-circuit multiplication as an abstraction-style optimization that triggers if matching multiplications are not needed to proof a goal.

• solverMode : SolverMode

  The SAT solver configuration to use. Defaults to .proof as that is the most relevant use case for bv_decide.