refactor: grind cutsat as solver extension (#10312)

This PR uses the new solver extension framework to implement `grind
cutsat`. All satellite solvers have been migrated to the new framework.

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

@@ -4,16 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Util
 public import Lean.Meta.Tactic.Grind.Arith.Types
 public import Lean.Meta.Tactic.Grind.Arith.Main
 public import Lean.Meta.Tactic.Grind.Arith.Offset
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat
 public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat
 public import Lean.Meta.Tactic.Grind.Arith.Simproc
-public import Lean.Meta.Tactic.Grind.Arith.Internalize
-
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv

src/Lean/Meta/Tactic/Grind/Arith/CommRing/GetSet.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Types
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-
-builtin_initialize ringExt : SolverExtension State ← registerSolverExtension (return {})
-
-def get' : GoalM State := do
-  ringExt.getState
-
-@[inline] def modify' (f : State → State) : GoalM Unit := do
-  ringExt.modifyState f
-
-end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -7,7 +7,6 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
-import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -11,7 +11,6 @@ import Init.Grind.Ring.Envelope
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Arith.Insts
-import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -5,10 +5,9 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -5,10 +5,9 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
 import Init.Grind.Ring.OfSemiring
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions

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

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Grind.Ring.OfSemiring
-public import Lean.Meta.Tactic.Grind.ExprPtr
-public import Lean.Meta.Tactic.Grind.Arith.Util
+public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 import Lean.Data.PersistentArray
 public section
@@ -279,4 +278,12 @@ structure State where
   steps := 0
   deriving Inhabited
 
+builtin_initialize ringExt : SolverExtension State ← registerSolverExtension (return {})
+
+def get' : GoalM State := do
+  ringExt.getState
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  ringExt.modifyState f
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Util.Trace
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
@@ -22,11 +21,8 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
-
 public section
-
-namespace Lean
-
+namespace Lean.Meta.Grind.Arith.Cutsat
 builtin_initialize registerTraceClass `grind.cutsat
 builtin_initialize registerTraceClass `grind.cutsat.nonlinear
 builtin_initialize registerTraceClass `grind.cutsat.model
@@ -48,4 +44,13 @@ 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
+builtin_initialize
+  cutsatExt.setMethods
+    (internalize := Cutsat.internalize)
+    (newEq       := Cutsat.processNewEq)
+    (newDiseq    := Cutsat.processNewDiseq)
+    (check       := Cutsat.check)
+    (checkInv    := Cutsat.checkInvariants)
+    (mbtc        := Cutsat.mbtc)
+
+end Lean.Meta.Grind.Arith.Cutsat

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Simp

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.PropagatorAttr

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Init.Data.Int.OfNat
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
@@ -428,8 +428,7 @@ private def processNewToIntEq (a b : Expr) : ToIntM Unit := do
   let c := { p, h := .coreToInt a b thm lhs rhs : EqCnstr }
   c.assertCore
 
-@[export lean_process_cutsat_eq]
-def processNewEqImpl (a b : Expr) : GoalM Unit := do
+def processNewEq (a b : Expr) : GoalM Unit := do
   unless (← getConfig).cutsat do return ()
   if (← isNatTerm a <&&> isNatTerm b) then
     processNewNatEq a b
@@ -484,8 +483,7 @@ private def processNewToIntDiseq (a b : Expr) : ToIntM Unit := do
   let c := { p, h := .coreToInt a b thm lhs rhs : DiseqCnstr }
   c.assertCore
 
-@[export lean_process_cutsat_diseq]
-def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
+def processNewDiseq (a b : Expr) : GoalM Unit := do
   unless (← getConfig).cutsat do return ()
   if (← isNatTerm a <&&> isNatTerm b) then
     processNewNatDiseq a b
@@ -659,7 +657,7 @@ private def internalizeNatTerm (e type : Expr) (parent? : Option Expr) (k : Supp
   modify' fun s => { s with
     natToIntMap := s.natToIntMap.insert { expr := e } e'h
   }
-  markAsCutsatTerm e
+  cutsatExt.markTerm e
   /-
   If `e'.h` is of the form `NatCast.natCast e`, then it is wasteful to
   assert an equality
@@ -690,7 +688,7 @@ private def internalizeToIntTerm (e type : Expr) : GoalM Unit := do
     modify' fun s => { s with
       toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α }
     }
