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 × Lean.Expr)) : Array (Lean.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.

Equations

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

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

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr
• proveFalse : Lean.Expr → Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr
• unusedHypotheses : Std.HashSet Lean.FVarId

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

A counter example generated from the bitblaster.

• unusedHypotheses : Std.HashSet Lean.FVarId

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

• equations : Array (Lean.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 : Lean.Expr
• lratCert : Lean.Elab.Tactic.BVDecide.Frontend.LratCert

@[reducible, inline]

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

Equations

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

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

The result of a spurious counter example diagnosis.

• uninterpretedSymbols : Std.HashSet Lean.Expr
• unusedRelevantHypotheses : Std.HashSet Lean.FVarId

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM = ReaderT Lean.Elab.Tactic.BVDecide.Frontend.CounterExample (StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.Diagnosis Lean.MetaM)

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

Equations

• x.run counterExample = do let __discr ← (ReaderT.run x counterExample).run { uninterpretedSymbols := ∅, unusedRelevantHypotheses := ∅ } match __discr with | (fst, issues) => pure issues

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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.unusedHyps = do let __do_lift ← read pure __do_lift.unusedHypotheses

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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.equations = do let __do_lift ← read pure __do_lift.equations

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.DiagnosisM.diagnose : Lean.Elab.Tactic.BVDecide.Frontend.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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.explainers = [Lean.Elab.Tactic.BVDecide.Frontend.uninterpretedExplainer, Lean.Elab.Tactic.BVDecide.Frontend.unusedRelevantHypothesesExplainer]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

The result of calling bv_decide.

• lratCert : Option Lean.Elab.Tactic.BVDecide.Frontend.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 : Lean.MVarId) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) : Lean.MetaM (Except Lean.Elab.Tactic.BVDecide.Frontend.CounterExample Lean.Elab.Tactic.BVDecide.Frontend.Result)

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

Equations

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

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

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

Equations

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

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

Equations

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