feat: add toPoly

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

@@ -10,6 +10,8 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 namespace Lean
 
 builtin_initialize registerTraceClass `grind.cutsat
+builtin_initialize registerTraceClass `grind.cutsat.assert
+builtin_initialize registerTraceClass `grind.cutsat.assert.dvd
 builtin_initialize registerTraceClass `grind.cutsat.internalize
 builtin_initialize registerTraceClass `grind.cutsat.internalize.term (inherited := true)
 

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

@@ -0,0 +1,22 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+def assertDvdCnstr (e : Expr) : GoalM Unit := do
+  let_expr Dvd.dvd _ inst a b ← e | return ()
+  unless (← isInstDvdInt inst) do return ()
+  let some k ← getIntValue? a
+    | reportIssue! "non-linear divisibility constraint found{indentExpr e}"
+  let p ← toPoly b
+  let c : DvdCnstr := { k, p }
+  trace[grind.cutsat.assert.dvd] "{e}, {repr c}"
+  -- TODO
+  return ()
+
+end Lean.Meta.Grind.Arith.Cutsat

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

@@ -6,12 +6,40 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 
+namespace Int.Linear
+/--
+Returns `true` if the variables in the given polynomial are sorted
+in decreasing order.
+-/
+def Poly.isSorted (p : Poly) : Bool :=
+  go none p
+where
+  go : Option Var → Poly → Bool
+  | _,      .num _     => true
+  | none,   .add _ y p => go (some y) p
+  | some x, .add _ y p => x > y && go (some y) p
+
+/-- Returns `true` if all coefficients are not `0`. -/
+def Poly.checkCoeffs : Poly → Bool
+  | .num _ => true
+  | .add k _ p => k != 0 && checkCoeffs p
+
+end Int.Linear
+
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 def checkDvdCnstrs : GoalM Unit := do
   let s ← get'
   assert! s.vars.size == s.dvdCnstrs.size
-  -- TODO: condition maximal variable
+  let mut x := 0
+  for c? in s.dvdCnstrs do
+    if let some { c, .. } := c? then
+      assert! c.p.checkCoeffs
+      assert! c.p.isSorted
+      assert! c.k > 1
+      let .add _ y _ := c.p | unreachable!
+      assert! x == y
+    x := x + 1
 
 def checkVars : GoalM Unit := do
   let s ← get'

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

@@ -4,8 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.IntInstTesters
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 
+def Int.Linear.Poly.isZero : Poly → Bool
+  | .num 0 => true
+  | _ => false
+
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 /-- Creates a new variable in the cutsat module. -/
@@ -21,4 +26,46 @@ def mkVar (expr : Expr) : GoalM Var := do
   }
   return var
 
+def isInt (e : Expr) : GoalM Bool := do
+  isDefEq (← inferType e) (mkConst ``Int)
+
+def isAdd? (e : Expr) : GoalM (Option (Expr × Expr)) := do
+  let_expr HAdd.hAdd _ _ _ inst a b ← e | return none
+  unless (← isInstHAddInt inst) do
+    reportIssue! "found term with non-standard instance{indentExpr e}"
+    return none
+  return some (a, b)
+
+def isMul? (e : Expr) : GoalM (Option (Int × Expr)) := do
+  let_expr HMul.hMul _ _ _ inst a b ← e
+    | return none
+  unless (← isInstHMulInt inst) do
+    reportIssue! "found term with non-standard instance{indentExpr e}"
+    return none
+  let some k ← getIntValue? a
+    | return none
+  return some (k, b)
+
+def addMonomial (e : Expr) (p : Poly) : GoalM Poly := do
+  if let some (k, x) ← isMul? e then
+    return .add k (← mkVar x) p
+  if let some k ← getIntValue? e then
+    if p.isZero then
+      return .num k
+    else
+      reportIssue! "monomial expected, found numeral{indentExpr e}\ninternalizing as variable"
+  return .add 1 (← mkVar e) p
+
+partial def toPoly (e : Expr) : GoalM Poly := do
+  if let some (a, b) ← isAdd? e then
+    go a (← addMonomial b (.num 0))
+  else
+    addMonomial e (.num 0)
+where
+  go (e : Expr) (p : Poly) : GoalM Poly := do
+    if let some (a, b) ← isAdd? e then
+      go a (← addMonomial b p)
+    else
+      addMonomial e p
+
 end Lean.Meta.Grind.Arith.Cutsat