def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.norm (c : EqCnstr) : EqCnstr

Equations

• c.norm = if c.p.isSorted = true then c else { p := c.p.norm, h := Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c }

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.norm (c : DiseqCnstr) : DiseqCnstr

Equations

• c.norm = if c.p.isSorted = true then c else { p := c.p.norm, h := Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c }

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DiseqCnstr) : GoalM DiseqCnstr

Given an equation c₁ containing the monomial a*x, and a disequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.applySubsts (c : DiseqCnstr) : GoalM DiseqCnstr

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit

Equations

• One or more equations did not get rendered due to their size.

def Int.Linear.Poly.pickVarToElim? (p : Poly) : Option (Int × Var)

Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.

Equations

• (Int.Linear.Poly.num k).pickVarToElim? = none
• (Int.Linear.Poly.add k' x' p_2).pickVarToElim? = some (Int.Linear.Poly.pickVarToElim?.go✝ k' x' p_2)

partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.applySubsts (c : EqCnstr) : GoalM EqCnstr

structure Lean.Meta.Grind.Arith.Cutsat.PropagateMul.State : Type

• a? : Option Expr
• k : Int
• cs : Array (Expr × Int × EqCnstr)
• n : Nat

@[export lean_cutsat_propagate_nonlinear]

def Lean.Meta.Grind.Arith.Cutsat.propagateNonlinearTermImpl (y x : Var) : GoalM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.propagateNonlinearTerms (y : Var) : GoalM Unit

Equations

• One or more equations did not get rendered due to their size.

def Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Lean.Meta.Grind.GoalM Unit

Similar to updateOccs, but does not assume first variable is ps "owner". Recall that when eliminating equalities we do not necessarily eliminate the maximal variable, but the one with unit coefficient. Remark: we keep occurrences for equations in elimEqs because we want to maintain them in solved form. Consider the following scenario: 1- Asserted a + 2*b + 1 = 0, and eliminated a 2- Asserted b + 1 = 0, and eliminated b.

At step 2, we want to substitute b at a + 2*b + 1 to ensure cutsat knows a is forced to be equal to a constant value. This is relevant for linearizing nonlinear terms.

Remark: x is the variable that was eliminated using p.

Equations

• p.updateOccsForElimEq x = Int.Linear.Poly.updateOccsForElimEq.go✝ x p

@[export lean_grind_cutsat_assert_eq]

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.processNewDiseq (a b : Expr) : GoalM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit

Internalizes an integer (and Nat) expression. Here are the different cases that are handled.

• a + b when parent? is not +, ≤, or ∣
• k * a when k is a numeral and parent? is not +, *, ≤, ∣
• numerals when parent? is not +, *, ≤, ∣. Recall that we must internalize numerals to make sure we can propagate equalities back to the congruence closure module. Example: we have f 5, f x, x - y = 3, y = 2.

Equations

• One or more equations did not get rendered due to their size.