Replace logInfos with trace messages (#1468)

Author: oluwatimilehin

SSA/Experimental/Bits/Generalize/Basic.lean

@@ -5,6 +5,7 @@ open Lean.Meta
 open Std.Sat
 open Std.Tactic.BVDecide
 
+initialize Lean.registerTraceClass `Generalize
 
 namespace Generalize
 /--

SSA/Experimental/Bits/Generalize/Generalize.lean

@@ -7,8 +7,6 @@ import SSA.Core.Util
 import SSA.Experimental.Bits.Generalize.Basic
 import SSA.Experimental.Bits.Generalize.Reflect
 
-initialize Lean.registerTraceClass `Generalize
-
 open Lean
 open Lean.Meta
 open Std.Sat
@@ -269,7 +267,7 @@ elab "#reducewidth" expr:term " : " target:term : command =>
       let some targetWidth ← getNatValue? targetExpr | throwError "Invalid width provided"
 
       let hExpr ← Term.elabTerm expr none
-      logInfo m! "hexpr: {hExpr}"
+      trace[Generalize] m! "hexpr: {hExpr}"
 
       match_expr hExpr with
       | Eq _ lhsExpr rhsExpr =>
@@ -278,7 +276,7 @@ elab "#reducewidth" expr:term " : " target:term : command =>
 
            let bvExpr := parsedBvExpr.bvLogicalExpr
            let state := parsedBvExpr.state
-           logInfo m! "bvExpr: {bvExpr}, state: {state}"
+           trace[Generalize] m! "bvExpr: {bvExpr}, state: {state}"
 
            let initialGeneralizerState : GeneralizerState :=
                 { startTime                := 0
@@ -452,7 +450,7 @@ def pruneEquivalentBVExprs (expressions: List (GenBVExpr w)) : GeneralizerStateM
       if let some _ ← solve subsumeCheckExpr then
         pruned := expr :: pruned
 
-    logInfo m! "Removed {expressions.length - pruned.length} expressions after pruning {expressions.length} expressions"
+    trace[Generalize] m! "Removed {expressions.length - pruned.length} expressions after pruning {expressions.length} expressions"
 
     pure pruned
 
@@ -906,6 +904,7 @@ def synthesizeWithNoPrecondition (constantAssignments : List (Std.HashMap Nat BV
         while currentLevel < lhs.symVars.size do
           logInfo m! "Expression Synthesis Processing level {currentLevel}"
 
+          --
           let bottomUpRes ← constantExprsEnumerationFromCache allLHSVars lhsAssignments rhsAssignments ops
           for (var, exprs) in bottomUpRes.toArray do
             let existingExprs := exprSynthesisResults.getD var []

SSA/Experimental/Bits/Generalize/Reflect.lean

@@ -5,13 +5,11 @@ import SSA.Experimental.Bits.Generalize.Basic
 
 namespace Generalize
 
-
 open Lean
 open Lean.Meta
 open Std.Sat
 open Std.Tactic.BVDecide
 
-
 structure ParsedBVExprState where
   maxFreeVarId : Nat
   numSymVars :  Nat
@@ -110,13 +108,10 @@ partial def toBVExpr (expr : Expr) (targetWidth: Nat) : ParseBVExprM (Option (BV
     | BitVec.rotateRight _ innerExpr distanceExpr =>
         rotateReflection innerExpr distanceExpr BVUnOp.rotateRight
     | BitVec.zeroExtend _ nExpr vExpr =>
-        logInfo m! "matched zero extend: {vExpr}"
         let some n ← getNatValue? nExpr | return none
-        logInfo m! "vExpr: {vExpr}"
         let some v ← go vExpr | return none
         return some {bvExpr := GenBVExpr.zeroExtend n v.bvExpr, width := _}
     | BitVec.truncate _ nExpr vExpr =>
-      logInfo m! "matched truncate: {vExpr}"
       let some n ← getNatValue? nExpr | return none
       let some v ← go vExpr | return none
       return some {bvExpr := GenBVExpr.truncate n v.bvExpr, width := _}
@@ -205,7 +200,6 @@ partial def toBVExpr (expr : Expr) (targetWidth: Nat) : ParseBVExprM (Option (BV
         return some {bvExpr := GenBVExpr.const (BitVec.ofNat n v), width := n}
 
   getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := OptionT.run do
-    logInfo m! "parsing: {e}"
     match_expr e with
     | BitVec.ofNat nExpr vExpr =>
       let n ← getNatValue? nExpr
@@ -264,11 +258,11 @@ def parseExprs (lhsExpr rhsExpr : Expr) (targetWidth : Nat): ParseBVExprM (Optio
 
   let rhs: ParsedBVExpr := {bvExpr := rhsRes.bvExpr, width := rhsRes.width, symVars := rhsSymVars, inputVars := rhsInputVars}
 
-  logInfo m! "lhs width: {lhsRes.width}; rhs width: {rhsRes.width}"
+  trace[Generalize] m! "lhs width: {lhsRes.width}; rhs width: {rhsRes.width}"
   if h : lhsRes.width = rhsRes.width then
     let rhsExpr := h ▸ rhsRes.bvExpr
     let bvLogicalExpr := BoolExpr.literal (GenBVPred.bin lhsRes.bvExpr BVBinPred.eq rhsExpr)
-    logInfo m! "BVLogicalExpr: {bvLogicalExpr}"
+    trace[Generalize] m! "BVLogicalExpr: {bvLogicalExpr}"
 
     return some {lhs := lhs, rhs := rhs, state := state, bvLogicalExpr := bvLogicalExpr}