def Lean.Meta.Grind.Arith.Linear.IneqCnstr.throwUnexpected {α : Type} (c : IneqCnstr) : LinearM α

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.throwUnexpected {α : Type} (c : DiseqCnstr) : LinearM α

def Lean.Meta.Grind.Arith.Linear.getBestLower? (x : Var) : LinearM (Option (Rat × IneqCnstr))

Assuming all variables smaller than x have already been assigned, returns the best lower bound for x using the given partial assignment and inequality constraints where x is the maximal variable.

def Lean.Meta.Grind.Arith.Linear.getBestUpper? (x : Var) : LinearM (Option (Rat × IneqCnstr))

Assuming all variables smaller than x have already been assigned, returns the best upper bound for x using the given partial assignment and inequality constraints where x is the maximal variable.

def Lean.Meta.Grind.Arith.Linear.getDiseqValues (x : Var) : LinearM (Array (Rat × DiseqCnstr))

Returns values we cannot assign x because of disequality constraints.

def Lean.Meta.Grind.Arith.Linear.findDiseq? (v : Rat) (dvals : Array (Rat × DiseqCnstr)) : Option DiseqCnstr

def Lean.Meta.Grind.Arith.Linear.inDiseqValues (v : Rat) (dvals : Array (Rat × DiseqCnstr)) : Bool

partial def Lean.Meta.Grind.Arith.Linear.geAvoiding (v : Rat) (dvals : Array (Rat × DiseqCnstr)) : Rat

partial def Lean.Meta.Grind.Arith.Linear.leAvoiding (v : Rat) (dvals : Array (Rat × DiseqCnstr)) : Rat

def Lean.Meta.Grind.Arith.Linear.resolveLowerUpperConflict (c₁ c₂ : IneqCnstr) : LinearM Unit

def Lean.Meta.Grind.Arith.Linear.findInt? (lower : Rat) (lowerStrict : Bool) (upper : Rat) (upperStrict : Bool) (dvals : Array (Rat × DiseqCnstr)) : Option Rat

Try to find integer between lower and upper bounds that is different for known disequalities

partial def Lean.Meta.Grind.Arith.Linear.findInt?.go (dvals : Array (Rat × DiseqCnstr)) (v stop : Int) : Option Rat

partial def Lean.Meta.Grind.Arith.Linear.findRat (lower upper : Rat) (dvals : Array (Rat × DiseqCnstr)) : Rat

Find rational value in the interval (lower, upper) that is different from all known disequalities.

def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.split (c : DiseqCnstr) : SearchM IneqCnstr

def Lean.Meta.Grind.Arith.Linear.resolveLowerDiseqConflict (c₁ : IneqCnstr) (c : DiseqCnstr) : SearchM Unit

Given an inequality c₁ which is a lower bound, i.e., leading coefficient is negative, and a disequality c, splits c and resolve with c₁.

def Lean.Meta.Grind.Arith.Linear.processVar (x : Var) : SearchM Unit

def Lean.Meta.Grind.Arith.Linear.hasAssignment : LinearM Bool

Returns true if we already have a complete assignment / model.

def Lean.Meta.Grind.Arith.Linear.resolveConflict (h : UnsatProof) : SearchM Unit

def Lean.Meta.Grind.Arith.Linear.check : GoalM Bool

Returns true if work/progress has been done. There are two kinds of progress:

• An assignment for satisfying constraints was constructed.
• An inconsistency was detected.

The result is false if module for every structure already has an assignment.