This module contains the implementation of counterexample recovery and explanation.

def Lean.Meta.Tactic.BVDecide.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.

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

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

Equations

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