This module contains the implementation of counterexample recovery and explanation.

def Lean.Meta.Tactic.BVDecide.reconstructCounterExample (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (assignment : Array (Bool × Nat)) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : Array (Expr × Bool × Std.Tactic.BVDecide.BVExpr.PackedBitVec)

Given:

• aig: The AIG that was used to produce the CNF.
• assignments: A model for the CNF as provided by a SAT solver.
• 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.Meta.Tactic.BVDecide.CounterExample : Type

A counter example generated from the bitblaster.

• goal : MVarId

  The goal in which to interpret this counter example.

• unusedHypotheses : Std.HashSet Normalize.Hyp

  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.

• functionAtoms : Array Expr

  Some of the expressions in the equations may be function atoms that were used by the UF theory solver. We want to inform the user that these are not just ordinary uninterpeted symbols.

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

Equations

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