This module contains the implementation of the reflection monad, used by all other components of this directory.

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBVBinOp : ToExpr Std.Tactic.BVDecide.BVBinOp

Equations

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

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBVUnOp : ToExpr Std.Tactic.BVDecide.BVUnOp

Equations

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

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBVExpr {w : Nat} : ToExpr (Std.Tactic.BVDecide.BVExpr w)

Equations

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

def Lean.Meta.Tactic.BVDecide.instToExprBVExpr.go {w : Nat} : Std.Tactic.BVDecide.BVExpr w → Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Tactic.BVDecide.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.var idx) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.var) (Lean.toExpr w) (Lean.toExpr idx)
• Lean.Meta.Tactic.BVDecide.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.const val) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.const) (Lean.toExpr w) (Lean.toExpr val)

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBVBinPred : ToExpr Std.Tactic.BVDecide.BVBinPred

Equations

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

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprGate : ToExpr Std.Tactic.BVDecide.Gate

Equations

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

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBVPred : ToExpr Std.Tactic.BVDecide.BVPred

Equations

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

def Lean.Meta.Tactic.BVDecide.instToExprBVPred.go : Std.Tactic.BVDecide.BVPred → Expr

Equations

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

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.instToExprBoolExpr {α : Type} [ToExpr α] : ToExpr (Std.Tactic.BVDecide.BoolExpr α)

Equations

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

def Lean.Meta.Tactic.BVDecide.instToExprBoolExpr.go {α : Type} [ToExpr α] : Std.Tactic.BVDecide.BoolExpr α → Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Tactic.BVDecide.instToExprBoolExpr.go (Std.Tactic.BVDecide.BoolExpr.literal lit) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BoolExpr.literal) (Lean.toTypeExpr α) (Lean.toExpr lit)
• Lean.Meta.Tactic.BVDecide.instToExprBoolExpr.go (Std.Tactic.BVDecide.BoolExpr.const b) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BoolExpr.const) (Lean.toTypeExpr α) (Lean.toExpr b)
• Lean.Meta.Tactic.BVDecide.instToExprBoolExpr.go x_1.not = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BoolExpr.not) (Lean.toTypeExpr α) (Lean.Meta.Tactic.BVDecide.instToExprBoolExpr.go x_1)

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

A BitVec atom.

• width : Nat

  The width of the BitVec that is being abstracted.

• atomNumber : Nat

  A unique numeric identifier for the atom.

• synthetic : Bool

  Whether the atom is synthetic. The effect of this is that values for this atom are not considered for the counter example derivation. This is for example useful when we introduce an atom over an expression, together with additional lemmas that fully describe the behavior of the atom.

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

• hypotheses : Array Normalize.Hyp
• config : Elab.Tactic.BVDecide.BVDecideConfig

def Lean.Meta.Tactic.BVDecide.mkBoolAtomWrapper (e : Expr) : Sym.SymM Expr

Equations

