Add profiling information. (#134)

Smt/Reconstruct.lean

@@ -57,20 +57,20 @@ where
         return e
     throwError "Failed to reconstruct sort {s} with kind {s.getKind}"
 
-def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : ReconstructM MessageData :=
-  return m!"{t} ↦ " ++ match r with
-    | .ok e    => m!"{e}"
-    | .error _ => m!"{bombEmoji}"
-
 def withNewTermCache (k : ReconstructM α) : ReconstructM α := do
   let termCache := (← get).termCache
   modify fun state => { state with termCache := {} }
   let r ← k
   modify fun state => { state with termCache := termCache }
   return r
 
+def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : ReconstructM MessageData :=
+  return m!"{t} ↦ " ++ match r with
+    | .ok e    => m!"{e}"
+    | .error _ => m!"{bombEmoji}"
+
 def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t => do
-  withTraceNode `smt.reconstruct.term (traceReconstructTerm t) do
+  withTraceNode ((`smt.reconstruct.term).str t.getKind.toString) (traceReconstructTerm t) do
     let rs ← getReconstructors ``TermReconstructor TermReconstructor
     go rs t
 where
@@ -155,11 +155,17 @@ def addTrust (type : Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
     m!"rule : {pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}"
   return mv
 
+def traceReconstructStep (r : Except Exception Expr) : ReconstructM MessageData :=
+  return match r with
+  | .ok _ => m!"{checkEmoji}"
+  | _     => m!"{bombEmoji}"
+
 partial def reconstructProof : cvc5.Proof → ReconstructM Expr := withProofCache fun pf => do
   let rs ← getReconstructors ``ProofReconstructor ProofReconstructor
   go rs pf
 where
-  go (rs : List (ProofReconstructor × Name)) (pf : cvc5.Proof) : ReconstructM Expr := do
+  go (rs : List (ProofReconstructor × Name)) (pf : cvc5.Proof) : ReconstructM Expr :=
+  withTraceNode ((`smt.reconstruct.proof).str pf.getRule.toString) traceReconstructStep do
     for (r, _) in rs do
       if let some e ← r pf then
         return e

Smt/Reconstruct/Bool/Tactic.lean

@@ -13,7 +13,12 @@ namespace Smt.Reconstruct.Bool
 
 open Lean
 
-def boolify (mv : MVarId) : MetaM MVarId := do
+def traceBoolify (r : Except Exception MVarId) : MetaM MessageData :=
+  return match r with
+  | .ok _ => m!"{checkEmoji}"
+  | _     => m!"{bombEmoji}"
+
+def boolify (mv : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruct.boolify traceBoolify do
   let ns := [``Bool.decide_eq_true, ``decide_true_eq, ``decide_false_eq, ``decide_not_eq, ``decide_and_eq, ``decide_or_eq, ``decide_eq_eq, ``decide_xor_eq]
   let simpTheorems ← ns.foldrM (fun n a => a.addTheorem (.decl n) (.const n [])) {}
   let (some mv, _) ← Meta.simpTarget mv { simpTheorems } | throwError "failed to boolify goal:{mv}"

Smt/Reconstruct/Builtin/AC.lean

@@ -6,13 +6,8 @@ namespace Lean.Meta.AC
 
 open Lean.Elab Tactic
 
-def traceACRflTop (r : Except Exception Unit) : MetaM MessageData :=
-  return match r with
-  | .ok _ => m!"{checkEmoji}"
-  | _     => m!"{bombEmoji}"
-
 /-- Similar to `rewriteUnnormalized`, but rewrite is only applied at the top level. -/
-def rewriteUnnormalizedTop (mv : MVarId) : MetaM Unit := withTraceNode `smt.reconstruct.acRflTop traceACRflTop do
+def rewriteUnnormalizedTop (mv : MVarId) : MetaM Unit := do
   let some (α, l, r) := (← mv.getType).eq?
     | throwError "[ac_rfl_top] expected a top level equality with AC operator on lhs and/or rhs, got {← mv.getType}"
   let lvl ← Meta.getLevel α

Smt/Reconstruct/Prop.lean

@@ -185,6 +185,12 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
     addThm q(ite $c $p $c = ite $c $p False) q(@Prop.ite_else_lookahead_self $c $p $h)
+  | .BOOL_NOT_ITE_ELIM =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[3]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q((¬ite $c $p $q) = ite $c (¬$p) (¬$q)) q(@Prop.bool_not_ite_elim $c $p $q $h)
   | _ => return none
 where
   reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do

Smt/Reconstruct/Prop/Rewrites.lean

@@ -126,4 +126,8 @@ theorem ite_else_lookahead_self [h : Decidable c] : ite c x c = ite c x False :=
   (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
   (fun hnc => if_neg hnc ▸ if_neg hnc ▸ eq_false hnc)
 
+theorem bool_not_ite_elim [h : Decidable c] : (¬ite c x y) = ite c (¬x) (¬y) := h.byCases
+  (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
+  (fun hnc => if_neg hnc ▸ if_neg hnc ▸ rfl)
+
 end Smt.Reconstruct.Prop

Smt/Reconstruct/Rewrite.lean

@@ -23,7 +23,7 @@ def traceSmtRw (r : Except Exception Unit) : MetaM MessageData :=
   | _     => m!"{bombEmoji}"
 
 def smtRw (mv : MVarId) (op : Expr) (id : Expr) (rr : Expr) (xss : Array (Array Expr)) : MetaM Unit :=
-  withTraceNode `smt.reconstruct.smtRw traceSmtRw do
+  withTraceNode `smt.reconstruct.DSL_REWRITE.tac traceSmtRw do
   let xs := xss.map (fun xs => xs[1:].foldr (mkApp2 op) (xs[0]?.getD id))
   let some (α, l, r) := (← mv.getType).eq?
     | throwError "[smt_rw] expected a top level equality with AC operator on lhs and/or rhs, got {← mv.getType}"

Test/Int/linarith.lean

@@ -84,8 +84,6 @@ example (prime : Int → Prop) (w x y z : Int) (h1 : 4*x + (-3)*y + 6*w ≤ 0) (
     (h5 : prime x) : False := by
   smt [h1, h2, h3, h4]
 
--- set_option maxRecDepth 2000000
-
 example (u v x y A B : Int)
 (a : 0 < A)
 (a_1 : 0 <= 1 - A)