From 32eedc2c22164243f7ae140b68c4c3878b3eac07 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jun 2025 12:40:44 -0400 Subject: [PATCH] feat: `grind -cutsat` (#8774) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds an option for disabling the cutsat procedure in `grind`. The linarith module takes over linear integer/nat constraints. Example: ```lean set_option trace.grind.cutsat.assert true in -- cutsat should **not** process the following constraints example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by grind -cutsat -- `linarith` module solves it ``` --- src/Init/Grind/Tactics.lean | 4 ++++ .../Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean | 1 + .../Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 3 +++ .../Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean | 1 + .../Meta/Tactic/Grind/Arith/Linear/StructId.lean | 2 +- tests/lean/run/grind_cutsat_div_1.lean | 4 ++++ tests/lean/run/grind_linarith_1.lean | 15 +++++++++++++++ 7 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 334b7465b7..14a69f67e6 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -189,6 +189,10 @@ structure Config where `CommRing`. -/ linarith := true + /-- + When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`. + -/ + cutsat := true deriving Inhabited, BEq end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index 40d05412a8..0b9d43e440 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -112,6 +112,7 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do pushNewFact <| mkApp3 (mkConst ``Nat.emod_pos_of_not_dvd) a b (mkOfEqFalseCore e (← mkEqFalseProof e)) builtin_grind_propagator propagateDvd ↓Dvd.dvd := fun e => do + unless (← getConfig).cutsat do return () let_expr Dvd.dvd α _ _ _ ← e | return () if α.isConstOf ``Nat then propagateNatDvd e diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index 3e976e92a0..5c7c663f91 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -254,6 +254,7 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do @[export lean_process_cutsat_eq] def processNewEqImpl (a b : Expr) : GoalM Unit := do + unless (← getConfig).cutsat do return () match (← foreignTerm? a), (← foreignTerm? b) with | none, none => processNewIntEq a b | some .nat, some .nat => processNewNatEq a b @@ -281,6 +282,7 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do @[export lean_process_cutsat_diseq] def processNewDiseqImpl (a b : Expr) : GoalM Unit := do + unless (← getConfig).cutsat do return () match (← foreignTerm? a), (← foreignTermOrLit? b) with | none, none => processNewIntDiseq a b | some .nat, some .nat => processNewNatDiseq a b @@ -404,6 +406,7 @@ Internalizes an integer (and `Nat`) expression. Here are the different cases tha back to the congruence closure module. Example: we have `f 5`, `f x`, `x - y = 3`, `y = 2`. -/ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do + unless (← getConfig).cutsat do return () let some (k, type) := getKindAndType? e | return () if isForbiddenParent parent? k then return () trace[grind.debug.cutsat.internalize] "{e} : {type}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean index d577701210..e7ee316181 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean @@ -162,6 +162,7 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do c.assert def propagateIfSupportedLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do + unless (← getConfig).cutsat do return () let_expr LE.le α _ _ _ := e | return () if α.isConstOf ``Nat then propagateNatLe e eqTrue diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index a8dad2baf9..5bbb60adf9 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -39,7 +39,7 @@ private def ensureDefEq (a b : Expr) : MetaM Unit := do throwError (← mkExpectedDefEqMsg a b) def getStructId? (type : Expr) : GoalM (Option Nat) := do - if Cutsat.isSupportedType type then + if (← getConfig).cutsat && Cutsat.isSupportedType type then -- If `type` is supported by cutsat, let it handle return none if let some id? := (← get').typeIdOf.find? { expr := type } then diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean index b2fb90f76c..5cad76a446 100644 --- a/tests/lean/run/grind_cutsat_div_1.lean +++ b/tests/lean/run/grind_cutsat_div_1.lean @@ -79,3 +79,7 @@ example (x : Int) (_ : 10 ∣ x) (_ : ¬ 5 ∣ x) : False := by example (x : Nat) (_ : 10 ∣ x) (_ : ¬ 5 ∣ x) : False := by grind + +example (a b : Int) (h₀ : 2 ∣ a + 1) (h₁ : 2 ∣ b + a) (h₂ : 2 ∣ b + 2*a) : False := by + fail_if_success grind -cutsat + sorry diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean index ab8b0fa133..0457e5461a 100644 --- a/tests/lean/run/grind_linarith_1.lean +++ b/tests/lean/run/grind_linarith_1.lean @@ -148,3 +148,18 @@ set_option trace.grind.linarith.internalize true example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α) : a < b + c + d → c = b → a < b + b + d := by grind + +/-- +trace: [grind.linarith.assert] -3 * y + 2 * x + One.one ≤ 0 +[grind.linarith.assert] 2 * z + -4 * x + One.one ≤ 0 +[grind.linarith.assert] -1 * z + 3 * y + One.one ≤ 0 +[grind.linarith.assert] 6 * y + -4 * x + 3 * One.one ≤ 0 +[grind.linarith.assert] 15 * One.one ≤ 0 +[grind.linarith.assert] Zero.zero < 0 +-/ +#guard_msgs (trace) in +set_option trace.grind.cutsat.assert true in -- cutsat should **not** process the following constraints +set_option trace.grind.linarith.assert true in -- linarith should take over +set_option trace.grind.linarith.assert.store false in +example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12*y - 4* z < 0 := by + grind -cutsat