-    markAsCutsatTerm e
+    cutsatExt.markTerm e
 
 /--
 Internalizes an integer (and `Nat`) expression. Here are the different cases that are handled.

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 public section

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Init.Grind.ToInt
 import Lean.Meta.Tactic.Grind.Arith.ModelUtil
 public section
@@ -18,12 +18,13 @@ private def isIntNatENode (n : ENode) : MetaM Bool :=
     <||>
     isDefEq type Nat.mkType
 
-private def getCutsatAssignment? (goal : Goal) (node : ENode) : Option Rat := Id.run do
+private def getCutsatAssignment? (goal : Goal) (node : ENode) : IO (Option Rat) := do
   assert! isSameExpr node.self node.root
-  let some e := node.cutsat? | return none
-  let some x := goal.arith.cutsat.varMap.find? { expr := e } | return none
-  if h : x < goal.arith.cutsat.assignment.size then
-    return goal.arith.cutsat.assignment[x]
+  let some e := cutsatExt.getTerm node | return none
+  let s ← cutsatExt.getStateCore goal
+  let some x := s.varMap.find? { expr := e } | return none
+  if h : x < s.assignment.size then
+    return s.assignment[x]
   else
     return none
 
@@ -37,7 +38,7 @@ private def natCastToInt? (e : Expr) : Option Expr :=
 
 def getAssignment? (goal : Goal) (e : Expr) : MetaM (Option Rat) := do
   let node ← goal.getENode (← goal.getRoot e)
-  if let some v := getCutsatAssignment? goal node then
+  if let some v ← getCutsatAssignment? goal node then
     return some v
   else if let some v ← getIntValue? node.self then
     return some v

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Init.Data.Int.OfNat
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Simp.Arith.Nat.Basic
@@ -25,7 +25,7 @@ def mkNatVar (e : Expr) : GoalM (Expr × Expr) := do
   modify' fun s => { s with
     natToIntMap := s.natToIntMap.insert { expr := e } r
   }
-  markAsCutsatTerm e
+  cutsatExt.markTerm e
   return r
 
 private def intIte : Expr := mkApp (mkConst ``ite [1]) Int.mkType

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

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Grind.Ring.Poly
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Init.Data.Int.OfNat
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
@@ -21,9 +21,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public section
-
 namespace Lean.Meta.Grind.Arith.Cutsat
-
 deriving instance Hashable for Int.Linear.Expr
 
 /--

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Init.Grind.ToIntLemmas
 import Lean.Meta.Tactic.Grind.SynthInstance
@@ -299,7 +299,7 @@ def mkToIntVar (e : Expr) : ToIntM (Expr × Expr) := do
   modify' fun s => { s with
     toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α }
   }
-  markAsCutsatTerm e
+  cutsatExt.markTerm e
   return (eToInt, he)
 
 def getToIntTermType? (e : Expr) : GoalM (Option Expr) := do

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

@@ -6,8 +6,9 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Data.Int.Linear
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
+public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
 import Lean.Data.PersistentArray
 import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
@@ -364,4 +365,6 @@ structure State where
   nonlinearOccs : PHashMap Var (List Var) := {}
   deriving Inhabited
 
+builtin_initialize cutsatExt : SolverExtension State ← registerSolverExtension (return {})
+
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Simp.Arith.Int.Simp
 public section
@@ -32,10 +32,10 @@ end Int.Linear
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 def get' : GoalM State := do
-  return (← get).arith.cutsat
+  cutsatExt.getState
 
 @[inline] def modify' (f : State → State) : GoalM Unit := do
