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. Currently set to false and ignored on Windows due to a bug in CaDiCal.

• acNf : Bool

  Canonicalize with respect to associativity and commutativitiy.

• 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.

• embeddedConstraintSubst : Bool

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

• 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.

def Lean.Parser.Tactic.bvCheck : Lean.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 : Lean.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:

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.

Equations

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

def Lean.Parser.Tactic.bvTrace : Lean.ParserDescr

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

Equations

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

def Lean.Parser.Tactic.bvNormalize : Lean.ParserDescr

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

Equations

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

def Lean.Parser.bvNormalizeProcBuiltinAttr : Lean.ParserDescr

Auxiliary attribute for builtin bv_normalize simprocs.

Equations

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