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 with the following changes:

• Division and remainder operations are not yet implemented.
• if-then-else is not yet implemented.
• BitVec.ofBool is not yet implemented.

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

• Lean.Parser.Tactic.bvDecide = Lean.ParserDescr.node `Lean.Parser.Tactic.bvDecide 1024 (Lean.ParserDescr.nonReservedSymbol "bv_decide" false)

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

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

Equations

• Lean.Parser.Tactic.bvTrace = Lean.ParserDescr.node `Lean.Parser.Tactic.bvTrace 1024 (Lean.ParserDescr.nonReservedSymbol "bv_decide?" false)

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

• Lean.Parser.Tactic.bvNormalize = Lean.ParserDescr.node `Lean.Parser.Tactic.bvNormalize 1024 (Lean.ParserDescr.nonReservedSymbol "bv_normalize" false)

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.