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
• 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.

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)

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.

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