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
• ringPolyMap : Std.HashMap CommRing.Poly Expr
• ringExprMap : Std.HashMap CommRing.RingExpr Expr

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

• ctx : Expr
• ctx' : Expr

  Variables before reordering

• natCtx : Expr
• ringCtx : Expr
• unordered : Bool

  unordered is true if we entered a .reorder c justification. The variables in c and its dependencies are unordered.

@[reducible, inline]

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

Auxiliary monad for constructing cutsat proofs.

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.

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