inductive Lean.Elab.Tactic.BVDecide.Frontend.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.Frontend.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 subsitution 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.

def Lean.Parser.Tactic.bvCheck : ParserDescr

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.bvDecide : ParserDescr

Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to

• the Lean equivalent of QF_BV
• automatically splitting up structures that contain information about BitVec or Bool

example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
  intros
  bv_decide

If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

If bv_decide fails to close a goal it provides a counter-example, containing assignments for all 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.

Note: include import Std.Tactic.BVDecide

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.bvTrace : ParserDescr

Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

Note: include import Std.Tactic.BVDecide

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.bvNormalize : ParserDescr

Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

Note: include import Std.Tactic.BVDecide

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.bv_normalize : ParserDescr

Theorems tagged with the bv_normalize attribute are used during the rewriting step of the bv_decide tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.bvNormalizeProcBuiltinAttr : ParserDescr

Auxiliary attribute for builtin bv_normalize simprocs.

Equations

• One or more equations did not get rendered due to their size.