This module provides the implementation of the bv_decide frontend itself.

def Lean.Elab.Tactic.BVDecide.Frontend.reconstructCounterExample (var2Cnf : Std.HashMap Std.Tactic.BVDecide.BVBit Nat) (assignment : Array (Bool × Nat)) (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : Array (Expr × Std.Tactic.BVDecide.BVExpr.PackedBitVec)

Given:

• var2Cnf: The mapping from AIG to CNF variables.
• assignments: A model for the CNF as provided by a SAT solver.
• aigSize: The amount of nodes in the AIG that was used to produce the CNF.
• atomsAssignment: The mapping of the reflection monad from atom indices to Expr.

Reconstruct bit by bit which value expression must have had which BitVec value and return all expression - pair values.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReflectionResult : Type

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reflected expression.

• proveFalse : Expr → M Expr

  Function to prove False given a satisfiability proof of bvExpr

• unusedHypotheses : Std.HashSet FVarId

  Set of unused hypotheses for diagnostic purposes.

• expr : Expr

  A cache for toExpr bvExpr.

structure Lean.Elab.Tactic.BVDecide.Frontend.CounterExample : Type

A counter example generated from the bitblaster.

• goal : MVarId

  The goal in which to interpret this counter example.

• unusedHypotheses : Std.HashSet FVarId

  The set of unused but potentially relevant hypotheses. Useful for diagnosing spurious counter examples.

• equations : Array (Expr × Std.Tactic.BVDecide.BVExpr.PackedBitVec)

  The actual counter example as a list of equations denoted as expr = value pairs.

structure Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver.Result : Type

• proof : Expr
• lratCert : LratCert

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver : Type

structure Lean.Elab.Tactic.BVDecide.Frontend.Diagnosis : Type

The result of a spurious counter example diagnosis.

• uninterpretedSymbols : Std.HashSet Expr
• unusedRelevantHypotheses : Std.HashSet FVarId
• derivedEquations : Array (Expr × Expr)

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM : Type → Type

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosis

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.unusedHyps : DiagnosisM (Std.HashSet FVarId)

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.equations : DiagnosisM (Array (Expr × Std.Tactic.BVDecide.BVExpr.PackedBitVec))

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.addUninterpretedSymbol (e : Expr) : DiagnosisM Unit

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.addDerivedEquation (var value : Expr) : DiagnosisM Unit

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.diagnose : DiagnosisM Unit

Diagnose spurious counter examples, currently this checks:

• Whether uninterpreted symbols were used
• Whether all hypotheses which contain any variable that was bitblasted were included

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.diagnose.transformEquation (var : Expr) (value : Std.Tactic.BVDecide.BVExpr.PackedBitVec) : DiagnosisM (Expr × Expr)

def Lean.Elab.Tactic.BVDecide.Frontend.uninterpretedExplainer (d : Diagnosis) : Option MessageData

def Lean.Elab.Tactic.BVDecide.Frontend.unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData

def Lean.Elab.Tactic.BVDecide.Frontend.explainers : List (Diagnosis → Option MessageData)

def Lean.Elab.Tactic.BVDecide.Frontend.explainCounterExampleQuality (counterExample : CounterExample) : MetaM MessageData

def Lean.Elab.Tactic.BVDecide.Frontend.LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr

Turn an LratCert into a proof that some reflectedExpr is UNSAT.

def Lean.Elab.Tactic.BVDecide.Frontend.LratCert.toReflectionProof.mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit

Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.

def Lean.Elab.Tactic.BVDecide.Frontend.lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : MetaM (Except CounterExample UnsatProver.Result)

def Lean.Elab.Tactic.BVDecide.Frontend.reflectBV (g : MVarId) : M ReflectionResult

def Lean.Elab.Tactic.BVDecide.Frontend.closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) : MetaM (Except CounterExample LratCert)

def Lean.Elab.Tactic.BVDecide.Frontend.bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert)

structure Lean.Elab.Tactic.BVDecide.Frontend.Result : Type

The result of calling bv_decide.

• lratCert : Option LratCert

  If the normalization step was not enough to solve the goal this contains the LRAT proof certificate.

def Lean.Elab.Tactic.BVDecide.Frontend.bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result)

Try to close g using a bitblaster. Return either a CounterExample if one is found or a Result if g is proven.

def Lean.Elab.Tactic.BVDecide.Frontend.bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result

Call bvDecide' and throw a pretty error if a counter example ends up being produced.

def Lean.Elab.Tactic.BVDecide.Frontend.evalBvDecide : Tactic