[sledge] Add number of solver steps to reported statistics

Reviewed By: jvillard

Differential Revision: D25756555

fbshipit-source-id: 8d5e8a141

sledge/report/sledge_report.ml

@@ -90,7 +90,8 @@ let add_cov base_cov cov row =
             Report.
               { steps= cov.steps - base_cov.steps
               ; hit= cov.hit - base_cov.hit
-              ; fraction= cov.fraction -. base_cov.fraction }
+              ; fraction= cov.fraction -. base_cov.fraction
+              ; solver_steps= cov.solver_steps - base_cov.solver_steps }
           in
           Some (covd :: Option.value row.cov_deltas ~default:[])
       | _ -> None
@@ -333,6 +334,8 @@ let write_html ranges rows chan =
           <th>%%</th>
           <th>&Delta;<br></th>
           <th>&Delta;%%<br></th>
+          <th>Solver<br>Steps</th>
+          <th>&Delta;<br></th>
         </tr>|} ;
   pf "\n" ;
   Iter.iter rows ~f:(fun row ->
@@ -408,6 +411,15 @@ let write_html ranges rows chan =
                   Printf.fprintf ppf "<td %s align=\"right\">%i</td>\n" attr
                     steps )
       in
+      let solver_steps attr ppf = function
+        | [] -> Printf.fprintf ppf "<td %s></td>\n" attr
+        | cs ->
+            List.iter cs ~f:(fun {Report.solver_steps} ->
+                if solver_steps = 0 then Printf.fprintf ppf "<td></td>\n"
+                else
+                  Printf.fprintf ppf "<td %s align=\"right\">%i</td>\n" attr
+                    solver_steps )
+      in
       let hit attr ppf = function
         | [] -> Printf.fprintf ppf "<td %s></td>\n" attr
         | cs ->
@@ -520,6 +532,9 @@ let write_html ranges rows chan =
         (hit " style=\"border-left: 2px solid #eee8d5\";")
         cov (coverage "") cov ;
       pf "%a%a" (coveraged hit) cov_deltas (coveraged coverage) cov_deltas ;
+      pf "%a%a"
+        (solver_steps " style=\"border-left: 2px solid #eee8d5\";")
+        cov (coveraged solver_steps) cov_deltas ;
       pf "</tr>\n" ) ;
   pf "<table>\n" ;
   pf "</body></html>\n"

sledge/src/report.ml

@@ -40,6 +40,8 @@ let invalid_access_term fmt_thunk term =
 
 (** Functional statistics *)
 
+let solver_steps = ref 0
+let step_solver () = Int.incr solver_steps
 let steps = ref 0
 let hit_insts = Llair.Inst.Tbl.create ()
 let hit_terms = Llair.Term.Tbl.create ()
@@ -101,7 +103,7 @@ type times =
   {etime: float; utime: float; stime: float; cutime: float; cstime: float}
 [@@deriving sexp]
 
-type coverage = {steps: int; hit: int; fraction: float}
+type coverage = {steps: int; hit: int; fraction: float; solver_steps: int}
 [@@deriving compare, equal, sexp]
 
 type entry =
@@ -171,6 +173,7 @@ let coverage (pgm : Llair.program) =
     Llair.Inst.Tbl.length hit_insts + Llair.Term.Tbl.length hit_terms
   in
   let fraction = Float.(of_int hit /. of_int size) in
-  output (Coverage {steps= !steps; hit; fraction})
+  output
+    (Coverage {steps= !steps; hit; fraction; solver_steps= !solver_steps})
 
 let status s = output (Status s)

sledge/src/report.mli

@@ -8,6 +8,7 @@
 (** Issue reporting *)
 
 val init : ?append:bool -> string -> unit
+val step_solver : unit -> unit
 val step_inst : Llair.inst -> unit
 val step_term : Llair.term -> unit
 val hit_bound : int -> unit
@@ -42,7 +43,7 @@ type times =
   {etime: float; utime: float; stime: float; cutime: float; cstime: float}
 [@@deriving sexp]
 
-type coverage = {steps: int; hit: int; fraction: float}
+type coverage = {steps: int; hit: int; fraction: float; solver_steps: int}
 [@@deriving compare, equal, sexp]
 
 type entry =

sledge/src/solver.ml

@@ -639,6 +639,7 @@ let pure_entails x q = Sh.is_empty q && Context.implies x (Sh.pure_approx q)
 
 let rec excise ({min; xs; sub; zs; pgs} as goal) =
   [%Trace.info "@[<2>excise@ %a@]" pp goal] ;
+  Report.step_solver () ;
   if Sh.is_unsat min then Some (Sh.false_ (Var.Set.diff sub.us zs))
   else if pure_entails min.ctx sub then
     Some (Sh.exists zs (Sh.extend_us xs min))