def Lean.Meta.Grind.Arith.Cutsat.CooperSplit.assert (cs : CooperSplit) : GoalM Unit

Asserts constraints implied by a CooperSplit.

def Lean.Meta.Grind.Arith.Cutsat.tightUsingDvd (c : LeCnstr) (dvd? : Option DvdCnstr) : GoalM LeCnstr

def Lean.Meta.Grind.Arith.Cutsat.getBestLower? (x : Var) (dvd? : Option DvdCnstr) : GoalM (Option (Rat × LeCnstr))

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.Cutsat.getBestUpper? (x : Var) (dvd? : Option DvdCnstr) : GoalM (Option (Rat × LeCnstr))

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.Cutsat.getDiseqValues (x : Var) : SearchM (Array (Rat × DiseqCnstr))

Returns values we cannot assign x because of disequality constraints.

structure Lean.Meta.Grind.Arith.Cutsat.DvdSolution : Type

Solution space for a divisibility constraint of the form d ∣ a*x + b See DvdCnstr.getSolutions? to understand how it is computed.

• d : Int
• b : Int

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.getSolutions? (c : DvdCnstr) : SearchM (Option DvdSolution)

def Lean.Meta.Grind.Arith.Cutsat.resolveDvdConflict (c : DvdCnstr) : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.DvdSolution.ge (s : DvdSolution) (v : Int) : Int

Given a divisibility constraint solution space s := { b, d }, and a candidate assignment v, we want to find an assignment w such that w ≥ v such that exists k, w = k*d + b Thus,

• k*d + b ≥ v
• k ≥ cdiv (v - b) d So, we take w = (cdiv (v - b) d)*d + b

def Lean.Meta.Grind.Arith.Cutsat.DvdSolution.le (s : DvdSolution) (v : Int) : Int

Given a divisibility constraint solution space s := { b, d }, and a candidate assignment v, we want to find an assignment w such that w ≤ v such that exists k, w = k*d + b Thus,

• k*d + b ≤ v
• k ≤ (v - b) / d So, we take w = ((v - b) / d)*d + b

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

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

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

partial def Lean.Meta.Grind.Arith.Cutsat.DvdSolution.geAvoiding (s : DvdSolution) (v : Int) (dvals : Array (Rat × DiseqCnstr)) : Int

partial def Lean.Meta.Grind.Arith.Cutsat.DvdSolution.leAvoiding (s : DvdSolution) (v : Int) (dvals : Array (Rat × DiseqCnstr)) : Int

inductive Lean.Meta.Grind.Arith.Cutsat.FindIntValResult : Type

• found (val : Int) : FindIntValResult
• diseq (c : DiseqCnstr) : FindIntValResult
• dvd : FindIntValResult

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedFindIntValResult : Inhabited FindIntValResult

def Lean.Meta.Grind.Arith.Cutsat.findIntVal (s : DvdSolution) (lower upper : Int) (dvals : Array (Rat × DiseqCnstr)) : FindIntValResult

Tries to find an integer v s.t. lower ≤ v ≤ upper, v ∉ dvals, and v ∈ s. Returns .found v if result was found, .dvd if it failed because of the divisibility constraint, and .diseq c because of the disequality constraint c.

partial def Lean.Meta.Grind.Arith.Cutsat.findIntVal.go (s : DvdSolution) (upper : Int) (dvals : Array (Rat × DiseqCnstr)) (v : Int) : FindIntValResult

partial def Lean.Meta.Grind.Arith.Cutsat.findRatVal (lower upper : Rat) (diseqVals : Array (Rat × DiseqCnstr)) : Rat

def Lean.Meta.Grind.Arith.Cutsat.resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool

def Lean.Meta.Grind.Arith.Cutsat.resolveCooperUnary (pred : CooperSplitPred) : SearchM Bool

def Lean.Meta.Grind.Arith.Cutsat.resolveCooperPred (pred : CooperSplitPred) : SearchM Unit

def Lean.Meta.Grind.Arith.Cutsat.resolveCooper (c₁ c₂ : LeCnstr) : SearchM Unit

def Lean.Meta.Grind.Arith.Cutsat.resolveCooperDvd (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr) : SearchM Unit

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.split (c : DiseqCnstr) : SearchM LeCnstr

def Lean.Meta.Grind.Arith.Cutsat.resolveCooperDiseq (c₁ : DiseqCnstr) (c₂ : LeCnstr) (c₃? : Option DvdCnstr) : SearchM Unit

Given c₁ of the form a₁*x + p₁ ≠ 0, and c₂ of the form b*x + p ≤ 0 splits c₁ and resolve with c₂.

def Lean.Meta.Grind.Arith.Cutsat.resolveRatDiseq (c₁ : LeCnstr) (c : DiseqCnstr) : SearchM Unit

Given c₁ of the form -a₁*x + p₁ ≤ 0, and c of the form b*x + p ≠ 0, splits c and resolve with c₁.

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

def Lean.Meta.Grind.Arith.Cutsat.hasAssignment : GoalM Bool

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

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

def Lean.Meta.Grind.Arith.Cutsat.searchAssigment : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.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 already has a satisfying assignment.