-  modify fun s => { s with arith.cutsat := f s.arith.cutsat }
+  cutsatExt.modifyState f
 
 /-- Returns `true` if the cutsat state is inconsistent. -/
 def inconsistent : GoalM Bool := do

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.IntInstTesters
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
@@ -76,7 +76,7 @@ def mkVarImpl (expr : Expr) : GoalM Var := do
     occurs    := s.occurs.push {}
     elimEqs   := s.elimEqs.push none
   }
-  markAsCutsatTerm expr
+  cutsatExt.markTerm expr
   assertNatCast expr var
   assertNonneg expr var
   assertToIntBounds expr var

src/Lean/Meta/Tactic/Grind/Arith/Insts.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.EvalNum
 public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Init.Grind.Ring
 public section
-
 namespace Lean.Meta.Grind.Arith
 
 def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Option (Expr × Nat)) := do withNewMCtxDepth do

src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
-import Lean.Meta.Tactic.Grind.Arith.Linear.Internalize
-public section
-namespace Lean.Meta.Grind.Arith
-
-@[export lean_grind_arith_internalize]
-def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
-  Cutsat.internalize e parent?
-
-end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Inv.lean

@@ -1,17 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv
-
-public section
-
-namespace Lean.Meta.Grind.Arith
-
-def checkInvariants : GoalM Unit := do
-  Cutsat.checkInvariants
-
-end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr

src/Lean/Meta/Tactic/Grind/Arith/Linear/Internalize.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
 public import Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var

src/Lean/Meta/Tactic/Grind/Arith/Linear/MBTC.lean

@@ -36,7 +36,7 @@ private def getAssignmentExt? (s : Struct) (a : Expr) : Option Rat := do
     toRatValue? a
 
 private def hasTheoryVar (e : Expr) : GoalM Bool := do
-  return (← linearExt.hasTerm e) || (toRatValue? e).isSome
+  return (← linearExt.hasTermAtRoot e) || (toRatValue? e).isSome
 
 private def isInterpreted (e : Expr) : GoalM Bool := do
   if isInterpretedTerm e then return true

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 import Lean.Meta.Tactic.Grind.Arith.Linear.Model
+import Lean.Meta.Tactic.Grind.Arith.Util
 public section
 namespace Lean.Meta.Grind.Arith.Linear
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -6,9 +6,9 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+public import Lean.Meta.Tactic.Grind.Arith.Util
 import Init.Grind.Module.OfNatModule
 import Lean.Data.RArray
-import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
 import Lean.Meta.Tactic.Grind.VarRename

src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Init.Data.Int.Gcd
 public section
 namespace Lean.Meta.Grind.Arith.Linear
 

src/Lean/Meta/Tactic/Grind/Arith/Main.lean

@@ -48,12 +48,4 @@ builtin_grind_propagator propagateLT ↓LT.lt := fun e => do
     Linear.propagateIneq e (eqTrue := false)
     Cutsat.propagateLt e (eqTrue := false)
 
-def check : GoalM Bool := do
-  let c₁ ← Cutsat.check
-  if c₁ then
-    processNewFacts
-    return true
-  else
-    return false
-
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/ModelUtil.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Data.Rat.Basic
+import Lean.Meta.Tactic.Grind.Arith.Util
 import Init.Grind.Module.Envelope
 public section
 

src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean

@@ -4,15 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Basic
 public import Init.Simproc
 public import Lean.Meta.Tactic.Simp.Simproc
 public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Init.Grind.Ring.Field
 public section
-
 namespace Lean.Meta.Grind.Arith
 
 private def mkSemiringThm (declName : Name) (α : Expr) : MetaM (Option Expr) := do

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

@@ -5,13 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+public import Init.Core
 public section
 namespace Lean.Meta.Grind.Arith
 
 /-- State for the arithmetic procedures. -/
 structure State where
-  cutsat : Cutsat.State := {}
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -4,16 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Basic
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.Basic
 public import Init.Data.Rat.Basic
-
 public section
-
 namespace Lean.Meta.Grind.Arith
