chore: fix tests

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

@@ -22,50 +22,17 @@ namespace Lean
 
 builtin_initialize registerTraceClass `grind.cutsat
 builtin_initialize registerTraceClass `grind.cutsat.model
-builtin_initialize registerTraceClass `grind.cutsat.subst
-builtin_initialize registerTraceClass `grind.cutsat.eq
-builtin_initialize registerTraceClass `grind.cutsat.eq.unsat (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.eq.trivial (inherited := true)
 builtin_initialize registerTraceClass `grind.cutsat.assert
-builtin_initialize registerTraceClass `grind.cutsat.assert.dvd
-builtin_initialize registerTraceClass `grind.cutsat.dvd
-builtin_initialize registerTraceClass `grind.cutsat.dvd.update (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.dvd.unsat (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.dvd.trivial (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.dvd.solve (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.dvd.solve.combine (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.dvd.solve.elim (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.internalize
-builtin_initialize registerTraceClass `grind.cutsat.internalize.term (inherited := true)
+builtin_initialize registerTraceClass `grind.cutsat.assert.trivial
+builtin_initialize registerTraceClass `grind.cutsat.assert.unsat
+builtin_initialize registerTraceClass `grind.cutsat.assert.store
 
-builtin_initialize registerTraceClass `grind.cutsat.assert.le
-builtin_initialize registerTraceClass `grind.cutsat.le
-builtin_initialize registerTraceClass `grind.cutsat.le.unsat (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.le.trivial (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.le.lower (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.le.upper (inherited := true)
-builtin_initialize registerTraceClass `grind.cutsat.assign
-builtin_initialize registerTraceClass `grind.cutsat.conflict
-
-builtin_initialize registerTraceClass `grind.cutsat.diseq
-builtin_initialize registerTraceClass `grind.cutsat.diseq.trivial (inherited := true)
-
-builtin_initialize registerTraceClass `grind.debug.cutsat.eq
-builtin_initialize registerTraceClass `grind.debug.cutsat.dvd.le
-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.cooper.diseq
-builtin_initialize registerTraceClass `grind.debug.cutsat.conflict
-builtin_initialize registerTraceClass `grind.debug.cutsat.assign
 builtin_initialize registerTraceClass `grind.debug.cutsat.subst
-builtin_initialize registerTraceClass `grind.debug.cutsat.getBestLower
-builtin_initialize registerTraceClass `grind.debug.cutsat.nat
-builtin_initialize registerTraceClass `grind.debug.cutsat.proof
+builtin_initialize registerTraceClass `grind.debug.cutsat.search
+builtin_initialize registerTraceClass `grind.debug.cutsat.search.split (inherited := true)
+builtin_initialize registerTraceClass `grind.debug.cutsat.search.assign (inherited := true)
+builtin_initialize registerTraceClass `grind.debug.cutsat.search.conflict (inherited := true)
+builtin_initialize registerTraceClass `grind.debug.cutsat.search.backtrack (inherited := true)
 builtin_initialize registerTraceClass `grind.debug.cutsat.internalize
-builtin_initialize registerTraceClass `grind.debug.cutsat.markTerm
-builtin_initialize registerTraceClass `grind.debug.cutsat.natCast
 
 end Lean

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

@@ -34,7 +34,7 @@ def DvdCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DvdC
   let q := c₂.p
   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}"
+  trace[grind.debug.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
   return { d, p, h := .subst x c₁ c₂ }
 
 partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDepth do
@@ -46,21 +46,20 @@ 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 ()
-  trace[grind.cutsat.dvd] "{← c.pp}"
+  trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm.applySubsts
   if c.isUnsat then
-    trace[grind.cutsat.dvd.unsat] "{← c.pp}"
+    trace[grind.cutsat.assert.unsat] "{← c.pp}"
     setInconsistent (.dvd c)
     return ()
   if c.isTrivial then
-    trace[grind.cutsat.dvd.trivial] "{← c.pp}"
+    trace[grind.cutsat.assert.trivial] "{← c.pp}"
     return ()
   let d₁ := c.d
   let .add a₁ x p₁ := c.p | c.throwUnexpected
   if (← c.satisfied) == .false then
     resetAssignmentFrom x
   if let some c' := (← get').dvds[x]! then
-    trace[grind.cutsat.dvd.solve] "{← c.pp}, {← c'.pp}"
     let d₂ := c'.d
     let .add a₂ _ p₂ := c'.p | c'.throwUnexpected
     let (d, α, β) := gcdExt (a₁*d₂) (a₂*d₁)
@@ -75,16 +74,14 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
     let α_d₂_p₁ := p₁.mul (α*d₂)
     let β_d₁_p₂ := p₂.mul (β*d₁)
     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 := { d, p := a₂_p₁.combine a₁_p₂, h := .solveElim c c' : DvdCnstr }
-    trace[grind.cutsat.dvd.solve.elim] "{← elim.pp}"
     elim.assert
   else
-    trace[grind.cutsat.dvd.update] "{← c.pp}"
+    trace[grind.cutsat.assert.store] "{← c.pp}"
     c.p.updateOccs
     modify' fun s => { s with dvds := s.dvds.set x (some c) }
 
@@ -97,7 +94,6 @@ def propagateIntDvd (e : Expr) : GoalM Unit := do
   if (← isEqTrue e) then
     let p ← toPoly b
     let c := { d, p, h := .core e : DvdCnstr }
-    trace[grind.cutsat.assert.dvd] "{← c.pp}"
     c.assert
   else if (← isEqFalse e) then
     pushNewFact <| mkApp4 (mkConst ``Int.Linear.of_not_dvd) a b reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))

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

@@ -38,12 +38,12 @@ def DiseqCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : Di
   let p := c₁.p
   let q := c₂.p
   let p := p.mul b |>.combine (q.mul (-a))
-  trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
+  trace[grind.debug.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
   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}"
+  trace[grind.debug.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
   applySubsts { p, h := .subst x c₁ c }
 
 /--
@@ -68,10 +68,11 @@ def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
   trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm.applySubsts
   if c.p.isUnsatDiseq then
+    trace[grind.cutsat.assert.unsat] "{← c.pp}"
     setInconsistent (.diseq c)
     return ()
   if c.isTrivial then
-    trace[grind.cutsat.diseq.trivial] "{← c.pp}"
+    trace[grind.cutsat.assert.trivial] "{← c.pp}"
     return ()
   let k := c.p.gcdCoeffs c.p.getConst
   let c := if k == 1 then
@@ -82,7 +83,7 @@ def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
     return ()
   let .add _ x _ := c.p | c.throwUnexpected
   c.p.updateOccs
-  trace[grind.cutsat.diseq] "{← c.pp}"
+  trace[grind.cutsat.assert.store] "{← c.pp}"
   modify' fun s => { s with diseqs := s.diseqs.modify x (·.push c) }
   if (← c.satisfied) == .false then
     resetAssignmentFrom x
@@ -108,7 +109,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}"
+  trace[grind.debug.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
   applySubsts { p, h := .subst x c₁ c : EqCnstr }
 
 private def updateDvdCnstr (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
@@ -197,10 +198,11 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm.applySubsts
   if c.p.isUnsatEq then
+    trace[grind.cutsat.assert.unsat] "{← c.pp}"
     setInconsistent (.eq c)
     return ()
   if c.isTrivial then
-    trace[grind.cutsat.eq.trivial] "{← c.pp}"
+    trace[grind.cutsat.assert.trivial] "{← c.pp}"
     return ()
   let k := c.p.gcdCoeffs'
   if c.p.getConst % k > 0 then
@@ -210,9 +212,9 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
     c
   else
     { p := c.p.div k, h := .divCoeffs c }
-  trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
   trace[grind.debug.cutsat.subst] ">> {← getVar x}, {← c.pp}"
+  trace[grind.cutsat.assert.store] "{← c.pp}"
   modify' fun s => { s with
     elimEqs := s.elimEqs.set x (some c)
     elimStack := x :: s.elimStack
@@ -252,7 +254,6 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do
 
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.eq] "{a} = {b}"
   match (← foreignTerm? a), (← foreignTerm? b) with
   | none, none => processNewIntEq a b
   | some .nat, some .nat => processNewNatEq a b
@@ -271,7 +272,6 @@ private def processNewIntLitEq (a ke : Expr) : GoalM Unit := do
 
 @[export lean_process_cutsat_eq_lit]
 def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.eq] "{a} = {ke}"
   match (← foreignTerm? a) with
   | none => processNewIntLitEq a ke
   | some .nat => processNewNatEq a ke
@@ -294,12 +294,10 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
   let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : DiseqCnstr }
