feat: grind -cutsat

This PR adds an option for disabling the cutsat procedure in
`grind`. The linarith module takes over linear integer/nat constraints.

Author: leodemoura

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

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

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}"

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

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

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

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