+/-- Returns `true` if `e` is a numeral and has type `Nat`. -/
+def isNatNum (e : Expr) : Bool := Id.run do
+  let_expr OfNat.ofNat _ _ inst := e | false
+  let_expr instOfNatNat _ := inst | false
+  true
+
+/-- Returns `true` if `e` is a nonnegative numeral and has type `Int`. -/
+def isNonnegIntNum (e : Expr) : Bool := Id.run do
+  let_expr OfNat.ofNat _ _ inst := e | false
+  let_expr instOfNat _ := inst | false
+  true
+
+/-- Returns `true` if `e` is a numeral and has type `Int`. -/
+def isIntNum (e : Expr) : Bool :=
+  match_expr e with
+  | Neg.neg _ inst e => Id.run do
+    let_expr Int.instNegInt := inst | false
+    isNonnegIntNum e
+  | _ => isNonnegIntNum e
+
+/-- Returns `true` if `e` is a numeral supported by cutsat. -/
+def isNum (e : Expr) : Bool :=
+  isNatNum e || isIntNum e
 
 /-- Returns `true` if `e` is of the form `Nat` -/
 def isNatType (e : Expr) : Bool :=

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

@@ -1,17 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.Main
-namespace Lean.Meta.Grind
-/--
-Checks whether satellite solvers can make progress (e.g., detect unsatisfiability, propagate equations, etc)
--/
-public def check : GoalM Bool := do
-  Arith.check
-
-namespace Lean.Meta.Grind

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

@@ -99,52 +99,6 @@ private partial def updateMT (root : Expr) : GoalM Unit := do
       setENode parent { node with mt := gmt }
       updateMT parent
 
-/--
-Equalities or disequalities to be propagated to a theory solver **after**
-two equivalence classes have been merged.
-
-Some solvers (e.g. `cutsat`) require the core data structures to satisfy
-their invariants.  During the merge operations some of these invariants do not hold.
-Thus, we first *record* the facts that must be propagated in a `PendingTheoryPropagation` value,
-complete the merge, and only then perform the propagation.
-
-We now use this workflow for *all* theory solvers, even when a particular
-solver does not rely on these invariants.  This keeps the core
-solver-agnostic and lets us modify solvers without further adjustments.
--/
-inductive PendingTheoryPropagation where
-  | /-- Nothing to propagate. -/
-    none
-  | /-- Propagate the equality `lhs = rhs`. -/
-    eq (lhs rhs : Expr)
-  | /-- Propagate the disequalities in `ps`. -/
-    diseqs (ps : ParentSet)
-
-/--
-Helper function for combining `ENode.cutsat?` fields and detecting what needs
-to be propagated to the cutsat module.
--/
-private def checkCutsatEq (rhsRoot lhsRoot : ENode) : GoalM PendingTheoryPropagation := do
-  match lhsRoot.cutsat? with
-  | some lhsCutsat =>
-    if let some rhsCutsat := rhsRoot.cutsat? then
-      return .eq lhsCutsat rhsCutsat
-    else
-      -- We have to retrieve the node because other fields have been updated
-      let rhsRoot ← getENode rhsRoot.self
-      setENode rhsRoot.self { rhsRoot with cutsat? := lhsCutsat }
-      return .diseqs (← getParents rhsRoot.self)
-  | none =>
-    if rhsRoot.cutsat?.isSome then
-      return .diseqs (← getParents lhsRoot.self)
-    else
-      return .none
-
-def propagateCutsat : PendingTheoryPropagation → GoalM Unit
-  | .eq lhs rhs => Arith.Cutsat.processNewEq lhs rhs
-  | .diseqs ps => propagateCutsatDiseqs ps
-  | .none => return ()
-
 /--
 Tries to apply beta-reduction using the parent applications of the functions in `fns` with
 the lambda expressions in `lams`.
@@ -275,7 +229,6 @@ where
     }
     propagateBeta lams₁ fns₁
     propagateBeta lams₂ fns₂
