max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: grind cutsat equations in solved form (#9958)

Browse source 
This PR ensures that equations in the `grind cutsat` module are
maintained in solved form. That is, given an equation `a*x + p = 0` used
to eliminate `x`, the linear polynomial `p` must not contain other
eliminated variables. Before this PR, equations were maintained in
triangular form. We are going to use the solved form to linearize
nonlinear terms.
This commit is contained in:
Leonardo de Moura 2025-08-17 18:34:37 -07:00 • committed by GitHub
parent 973885d087
commit f5bab3c8ba
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 36 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
View file

@ -45,5 +45,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.internalize
builtin_initialize registerTraceClass `grind.debug.cutsat.toInt
builtin_initialize registerTraceClass `grind.debug.cutsat.search.cnstrs
builtin_initialize registerTraceClass `grind.debug.cutsat.search.reorder
builtin_initialize registerTraceClass `grind.debug.cutsat.elimEq
end Lean

35
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
View file

@ -169,6 +169,16 @@ private def updateDiseqs (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Uni
c₂.assert
if (← inconsistent) then return ()
private def updateElimEqs (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
if (← inconsistent) then return ()
assert! x != y
let some c₂ := (← get').elimEqs[y]! | return ()
let b := c₂.p.coeff x
if b == 0 then return ()
let c₂ := { p := c₂.p.mul a |>.combine (c.p.mul (-b)), h := .subst x c₂ c : EqCnstr }
trace[grind.debug.cutsat.elimEq] "updated: {← getVar y}, {← c₂.pp}"
modify' fun s => { s with elimEqs := s.elimEqs.set y (some c₂) }
private def updateOccsAt (k : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
updateDvdCnstr k x c y
updateLowers k x c y
@ -181,6 +191,29 @@ private def updateOccs (k : Int) (x : Var) (c : EqCnstr) : GoalM Unit := do
updateOccsAt k x c x
for y in ys do
updateOccsAt k x c y
updateElimEqs k x c y
/--
Similar to `updateOccs`, but does not assume first variable is `p`s "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`.
-/
partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : GoalM Unit := do
let rec go (p : Poly) : GoalM Unit := do
let .add _ y p := p | return ()
unless x == y do addOcc y x
go p
go p
@[export lean_grind_cutsat_assert_eq]
def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
@ -205,11 +238,13 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
trace[grind.debug.cutsat.subst] ">> {← getVar x}, {← c.pp}"
trace[grind.cutsat.assert.store] "{← c.pp}"
trace[grind.debug.cutsat.elimEq] "{← getVar x}, {← c.pp}"
modify' fun s => { s with
elimEqs := s.elimEqs.set x (some c)
elimStack := x :: s.elimStack
}
updateOccs k x c
c.p.updateOccsForElimEq x
if (← inconsistent) then return ()
-- assert a divisibility constraint IF `|k| != 1`
if k.natAbs != 1 then