feat: add the liaSteps configuration option to grind (#14392)

This PR adds a new `liaSteps` configuration option to `grind`. The
motivation is to quickly interrupt the search for hard linear integer
arithmetic problems.

Author: leodemoura

src/Init/Grind/Config.lean

@@ -134,6 +134,15 @@ structure Config where
   -/
   lia := true
   /--
+  Maximum number of steps performed by the `lia` solver while searching for an assignment
+  satisfying the linear integer arithmetic constraints.
+  A step is counted for each variable processed during the search. This threshold prevents
+  case-split explosion in examples that require enumerating a huge number of cases
+  (e.g., Cooper conflict resolution with large coefficients).
+  When the threshold is reached, the search is interrupted, and the solver becomes incomplete.
+  -/
+  liaSteps : Nat := 10000
+  /--
   When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
   -/
   ac := true

src/Init/Grind/Tactics.lean

@@ -175,6 +175,7 @@ This *model-based* search is **complete for LIA**.
 
 * `grind -lia` disable the solver (useful for debugging)
 * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ)
+* `grind (liaSteps := n)` cap the number of steps performed by the model search (the solver becomes incomplete when the threshold is reached)
 
 #### Examples:
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean

@@ -512,6 +512,12 @@ private def searchAssignmentMain : SearchM Unit := do
       return ()
     if let some c := (← get').conflict? then
       resolveConflict c
+    else if (← checkMaxSteps) then
+      -- Interrupt the search. Remark: we do not interrupt while a conflict is unresolved
+      -- because the cutsat state would be left with a pending `conflict?`.
+      trace[grind.debug.lia.search] "search interrupted, maximum number of steps reached"
+      setImprecise
+      return ()
     else
       let x : Var := (← get').assignment.size
       trace[grind.debug.lia.search] "next var: {← getVar x}, {x}, {(← get').assignment.toList}"
@@ -530,6 +536,7 @@ private def searchQLiaAssignment : GoalM Bool := do
     searchAssignmentMain
     let precise := (← get).precise
     resetDecisionStack
+    saveSteps
     return precise
   go .rat |>.run' {}
 
@@ -551,6 +558,7 @@ private def searchLiaAssignment : GoalM Unit := do
   let go : SearchM Unit := do
     searchAssignmentMain
     resetDecisionStack
+    saveSteps
   traceActiveCnstrs
   reorderVars
   traceActiveCnstrs
@@ -566,6 +574,8 @@ def searchAssignment : GoalM Unit := do
     searchLiaAssignment
     trace[grind.debug.lia.search] "after search int model, inconsistent: {← isInconsistent}"
     if (← isInconsistent) then return ()
+  -- If the search was interrupted (`liaSteps` threshold), the assignment is partial.
+  unless (← hasAssignment) do return ()
   -- TODO: constructing a model is only worth if `grind` will **not** continue searching.
   assignElimVars
 
@@ -580,6 +590,10 @@ The result is `false` if module already has a satisfying assignment.
 def check : GoalM Bool := do profileitM Exception "grind cutsat" (← getOptions) do
   if (← hasAssignment) then
     return false
+  else if (← get').steps ≥ (← getConfig).liaSteps then
+    -- A previous search reached the `liaSteps` threshold. The solver is disabled to
+    -- ensure `grind` does not keep restarting the (bounded) search at every iteration.
+    return false
   else
     searchAssignment
     return true

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean

@@ -57,6 +57,12 @@ structure Search.State where
   precise : Bool := true
   /-- Set of decision variables in `cases`. -/
   decVars : FVarIdSet := {}
+  /--
+  Number of steps performed by the current search.
+  Remark: we cannot use the `steps` counter in the cutsat state because it is rolled
+  back when backtracking case splits.
+  -/
+  steps : Nat := 0
 
 abbrev SearchM := ReaderT Search.Kind (StateRefT Search.State GoalM)
 
@@ -68,6 +74,23 @@ def isApprox : SearchM Bool :=
 def setImprecise : SearchM Unit := do
   modify fun s => { s with precise := false }
 
+/--
+Increments the search steps counter, and returns `true` if the cumulative number of
+steps reached the `liaSteps` configuration threshold.
+-/
+def checkMaxSteps : SearchM Bool := do
+  modify fun s => { s with steps := s.steps + 1 }
+  return (← get').steps + (← get).steps > (← getConfig).liaSteps
+
+/--
+Adds the number of steps performed by the current search to the cumulative counter
+in the cutsat state. It must be invoked after `resetDecisionStack` because backtracking
+rolls back the cutsat state.
+-/
+def saveSteps : SearchM Unit := do
+  let steps := (← get).steps
+  modify' fun s => { s with steps := s.steps + steps }
+
 def mkCase (kind : CaseKind) : SearchM FVarId := do
   let fvarId ← mkFreshFVarId
   let saved ← get'

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -319,6 +319,12 @@ structure State where
   -/
   caseSplits : Bool := false
   /--
+  Cumulative number of steps performed by the model search.
+  The model search is interrupted when this counter reaches the `liaSteps`
+  configuration threshold, and the solver becomes incomplete.
+  -/
+  steps : Nat := 0
+  /--
   `conflict?` is `some ..` if a contradictory constraint was derived.
   This field is only set when `caseSplits` is `true`. Otherwise, we
   can convert `UnsatProof` into a Lean term and close the current `grind` goal.

src/Lean/Meta/Tactic/Grind/PP.lean

@@ -200,6 +200,9 @@ def Arith.Cutsat.pp? (goal : Goal) : MetaM (Option MessageData) := do
   let s ← Arith.Cutsat.cutsatExt.getStateCore goal
   let nodes := s.varMap
   if nodes.isEmpty then return none
+  -- The assignment is partial (and does not satisfy the constraints) if the search
+  -- was interrupted because the `liaSteps` threshold was reached.
+  if s.assignment.size < s.vars.size then return none
   let model ← Arith.Cutsat.mkModel goal
   if model.isEmpty then return none
   let mut ms := #[]
@@ -240,6 +243,9 @@ private def ppThresholds (c : Grind.Config) : M Unit := do
   if maxGen ≥ c.gen then
     msgs := msgs.push <| .trace { cls := `limit } m!"maximum term generation has been reached, threshold: `(gen := {c.gen})`" #[]
   msgs ← Arith.CommRing.addThresholdMessage goal c msgs
+  let cutsat ← Arith.Cutsat.cutsatExt.getStateCore goal
+  if cutsat.steps ≥ c.liaSteps then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of steps performed by the `lia` solver has been reached, threshold: `(liaSteps := {c.liaSteps})`" #[]
   unless msgs.isEmpty do
     pushMsg <| .trace { cls := `limits } "Thresholds reached" msgs
 

tests/elab/grind_cutsat_lia_steps.lean

@@ -0,0 +1,59 @@
+module
+set_option warn.sorry false
+
+/-!
+Tests the `liaSteps` threshold that interrupts the cutsat model search.
+
+The "tight rhombus" example below requires enumerating thousands of cases during
+Cooper conflict resolution. Without the threshold, `grind` used to spend a long time
+searching and then produce a proof term so large that the kernel failed with a
+deep-recursion error. With the default configuration, `grind` must fail quickly.
+-/
+
+example (x : Int) (y : Int)
+    (h0 : ((0 <= ((27300 * x) - (24501 * y))) ∧ (((27300 * x) - (24501 * y)) <= 99) ∧
+           (1 <= ((27301 * x) - (24500 * y))) ∧ (((27301 * x) - (24500 * y)) <= 100))) : False := by
+  fail_if_success grind
+  sorry
+
+/-!
+Checks that the `liaSteps` configuration option is wired: this example is solvable with
+the default budget, but not with `liaSteps := 1`.
+-/
+
+example (x y : Int) :
+    27 ≤ 11*x + 13*y →
+    11*x + 13*y ≤ 45 →
+    -10 ≤ 7*x - 9*y →
+    7*x - 9*y ≤ 4 → False := by
+  fail_if_success grind (liaSteps := 1)
+  grind
+
+
+/--
+error: `grind` failed
+case grind
+x y : Int
+h0 : 0 ≤ 27300 * x - 24501 * y ∧ 27300 * x - 24501 * y ≤ 99 ∧ 1 ≤ 27301 * x - 24500 * y ∧ 27301 * x - 24500 * y ≤ 100
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] -9100 * x + 8167 * y ≤ 0 ∧
+          9100 * x + -8167 * y + -33 ≤ 0 ∧ -27301 * x + 24500 * y + 1 ≤ 0 ∧ 27301 * x + -24500 * y + -100 ≤ 0
+  [eqc] True propositions
+    [prop] -27301 * x + 24500 * y + 1 ≤ 0 ∧ 27301 * x + -24500 * y + -100 ≤ 0
+    [prop] 9100 * x + -8167 * y + -33 ≤ 0 ∧ -27301 * x + 24500 * y + 1 ≤ 0 ∧ 27301 * x + -24500 * y + -100 ≤ 0
+    [prop] -9100 * x + 8167 * y ≤ 0 ∧
+          9100 * x + -8167 * y + -33 ≤ 0 ∧ -27301 * x + 24500 * y + 1 ≤ 0 ∧ 27301 * x + -24500 * y + -100 ≤ 0
+    [prop] -27301 * x + 24500 * y + 1 ≤ 0
+    [prop] 9100 * x + -8167 * y + -33 ≤ 0
+    [prop] 27301 * x + -24500 * y + -100 ≤ 0
+    [prop] -9100 * x + 8167 * y ≤ 0
+  [limits] Thresholds reached
+    [limit] maximum number of steps performed by the `lia` solver has been reached, threshold: `(liaSteps := 1)`
+-/
+#guard_msgs in
+example (x : Int) (y : Int)
+    (h0 : ((0 <= ((27300 * x) - (24501 * y))) ∧ (((27300 * x) - (24501 * y)) <= 99) ∧
+           (1 <= ((27301 * x) - (24500 * y))) ∧ (((27301 * x) - (24500 * y)) <= 100))) : False := by
+  grind (liaSteps := 1)