-    let cutsatTodo ← checkCutsatEq rhsRoot lhsRoot
     let todo ← Solvers.mergeTerms rhsRoot lhsRoot
     resetParentsOf lhsRoot.self
     copyParentsTo parents rhsNode.root
@@ -287,7 +240,6 @@ where
       for e in toPropagateDown do
         propagateDown e
       propagateUnitConstFuns lams₁ lams₂
-      propagateCutsat cutsatTodo
       todo.propagate
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
     let isFalseRoot ← isFalseExpr rootNew

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

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Grind.Util
 public import Init.Grind.Lemmas
-public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
@@ -21,9 +21,6 @@ import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 public section
 namespace Lean.Meta.Grind
 
-@[extern "lean_grind_arith_internalize"] -- forward definition
-opaque Arith.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
-
 /-- Adds `e` to congruence table. -/
 def addCongrTable (e : Expr) : GoalM Unit := do
   if let some { e := e' } := (← get).congrTable.find? { e } then
@@ -362,9 +359,6 @@ private def tryEta (e : Expr) (generation : Nat) : GoalM Unit := do
     internalize e' generation
     pushEq e e' (← mkEqRefl e)
 
-private def internalizeTheories (e : Expr) (parent? : Option Expr := none) : GoalM Unit := do
-  Arith.internalize e parent?
-
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then
@@ -377,7 +371,6 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
     Later, if we try to internalize `f 1`, the arithmetic module must create a node for `1`.
     Otherwise, it will not be able to propagate that `a + 1 = 1` when `a = 0`
     -/
-    internalizeTheories e parent?
     Solvers.internalize e parent?
   else
     go
@@ -427,7 +420,6 @@ where
       if (← isLitValue e) then
         -- We do not want to internalize the components of a literal value.
         mkENode e generation
-        internalizeTheories e parent?
         Solvers.internalize e parent?
       else if e.isAppOfArity ``Grind.MatchCond 1 then
         internalizeMatchCond e generation
@@ -465,7 +457,6 @@ where
             internalize arg generation e
             registerParent e arg
         addCongrTable e
-        internalizeTheories e parent?
         Solvers.internalize e parent?
         propagateUp e
         propagateBetaForNewApp e

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

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.MatchCond
-import Lean.Meta.Tactic.Grind.Arith.Inv
 namespace Lean.Meta.Grind
 /-!
 Debugging support code for checking basic invariants.
@@ -124,7 +123,6 @@ public def checkInvariants (expensive := false) : GoalM Unit := do
         checkEqc node
     if expensive then
       checkPtrEqImpliesStructEq
-    Arith.checkInvariants
     Solvers.checkInvariants
   if expensive && grind.debug.proofs.get (← getOptions) then
     checkProofs

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

@@ -10,7 +10,6 @@ import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.SearchM
-import Lean.Meta.Tactic.Grind.Check
 public section
 namespace Lean.Meta.Grind
 
@@ -19,7 +18,7 @@ private partial def solve (generation : Nat) : SearchM Bool := withIncRecDepth d
     return false -- `splitNext` should have been configured to not create choice points
   if (← getGoal).inconsistent then
     return true
-  if (← intros' generation <||> assertAll <||> check <||> Solvers.check <||> splitNext <||> ematch) then
+  if (← intros' generation <||> assertAll <||> Solvers.check <||> splitNext <||> ematch) then
     solve generation
   else
     return false

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

@@ -138,7 +138,7 @@ private def ppOffset : M Unit := do
 
 private def ppCutsat : M Unit := do
   let goal ← read
-  let s := goal.arith.cutsat
+  let s ← Arith.Cutsat.cutsatExt.getStateCore goal
   let nodes := s.varMap
   if nodes.isEmpty then return ()
   let model ← Arith.Cutsat.mkModel goal

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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind
 public import Lean.Meta.Tactic.Grind.Proof
@@ -13,11 +12,8 @@ public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.Ext
 public import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Diseq
-
 public section
-
 namespace Lean.Meta.Grind
-
 /--
 Propagates equalities for a conjunction `a ∧ b` based on the truth values
 of its components `a` and `b`. This function checks the truth value of `a` and `b`,
@@ -183,7 +179,6 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
     let_expr Eq α lhs rhs := e | return ()
     if α.isConstOf ``Bool then
       propagateBoolDiseq e lhs rhs
-    propagateCutsatDiseq lhs rhs
     Solvers.propagateDiseqs lhs rhs
     let thms ← getExtTheorems α
     if !thms.isEmpty then

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

@@ -9,10 +9,8 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.EMatch
-import Lean.Meta.Tactic.Grind.Arith
 import Lean.Meta.Tactic.Grind.Lookahead
 import Lean.Meta.Tactic.Grind.Intro
-import Lean.Meta.Tactic.Grind.Check
 public section
 namespace Lean.Meta.Grind
 def tryFallback : GoalM Bool := do
@@ -51,8 +49,8 @@ where
           intros gen
         else
           break
-      if (← assertAll <||> check <||> Solvers.check <||> ematch <||> lookahead <||> splitNext <||> Arith.Cutsat.mbtc
-          <||> Arith.Linear.mbtc <||> Solvers.mbtc <||> tryFallback) then
+      if (← assertAll <||> Solvers.check <||> ematch <||> lookahead <||> splitNext
+           <||> Solvers.mbtc <||> tryFallback) then
         continue
       return some (← getGoal) -- failed
     return none -- solved

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

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Tactics
 public import Init.Data.Queue
@@ -15,14 +14,11 @@ public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
 public import Lean.Meta.Tactic.Grind.ExtAttr
-public import Lean.Meta.Tactic.Grind.Arith.Types
 public import Lean.Meta.Tactic.Grind.EMatchTheorem
 meta import Lean.Parser.Do
 import Lean.Meta.Match.MatchEqsExt
 import Lean.PrettyPrinter
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- We use this auxiliary constant to mark delayed congruence proofs. -/
@@ -439,11 +435,6 @@ structure ENode where
   generation : Nat := 0
   /-- Modification time -/
   mt : Nat := 0
-  /--
-  The `cutsat?` field is used to propagate equalities from the `grind` congruence closure module
-  to the cutsat module.
-  -/
-  cutsat? : Option Expr := none
   /-- Solver terms attached to this E-node. -/
   sTerms : SolverTerms := .nil
   deriving Inhabited, Repr
@@ -765,8 +756,6 @@ structure Goal where
   ematch       : EMatch.State
   /-- State of the case-splitting module. -/
   split        : Split.State := {}
-  /-- State of arithmetic procedures. -/
-  arith        : Arith.State := {}
   /-- State of the clean name generator. -/
   clean        : Clean.State := {}
   /-- Solver states. -/
@@ -1082,44 +1071,6 @@ def setENode (e : Expr) (n : ENode) : GoalM Unit :=
     congrTable := unsafe unsafeCast s.congrTable
   }
 
-/-- Returns `true` if `e` is a numeral and has type `Nat`. -/
-def isNatNum (e : Expr) : Bool := Id.run do
-  let_expr OfNat.ofNat _ _ inst := e | false
-  let_expr instOfNatNat _ := inst | false
-  true
-
-/--
-Notifies the cutsat module that `a = b` where
-`a` and `b` are terms that have been internalized by this module.
--/
-@[extern "lean_process_cutsat_eq"] -- forward definition
-opaque Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit
-
-/--
-Notifies the cutsat module that `a ≠ b` where
-`a` and `b` are terms that have been internalized by this module.
--/
-@[extern "lean_process_cutsat_diseq"] -- forward definition
-opaque Arith.Cutsat.processNewDiseq (a b : Expr) : GoalM Unit
-
-/-- Returns `true` if `e` is a nonnegative numeral and has type `Int`. -/
-def isNonnegIntNum (e : Expr) : Bool := Id.run do
-  let_expr OfNat.ofNat _ _ inst := e | false
-  let_expr instOfNat _ := inst | false
-  true
-
-/-- Returns `true` if `e` is a numeral and has type `Int`. -/
-def isIntNum (e : Expr) : Bool :=
-  match_expr e with
-  | Neg.neg _ inst e => Id.run do
-    let_expr Int.instNegInt := inst | false
-    isNonnegIntNum e
-  | _ => isNonnegIntNum e
-
-/-- Returns `true` if `e` is a numeral supported by cutsat. -/
-def isNum (e : Expr) : Bool :=
-  isNatNum e || isIntNum e
-
 /--
 Returns `true` if type of `t` is definitionally equal to `α`
 -/
@@ -1136,40 +1087,6 @@ For each equality `b = c` in `parents`, executes `k b c` IF
     if (← isEqFalse parent) then
       k b c
 
-/--
-Given `lhs` and `rhs` that are known to be disequal, checks whether
-`lhs` and `rhs` have cutsat terms `e₁` and `e₂` attached to them,
-and invokes process `Arith.Cutsat.processNewDiseq e₁ e₂`
--/
-def propagateCutsatDiseq (lhs rhs : Expr) : GoalM Unit := do
-  let some lhs ← get? lhs | return ()
-  let some rhs ← get? rhs | return ()
-  Arith.Cutsat.processNewDiseq lhs rhs
-where
-  get? (a : Expr) : GoalM (Option Expr) := do
-    let root ← getRootENode a
-    return root.cutsat?
-
-/--
-Traverses disequalities in `parents`, and propagate the ones relevant to the
-cutsat module.
--/
-def propagateCutsatDiseqs (parents : ParentSet) : GoalM Unit := do
-  forEachDiseq parents propagateCutsatDiseq
-
-/--
-Marks `e` as a term of interest to the cutsat module.
-If the root of `e`s equivalence class has already a term of interest,
-a new equality is propagated to the cutsat module.
--/
-def markAsCutsatTerm (e : Expr) : GoalM Unit := do
-  let root ← getRootENode e
-  if let some e' := root.cutsat? then
-    Arith.Cutsat.processNewEq e e'
-  else
-    setENode root.self { root with cutsat? := some e }
-    propagateCutsatDiseqs (← getParents root.self)
-
 /-- Returns `true` is `e` is the root of its congruence class. -/
 def isCongrRoot (e : Expr) : GoalM Bool := do
   return (← getENode e).isCongrRoot
@@ -1653,11 +1570,21 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit
     setENode root.self { root with sTerms := sTermsNew }
     forEachDiseq (← getParents root.self) (propagateDiseqOf id)
 
+/--
+Returns `some t` if `t` is the solver term for `ext` associated with `e`.
+-/
+def SolverExtension.getTerm (ext : SolverExtension σ) (e : ENode) : Option Expr :=
+  go ext.id e.sTerms
+where
+  go (solverId : Nat) : SolverTerms → Option Expr
+    | .nil => none
+    | .next id t rest => if id == solverId then some t else go solverId rest
+
 /--
 Returns `true` if the root of `e`s equivalence class is already attached to a term
 of the given solver.
 -/
-def SolverExtension.hasTerm (ext : SolverExtension σ) (e : Expr) : GoalM Bool := do
+def SolverExtension.hasTermAtRoot (ext : SolverExtension σ) (e : Expr) : GoalM Bool := do
   return go ext.id (← getRootENode e).sTerms
 where
   go (solverId : Nat) : SolverTerms → Bool

stage0/src/stdlib_flags.h

@@ -1,5 +1,6 @@
+// update me!
 #include "util/options.h"
-// Please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/grind_ring_1.lean

@@ -28,9 +28,9 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
   grind
 
 /--
-trace: [grind.ring] new ring: Int
+trace: [grind.ring] new ring: Ring.OfSemiring.Q Nat
 [grind.ring] NoNatZeroDivisors available: true
-[grind.ring] new ring: Ring.OfSemiring.Q Nat
+[grind.ring] new ring: Int
 [grind.ring] NoNatZeroDivisors available: true
 [grind.ring] new ring: BitVec 8
 [grind.ring] NoNatZeroDivisors available: false