-  trace[grind.debug.cutsat.nat] "{← c.pp}"
   c.assert
 
 @[export lean_process_cutsat_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
-  trace[grind.debug.cutsat.diseq] "{a} ≠ {b}"
   match (← foreignTerm? a), (← foreignTermOrLit? b) with
   | none, none => processNewIntDiseq a b
   | some .nat, some .nat => processNewNatDiseq a b
@@ -342,7 +340,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
 private def internalizeInt (e : Expr) : GoalM Unit := do
   if (← hasVar e) then return ()
   let p ← toPoly e
-  trace[grind.cutsat.internalize] "{aquote e}:= {← p.pp}"
+  trace[grind.debug.cutsat.internalize] "{aquote e}:= {← p.pp}"
   let x ← mkVar e
   if p == .add 1 x (.num 0) then
     -- It is pointless to assert `x = x`
@@ -403,9 +401,8 @@ private def internalizeNat (e : Expr) : GoalM Unit := do
   let e'' : Int.Linear.Expr ← toLinearExpr e'' gen
   let p := e''.norm
   let natCast_e ← shareCommon (mkIntNatCast e)
-  trace[grind.cutsat.internalize] "natCast: {natCast_e}"
   internalize natCast_e gen
-  trace[grind.cutsat.internalize] "{aquote natCast_e}:= {← p.pp}"
+  trace[grind.debug.cutsat.internalize] "{aquote natCast_e}:= {← p.pp}"
   let x ← mkVar natCast_e
   modify' fun s => { s with foreignDef := s.foreignDef.insert { expr := e } x }
   let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }

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

