test: cooper

Using pointer address instead.

src/Init/Data/Int/Linear.lean

@@ -1213,7 +1213,7 @@ def cooper_dvd_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' :
   p₂.leadCoeff == b && p' == p₁.addConst (b*k)
 
 theorem cooper_dvd_left_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_ineq_cert p₁ p₂ k b p' → p'.denote ctx ≤ 0 := by
+    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_ineq_cert p₁ p₂ k b p' → p'.denote' ctx ≤ 0 := by
   simp [cooper_dvd_left_split_ineq_cert, cooper_dvd_left_split]
   intros; subst p' b; simp [denote'_mul_combine_mul_addConst_eq]; assumption
 
@@ -1221,7 +1221,7 @@ def cooper_dvd_left_split_dvd1_cert (p₁ p' : Poly) (a : Int) (k : Int) : Bool
   a == p₁.leadCoeff && p' == p₁.tail.addConst k
 
 theorem cooper_dvd_left_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd1_cert p₁ p' a k → a ∣ p'.denote ctx := by
+    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd1_cert p₁ p' a k → a ∣ p'.denote' ctx := by
   simp [cooper_dvd_left_split_dvd1_cert, cooper_dvd_left_split]
   intros; subst a p'; simp; assumption
 
@@ -1234,7 +1234,7 @@ def cooper_dvd_left_split_dvd2_cert (p₁ p₃ : Poly) (d : Int) (k : Nat) (d' :
   d' == a*d && p' == p₂.addConst (c*k)
 
 theorem cooper_dvd_left_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' → d' ∣ p'.denote ctx := by
+    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' → d' ∣ p'.denote' ctx := by
   simp [cooper_dvd_left_split_dvd2_cert, cooper_dvd_left_split]
   intros; subst d' p'; simp; assumption
 
@@ -1295,7 +1295,7 @@ def cooper_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' : Pol
   p₂.leadCoeff == b && p' == p₁.addConst (b*k)
 
 theorem cooper_left_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_ineq_cert p₁ p₂ k b p' → p'.denote ctx ≤ 0 := by
+    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_ineq_cert p₁ p₂ k b p' → p'.denote' ctx ≤ 0 := by
   simp [cooper_left_split_ineq_cert, cooper_left_split]
   intros; subst p' b; simp [denote'_mul_combine_mul_addConst_eq]; assumption
 
@@ -1303,7 +1303,7 @@ def cooper_left_split_dvd_cert (p₁ p' : Poly) (a : Int) (k : Int) : Bool :=
   a == p₁.leadCoeff && p' == p₁.tail.addConst k
 
 theorem cooper_left_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_dvd_cert p₁ p' a k → a ∣ p'.denote ctx := by
+    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_dvd_cert p₁ p' a k → a ∣ p'.denote' ctx := by
   simp [cooper_left_split_dvd_cert, cooper_left_split]
   intros; subst a p'; simp; assumption
 
@@ -1380,7 +1380,7 @@ def cooper_dvd_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p'
   p₁.leadCoeff == a && p' == p₂.addConst ((-a)*k)
 
 theorem cooper_dvd_right_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' → p'.denote ctx ≤ 0 := by
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' → p'.denote' ctx ≤ 0 := by
   simp [cooper_dvd_right_split_ineq_cert, cooper_dvd_right_split]
   intros; subst a p'; simp [denote'_mul_combine_mul_addConst_eq]; assumption
 
@@ -1388,7 +1388,7 @@ def cooper_dvd_right_split_dvd1_cert (p₂ p' : Poly) (b : Int) (k : Int) : Bool
   b == p₂.leadCoeff && p' == p₂.tail.addConst k
 
 theorem cooper_dvd_right_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd1_cert p₂ p' b k → b ∣ p'.denote ctx := by
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd1_cert p₂ p' b k → b ∣ p'.denote' ctx := by
   simp [cooper_dvd_right_split_dvd1_cert, cooper_dvd_right_split]
   intros; subst b p'; simp; assumption
 
@@ -1401,7 +1401,7 @@ def cooper_dvd_right_split_dvd2_cert (p₂ p₃ : Poly) (d : Int) (k : Nat) (d'
   d' == b*d && p' == p₂.addConst ((-c)*k)
 
 theorem cooper_dvd_right_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' → d' ∣ p'.denote ctx := by
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' → d' ∣ p'.denote' ctx := by
   simp [cooper_dvd_right_split_dvd2_cert, cooper_dvd_right_split]
   intros; subst d' p'; simp; assumption
 
@@ -1461,7 +1461,7 @@ def cooper_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Po
   p₁.leadCoeff == a && p' == p₂.addConst ((-a)*k)
 
 theorem cooper_right_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_ineq_cert p₁ p₂ k a p' → p'.denote ctx ≤ 0 := by
+    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_ineq_cert p₁ p₂ k a p' → p'.denote' ctx ≤ 0 := by
   simp [cooper_right_split_ineq_cert, cooper_right_split]
   intros; subst a p'; simp [denote'_mul_combine_mul_addConst_eq]; assumption
 
@@ -1469,7 +1469,7 @@ def cooper_right_split_dvd_cert (p₂ p' : Poly) (b : Int) (k : Int) : Bool :=
   b == p₂.leadCoeff && p' == p₂.tail.addConst k
 
 theorem cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_dvd_cert p₂ p' b k → b ∣ p'.denote ctx := by
+    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_dvd_cert p₂ p' b k → b ∣ p'.denote' ctx := by
   simp [cooper_right_split_dvd_cert, cooper_right_split]
   intros; subst b p'; simp; assumption
 

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

@@ -54,5 +54,7 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.diseq
 builtin_initialize registerTraceClass `grind.debug.cutsat.diseq.split
 builtin_initialize registerTraceClass `grind.debug.cutsat.backtrack
 builtin_initialize registerTraceClass `grind.debug.cutsat.search
+builtin_initialize registerTraceClass `grind.debug.cutsat.cooper
+builtin_initialize registerTraceClass `grind.debug.cutsat.conflict
 
 end Lean

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

@@ -12,19 +12,16 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
-def mkDvdCnstr (d : Int) (p : Poly) (h : DvdCnstrProof) : GoalM DvdCnstr := do
-  return { d, p, h, id := (← mkCnstrId) }
-
-def DvdCnstr.norm (c : DvdCnstr) : GoalM DvdCnstr := do
-  let c ← if c.p.isSorted then
-    pure c
+def DvdCnstr.norm (c : DvdCnstr) : DvdCnstr :=
+  let c := if c.p.isSorted then
+    c
   else
-    mkDvdCnstr c.d c.p.norm (.norm c)
+    { d := c.d, p := c.p.norm, h :=.norm c }
   let g := c.p.gcdCoeffs c.d
   if c.p.getConst % g == 0 && g != 1 then
-    mkDvdCnstr (c.d/g) (c.p.div g) (.divCoeffs c)
+    { d := c.d/g, p := c.p.div g, h := .divCoeffs c }
   else
-    return c
+    c
 
 /--
 Given an equation `c₁` containing the monomial `a*x`, and a divisibility constraint `c₂`
@@ -36,7 +33,7 @@ def DvdCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DvdC
   let d := Int.ofNat (a * c₂.d).natAbs
   let p := (q.mul a |>.combine (p.mul (-b)))
   trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
-  mkDvdCnstr d p (.subst x c₁ c₂)
+  return { d, p, h := .subst x c₁ c₂ }
 
 partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDepth do
   let some (b, x, c₁) ← c.p.findVarToSubst | return c
@@ -47,9 +44,10 @@ partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDe
 /-- Asserts divisibility constraint. -/
 partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
   if (← inconsistent) then return ()
-  let c ← c.norm
-  let c ← c.applySubsts
+  trace[grind.cutsat.dvd] "{← c.pp}"
+  let c ← c.norm.applySubsts
   if c.isUnsat then
+    trace[grind.cutsat.dvd.unsat] "{← c.pp}"
     setInconsistent (.dvd c)
     return ()
   if c.isTrivial then
@@ -74,13 +72,13 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
     -/
     let α_d₂_p₁ := p₁.mul (α*d₂)
     let β_d₁_p₂ := p₂.mul (β*d₁)
-    let combine ← mkDvdCnstr (d₁*d₂) (.add d x (α_d₂_p₁.combine β_d₁_p₂)) (.solveCombine c c')
+    let combine := { d := d₁*d₂, p := .add d x (α_d₂_p₁.combine β_d₁_p₂), h := .solveCombine c c' : DvdCnstr }
     trace[grind.cutsat.dvd.solve.combine] "{← combine.pp}"
     modify' fun s => { s with dvds := s.dvds.set x none}
     combine.assert
     let a₂_p₁ := p₁.mul a₂
     let a₁_p₂ := p₂.mul (-a₁)
-    let elim ← mkDvdCnstr d (a₂_p₁.combine a₁_p₂) (.solveElim c c')
+    let elim := { d, p := a₂_p₁.combine a₁_p₂, h := .solveElim c c' : DvdCnstr }
     trace[grind.cutsat.dvd.solve.elim] "{← elim.pp}"
     elim.assert
   else
@@ -96,7 +94,7 @@ builtin_grind_propagator propagateDvd ↓Dvd.dvd := fun e => do
       return ()
   if (← isEqTrue e) then
     let p ← toPoly b
-    let c ← mkDvdCnstr d p (.expr (← mkOfEqTrue (← mkEqTrueProof e)))
+    let c := { d, p, h := .expr (← mkOfEqTrue (← mkEqTrueProof e)) : DvdCnstr }
     trace[grind.cutsat.assert.dvd] "{← c.pp}"
     c.assert
   else if (← isEqFalse e) then

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

@@ -17,20 +17,17 @@ private def _root_.Int.Linear.Poly.substVar (p : Poly) : GoalM (Option (Var × E
   let p := p.mul (-b) |>.combine (c.p.mul a)
   return some (x, c, p)
 
-def EqCnstr.norm (c : EqCnstr) : GoalM EqCnstr := do
-  let c ← if c.p.isSorted then
-    pure c
+def EqCnstr.norm (c : EqCnstr) : EqCnstr :=
+  if c.p.isSorted then
+    c
   else
-    mkEqCnstr c.p.norm (.norm c)
+    { p := c.p.norm, h := .norm c }
 
-def mkDiseqCnstr (p : Poly) (h : DiseqCnstrProof) : GoalM DiseqCnstr := do
-  return { p, h, id := (← mkCnstrId) }
-
-def DiseqCnstr.norm (c : DiseqCnstr) : GoalM DiseqCnstr := do
-  let c ← if c.p.isSorted then
-    pure c
+def DiseqCnstr.norm (c : DiseqCnstr) : DiseqCnstr :=
+  if c.p.isSorted then
+    c
   else
-    mkDiseqCnstr c.p.norm (.norm c)
+    { p := c.p.norm, h := .norm c }
 
 /--
 Given an equation `c₁` containing the monomial `a*x`, and a disequality constraint `c₂`
@@ -41,13 +38,12 @@ def DiseqCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : Di
   let q := c₂.p
   let p := p.mul b |>.combine (q.mul (-a))
   trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
-  mkDiseqCnstr p (.subst x c₁ c₂)
+  return { p, h := .subst x c₁ c₂ }
 
 partial def DiseqCnstr.applySubsts (c : DiseqCnstr) : GoalM DiseqCnstr := withIncRecDepth do
   let some (x, c₁, p) ← c.p.substVar | return c
   trace[grind.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
-  let c ← mkDiseqCnstr p (.subst x c₁ c)
-  applySubsts c
+  applySubsts { p, h := .subst x c₁ c }
 
 /--
 Given a disequality `c`, tries to find an inequality to be refined using
@@ -61,8 +57,7 @@ private def DiseqCnstr.findLe (c : DiseqCnstr) : GoalM Bool := do
     for c' in cs' do
       if c.p == c'.p || c.p.isNegEq c'.p then
         c'.erase
-        let le ← mkLeCnstr (c'.p.addConst 1) (.ofLeDiseq c' c)
-        le.assert
+        { p := c'.p.addConst 1, h := .ofLeDiseq c' c : LeCnstr }.assert
         return true
     return false
   go true <||> go false
@@ -70,8 +65,7 @@ private def DiseqCnstr.findLe (c : DiseqCnstr) : GoalM Bool := do
 def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()
   trace[grind.cutsat.assert] "{← c.pp}"
-  let c ← c.norm
-  let c ← c.applySubsts
+  let c ← c.norm.applySubsts
   if c.p.isUnsatDiseq then
     setInconsistent (.diseq c)
     return ()
@@ -79,10 +73,10 @@ def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
     trace[grind.cutsat.diseq.trivial] "{← c.pp}"
     return ()
   let k := c.p.gcdCoeffs c.p.getConst
-  let c ← if k == 1 then
-    pure c
+  let c := if k == 1 then
+    c
   else
-    mkDiseqCnstr (c.p.div k) (.divCoeffs c)
+    { p := c.p.div k, h := .divCoeffs c }
   if (← c.findLe) then
     return ()
   let .add _ x _ := c.p | c.throwUnexpected
@@ -114,8 +108,7 @@ where
 partial def EqCnstr.applySubsts (c : EqCnstr) : GoalM EqCnstr := withIncRecDepth do
   let some (x, c₁, p) ← c.p.substVar | return c
   trace[grind.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
-  let c ← mkEqCnstr p (.subst x c₁ c)
-  applySubsts c
+  applySubsts { p, h := .subst x c₁ c : EqCnstr }
 
 private def updateDvdCnstr (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
   let some c' := (← get').dvds[y]! | return ()
@@ -201,22 +194,21 @@ private def updateOccs (k : Int) (x : Var) (c : EqCnstr) : GoalM Unit := do
 def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()
   trace[grind.cutsat.assert] "{← c.pp}"
-  let c ← c.norm
-  let c ← c.applySubsts
+  let c ← c.norm.applySubsts
   if c.p.isUnsatEq then
     setInconsistent (.eq c)
     return ()
   if c.isTrivial then
-    trace[grind.cutsat.le.trivial] "{← c.pp}"
+    trace[grind.cutsat.eq.trivial] "{← c.pp}"
     return ()
   let k := c.p.gcdCoeffs'
   if c.p.getConst % k > 0 then
     setInconsistent (.eq c)
     return ()
-  let c ← if k == 1 then
-    pure c
+  let c := if k == 1 then
+    c
   else
-    mkEqCnstr (c.p.div k) (.divCoeffs c)
+    { p := c.p.div k, h := .divCoeffs c }
   trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
   updateOccs k x c
@@ -225,8 +217,7 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if k.natAbs != 1 then
     let p := c.p.insert (-k) x
     let d := Int.ofNat k.natAbs
-    let c ← mkDvdCnstr d p (.ofEq x c)
-    c.assert
+    { d, p, h := .ofEq x c : DvdCnstr }.assert
   modify' fun s => { s with
     elimEqs := s.elimEqs.set x (some c)
     elimStack := x :: s.elimStack
@@ -248,8 +239,7 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
   let p₁ ← exprAsPoly a
   let p₂ ← exprAsPoly b
   let p := p₁.combine (p₂.mul (-1))
-  let c ← mkEqCnstr p (.core p₁ p₂ (← mkEqProof a b))
-  c.assert
+  { p, h := .core p₁ p₂ (← mkEqProof a b) : EqCnstr }.assert
 
 @[export lean_process_cutsat_eq_lit]
 def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
@@ -258,11 +248,11 @@ def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
   let p₁ ← exprAsPoly a
   let h ← mkEqProof a ke
   let c ← if k == 0 then
-    mkEqCnstr p₁ (.expr h)
+    pure { p := p₁, h := .expr h : EqCnstr }
   else
     let p₂ ← exprAsPoly ke
     let p := p₁.combine (p₂.mul (-1))
-    mkEqCnstr p (.core p₁ p₂ h)
+    pure { p, h := .core p₁ p₂ h : EqCnstr }
   c.assert
 
 @[export lean_process_cutsat_diseq]
@@ -272,11 +262,11 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
   let some h ← mkDiseqProof? a b
     | throwError "internal `grind` error, failed to build disequality proof for{indentExpr a}\nand{indentExpr b}"
   let c ← if let some 0 ← getIntValue? b then
-    mkDiseqCnstr p₁ (.expr h)
+    pure { p := p₁, h := .expr h : DiseqCnstr }
   else
     let p₂ ← exprAsPoly b
     let p := p₁.combine (p₂.mul (-1))
-    mkDiseqCnstr p (.core p₁ p₂ h)
+    pure {p, h := .core p₁ p₂ h : DiseqCnstr }
   c.assert
 
 /-- Different kinds of terms internalized by this module. -/

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

@@ -11,19 +11,17 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 
 namespace Lean.Meta.Grind.Arith.Cutsat
-def mkLeCnstr (p : Poly) (h : LeCnstrProof) : GoalM LeCnstr := do
-  return { p, h, id := (← mkCnstrId) }
 
-def LeCnstr.norm (c : LeCnstr) : GoalM LeCnstr := do
-  let c ← if c.p.isSorted then
-    pure c
+def LeCnstr.norm (c : LeCnstr) : LeCnstr :=
+  let c := if c.p.isSorted then
+    c
   else
-    mkLeCnstr c.p.norm (.norm c)
+    { p := c.p.norm, h := .norm c }
   let k := c.p.gcdCoeffs'
   if k != 1 then
-    mkLeCnstr (c.p.div k) (.divCoeffs c)
+    { p := c.p.div k, h := .divCoeffs c }
   else
-    return c
+    c
 
 /--
 Given an equation `c₁` containing the monomial `a*x`, and an inequality constraint `c₂`
@@ -37,7 +35,7 @@ def LeCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : LeCns
   else
     p.mul b |>.combine (q.mul (-a))
   trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
-  mkLeCnstr p (.subst x c₁ c₂)
+  return { p, h := .subst x c₁ c₂ }
 
 partial def LeCnstr.applySubsts (c : LeCnstr) : GoalM LeCnstr := withIncRecDepth do
   let some (b, x, c₁) ← c.p.findVarToSubst | return c
@@ -70,7 +68,8 @@ private def findEq (c : LeCnstr) : GoalM Bool := do
   for c' in cs' do
     if c.p.isNegEq c'.p then
       c'.erase
-      let eq ← mkEqCnstr c.p (.ofLeGe c c')
+      let eq := { p := c.p, h := .ofLeGe c c' : EqCnstr }
+      trace[grind.debug.cutsat.eq] "new eq: {← eq.pp}"
       eq.assert
       return true
   return false
@@ -93,14 +92,14 @@ where
       if c.p == c'.p || c.p.isNegEq c'.p then
         -- Remove `c'`
         modify' fun s => { s with diseqs := s.diseqs.modify x fun cs' => cs'.filter fun c => c.p != c'.p }
-        return some (← mkLeCnstr (c.p.addConst 1) (.ofLeDiseq c c'))
+        return some { p := c.p.addConst 1, h := .ofLeDiseq c c' }
     return none
 
 def LeCnstr.assert (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()
-  let c ← c.norm
-  let c ← c.applySubsts
+  let c ← c.norm.applySubsts
   if c.isUnsat then
+    trace[grind.cutsat.le.unsat] "{← c.pp}"
     setInconsistent (.le c)
     return ()
   if c.isTrivial then
@@ -140,9 +139,9 @@ integer inequality, asserts it to the cutsat state.
 def propagateIfIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   let some p ← toPolyLe? e | return ()
   let c ← if eqTrue then
-    mkLeCnstr p (.expr (← mkOfEqTrue (← mkEqTrueProof e)))
+    pure { p, h := .expr (← mkOfEqTrue (← mkEqTrueProof e)) : LeCnstr }
   else
-    mkLeCnstr (p.mul (-1) |>.addConst 1) (.notExpr p (← mkOfEqFalse (← mkEqFalseProof e)))
+    pure { p := p.mul (-1) |>.addConst 1, h := .notExpr p (← mkOfEqFalse (← mkEqFalseProof e)) : LeCnstr }
   trace[grind.cutsat.assert.le] "{← c.pp}"
   c.assert
 

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

@@ -14,7 +14,7 @@ private def DvdCnstr.get_d_a (c : DvdCnstr) : GoalM (Int × Int) := do
   return (d, a)
 
 mutual
-partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
+partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
   match c'.h with
   | .expr h =>
     return h
@@ -34,7 +34,7 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
       (← getContext) (toExpr c₁.p) (toExpr c₂.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
-partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
+partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
   match c'.h with
   | .expr h =>
     return h
@@ -87,7 +87,7 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
     return mkApp10 (mkConst thmName)
       (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
-partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
+partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
   match c'.h with
   | .expr h =>
     return h
@@ -127,7 +127,7 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
     let { c₁, c₂, c₃?, left } := s.pred
     let p₁ := c₁.p
     let p₂ := c₂.p
-    let coeff := if left then p₁.leadCoeff else p₂.leadCoeff
+    let coeff := if left then p₂.leadCoeff else p₁.leadCoeff
     match c₃? with
     | none =>
       let thmName := if left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq
@@ -138,7 +138,7 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
       return mkApp10 (mkConst thmName)
         (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
-partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching do
+partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do
   match c'.h with
   | .expr h =>
     return h
@@ -156,7 +156,7 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching
       (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
-partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s.id do
+partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s do
   match s.h with
   | .dec h => return mkFVar h
   | .last hs _ =>
@@ -190,7 +190,7 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
       let h ← c.toExprProofCore -- proof of `False`
       -- `hNotCase` is a proof for `¬ pred (k-1)`
       let hNotCase := mkLambda `h .default type (h.abstract #[mkFVar fvarId])
-      result := mkApp4 (mkConst ``Int.Linear.orOver_resolve) (toExpr k) pred result hNotCase
+      result := mkApp4 (mkConst ``Int.Linear.orOver_resolve) (toExpr (k-1)) pred result hNotCase
       k := k - 1
     -- `result` is now a proof of `OrOver 1 pred`
     return mkApp2 (mkConst ``Int.Linear.orOver_one) pred result
@@ -198,20 +198,16 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
 partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do
   match h with
   | .le c =>
-    trace[grind.cutsat.le.unsat] "{← c.pp}"
     return mkApp4 (mkConst ``Int.Linear.le_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
   | .dvd c =>
-    trace[grind.cutsat.dvd.unsat] "{← c.pp}"
     return mkApp5 (mkConst ``Int.Linear.dvd_unsat) (← getContext) (toExpr c.d) (toExpr c.p) reflBoolTrue (← c.toExprProof)
   | .eq c =>
-    trace[grind.cutsat.eq.unsat] "{← c.pp}"
     if c.p.isUnsatEq then
       return mkApp4 (mkConst ``Int.Linear.eq_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
     else
       let k := c.p.gcdCoeffs'
       return mkApp5 (mkConst ``Int.Linear.eq_unsat_coeff) (← getContext) (toExpr c.p) (toExpr (Int.ofNat k)) reflBoolTrue (← c.toExprProof)
   | .diseq c =>
-    trace[grind.cutsat.diseq.unsat] "{← c.pp}"
     return mkApp4 (mkConst ``Int.Linear.diseq_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
 
 end
@@ -220,6 +216,7 @@ def UnsatProof.toExprProof (h : UnsatProof) : GoalM Expr := do
   withProofContext do h.toExprProofCore
 
 def setInconsistent (h : UnsatProof) : GoalM Unit := do
+  trace[grind.debug.cutsat.conflict] "setInconsistent [{← inconsistent}]: {← h.pp}"
   if (← get').caseSplits then
     -- Let the search procedure in `SearchM` resolve the conflict.
     modify' fun s => { s with conflict? := some h }
@@ -233,14 +230,14 @@ We collect them and perform non chronological backtracking.
 -/
 
 structure CollectDecVars.State where
-  visited : Std.HashSet Nat := {}
+  visited : Std.HashSet UInt64 := {}
   found : FVarIdSet := {}
-
 abbrev CollectDecVarsM := ReaderT FVarIdSet (StateM CollectDecVars.State)
 
-private def alreadyVisited (id : Nat) : CollectDecVarsM Bool := do
-  if (← get).visited.contains id then return true
-  modify fun s => { s with visited := s.visited.insert id }
+private def alreadyVisited (c : α) : CollectDecVarsM Bool := do
+  let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2
+  if (← get).visited.contains addr then return true
+  modify fun s => { s with visited := s.visited.insert addr }
   return false
 
 private def markAsFound (fvarId : FVarId) : CollectDecVarsM Unit := do
@@ -252,26 +249,30 @@ private def collectExpr (e : Expr) : CollectDecVarsM Unit := do
     markAsFound fvarId
 
 mutual
-partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
+partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .expr h => collectExpr h
   | .core .. => return () -- Equalities coming from the core never contain cutsat decision variables
   | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
-partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s.id) do
+partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s) do
+  s.pred.c₁.collectDecVars
+  s.pred.c₂.collectDecVars
+  if let some c₃ := s.pred.c₃? then
+    c₃.collectDecVars
   match s.h with
   | .dec h => markAsFound h
   | .last (decVars := decVars) .. => decVars.forM markAsFound
 
-partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
+partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .expr h => collectExpr h
   | .cooper₁ c | .cooper₂ c
   | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars
   | .solveCombine c₁ c₂ | .solveElim c₁ c₂ | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
-partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
+partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .expr h => collectExpr h
   | .notExpr .. => return () -- This kind of proof is used for connecting with the `grind` core.
@@ -279,7 +280,7 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u
   | .combine c₁ c₂ | .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
   | .ofDiseqSplit (decVars := decVars) .. => decVars.forM markAsFound
 
-partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
+partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .expr h => collectExpr h
   | .core .. => return () -- Disequalities coming from the core never contain cutsat decision variables

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

@@ -26,25 +26,30 @@ def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
   let b   := p₂.leadCoeff
   let p₁' := p.mul b |>.combine (q.mul (-a))
   let p₁' := p₁'.addConst <| if left then b*k else (-a)*k
-  let c₁' ← mkLeCnstr p₁' (.cooper cs)
+  let c₁' := { p := p₁', h := .cooper cs : LeCnstr }
+  trace[grind.debug.cutsat.cooper] "{← c₁'.pp}"
   c₁'.assert
+  if (← inconsistent) then return ()
   let p₂' := if left then p else q
   let p₂' := p₂'.addConst k
-  let c₂' ← mkDvdCnstr (if left then a else b) p₂' (.cooper₁ cs)
+  let c₂' := { d := if left then a else b, p := p₂', h := .cooper₁ cs : DvdCnstr }
+  trace[grind.debug.cutsat.cooper] "dvd₁: {← c₂'.pp}"
   c₂'.assert
+  if (← inconsistent) then return ()
   let some c₃ := c₃? | return ()
   let p₃  := c₃.p
   let d   := c₃.d
   let s   := p₃.tail
   let c   := p₃.leadCoeff
-  let c₃' ← if left then
+  let c₃' := if left then
     let p₃' := p.mul c |>.combine (s.mul (-a))
     let p₃' := p₃'.addConst (c*k)
-    mkDvdCnstr (a*d) p₃' (.cooper₂ cs)
+    { d := a*d, p := p₃', h := .cooper₂ cs : DvdCnstr }
   else
     let p₃' := q.mul (-c) |>.combine (s.mul b)
     let p₃' := p₃'.addConst (-c*k)
-    mkDvdCnstr (b*d) p₃' (.cooper₂ cs)
+    { d := b*d, p := p₃', h := .cooper₂ cs : DvdCnstr }
+  trace[grind.debug.cutsat.cooper] "dvd₂: {← c₃'.pp}"
   c₃'.assert
 
 private def checkIsNextVar (x : Var) : GoalM Unit := do
@@ -178,7 +183,7 @@ def resolveDvdConflict (c : DvdCnstr) : GoalM Unit := do
   trace[grind.cutsat.conflict] "{← c.pp}"
   let d := c.d
   let .add a _ p := c.p | c.throwUnexpected
-  (← mkDvdCnstr (a.gcd d) p (.elim c)).assert
+  { d := a.gcd d, p, h := .elim c : DvdCnstr }.assert
 
 /--
 Given a divisibility constraint solution space `s := { b, d }`,
@@ -266,17 +271,19 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
   let .add a₂ _ p₂ := c₂.p | c₂.throwUnexpected
   let p := p₁.mul a₂.natAbs |>.combine (p₂.mul a₁.natAbs)
   if (← p.satisfiedLe) != .false then
+    trace[grind.cutsat.conflict] "not resolved"
     return false
   else
-    let c ← mkLeCnstr p (.combine c₁ c₂)
+    let c := { p, h := .combine c₁ c₂ : LeCnstr }
+    trace[grind.cutsat.conflict] "resolved: {← c.pp}"
     c.assert
     return true
 
 def resolveCooperPred (pred : CooperSplitPred) : SearchM Unit := do
+  trace[grind.cutsat.conflict] "[{pred.numCases}]: {← pred.pp}"
   let n := pred.numCases
-  let fvarId ← mkCase (.cooper pred #[])
-  let s : CooperSplit := { pred, k := n - 1, id := (← mkCnstrId), h := .dec fvarId }
-  s.assert
+  let fvarId ← mkCase (.cooper pred #[] {})
+  { pred, k := n - 1, h := .dec fvarId : CooperSplit }.assert
 
 def resolveCooper (c₁ c₂ : LeCnstr) : SearchM Unit := do
   let left : Bool := c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs
@@ -295,10 +302,10 @@ splits `c` and resolve with `c₁`.
 Recall that a disequality
 -/
 def resolveRatDiseq (c₁ : LeCnstr) (c : DiseqCnstr) : SearchM Unit := do
-  let c ← if c.p.leadCoeff < 0 then
-    mkDiseqCnstr (c.p.mul (-1)) (.neg c)
+  let c := if c.p.leadCoeff < 0 then
+    { p := c.p.mul (-1), h := .neg c : DiseqCnstr }
   else
-    pure c
+    c
   let fvarId ← if let some fvarId := (← get').diseqSplits.find? c.p then
     trace[grind.debug.cutsat.diseq.split] "{← c.pp}, reusing {fvarId.name}"
     pure fvarId
@@ -308,12 +315,13 @@ def resolveRatDiseq (c₁ : LeCnstr) (c : DiseqCnstr) : SearchM Unit := do
     modify' fun s => { s with diseqSplits := s.diseqSplits.insert c.p fvarId }
     pure fvarId
   let p₂ := c.p.addConst 1
-  let c₂ ← mkLeCnstr p₂ (.expr (mkFVar fvarId))
+  let c₂ := { p := p₂, h := .expr (mkFVar fvarId) : LeCnstr }
   let b ← resolveRealLowerUpperConflict c₁ c₂
   assert! b
 
 def processVar (x : Var) : SearchM Unit := do
   if (← eliminated x) then
+    trace[grind.debug.cutsat.search] "eliminated: {← getVar x}"
     /-
     Variable has been eliminated, and will be assigned later after we have assigned
     variables that have not been eliminated.
@@ -325,6 +333,7 @@ def processVar (x : Var) : SearchM Unit := do
     if let some solutions ← c.getSolutions? then
       pure solutions
     else
+      trace[grind.debug.cutsat.search] "dvd conflict: {← c.pp}"
       resolveDvdConflict c
       return ()
   else
@@ -392,36 +401,57 @@ private def findCase (decVars : FVarIdSet) : SearchM Case := do
     trace[grind.debug.cutsat.backtrack] "skipping {case.fvarId.name}"
   unreachable!
 
-def resolveConflict (h : UnsatProof) : SearchM Bool := do
+private def union (vs₁ vs₂ : FVarIdSet) : FVarIdSet :=
+  vs₁.fold (init := vs₂) (·.insert ·)
+
+def resolveConflict (h : UnsatProof) : SearchM Unit := do
+  trace[grind.debug.cutsat.backtrack] "resolve conflict, decision stack: {(← get).cases.toList.map fun c => c.fvarId.name}"
   let decVars := h.collectDecVars.run (← get).decVars
+  trace[grind.debug.cutsat.backtrack] "dec vars: {decVars.toList.map (·.name)}"
   if decVars.isEmpty then
+    trace[grind.debug.cutsat.backtrack] "close goal: {← h.pp}"
     closeGoal (← h.toExprProof)
-    return false
+    return ()
   let c ← findCase decVars
   modify' fun _  => c.saved
+  trace[grind.debug.cutsat.backtrack] "backtracking {c.fvarId.name}"
+  let decVars := decVars.erase c.fvarId
   match c.kind with
   | .diseq c₁ =>
-    let decVars := decVars.erase c.fvarId |>.toArray
+    let decVars := decVars.toArray
     let p' := c₁.p.mul (-1) |>.addConst 1
-    let c' ← mkLeCnstr p' (.ofDiseqSplit c₁ c.fvarId h decVars)
+    let c' := { p := p', h := .ofDiseqSplit c₁ c.fvarId h decVars : LeCnstr }
     trace[grind.debug.cutsat.backtrack] "resolved diseq split: {← c'.pp}"
     c'.assert
-    return true
-  | _ => throwError "NIY resolve conflict"
+  | .cooper pred hs decVars' =>
+    let decVars' := union decVars decVars'
+    let n := pred.numCases
+    let hs := hs.push (c.fvarId, h)
+    trace[grind.debug.cutsat.backtrack] "cooper #{hs.size + 1}, {← pred.pp}, {hs.map fun p => p.1.name}"
+    let s ← if hs.size + 1 < n then
+      let fvarId ← mkCase (.cooper pred hs decVars')
+      pure { pred, k := n - hs.size - 1, h := .dec fvarId : CooperSplit }
+    else
+      let decVars' := decVars'.toArray
+      trace[grind.debug.cutsat.backtrack] "cooper last case, {← pred.pp}, dec vars: {decVars'.map (·.name)}"
+      pure { pred, k := 0, h := .last hs decVars' : CooperSplit }
+    s.assert
 
 /-- Search for an assignment/model for the linear constraints. -/
 def searchAssigmentMain : SearchM Unit := do
   repeat
+    trace[grind.debug.cutsat.search] "main loop"
     if (← hasAssignment) then
       return ()
     if (← isInconsistent) then
       -- `grind` state is inconsistent
       return ()
     if let some c := (← get').conflict? then
-      unless (← resolveConflict c) do
-        return ()
-    let x : Var := (← get').assignment.size
-    processVar x
+      resolveConflict c
+    else
+      let x : Var := (← get').assignment.size
+      trace[grind.debug.cutsat.search] "next var: {← getVar x}"
+      processVar x
 
 def traceModel : GoalM Unit := do
   if (← isTracingEnabledFor `grind.cutsat.model) then
@@ -436,6 +466,7 @@ def searchAssigment : GoalM Unit := do
     trace[grind.debug.cutsat.search] "restart using Cooper resolution"
     modify' fun s => { s with assignment := {} }
     searchAssigmentMain .int |>.run' {}
+    trace[grind.debug.cutsat.search] "after search int model, inconsistent: {← isInconsistent}"
     if (← isInconsistent) then return ()
   assignElimVars
   traceModel

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

@@ -14,7 +14,7 @@ In principle, we only need to support two kinds of case split.
 -/
 inductive CaseKind where
   | diseq (d : DiseqCnstr)
-  | cooper (s : CooperSplitPred) (hs : Array (FVarId × UnsatProof))
+  | cooper (s : CooperSplitPred) (hs : Array (FVarId × UnsatProof)) (decVars : FVarIdSet)
   deriving Inhabited
 
 structure Case where
@@ -74,6 +74,7 @@ def mkCase (kind : CaseKind) : SearchM FVarId := do
     decVars := s.decVars.insert fvarId
   }
   modify' fun s => { s with caseSplits := true }
+  trace[grind.debug.cutsat.backtrack] "mkCase fvarId: {fvarId.name}"
   return fvarId
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -75,7 +75,6 @@ mutual
 structure EqCnstr where
   p  : Poly
   h  : EqCnstrProof
-  id : Nat
 
 inductive EqCnstrProof where
   | expr (h : Expr)
@@ -90,8 +89,6 @@ structure DvdCnstr where
   d  : Int
   p  : Poly
   h  : DvdCnstrProof
-  /-- Unique id for caching proofs in `ProofM` -/
-  id : Nat
 
 /--
 The predicate of type `Nat → Prop`, which serves as the conclusion of the
@@ -118,7 +115,6 @@ structure CooperSplit where
   pred  : CooperSplitPred
   k     : Nat
   h     : CooperSplitProof
-  id    : Nat
 
 /--
 The `cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems have a resulting type
@@ -150,7 +146,6 @@ inductive DvdCnstrProof where
 structure LeCnstr where
   p  : Poly
   h  : LeCnstrProof
-  id : Nat
 
 inductive LeCnstrProof where
   | expr (h : Expr)
@@ -169,7 +164,6 @@ inductive LeCnstrProof where
 structure DiseqCnstr where
   p  : Poly
   h  : DiseqCnstrProof
-  id : Nat
 
 inductive DiseqCnstrProof where
   | expr (h : Expr)
@@ -192,16 +186,16 @@ inductive UnsatProof where
 end
 
 instance : Inhabited LeCnstr where
-  default := { p := .num 0, h := .expr default, id := 0 }
+  default := { p := .num 0, h := .expr default }
 
 instance : Inhabited DvdCnstr where
-  default := { d := 0, p := .num 0, h := .expr default, id := 0 }
+  default := { d := 0, p := .num 0, h := .expr default }
 
 instance : Inhabited CooperSplitPred where
   default := { left := false, c₁ := default, c₂ := default, c₃? := none }
 
 instance : Inhabited CooperSplit where
-  default := { pred := default, k := 0, h := .dec default, id := 0 }
+  default := { pred := default, k := 0, h := .dec default }
 
 abbrev VarSet := RBTree Var compare
 

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

@@ -64,9 +64,6 @@ def mkCnstrId : GoalM Nat := do
   modify' fun s => { s with nextCnstrId := id + 1 }
   return id
 
-def mkEqCnstr (p : Poly) (h : EqCnstrProof) : GoalM EqCnstr := do
-  return { p, h, id := (← mkCnstrId) }
-
 @[extern "lean_grind_cutsat_assert_eq"] -- forward definition
 opaque EqCnstr.assert (c : EqCnstr) : GoalM Unit
 
@@ -189,7 +186,7 @@ def toContextExpr : GoalM Expr := do
     return RArray.toExpr (mkConst ``Int) id (RArray.leaf (mkIntLit 0))
 
 structure ProofM.State where
-  cache : Std.HashMap Nat Expr := {}
+  cache : Std.HashMap UInt64 Expr := {}
 
 /-- Auxiliary monad for constructing cutsat proofs. -/
 abbrev ProofM := ReaderT Expr (StateRefT ProofM.State GoalM)
@@ -198,19 +195,15 @@ abbrev ProofM := ReaderT Expr (StateRefT ProofM.State GoalM)
 abbrev getContext : ProofM Expr := do
   read
 
-abbrev caching (id : Nat) (k : ProofM Expr) : ProofM Expr := do
-  if let some h := (← get).cache[id]? then
+abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
+  let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2
+  if let some h := (← get).cache[addr]? then
     return h
   else
     let h ← k
-    modify fun s => { s with cache := s.cache.insert id h }
+    modify fun s => { s with cache := s.cache.insert addr h }
     return h
 
-abbrev DvdCnstr.caching (c : DvdCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
-abbrev LeCnstr.caching (c : LeCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
-abbrev EqCnstr.caching (c : EqCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
-abbrev DiseqCnstr.caching (c : DiseqCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
-
 abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
   withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx => do
     let h ← x ctx |>.run' {}
@@ -291,4 +284,11 @@ def CooperSplitPred.numCases (pred : CooperSplitPred) : Nat :=
     else
       Int.lcm b (b * d / Int.gcd (b * d) c)
 
+def CooperSplitPred.pp (pred : CooperSplitPred) : GoalM MessageData := do
+  return m!"{← pred.c₁.pp}, {← pred.c₂.pp}, {← if let some c₃ := pred.c₃? then c₃.pp else pure "none"}"
+
+def UnsatProof.pp (h : UnsatProof) : GoalM MessageData := do
+  match h with
+  | .le c | .eq c | .dvd c | .diseq c => c.pp
+
 end Lean.Meta.Grind.Arith.Cutsat

tests/lean/run/grind_cutsat_cooper.lean

@@ -0,0 +1,9 @@
+set_option grind.warning false
+
+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
+  -- `omega` fails in this example
+  grind

tests/lean/run/grind_cutsat_div_1.lean

@@ -32,7 +32,9 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
   sorry
 
 /--
-info: [grind.cutsat.dvd.update] 2 ∣ a + 3
+info: [grind.cutsat.dvd] 2 ∣ a + 3
+[grind.cutsat.dvd.update] 2 ∣ a + 3
+[grind.cutsat.dvd] 3 ∣ a + 3*b + -4
 [grind.cutsat.dvd.update] 3 ∣ 3*b + a + -4
 [grind.cutsat.assign] a := 1
 [grind.cutsat.assign] b := 0