Skip to content

Commit 90e6f97

Browse files
leodemouraleodemoura
committed
chore: trace messages cutsat => lia
1 parent ecfe122 commit 90e6f97

File tree

11 files changed

+93
-93
lines changed

11 files changed

+93
-93
lines changed

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

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -23,26 +23,26 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
2323
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Action
2424
public section
2525
namespace Lean.Meta.Grind.Arith.Cutsat
26-
builtin_initialize registerTraceClass `grind.cutsat
27-
builtin_initialize registerTraceClass `grind.cutsat.nonlinear
28-
builtin_initialize registerTraceClass `grind.cutsat.model
29-
builtin_initialize registerTraceClass `grind.cutsat.assert
30-
builtin_initialize registerTraceClass `grind.cutsat.assert.trivial
31-
builtin_initialize registerTraceClass `grind.cutsat.assert.unsat
32-
builtin_initialize registerTraceClass `grind.cutsat.assert.store
33-
builtin_initialize registerTraceClass `grind.cutsat.assert.nonlinear
26+
builtin_initialize registerTraceClass `grind.lia
27+
builtin_initialize registerTraceClass `grind.lia.nonlinear
28+
builtin_initialize registerTraceClass `grind.lia.model
29+
builtin_initialize registerTraceClass `grind.lia.assert
30+
builtin_initialize registerTraceClass `grind.lia.assert.trivial
31+
builtin_initialize registerTraceClass `grind.lia.assert.unsat
32+
builtin_initialize registerTraceClass `grind.lia.assert.store
33+
builtin_initialize registerTraceClass `grind.lia.assert.nonlinear
3434

