This module provides the basic infrastructure for the CEGAR (Counter Example Guided Abstraction Refinement) solver.

structure Lean.Meta.Tactic.BVDecide.CegarHyp : Type

A hypothesis generated by the CEGAR refinement procedure.

• hyp : Normalize.Hyp

  The Expr-level non-internalized hypothesis.

• tacticProof : MetaM (TSyntax `Lean.Parser.Tactic.tacticSeq)

  A Syntax-level regular tactic proof for the hypothesis.

• grindProof : MetaM (Option (TSyntax `Lean.Parser.Tactic.tacticSeq))

  A Syntax-level grind tactic proof for the hypothesis. If none we will use have : hyp and let grind modes' automation figure it out.

structure Lean.Meta.Tactic.BVDecide.CegarM.Context : Type

• goal : MVarId

  The meta variable that the CEGAR procedure is operating on.

• unusedHypotheses : Std.HashSet Normalize.Hyp

  The set of unused hypothesis from the initial pre-processing, used for error messages later on.

• tacticContext : TacticContext

  The bv_decide general TacticContext.

structure Lean.Meta.Tactic.BVDecide.CegarM.FunState : Type

State of the UF theory solver.

• congrCache : Std.HashMap Sym.ExprPtr Expr

  Cache for congruence lemmas on UF theory atoms.

structure Lean.Meta.Tactic.BVDecide.CegarM.BitVecState : Type

State of the BitVec theory solver.

• aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit

  The AIG built so far, incrementally extended every CEGAR step.

• blastCache : Std.Tactic.BVDecide.BVExpr.Cache self.aig

  The bitblasting cached used so far, incrementally extended every CEGAR step.

• cnfCache : Std.Sat.AIG.toCNF.State self.aig

  Both the CNF cache and CNF formula built up so far, incrementally extended every CEGAR step.

structure Lean.Meta.Tactic.BVDecide.CegarM.TheoryState : Type

State carried around by our theory solvers.

• funState : FunState

  UF theory state.

• bitvecState : BitVecState

  BitVec theory state.

• preprocessCaches : Grind.BVDecide.Caches

  Caches for the hypothesis preprocessor.

• satSolver : Cadical.Solver

  The incremental SAT solver.

structure Lean.Meta.Tactic.BVDecide.CegarM.State : Type

• satExpr : SatAtBVLogical

  The conjunction of all reflected expressions so far.

• hypQueue : Array CegarHyp

  The queue of facts that will be processed at the beginning of the next CEGAR round.

• usedHyps : Array CegarHyp

  The collection of hypotheses that have been used so far, used for proof recovery later on.

• didChange : Bool

  Whether we should run another iteration of the procedure.

• theoryState : TheoryState

  State for our various theory solvers.

• solverTimeBudgetMs : Nat

  How many more milliseconds the SAT solver has to run.

• roundBudget : Nat

  How many more CEGAR rounds the solver has left.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.CegarM (α : Type) : Type

Equations

• Lean.Meta.Tactic.BVDecide.CegarM α = ReaderT Lean.Meta.Tactic.BVDecide.CegarM.Context (StateRefT' IO.RealWorld Lean.Meta.Tactic.BVDecide.CegarM.State Lean.Meta.Tactic.BVDecide.LemmaM) α

def Lean.Meta.Tactic.BVDecide.CegarM.getReflectionResult : CegarM ReflectionResult

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getReflectionResult = do let __do_lift ← get let __do_lift_1 ← read pure { satExpr := __do_lift.satExpr, unusedHypotheses := __do_lift_1.unusedHypotheses }

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getDidChange : CegarM Bool

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getDidChange = do let __do_lift ← get pure __do_lift.didChange

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.setDidChange (v : Bool) : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getTheoryState : CegarM TheoryState

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getTheoryState = do let __do_lift ← get pure __do_lift.theoryState

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.modifyTheoryState (f : TheoryState → TheoryState) : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.clearCaches : CegarM Unit

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.clearCaches = Lean.Meta.Tactic.BVDecide.CegarM.modifyTheoryState fun (s : Lean.Meta.Tactic.BVDecide.CegarM.TheoryState) => { satSolver := s.satSolver }

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.pushNewHyp (hyp : CegarHyp) : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getUsedHyps : CegarM (Array CegarHyp)

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getUsedHyps = do let __do_lift ← get pure __do_lift.usedHyps

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.drainNewHyps : CegarM (Array CegarHyp)

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getTacticContext : CegarM TacticContext

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getTacticContext = do let __do_lift ← read pure __do_lift.tacticContext

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.hasRefinementProcedures : CegarM Bool

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.consumeSolverTime (ms : Nat) : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getSolverTime : CegarM Nat

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getSolverTime = do let __do_lift ← get pure __do_lift.solverTimeBudgetMs

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.consumeRound : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.getRounds : CegarM Nat

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getRounds = do let __do_lift ← get pure __do_lift.roundBudget

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.takePreProcessCaches : CegarM Grind.BVDecide.Caches

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.setPreProcessCaches (caches : Grind.BVDecide.Caches) : CegarM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.CegarM.run {α : Type} (ctx : TacticContext) (x : CegarM (Except BVDecide.CounterExample α)) : UnsatProver α

Equations

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

def Lean.Meta.Tactic.BVDecide.CegarM.getSatSolver : CegarM Cadical.Solver

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.getSatSolver = do let __do_lift ← get pure __do_lift.theoryState.satSolver

structure Lean.Meta.Tactic.BVDecide.CegarM.CounterExample : Type

• exprCex : Std.HashMap Expr Std.Tactic.BVDecide.BVExpr.PackedBitVec
• atomCex : Std.HashMap Nat Std.Tactic.BVDecide.BVExpr.PackedBitVec

def Lean.Meta.Tactic.BVDecide.CegarM.CounterExample.ofArray (arr : Array (Expr × Bool × Std.Tactic.BVDecide.BVExpr.PackedBitVec)) : ReifyM CounterExample

Equations

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

structure Lean.Meta.Tactic.BVDecide.CegarCert : Type

• lemmas : Array CegarHyp
• lratCert : Option LratCert

def Lean.Meta.Tactic.BVDecide.CegarCert.solvedWithPreProcessing : CegarCert

Equations

• Lean.Meta.Tactic.BVDecide.CegarCert.solvedWithPreProcessing = { lemmas := #[], lratCert := none }

def Lean.Meta.Tactic.BVDecide.CegarCert.ofLratCert (cert : LratCert) : CegarCert

Equations

• Lean.Meta.Tactic.BVDecide.CegarCert.ofLratCert cert = { lemmas := #[], lratCert := some cert }

def Lean.Meta.Tactic.BVDecide.CegarM.createCert (cert : Option LratCert) : CegarM CegarCert

Equations

• Lean.Meta.Tactic.BVDecide.CegarM.createCert cert = do let lemmas ← Lean.Meta.Tactic.BVDecide.CegarM.getUsedHyps pure { lemmas := lemmas, lratCert := cert }