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

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

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.

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

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

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

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

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

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

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

@[reducible, inline]

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