@@ -24,7 +24,6 @@ def mkForeignVar (e : Expr) (t : ForeignType) : GoalM Var := do
     foreignVars := s.foreignVars.insert t (vars.push e)
     foreignVarMap := s.foreignVarMap.insert { expr := e} (x, t)
   }
-  trace[grind.debug.cutsat.markTerm] "mkForeignVar: {e}"
   markAsCutsatTerm e
   return x
 

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

@@ -100,24 +100,24 @@ where
 @[export lean_grind_cutsat_assert_le]
 def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()
+  trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm.applySubsts
   if c.isUnsat then
-    trace[grind.cutsat.le.unsat] "{← c.pp}"
+    trace[grind.cutsat.assert.unsat] "{← c.pp}"
     setInconsistent (.le c)
     return ()
   if c.isTrivial then
-    trace[grind.cutsat.le.trivial] "{← c.pp}"
+    trace[grind.cutsat.assert.trivial] "{← c.pp}"
     return ()
   let .add a x _ := c.p | c.throwUnexpected
   if (← findEq c) then
     return ()
   let c ← refineWithDiseq c
+  trace[grind.cutsat.assert.store] "{← c.pp}"
   if a < 0 then
-    trace[grind.cutsat.le.lower] "{← c.pp}"
     c.p.updateOccs
     modify' fun s => { s with lowers := s.lowers.modify x (·.push c) }
   else
-    trace[grind.cutsat.le.upper] "{← c.pp}"
     c.p.updateOccs
     modify' fun s => { s with uppers := s.uppers.modify x (·.push c) }
   if (← c.satisfied) == .false then
@@ -145,7 +145,6 @@ def propagateIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
     pure { p, h := .core e : LeCnstr }
   else
     pure { p := p.mul (-1) |>.addConst 1, h := .coreNeg e p : LeCnstr }
-  trace[grind.cutsat.assert.le] "{← c.pp}"
   c.assert
 
 def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
@@ -155,7 +154,6 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen
   let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
-  trace[grind.debug.cutsat.nat] "{← p.pp}"
   let c ← if eqTrue then
     pure { p, h := .coreNat e lhs rhs lhs' rhs' : LeCnstr }
   else

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

@@ -136,9 +136,7 @@ def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := withIncRecDepth do
   let lhs' : Int.Linear.Expr := .num 0
   let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
