instance Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean : Hashable Int.Linear.Expr

Equations

• Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean = { hash := Lean.Meta.Grind.Arith.Cutsat.hashExpr✝ }

instance Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean_1 : Hashable Int.OfNat.Expr

Equations

• Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean_1 = { hash := Lean.Meta.Grind.Arith.Cutsat.hashExpr✝ }

structure Lean.Meta.Grind.Arith.Cutsat.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• polyMap : Std.HashMap Poly Expr
• exprMap : Std.HashMap Int.Linear.Expr Expr
• natExprMap : Std.HashMap Int.OfNat.Expr Expr

structure Lean.Meta.Grind.Arith.Cutsat.ProofM.Context : Type

• ctx : Expr
• foreignCtxs : Std.HashMap ForeignType Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.ProofM (α : Type) : Type

Auxiliary monad for constructing cutsat proofs.

Equations

• Lean.Meta.Grind.Arith.Cutsat.ProofM = ReaderT Lean.Meta.Grind.Arith.Cutsat.ProofM.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.Arith.Cutsat.ProofM.State Lean.Meta.Grind.GoalM)

def Lean.Meta.Grind.Arith.Cutsat.mkPolyDecl (p : Poly) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.mkExprDecl (e : Int.Linear.Expr) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr

Equations

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

partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr

def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProof (h : UnsatProof) : GoalM Expr

Equations

• h.toExprProof = Lean.Meta.Grind.Arith.Cutsat.withProofContext✝ h.toExprProofCore

def Lean.Meta.Grind.Arith.Cutsat.setInconsistent (h : UnsatProof) : GoalM Unit

Equations

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

A cutsat proof may depend on decision variables. We collect them and perform non chronological backtracking.

structure Lean.Meta.Grind.Arith.Cutsat.CollectDecVars.State : Type

• visited : Std.HashSet UInt64
• found : FVarIdSet

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM = ReaderT Lean.FVarIdSet (StateM Lean.Meta.Grind.Arith.Cutsat.CollectDecVars.State)

partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Cutsat.CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit

def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.collectDecVars (h : UnsatProof) : CollectDecVarsM Unit

Equations

• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁ c₂ c₃).collectDecVars = do c₁.collectDecVars c₂.collectDecVars c₃.collectDecVars

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.CollectDecVarsM.run (x : CollectDecVarsM Unit) (decVars : FVarIdSet) : FVarIdSet

Equations

• x.run decVars = match StateT.run (x decVars) { } with | (fst, s) => s.found