def Lean.Meta.Grind.Arith.Linear.toContextExpr : LinearM Expr

Returns a context of type RArray α containing the variables of the given structure, where α is (← getStruct).type.

def Lean.Meta.Grind.Arith.Linear.toRingContextExpr : LinearM Expr

Similar to toContextExpr, but for the CommRing module. Recall that this module interfaces with the CommRing module and their variable contexts may not be necessarily identical. For example, for this module, the term x*y does not have an interpretation and we have a "variable" representing it, but it is interpreted in the CommRing module, and such variable does not exist there. On the other direction, suppose we have the inequality z < 0, and z does not occur in any equality or disequality. Then, the CommRing does not even "see" z, and z does not occur in its context, but it occurs in the variable context created by this module.

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

• cache : Std.HashMap UInt64 Expr
• polyMap : Std.HashMap Poly Expr
• exprMap : Std.HashMap LinExpr Expr
• ringPolyMap : Std.HashMap CommRing.Poly Expr
• ringExprMap : Std.HashMap CommRing.RingExpr Expr

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

• ctx : Expr
• ringCtx : Expr

@[reducible, inline]

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

Auxiliary monad for constructing linarith proofs.

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

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

def Lean.Meta.Grind.Arith.Linear.mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr

def Lean.Meta.Grind.Arith.Linear.mkRingExprDecl (e : CommRing.RingExpr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr

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

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

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

def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProof (h : UnsatProof) : LinearM Expr

def Lean.Meta.Grind.Arith.Linear.setInconsistent (h : UnsatProof) : LinearM Unit

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

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit

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

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

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