-  trace[grind.debug.cutsat.nat] "{← p.pp}"
   let c := { p, h := .denoteAsIntNonneg rhs rhs' : LeCnstr }
-  trace[grind.cutsat.assert.le] "{← c.pp}"
   c.assert
 
 /--
@@ -149,7 +147,6 @@ def assertNatCast (e : Expr) (x : Var) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
   if (← get').foreignDef.contains { expr := a } then return ()
-  trace[grind.debug.cutsat.natCast] "{a}"
   let n ← mkForeignVar a .nat
   let p := .add (-1) x (.num 0)
   let c := { p, h := .denoteAsIntNonneg (.var n) (.var x) : LeCnstr}

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

@@ -301,7 +301,6 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
         (← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (← mkPolyDecl c'.p) (← s.toExprProof) reflBoolTrue
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do
-  trace[grind.debug.cutsat.proof] "{← c'.pp}"
   match c'.h with
   | .core0 a zero =>
     mkDiseqProof a zero
@@ -352,7 +351,6 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
     -- `pred` is an expressions of the form `cooper_*_split ...` with type `Nat → Prop`
     let mut k := n
     let mut result := base -- `OrOver k (cooper_*_splti)
-    trace[grind.debug.cutsat.proof] "orOver_cases {n}"
     result := mkApp3 (mkConst ``Int.Linear.orOver_cases) (toExpr (n-1)) pred result
     for (fvarId, c) in hs do
       let type := mkApp pred (toExpr (k-1))
@@ -365,7 +363,6 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
     return result
 
 partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do
-  trace[grind.debug.cutsat.proof] "{← h.pp}"
   match h with
   | .le c =>
     return mkApp4 (mkConst ``Int.Linear.le_unsat) (← getContext) (← mkPolyDecl c.p) reflBoolTrue (← c.toExprProof)
@@ -392,7 +389,6 @@ 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 }

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

@@ -27,7 +27,6 @@ def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
   let p₁' := p.mul b |>.combine (q.mul (-a))
   let p₁' := p₁'.addConst <| if left then b*k else (-a)*k
   let c₁' := { p := p₁', h := .cooper cs : LeCnstr }
-  trace[grind.debug.cutsat.cooper] "{← c₁'.pp}"
   c₁'.assert
   if (← inconsistent) then return ()
   let d := if left then a else b
@@ -35,7 +34,6 @@ def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
     let p₂' := if left then p else q
     let p₂' := p₂'.addConst k
     let c₂' := { d, 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 ()
@@ -51,7 +49,6 @@ def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
     let p₃' := q.mul (-c) |>.combine (s.mul b)
     let p₃' := p₃'.addConst (-c*k)
     { 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
@@ -59,7 +56,7 @@ private def checkIsNextVar (x : Var) : GoalM Unit := do
     throwError "`grind` internal error, assigning variable out of order"
 
 private def traceAssignment (x : Var) (v : Rat) : GoalM Unit := do
-  trace[grind.cutsat.assign] "{quoteIfArithTerm (← getVar x)} := {v}"
+  trace[grind.debug.cutsat.search.assign] "{quoteIfArithTerm (← getVar x)} := {v}"
 
 private def setAssignment (x : Var) (v : Rat) : GoalM Unit := do
   checkIsNextVar x
@@ -88,7 +85,6 @@ where
       modify' fun s => { s with assignment := s.assignment.set x 0 }
       let some v ← c.p.eval? | c.throwUnexpected
       let v := (-v) / a
-      trace[grind.debug.cutsat.assign] "{← getVar x}, {← c.pp}, {v}"
       traceAssignment x v
       modify' fun s => { s with assignment := s.assignment.set x v }
       go xs
@@ -108,7 +104,6 @@ def tightUsingDvd (c : LeCnstr) (dvd? : Option DvdCnstr) : GoalM LeCnstr := do
     let b₂ := c.p.getConst
     if (b₂ - b₁) % d != 0 then
       let b₂' := b₁ - d * ((b₁ - b₂) / d)
-      trace[grind.debug.cutsat.dvd.le] "[pos] {← c.pp}, {← dvd.pp}, {b₂'}"
       let p := c.p.addConst (b₂'-b₂)
       return { p, h := .dvdTight dvd c }
   if eqCoeffs dvd.p c.p true then
@@ -116,7 +111,6 @@ def tightUsingDvd (c : LeCnstr) (dvd? : Option DvdCnstr) : GoalM LeCnstr := do
     let b₂ := c.p.getConst
     if (b₂ - b₁) % d != 0 then
       let b₂' := b₁ - d * ((b₁ - b₂) / d)
-      trace[grind.debug.cutsat.dvd.le] "[neg] {← c.pp}, {← dvd.pp}, {b₂'}"
       let p := c.p.addConst (b₂'-b₂)
       return { p, h := .negDvdTight dvd c }
   return c
@@ -134,7 +128,6 @@ def getBestLower? (x : Var) (dvd? : Option DvdCnstr) : GoalM (Option (Rat × LeC
     let .add k _ p := c.p | c.throwUnexpected
     let some v ← p.eval? | c.throwUnexpected
     let lower' := v / (-k)
-    trace[grind.debug.cutsat.getBestLower] "k: {k}, x: {x}, p: {repr p}, v: {v}, best?: {best?.map (·.1)}, c: {← c.pp}"
     if let some (lower, _) := best? then
       if lower' > lower then
         best? := some (lower', c)
@@ -214,7 +207,7 @@ def DvdCnstr.getSolutions? (c : DvdCnstr) : SearchM (Option DvdSolution) := do
   return some { d, b := -b*a' }
 
 def resolveDvdConflict (c : DvdCnstr) : GoalM Unit := do
-  trace[grind.cutsat.conflict] "{← c.pp}"
+  trace[grind.debug.cutsat.search.conflict] "{← c.pp}"
   let d := c.d
   let .add a _ p := c.p | c.throwUnexpected
   { d := a.gcd d, p, h := .elim c : DvdCnstr }.assert
@@ -300,7 +293,7 @@ partial def findRatVal (lower upper : Rat) (diseqVals : Array (Rat × DiseqCnstr
     v
 
 def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
-  trace[grind.cutsat.conflict] "{← c₁.pp}, {← c₂.pp}"
+  trace[grind.debug.cutsat.search.conflict] "{← c₁.pp}, {← c₂.pp}"
   let .add a₁ _ p₁ := c₁.p | c₁.throwUnexpected
   let .add a₂ _ p₂ := c₂.p | c₂.throwUnexpected
   let p := p₁.mul a₂.natAbs |>.combine (p₂.mul a₁.natAbs)
@@ -313,7 +306,7 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
       { p, h := .combine c₁ c₂ : LeCnstr }
     else
       { p := p.div k, h := .combineDivCoeffs c₁ c₂ k : LeCnstr }
-    trace[grind.cutsat.conflict] "resolved: {← c.pp}"
+    trace[grind.debug.cutsat.search.conflict] "resolved: {← c.pp}"
     c.assert
     return true
 
@@ -330,7 +323,7 @@ def resolveCooperUnary (pred : CooperSplitPred) : SearchM Bool := do
   return true
 
 def resolveCooperPred (pred : CooperSplitPred) : SearchM Unit := do
-  trace[grind.cutsat.conflict] "[{pred.numCases}]: {← pred.pp}"
+  trace[grind.debug.cutsat.search.conflict] "[{pred.numCases}]: {← pred.pp}"
   if (← resolveCooperUnary pred) then
     return
   let n := pred.numCases
@@ -347,11 +340,11 @@ def resolveCooperDvd (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr) : SearchM Unit := d
 
 def DiseqCnstr.split (c : DiseqCnstr) : SearchM LeCnstr := do
   let fvarId ← if let some fvarId := (← get').diseqSplits.find? c.p then
-    trace[grind.debug.cutsat.diseq.split] "{← c.pp}, reusing {fvarId.name}"
+    trace[grind.debug.cutsat.search.split] "{← c.pp}, reusing {fvarId.name}"
     pure fvarId
   else
     let fvarId ← mkCase (.diseq c)
-    trace[grind.debug.cutsat.diseq.split] "{← c.pp}, {fvarId.name}"
+    trace[grind.debug.cutsat.search.split] "{← c.pp}, {fvarId.name}"
     modify' fun s => { s with diseqSplits := s.diseqSplits.insert c.p fvarId }
     pure fvarId
   let p₂ := c.p.addConst 1
@@ -428,7 +421,6 @@ def processVar (x : Var) : SearchM Unit := do
     setAssignment x v
   | some (lower, c₁), some (upper, c₂) =>
     trace[grind.debug.cutsat.search] "{lower} ≤ {lower.ceil} ≤ {quoteIfArithTerm (← getVar x)} ≤ {upper.floor} ≤ {upper}"
-    trace[grind.debug.cutsat.getBestLower] "lower: {lower}, c₁: {← c₁.pp}"
     if lower > upper then
       let .true ← resolveRealLowerUpperConflict c₁ c₂
         | throwError "`grind` internal error, conflict resolution failed"
@@ -472,43 +464,42 @@ private def findCase (decVars : FVarIdSet) : SearchM Case := do
     if decVars.contains case.fvarId then
       return case
     -- Conflict does not depend on this case.
-    trace[grind.debug.cutsat.backtrack] "skipping {case.fvarId.name}"
+    trace[grind.debug.cutsat.search.backtrack] "skipping {case.fvarId.name}"
   unreachable!
 
 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}"
+  trace[grind.debug.cutsat.search.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)}"
+  trace[grind.debug.cutsat.search.backtrack] "dec vars: {decVars.toList.map (·.name)}"
   if decVars.isEmpty then
-    trace[grind.debug.cutsat.backtrack] "close goal: {← h.pp}"
+    trace[grind.debug.cutsat.search.backtrack] "close goal: {← h.pp}"
     closeGoal (← h.toExprProof)
     return ()
   let c ← findCase decVars
   modify' fun _  => c.saved
-  trace[grind.debug.cutsat.backtrack] "backtracking {c.fvarId.name}"
+  trace[grind.debug.cutsat.search.backtrack] "backtracking {c.fvarId.name}"
   let decVars := decVars.erase c.fvarId
   match c.kind with
   | .diseq c₁ =>
     let decVars := decVars.toArray
     let p' := c₁.p.mul (-1) |>.addConst 1
     let c' := { p := p', h := .ofDiseqSplit c₁ c.fvarId h decVars : LeCnstr }
-    trace[grind.debug.cutsat.backtrack] "resolved diseq split: {← c'.pp}"
+    trace[grind.debug.cutsat.search.backtrack] "resolved diseq split: {← c'.pp}"
     c'.assert
   | .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}"
+    trace[grind.debug.cutsat.search.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)}"
-      trace[grind.debug.cutsat.proof] "CooperSplit.last"
+      trace[grind.debug.cutsat.search.backtrack] "cooper last case, {← pred.pp}, dec vars: {decVars'.map (·.name)}"
       pure { pred, k := 0, h := .last hs decVars' : CooperSplit }
     s.assert
 

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

@@ -74,7 +74,6 @@ 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/Var.lean

@@ -16,7 +16,7 @@ def mkVarImpl (expr : Expr) : GoalM Var := do
   if let some var := (← get').varMap.find? { expr } then
     return var
   let var : Var := (← get').vars.size
-  trace[grind.cutsat.internalize.term] "{expr} ↦ #{var}"
+  trace[grind.debug.cutsat.internalize] "{expr} ↦ #{var}"
   modify' fun s => { s with
     vars      := s.vars.push expr
     varMap    := s.varMap.insert { expr } var
@@ -27,7 +27,6 @@ def mkVarImpl (expr : Expr) : GoalM Var := do
     occurs    := s.occurs.push {}
     elimEqs   := s.elimEqs.push none
   }
-  trace[grind.debug.cutsat.markTerm] "mkVar: {expr}"
   markAsCutsatTerm expr
   assertNatCast expr var
   assertDenoteAsIntNonneg expr

tests/lean/run/grind_cutsat_diseq_1.lean

@@ -2,10 +2,12 @@ set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
-set_option trace.grind.debug.cutsat.diseq true
-set_option trace.grind.debug.cutsat.eq true
+set_option trace.grind.cutsat.assert true
 
-/-- info: [grind.debug.cutsat.diseq] a ≠ b -/
+/--
+info: [grind.cutsat.assert] a + b + 1 ≤ 0
+[grind.cutsat.assert] a + -1*b ≠ 0
+-/
 #guard_msgs (info) in
 example (a b : Int) : a + b < 0 → a ≠ b → False := by
   (fail_if_success grind); sorry
@@ -14,45 +16,63 @@ example (a b : Int) : a + b < 0 → a ≠ b → False := by
 example (a b : Int) : a ≠ b → False := by
   (fail_if_success grind); sorry
 
-/-- info: [grind.debug.cutsat.diseq] a ≠ b -/
+/--
+info: [grind.cutsat.assert] a + -1*b ≠ 0
+[grind.cutsat.assert] a + b + 1 ≤ 0
+-/
 #guard_msgs (info) in
 example (a b : Int) : a ≠ b → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
-/-- info: [grind.debug.cutsat.diseq] a ≠ b -/
+/--
+info: [grind.cutsat.assert] a + -1*b ≠ 0
+[grind.cutsat.assert] a + b + 1 ≤ 0
+-/
 #guard_msgs (info) in
 example (a b c : Int) : a ≠ c → c = b → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
-/-- info: [grind.debug.cutsat.diseq] a ≠ b -/
+/--
+info: [grind.cutsat.assert] a + -1*b ≠ 0
+[grind.cutsat.assert] a + b + 1 ≤ 0
+-/
 #guard_msgs (info) in
 example (a b c d : Int) : d ≠ c → c = b → a = d → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
-/-- info: [grind.debug.cutsat.diseq] a ≠ b -/
+/--
+info: [grind.cutsat.assert] a + b + 1 ≤ 0
+[grind.cutsat.assert] a + -1*b ≠ 0
+-/
 #guard_msgs (info) in
 example (a b c d : Int) : d ≠ c → a = d → a + b < 0 → c = b → False := by
   (fail_if_success grind); sorry
 
 /--
-info: [grind.debug.cutsat.diseq] a ≠ b
-[grind.debug.cutsat.eq] e = b
+info: [grind.cutsat.assert] a + b + 1 ≤ 0
+[grind.cutsat.assert] a + -1*b ≠ 0
+[grind.cutsat.assert] e + -1*b = 0
+[grind.cutsat.assert] -1*e + 1 ≤ 0
 -/
 #guard_msgs (info) in
 example (a b c d e : Int) : d ≠ c → a = d → a + b < 0 → c = b → c = e → e > 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-info: [grind.debug.cutsat.eq] b = e
-[grind.debug.cutsat.diseq] a ≠ e
+info: [grind.cutsat.assert] -1*e + 1 ≤ 0
+[grind.cutsat.assert] b + -1*e = 0
+[grind.cutsat.assert] a + -1*e ≠ 0
+[grind.cutsat.assert] a + b + 1 ≤ 0
 -/
 #guard_msgs (info) in
 example (a b c d e : Int) : d ≠ c → a = d → c = b → c = e → e > 0 → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-info: [grind.debug.cutsat.eq] b = e
-[grind.debug.cutsat.diseq] a ≠ e
+info: [grind.cutsat.assert] -1*e + 1 ≤ 0
+[grind.cutsat.assert] b + -1*e = 0
+[grind.cutsat.assert] a + b + 1 ≤ 0
+[grind.cutsat.assert] a + -1*e ≠ 0
 -/
 #guard_msgs (info) in
 example (a b c d e : Int) : a = d → c = b → c = e → e > 0 → a + b < 0 → d ≠ c → False := by

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -16,13 +16,11 @@ info: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
 [grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0
 [grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
 [grind.cutsat.assert] 「a + -2 * b + -2 * d」 ≠ 0
-[grind.cutsat.diseq] d + -1*c ≠ 0
 [grind.cutsat.assert] -1*d + c = 0
 [grind.cutsat.assert] 0 ≠ 0
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.assert true in
-set_option trace.grind.cutsat.diseq true in
 theorem ex₄ (a b c d : Int) : a = 2*b + 2*c → a - 2*b - 2*d ≠ 0 → c ≠ d := by
   grind
 

tests/lean/run/grind_cutsat_div_1.lean

@@ -21,64 +21,54 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3
 #print ex₄
 
 /--
-info: [grind.cutsat.assign] a := 1
-[grind.cutsat.assign] b := 0
+info: [grind.debug.cutsat.search.assign] a := 1
+[grind.debug.cutsat.search.assign] b := 0
 -/
 #guard_msgs (info) in -- finds the model without any backtracking
-set_option trace.grind.cutsat.assign true in
-set_option trace.grind.cutsat.conflict true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
   fail_if_success grind
   sorry
 
 /--
-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
+info: [grind.cutsat.assert] 2 ∣ a + 3
+[grind.cutsat.assert] 3 ∣ a + 3*b + -4
+[grind.debug.cutsat.search.assign] a := 1
+[grind.debug.cutsat.search.assign] b := 0
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.assign true in
-set_option trace.grind.cutsat.dvd true in
-set_option trace.grind.cutsat.dvd.solve.elim false in
-set_option trace.grind.cutsat.dvd.solve.combine false in
-set_option trace.grind.cutsat.dvd.trivial false in
-set_option trace.grind.cutsat.conflict true in
+set_option trace.grind.cutsat.assert true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
   fail_if_success grind
   sorry
 
 /--
-info: [grind.cutsat.assign] a := 1
-[grind.cutsat.assign] b := 15
+info: [grind.debug.cutsat.search.assign] a := 1
+[grind.debug.cutsat.search.assign] b := 15
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.assign true in
-set_option trace.grind.cutsat.conflict true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False := by
   fail_if_success grind
   sorry
 
 /--
-info: [grind.cutsat.assign] a := 1
-[grind.cutsat.assign] b := 12
+info: [grind.debug.cutsat.search.assign] a := 1
+[grind.debug.cutsat.search.assign] b := 12
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.assign true in
-set_option trace.grind.cutsat.conflict true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): False := by
   fail_if_success grind
   sorry
 
 /--
-info: [grind.cutsat.assign] f 0 := 11
-[grind.cutsat.assign] f 1 := 2
+info: [grind.debug.cutsat.search.assign] f 0 := 11
+[grind.debug.cutsat.search.assign] f 1 := 2
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.assign true in
-set_option trace.grind.cutsat.conflict true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (f : Int → Int) (_ : 2 ∣ f 0 + 3) (_ : 3 ∣ f 0 + f 1 - 4) (_ : f 0 ≥ 11): False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_eq_1.lean

@@ -2,15 +2,12 @@ set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 
--- set_option trace.grind.cutsat.assert true
--- set_option trace.grind.cutsat.internalize true
-
 /--
-info: [grind.cutsat.eq] -1*「b + f a + 1」 + b + f a + 1 = 0
-[grind.cutsat.eq] b + f a + 1 = 0
+info: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
+[grind.cutsat.assert] 「b + f a + 1」 = 0
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.eq true in
+set_option trace.grind.cutsat.assert true in
 example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_le_1.lean

@@ -2,11 +2,11 @@ set_option grind.warning false
 set_option grind.debug true
 
 /--
-info: [grind.cutsat.assign] b := -1
-[grind.cutsat.assign] a := 3
+info: [grind.debug.cutsat.search.assign] b := -1
+[grind.debug.cutsat.search.assign] a := 3
 -/
 #guard_msgs (info) in
-set_option trace.grind.cutsat.assign true in
+set_option trace.grind.debug.cutsat.search.assign true in
 example (a b : Int) (h₁ : a ≤ 3) (h₂ : a > 2) (h₃ : a + b < 3) : False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_nat_le.lean

@@ -29,11 +29,15 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
   grind
 
 /--
-info: [grind.debug.cutsat.eq] c = 0
+info: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
+[grind.cutsat.assert] -1*↑c ≤ 0
+[grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
 [grind.cutsat.assert] ↑c = 0
+[grind.cutsat.assert] 0 ≤ 0
+[grind.cutsat.assert] 「↑a * ↑b」 + 1 ≤ 0
+[grind.cutsat.assert] 1 ≤ 0
 -/
 #guard_msgs (info) in
-set_option trace.grind.debug.cutsat.eq true in
 set_option trace.grind.cutsat.assert true in
 example (a b c : Nat) : c > a * b → c >= 1 := by
   grind