• Lean.Meta.Tactic.BVDecide.mkBoolAtomWrapper e = Lean.Meta.Sym.share (Lean.mkApp (Lean.mkConst `BitVec.ofBool) e)

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

An atom interpreted by the UF theory.

• funExpr : Expr

  The function expression associated with the atom.

• isBoolAtom : Bool

  If true then the actual atom is BitVec.ofBool funExpr.

def Lean.Meta.Tactic.BVDecide.FunAtom.atomExpr (funAtom : FunAtom) : Sym.SymM Expr

Equations

• funAtom.atomExpr = if funAtom.isBoolAtom = true then Lean.Meta.Tactic.BVDecide.mkBoolAtomWrapper funAtom.funExpr else pure funAtom.funExpr

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

The state associated with the theory of uninterpreted functions (UF).

• atoms : Array FunAtom

  The list of function atoms collected so far.

• masks : Array (Array Bool)

  The list of congruence masks per function atom.

• patterns : Array Expr

  The function atoms with their congruence-relevant arguments abstracted as lambda binders.

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

Theory solver state.

• funState : FunState

  State associated with the theory of uninterpreted functions (UF).

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

The state of the reflection monad

• atoms : Std.HashMap Sym.ExprPtr Atom

  The atoms encountered so far. Saved as a map from BitVec expressions to a (width, atomNumber) pair.

• atomsAssignmentExprCache : Option Expr

  A cache for atomsAssignmentExpr. If it is none the cache is currently invalidated as new atoms have been added since it was last updated, if it is some it must be consistent with the atoms contained in atoms.

• atomsAssignmentMapCache : Option (Std.HashMap Nat (Nat × Expr × Bool))

  The equivalent of atomsAssignmentExprCache but computed as a efficiently computable hashmap.

• evalsAtCache : Std.HashMap Sym.ExprPtr (Option Expr)

  Cached calls to evalsAtAtoms of various reflection structures. Whenever atoms is modified this cache is invalidated as evalsAtAtoms relies on atoms.

• theoryState : TheoryState

  State for theory solvers.

@[reducible, inline]

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

The reflection monad, used to track BitVec variables that we see as we traverse the context.

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM = ReaderT Lean.Meta.Tactic.BVDecide.Context (StateRefT' IO.RealWorld Lean.Meta.Tactic.BVDecide.State Lean.Meta.Grind.GrindM)

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

A reified version of an Expr representing a BVExpr.

• width : Nat
• bvExpr : Std.Tactic.BVDecide.BVExpr self.width

  The reified expression.

• originalExpr : Expr

  The expression that was reflected, used for caching of evalsAtAtoms.

• evalsAtAtoms' : ReifyM (Option Expr)

  A proof that bvExpr.eval atomsAssignment = originalExpr, none if it holds by rfl.

• expr : Expr

  A cache for toExpr bvExpr.

def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.evalsAtAtoms (reified : ReifiedBVExpr) : ReifyM (Option Expr)

Equations

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

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

A reified version of an Expr representing a BVPred.

• bvPred : Std.Tactic.BVDecide.BVPred

  The reified expression.

• originalExpr : Expr

  The expression that was reflected, usef for caching of evalsAtAtoms.

• evalsAtAtoms' : ReifyM (Option Expr)

  A proof that bvPred.eval atomsAssignment = originalExpr, none if it holds by rfl.

• expr : Expr

  A cache for toExpr bvPred

def Lean.Meta.Tactic.BVDecide.ReifiedBVPred.evalsAtAtoms (reified : ReifiedBVPred) : ReifyM (Option Expr)

Equations

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

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

A reified version of an Expr representing a BVLogicalExpr.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• originalExpr : Expr

  The expression that was reflected, usef for caching of evalsAtAtoms.

• evalsAtAtoms' : ReifyM (Option Expr)

  A proof that bvExpr.eval atomsAssignment = originalExpr, none if it holds by rfl.

• expr : Expr

  A cache for toExpr bvExpr

def Lean.Meta.Tactic.BVDecide.ReifiedBVLogical.evalsAtAtoms (reified : ReifiedBVLogical) : ReifyM (Option Expr)

Equations

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

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

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• satAtAtoms : ReifyM Expr

  A proof that bvExpr.eval atomsAssignment = true.

• expr : Expr

  A cache for toExpr bvExpr

def Lean.Meta.Tactic.BVDecide.ReifyM.run {α : Type} (m : ReifyM α) (hypotheses : Array Normalize.Hyp) (cfg : Elab.Tactic.BVDecide.BVDecideConfig) : Grind.GrindM α

Run a reflection computation as a SymM one.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifyM.atoms : ReifyM (Array (Nat × Expr))

Retrieve the atoms as pairs of their width and expression.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifyM.atomsAssignmentMap : ReifyM (Std.HashMap Nat (Nat × Expr × Bool))

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifyM.atomsAssignmentExpr : ReifyM Expr

Retrieve a BitVec.Assignment representing the atoms we found so far.

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifyM.isAtom (e : Expr) : ReifyM Bool

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM.isAtom e = do let __do_lift ← getThe Lean.Meta.Tactic.BVDecide.State pure (__do_lift.atoms.contains { expr := e })

def Lean.Meta.Tactic.BVDecide.ReifyM.getAtomNumber (e : Expr) : ReifyM (Option Nat)

Equations

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

def Lean.Meta.Tactic.BVDecide.ReifyM.lookup (e : Expr) (width : Nat) (synthetic : Bool) : ReifyM Nat

Look up an expression in the atoms, recording it if it has not previously appeared.

Equations

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

@[inline]

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

Equations

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

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' (mkFRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (mkSRefl : Expr → Expr) (snd : Expr) (sproof : Option Expr) : Option (Expr × Expr)

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' mkFRefl fst (some fproof_2) mkSRefl snd (some sproof_2) = some (fproof_2, sproof_2)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' mkFRefl fst (some fproof_2) mkSRefl snd none = some (fproof_2, mkSRefl snd)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' mkFRefl fst none mkSRefl snd (some sproof_2) = some (mkFRefl fst, sproof_2)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' mkFRefl fst none mkSRefl snd none = none

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) : Option (Expr × Expr)

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof mkRefl fst fproof snd sproof = Lean.Meta.Tactic.BVDecide.ReifyM.simplifyBinaryProof' mkRefl fst fproof mkRefl snd sproof

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.ReifyM.simplifyTernaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) : Option (Expr × Expr × Expr)

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyTernaryProof mkRefl fst (some fproof_2) snd sproof thd tproof = some (fproof_2, stproof)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyTernaryProof mkRefl fst (some fproof_2) snd sproof thd tproof = some (fproof_2, mkRefl snd, mkRefl thd)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyTernaryProof mkRefl fst none snd sproof thd tproof = some (mkRefl fst, stproof)
• Lean.Meta.Tactic.BVDecide.ReifyM.simplifyTernaryProof mkRefl fst none snd sproof thd tproof = none

@[inline]

def Lean.Meta.Tactic.BVDecide.ReifyM.getHyps : ReifyM (Array Normalize.Hyp)

Equations

• Lean.Meta.Tactic.BVDecide.ReifyM.getHyps = do let __do_lift ← read pure __do_lift.hypotheses

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

The state of the lemma reflection monad.

• lemmas : Array SatAtBVLogical

  The list of top level lemmas that got created on the fly during reflection.

• bvExprCache : Std.HashMap Sym.ExprPtr (Option ReifiedBVExpr)

  Cache for reification of BVExpr.

• bvPredCache : Std.HashMap Sym.ExprPtr (Option ReifiedBVPred)

  Cache for reification of BVPred.

• bvLogicalCache : Std.HashMap Sym.ExprPtr (Option ReifiedBVLogical)

  Cache for reification of BVLogicalExpr.

@[reducible, inline]

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

The lemma reflection monad. It extends the usual reflection monad ReifyM by adding the ability to add additional top level lemmas on the fly.

Equations

• Lean.Meta.Tactic.BVDecide.LemmaM = StateRefT' IO.RealWorld Lean.Meta.Tactic.BVDecide.LemmaState Lean.Meta.Tactic.BVDecide.ReifyM

def Lean.Meta.Tactic.BVDecide.LemmaM.run {α : Type} (m : LemmaM α) (state : LemmaState := { }) : ReifyM (α × Array SatAtBVLogical)

Equations

• m.run state = do let __x ← StateRefT'.run m state match __x with | (res, state) => pure (res, state.lemmas)

def Lean.Meta.Tactic.BVDecide.LemmaM.addLemma (lemma : SatAtBVLogical) : LemmaM Unit

Add another top level lemma.

Equations

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

def Lean.Meta.Tactic.BVDecide.LemmaM.resetLemmas : LemmaM Unit

Drop all of the lemmas recorded so far.

Equations

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

def Lean.Meta.Tactic.BVDecide.LemmaM.getLemmas : LemmaM (Array SatAtBVLogical)

Equations

• Lean.Meta.Tactic.BVDecide.LemmaM.getLemmas = do let __do_lift ← get pure __do_lift.lemmas

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.LemmaM.withBVExprCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVExpr)) : LemmaM (Option ReifiedBVExpr)

Equations

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

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.LemmaM.withBVPredCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVPred)) : LemmaM (Option ReifiedBVPred)

Equations

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

@[specialize #[]]

def Lean.Meta.Tactic.BVDecide.LemmaM.withBVLogicalCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVLogical)) : LemmaM (Option ReifiedBVLogical)

Equations

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