35-
builtin_initialize registerTraceClass `grind.debug.cutsat.subst
36-
builtin_initialize registerTraceClass `grind.debug.cutsat.search
37-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.split (inherited := true)
38-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.assign (inherited := true)
39-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.conflict (inherited := true)
40-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.backtrack (inherited := true)
41-
builtin_initialize registerTraceClass `grind.debug.cutsat.internalize
42-
builtin_initialize registerTraceClass `grind.debug.cutsat.toInt
43-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.cnstrs
44-
builtin_initialize registerTraceClass `grind.debug.cutsat.search.reorder
45-
builtin_initialize registerTraceClass `grind.debug.cutsat.elimEq
35+
builtin_initialize registerTraceClass `grind.debug.lia.subst
36+
builtin_initialize registerTraceClass `grind.debug.lia.search
37+
builtin_initialize registerTraceClass `grind.debug.lia.search.split (inherited := true)
38+
builtin_initialize registerTraceClass `grind.debug.lia.search.assign (inherited := true)
39+
builtin_initialize registerTraceClass `grind.debug.lia.search.conflict (inherited := true)
40+
builtin_initialize registerTraceClass `grind.debug.lia.search.backtrack (inherited := true)
41+
builtin_initialize registerTraceClass `grind.debug.lia.internalize
42+
builtin_initialize registerTraceClass `grind.debug.lia.toInt
43+
builtin_initialize registerTraceClass `grind.debug.lia.search.cnstrs
44+
builtin_initialize registerTraceClass `grind.debug.lia.search.reorder
45+
builtin_initialize registerTraceClass `grind.debug.lia.elimEq
4646

4747
builtin_initialize
4848
cutsatExt.setMethods

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.Ri
5555
let p'' ← toPoly e'
5656
if p == p'' then return none
5757
modify' fun s => { s with usedCommRing := true }
58-
trace[grind.cutsat.assert.nonlinear] "{← p.pp} ===> {← p''.pp}"
58+
trace[grind.lia.assert.nonlinear] "{← p.pp} ===> {← p''.pp}"
5959
return some (re, p', p'')
6060

6161
end Lean.Meta.Grind.Arith.Cutsat

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ def DvdCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DvdC
4040
let q := c₂.p
4141
let d := Int.ofNat (a * c₂.d).natAbs
4242
let p := (q.mul a |>.combine (p.mul (-b)))
43-
trace[grind.debug.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
43+
trace[grind.debug.lia.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
4444
return { d, p, h := .subst x c₁ c₂ }
4545

4646
partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDepth do
@@ -52,14 +52,14 @@ partial def DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr := withIncRecDe
5252
/-- Asserts divisibility constraint. -/
5353
partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
5454
if (← inconsistent) then return ()
55-
trace[grind.cutsat.assert] "{← c.pp}"
55+
trace[grind.lia.assert] "{← c.pp}"
5656
let c ← c.norm.applySubsts
5757
if c.isUnsat then
58-
trace[grind.cutsat.assert.unsat] "{← c.pp}"
58+
trace[grind.lia.assert.unsat] "{← c.pp}"
5959
setInconsistent (.dvd c)
6060
return ()
6161
if c.isTrivial then
62-
trace[grind.cutsat.assert.trivial] "{← c.pp}"
62+
trace[grind.lia.assert.trivial] "{← c.pp}"
6363
return ()
6464
let d₁ := c.d
6565
let .add a₁ x p₁ := c.p | c.throwUnexpected
@@ -87,7 +87,7 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
8787
let elim := { d, p := a₂_p₁.combine a₁_p₂, h := .solveElim c c' : DvdCnstr }
8888
elim.assert
8989
else
90-
trace[grind.cutsat.assert.store] "{← c.pp}"
90+
trace[grind.lia.assert.store] "{← c.pp}"
9191
c.p.updateOccs
9292
modify' fun s => { s with dvds := s.dvds.set x (some c) }
9393

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

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ private def _root_.Int.Linear.Poly.substVar (p : Poly) : GoalM (Option (Var × E
2323
let some (a, x, c) ← p.findVarToSubst | return none
2424
let b := c.p.coeff x
2525
let p' := p.mul (-b) |>.combine (c.p.mul a)
26-
trace[grind.debug.cutsat.subst] "{← p.pp}, {a}, {← getVar x}, {← c.pp}, {b}, {← p'.pp}"
26+
trace[grind.debug.lia.subst] "{← p.pp}, {a}, {← getVar x}, {← c.pp}, {b}, {← p'.pp}"
2727
return some (x, c, p')
2828

2929
def EqCnstr.norm (c : EqCnstr) : EqCnstr :=
@@ -46,12 +46,12 @@ def DiseqCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : Di
4646
let p := c₁.p
4747
let q := c₂.p
4848
let p := p.mul b |>.combine (q.mul (-a))
49-
trace[grind.debug.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
49+
trace[grind.debug.lia.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
5050
return { p, h := .subst x c₁ c₂ }
5151

5252
partial def DiseqCnstr.applySubsts (c : DiseqCnstr) : GoalM DiseqCnstr := withIncRecDepth do
5353
let some (x, c₁, p) ← c.p.substVar | return c
54-
trace[grind.debug.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
54+
trace[grind.debug.lia.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
5555
applySubsts { p, h := .subst x c₁ c }
5656

5757
/--
@@ -73,14 +73,14 @@ private def DiseqCnstr.findLe (c : DiseqCnstr) : GoalM Bool := do
7373

7474
def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
7575
if (← inconsistent) then return ()
76-
trace[grind.cutsat.assert] "{← c.pp}"
76+
trace[grind.lia.assert] "{← c.pp}"
7777
let c ← c.norm.applySubsts
7878
if c.p.isUnsatDiseq then
79-
trace[grind.cutsat.assert.unsat] "{← c.pp}"
79+
trace[grind.lia.assert.unsat] "{← c.pp}"
8080
setInconsistent (.diseq c)
8181
return ()
8282
if c.isTrivial then
83-
trace[grind.cutsat.assert.trivial] "{← c.pp}"
83+
trace[grind.lia.assert.trivial] "{← c.pp}"
8484
return ()
8585
let k := c.p.gcdCoeffs c.p.getConst
8686
let c := if k == 1 then
@@ -91,7 +91,7 @@ def DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit := do
9191
return ()
9292
let .add _ x _ := c.p | c.throwUnexpected
9393
c.p.updateOccs
94-
trace[grind.cutsat.assert.store] "{← c.pp}"
94+
trace[grind.lia.assert.store] "{← c.pp}"
9595
modify' fun s => { s with diseqs := s.diseqs.modify x (·.push c) }
9696
if (← c.satisfied) == .false then
9797
resetAssignmentFrom x
@@ -117,7 +117,7 @@ where
117117

118118
partial def EqCnstr.applySubsts (c : EqCnstr) : GoalM EqCnstr := withIncRecDepth do
119119
let some (x, c₁, p) ← c.p.substVar | return c
120-
trace[grind.debug.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
120+
trace[grind.debug.lia.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
121121
applySubsts { p, h := .subst x c₁ c : EqCnstr }
122122

123123
private def updateDvdCnstr (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Unit := do
@@ -295,7 +295,7 @@ private def updateElimEqs (a : Int) (x : Var) (c : EqCnstr) (y : Var) : GoalM Un
295295
let b := c₂.p.coeff x
296296
if b == 0 then return ()
297297
let c₂ := { p := c₂.p.mul a |>.combine (c.p.mul (-b)), h := .subst x c₂ c : EqCnstr }
298-
trace[grind.debug.cutsat.elimEq] "updated: {← getVar y}, {← c₂.pp}"
298+
trace[grind.debug.lia.elimEq] "updated: {← getVar y}, {← c₂.pp}"
299299
modify' fun s => { s with elimEqs := s.elimEqs.set y (some c₂) }
300300
propagateNonlinearTerms y
301301

@@ -338,14 +338,14 @@ partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Go
338338
@[export lean_grind_cutsat_assert_eq]
339339
def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
340340
if (← inconsistent) then return ()
341-
trace[grind.cutsat.assert] "{← c.pp}"
341+
trace[grind.lia.assert] "{← c.pp}"
342342
let c ← c.norm.applySubsts
343343
if c.p.isUnsatEq then
344-
trace[grind.cutsat.assert.unsat] "{← c.pp}"
344+
trace[grind.lia.assert.unsat] "{← c.pp}"
345345
setInconsistent (.eq c)
346346
return ()
347347
if c.isTrivial then
348-
trace[grind.cutsat.assert.trivial] "{← c.pp}"
348+
trace[grind.lia.assert.trivial] "{← c.pp}"
349349
return ()
350350
let k := c.p.gcdCoeffs'
351351
if c.p.getConst % k > 0 then
@@ -356,9 +356,9 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
356356
else
357357
{ p := c.p.div k, h := .divCoeffs c }
358358
let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
359-
trace[grind.debug.cutsat.subst] ">> {← getVar x}, {← c.pp}"
360-
trace[grind.cutsat.assert.store] "{← c.pp}"
361-
trace[grind.debug.cutsat.elimEq] "{← getVar x}, {← c.pp}"
359+
trace[grind.debug.lia.subst] ">> {← getVar x}, {← c.pp}"
360+
trace[grind.lia.assert.store] "{← c.pp}"
361+
trace[grind.debug.lia.elimEq] "{← getVar x}, {← c.pp}"
362362
if (← c.satisfied) == .false then
363363
resetAssignmentFrom x
364364
modify' fun s => { s with
@@ -539,7 +539,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
539539
private def internalizeInt (e : Expr) : GoalM Unit := do
540540
if (← hasVar e) then return ()
541541
let p ← toPoly e
542-
trace[grind.debug.cutsat.internalize] "{aquote e}:= {← p.pp}"
542+
trace[grind.debug.lia.internalize] "{aquote e}:= {← p.pp}"
543543
let x ← mkVar e
544544
if p == .add 1 x (.num 0) then
545545
-- It is pointless to assert `x = x`
@@ -632,7 +632,7 @@ private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
632632

633633
private def internalizeIntTerm (e type : Expr) (parent? : Option Expr) (k : SupportedTermKind) : GoalM Unit := do
634634
if isForbiddenParent parent? k then return ()
635-
trace[grind.debug.cutsat.internalize] "{e} : {type}"
635+
trace[grind.debug.lia.internalize] "{e} : {type}"
636636
match k with
637637
| .div => propagateDiv e
638638
| .mod => propagateMod e
@@ -656,8 +656,8 @@ private def internalizeNatTerm (e type : Expr) (parent? : Option Expr) (k : Supp
656656
if isForbiddenParent parent? k then return ()
657657
if (← get').natToIntMap.contains { expr := e } then return ()
658658
let e'h ← natToInt e
659-
trace[grind.debug.cutsat.internalize] "{e} : {type}"
660-
trace[grind.debug.cutsat.toInt] "{e} ==> {e'h.1}"
659+
trace[grind.debug.lia.internalize] "{e} : {type}"
660+
trace[grind.debug.lia.toInt] "{e} ==> {e'h.1}"
661661
modify' fun s => { s with
662662
natToIntMap := s.natToIntMap.insert { expr := e } e'h
663663
}
@@ -686,8 +686,8 @@ private def internalizeNatTerm (e type : Expr) (parent? : Option Expr) (k : Supp
686686
private def internalizeToIntTerm (e type : Expr) : GoalM Unit := do
687687
if (← isToIntTerm e) then return () -- already internalized
688688
if let some (eToInt, he) ← toInt? e type then
689-
trace[grind.debug.cutsat.internalize] "{e} : {type}"
690-
trace[grind.debug.cutsat.toInt] "{e} ==> {eToInt}"
689+
trace[grind.debug.lia.internalize] "{e} : {type}"
690+
trace[grind.debug.lia.toInt] "{e} ==> {eToInt}"
691691
let α := type
692692
modify' fun s => { s with
693693
toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α }

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ def LeCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : LeCns
3939
q.mul a |>.combine (p.mul (-b))
4040
else
4141
p.mul b |>.combine (q.mul (-a))
42-
trace[grind.cutsat.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
42+
trace[grind.lia.subst] "{← getVar x}, {← c₁.pp}, {← c₂.pp}"
4343
return { p, h := .subst x c₁ c₂ }
4444

4545
partial def LeCnstr.applySubsts (c : LeCnstr) : GoalM LeCnstr := withIncRecDepth do
@@ -74,7 +74,7 @@ private def findEq (c : LeCnstr) : GoalM Bool := do
7474
if c.p.isNegEq c'.p then
7575
c'.erase
7676
let eq := { p := c.p, h := .ofLeGe c c' : EqCnstr }
77-
trace[grind.debug.cutsat.eq] "new eq: {← eq.pp}"
77+
trace[grind.debug.lia.eq] "new eq: {← eq.pp}"
7878
eq.assert
7979
return true
8080
return false
@@ -103,20 +103,20 @@ where
103103
@[export lean_grind_cutsat_assert_le]
104104
def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
105105
if (← inconsistent) then return ()
106-
trace[grind.cutsat.assert] "{← c.pp}"
106+
trace[grind.lia.assert] "{← c.pp}"
107107
let c ← c.norm.applySubsts
108108
if c.isUnsat then
109-
trace[grind.cutsat.assert.unsat] "{← c.pp}"
109+
trace[grind.lia.assert.unsat] "{← c.pp}"
110110
setInconsistent (.le c)
111111
return ()
112112
if c.isTrivial then
113-
trace[grind.cutsat.assert.trivial] "{← c.pp}"
113+
trace[grind.lia.assert.trivial] "{← c.pp}"
114114
return ()
115115
let .add a x _ := c.p | c.throwUnexpected
116116
if (← findEq c) then
117117
return ()
118118
let c ← refineWithDiseq c
119-
trace[grind.cutsat.assert.store] "{← c.pp}"
119+
trace[grind.lia.assert.store] "{← c.pp}"
120120
c.p.updateOccs
121121
if a < 0 then
122122
modify' fun s => { s with lowers := s.lowers.modify x (·.push c) }

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
7373
let some v := model[i]? | pure ()
7474
model := assignEqc goal n v model
7575
let r ← finalizeModel goal isIntNatENode model
76-
traceModel `grind.cutsat.model r
76+
traceModel `grind.lia.model r
7777
return r
7878

7979
end Lean.Meta.Grind.Arith.Cutsat

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -325,7 +325,7 @@ private def mkPowEqProof (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Opt
325325
mutual
326326
@[export lean_cutsat_eq_cnstr_to_proof]
327327
private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := caching c' do
328-
trace[grind.debug.cutsat.proof] "{← c'.pp}"
328+
trace[grind.debug.lia.proof] "{← c'.pp}"
329329
match c'.h with
330330
| .core0 a zero =>
331331
mkEqProof a zero
@@ -377,7 +377,7 @@ private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := cach
377377
| .pow ka ca? kb cb? => mkPowEqProof ka ca? kb cb? c'
378378

379379
private partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
380-
trace[grind.debug.cutsat.proof] "{← c'.pp}"
380+
trace[grind.debug.lia.proof] "{← c'.pp}"
381381
match c'.h with
382382
| .core e =>
383383
mkOfEqTrue (← mkEqTrueProof e)
@@ -441,7 +441,7 @@ private partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := cachin
441441
return mkApp6 (mkConst ``Int.Linear.dvd_norm_poly) (← getContext) (toExpr c.d) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
442442

443443
private partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
444-
trace[grind.debug.cutsat.proof] "{← c'.pp}"
444+
trace[grind.debug.lia.proof] "{← c'.pp}"
445445
match c'.h with
446446
| .core e =>
447447
mkOfEqTrue (← mkEqTrueProof e)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -162,8 +162,8 @@ def reorderVars : GoalM Unit := do
162162
for c in dvds do c.assert
163163
for c in ineqs do c.assert
164164
for c in diseqs do c.assert
165-
trace[grind.debug.cutsat.search.reorder] "new2old: {new2old}"
166-
trace[grind.debug.cutsat.search.reorder] "old2new: {old2new}"
165+
trace[grind.debug.lia.search.reorder] "new2old: {new2old}"
166+
trace[grind.debug.lia.search.reorder] "old2new: {old2new}"
167167
checkInvariants
168168

169169
end Lean.Meta.Grind.Arith.Cutsat

0 commit comments

Comments
 (0)