]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/saturation.ml
profiling experiments...
[helm.git] / helm / ocaml / paramodulation / saturation.ml
index 4c1480d100c86a72a88ee652de5d4dcd5d697a69..25314a100794c5fda5094dabd49c6d432f6ca309 100644 (file)
@@ -7,21 +7,13 @@ type result =
 ;;
 
 
-type equality_sign = Negative | Positive;;
-
-let string_of_sign = function
-  | Negative -> "Negative"
-  | Positive -> "Positive"
-;;
-
-
 (*
 let symbols_of_equality (_, (_, left, right), _, _) =
   TermSet.union (symbols_of_term left) (symbols_of_term right)
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
+let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -49,8 +41,8 @@ struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right), _, _ = eq1
-        and _, (ty', left', right'), _, _ = eq2 in
+        let _, (ty, left, right, _), _, _ = eq1
+        and _, (ty', left', right', _), _, _ = eq2 in
         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
@@ -69,10 +61,10 @@ let symbols_ratio = ref 0;;
 let symbols_counter = ref 0;;
 
 
-let select env passive active =
-  let (neg_list, neg_set), (pos_list, pos_set) = passive in
+let select env passive (active, _) =
+  let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
   let remove eq l =
-    List.filter (fun e -> not (e = eq)) l
+    List.filter (fun e -> e <> eq) l
   in
   if !weight_age_ratio > 0 then
     weight_age_counter := !weight_age_counter - 1;
@@ -81,9 +73,13 @@ let select env passive active =
       weight_age_counter := !weight_age_ratio;
       match neg_list, pos_list with
       | hd::tl, pos ->
-          (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set))
+          (* Negatives aren't indexed, no need to remove them... *)
+          (Negative, hd),
+          ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
       | [], hd::tl ->
-          (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set))
+          let passive_table = Indexing.remove_index passive_table hd in
+          (Positive, hd),
+          (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
       | _, _ -> assert false
     )
   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
@@ -133,14 +129,17 @@ let select env passive active =
           let _, current = EqualitySet.fold f pos_set initial in
 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 (*             (string_of_equality ~env current); *)
+          let passive_table = Indexing.remove_index passive_table current in
           (Positive, current),
           (([], neg_set),
-           (remove current pos_list, EqualitySet.remove current pos_set))
+           (remove current pos_list, EqualitySet.remove current pos_set),
+           passive_table)
       | _ ->
             let current = EqualitySet.min_elt pos_set in
           let passive =
             (neg_list, neg_set),
-            (remove current pos_list, EqualitySet.remove current pos_set)
+            (remove current pos_list, EqualitySet.remove current pos_set),
+            Indexing.remove_index passive_table current
           in
           (Positive, current), passive
     )
@@ -151,14 +150,16 @@ let select env passive active =
         let current = set_selection pos_set in
         let passive =
           (neg_list, neg_set),
-          (remove current pos_list, EqualitySet.remove current pos_set)
+          (remove current pos_list, EqualitySet.remove current pos_set),
+          Indexing.remove_index passive_table current
         in
         (Positive, current), passive
       else
         let current = set_selection neg_set in
         let passive =
           (remove current neg_list, EqualitySet.remove current neg_set),
-          (pos_list, pos_set)
+          (pos_list, pos_set),
+          passive_table
         in
         (Negative, current), passive
 ;;
@@ -168,24 +169,34 @@ let make_passive neg pos =
   let set_of equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
   in
-  (neg, set_of neg), (pos, set_of pos)
+  let table = Hashtbl.create (List.length pos) in
+  (neg, set_of neg),
+  (pos, set_of pos),
+  List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+;;
+
+
+let make_active () =
+  [], Hashtbl.create 1
 ;;
 
 
 let add_to_passive passive (new_neg, new_pos) =
-  let (neg_list, neg_set), (pos_list, pos_set) = passive in
+  let (neg_list, neg_set), (pos_list, pos_set), table = passive in
   let ok set equality = not (EqualitySet.mem equality set) in
   let neg = List.filter (ok neg_set) new_neg
   and pos = List.filter (ok pos_set) new_pos in
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
   in
-  (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos)
+  (neg @ neg_list, add neg_set neg),
+  (pos_list @ pos, add pos_set pos),
+  List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 ;;
 
 
 let passive_is_empty = function
-  | ([], _), ([], _) -> true
+  | ([], _), ([], _), _ -> true
   | _ -> false
 ;;
 
@@ -193,39 +204,30 @@ let passive_is_empty = function
 (* TODO: find a better way! *)
 let maxmeta = ref 0;;
 
-let infer env sign current active =
-  let rec infer_negative current = function
-    | [] -> [], []
-    | (Negative, _)::tl -> infer_negative current tl
-    | (Positive, equality)::tl ->
-        let res = superposition_left env current equality in
-        let neg, pos = infer_negative current tl in
-        res @ neg, pos
-
-  and infer_positive current = function
-    | [] -> [], []
-    | (Negative, equality)::tl ->
-        let res = superposition_left env equality current in
-        let neg, pos = infer_positive current tl in
-        res @ neg, pos
-    | (Positive, equality)::tl ->
-        let maxm, res = superposition_right !maxmeta env current equality in
-        let maxm, res' = superposition_right maxm env equality current in
-        maxmeta := maxm;
-        let neg, pos = infer_positive current tl in
-
-(*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
-(*           (string_of_equality ~env current) (string_of_equality ~env equality) *)
-(*           (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
-(*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
-(*           (string_of_equality ~env equality) (string_of_equality ~env current) *)
-(*           (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
-        
-        neg, res @ res' @ pos
-  in
+let infer env sign current (active_list, active_table) =
   match sign with
-  | Negative -> infer_negative current active
-  | Positive -> infer_positive current active
+  | Negative ->
+      Indexing.superposition_left env active_table current, []
+  | Positive ->
+      let maxm, res =
+        Indexing.superposition_right !maxmeta env active_table current in
+      maxmeta := maxm;
+      let rec infer_positive table = function
+        | [] -> [], []
+        | (Negative, equality)::tl ->
+            let res = Indexing.superposition_left env table equality in
+            let neg, pos = infer_positive table tl in
+            res @ neg, pos
+        | (Positive, equality)::tl ->
+            let maxm, res =
+              Indexing.superposition_right !maxmeta env table equality in
+            maxmeta := maxm;
+            let neg, pos = infer_positive table tl in
+            neg, res @ pos
+      in
+      let curr_table = Indexing.index (Hashtbl.create 1) current in
+      let neg, pos = infer_positive curr_table active_list in
+      neg, res @ pos
 ;;
 
 
@@ -234,7 +236,7 @@ let contains_empty env (negative, positive) =
   try
     let (proof, _, _, _) =
       List.find
-        (fun (proof, (ty, left, right), m, a) ->
+        (fun (proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -244,15 +246,16 @@ let contains_empty env (negative, positive) =
 ;;
 
 
-let forward_simplify env (sign, current) ?passive active =
-  let pn, pp =
+let forward_simplify env (sign, current) ?passive (active_list, active_table) =
+  let pl, passive_table =
     match passive with
-    | None -> [], []
-    | Some ((pn, _), (pp, _)) ->
-        (List.map (fun e -> Negative, e) pn),
-        (List.map (fun e -> Positive, e) pp)
+    | None -> [], None
+    | Some ((pn, _), (pp, _), pt) ->
+        let pn = List.map (fun e -> (Negative, e)) pn
+        and pp = List.map (fun e -> (Positive, e)) pp in
+        pn @ pp, Some pt
   in
-  let all = active @ pn @ pp in
+  let all = active_list @ pl in
   let rec find_duplicate sign current = function
     | [] -> false
     | (s, eq)::tl when s = sign ->
@@ -260,28 +263,24 @@ let forward_simplify env (sign, current) ?passive active =
         else find_duplicate sign current tl
     | _::tl -> find_duplicate sign current tl
   in
-(*   let duplicate = find_duplicate sign current all in *)
-(*   if duplicate then *)
-(*     None *)
-(*   else *)
-  let rec aux env (sign, current) = function
-    | [] -> Some (sign, current)
-    | (Negative, _)::tl -> aux env (sign, current) tl
-    | (Positive, equality)::tl ->
-        let newmeta, newcurrent =
-          demodulation !maxmeta env current equality in
-        maxmeta := newmeta;
-        if is_identity env newcurrent then
-          if sign = Negative then
-            Some (sign, current)
-          else
-            None
-        else if newcurrent <> current then
-          aux env (sign, newcurrent) active
-        else
-          aux env (sign, newcurrent) tl
+  let demodulate table current = 
+    let newmeta, newcurrent =
+      Indexing.demodulation !maxmeta env table current in
+    maxmeta := newmeta;
+    if is_identity env newcurrent then
+      if sign = Negative then Some (sign, newcurrent) else None
+    else
+      Some (sign, newcurrent)
+  in
+  let res =
+    let res = demodulate active_table current in
+    match res with
+    | None -> None
+    | Some (sign, newcurrent) ->
+        match passive_table with
+        | None -> res
+        | Some passive_table -> demodulate passive_table newcurrent
   in
-  let res = aux env (sign, current) all in
   match res with
   | None -> None
   | Some (s, c) ->
@@ -296,86 +295,112 @@ let forward_simplify env (sign, current) ?passive active =
         else res
 ;;
 
+type fs_time_info_t = {
+  mutable build_all: float;
+  mutable demodulate: float;
+  mutable subsumption: float;
+};;
+
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+
 
 let forward_simplify_new env (new_neg, new_pos) ?passive active =
-  let pn, pp =
+  let t1 = Unix.gettimeofday () in
+
+  let active_list, active_table = active in
+  let pl, passive_table =
     match passive with
-    | None -> [], []
-    | Some ((pn, _), (pp, _)) ->
-        (List.map (fun e -> Negative, e) pn),
-        (List.map (fun e -> Positive, e) pp)
+    | None -> [], None
+    | Some ((pn, _), (pp, _), pt) ->
+        let pn = List.map (fun e -> (Negative, e)) pn
+        and pp = List.map (fun e -> (Positive, e)) pp in
+        pn @ pp, Some pt
   in
-  let all = active @ pn @ pp in
-  let remove_identities equalities =
-    let ok eq = not (is_identity env eq) in
-    List.filter ok equalities
+  let all = active_list @ pl in
+  
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
+  
+  let demodulate table target =
+    let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
+    maxmeta := newmeta;
+    newtarget
   in
-  let rec simpl all' target =
-    match all' with
-    | [] -> target
-    | (Negative, _)::tl -> simpl tl target
-    | (Positive, source)::tl ->
-        let newmeta, newtarget = demodulation !maxmeta env target source in
-        maxmeta := newmeta;
-        if is_identity env newtarget then newtarget
-        else if newtarget <> target then (
-(*           Printf.printf "OK:\n%s\n%s\n" *)
-(*             (string_of_equality ~env target) *)
-(*             (string_of_equality ~env newtarget); *)
-(*           print_newline (); *)
-          simpl all newtarget
-        )
-        else simpl tl newtarget
+  let f sign' target (sign, eq) =
+    if sign <> sign' then false
+    else subsumption env target eq 
   in
-  let new_neg = List.map (simpl all) new_neg
-  and new_pos = remove_identities (List.map (simpl all) new_pos) in
+
+  let t1 = Unix.gettimeofday () in
+
+  let new_neg, new_pos = 
+    (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
+     List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+  in
+
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
+  let t1 = Unix.gettimeofday () in
+
+  let new_neg, new_pos =
+    let new_neg = List.map (demodulate active_table) new_neg
+    and new_pos = List.map (demodulate active_table) new_pos in
+    match passive_table with
+    | None -> new_neg, new_pos
+    | Some passive_table ->
+        List.map (demodulate passive_table) new_neg,
+        List.map (demodulate passive_table) new_pos
+  in
+
+  let t2 = Unix.gettimeofday () in
+  fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
+
   let new_pos_set =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
+    List.fold_left
+      (fun s e ->
+         if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+      EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
-  let f sign' target (sign, eq) =
-(*     Printf.printf "f %s <%s> (%s, <%s>)\n" *)
-(*       (string_of_sign sign') (string_of_equality ~env target) *)
-(*       (string_of_sign sign) (string_of_equality ~env eq); *)
-    if sign <> sign' then false
-    else subsumption env target eq
-  in
-(*   new_neg, new_pos *)
-  (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
-   List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
+  new_neg, new_pos
+(*   let res = *)
+(*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
+(*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
+(*   in *)
+(*   res *)
 ;;
 
 
 let backward_simplify_active env (new_neg, new_pos) active =
-  let new_pos = List.map (fun e -> Positive, e) new_pos in
-  let active, newa = 
+  let active_list, active_table = active in
+  let new_pos, new_table =
+    List.fold_left
+      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+      ([], Hashtbl.create (List.length new_pos)) new_pos
+  in
+  let active_list, newa = 
     List.fold_right
       (fun (s, equality) (res, newn) ->
-         match forward_simplify env (s, equality) new_pos with
-         | None when s = Negative ->
-             Printf.printf "\nECCO QUI: %s\n"
-               (string_of_equality ~env equality);
-             print_newline ();
-             res, newn
+         match forward_simplify env (s, equality) (new_pos, new_table) with
          | None -> res, newn
          | Some (s, e) ->
              if equality = e then
                (s, e)::res, newn
-             else
+             else 
                res, (s, e)::newn)
-      active ([], [])
+      active_list ([], [])
   in
   let find eq1 where =
     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
   in
   let active, newa =
-    let f (s, eq) res =
-      if (is_identity env eq) || (find eq res) then res else (s, eq)::res
-    in
     List.fold_right
-      (fun (s, eq) res ->
-         if (is_identity env eq) || (find eq res) then res else (s, eq)::res)
-      active [],
+      (fun (s, eq) (res, tbl) ->
+         if (is_identity env eq) || (find eq res) then
+           res, tbl
+         else
+           (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
+      active_list ([], Hashtbl.create (List.length active_list)),
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then
@@ -392,10 +417,14 @@ let backward_simplify_active env (new_neg, new_pos) active =
 
 
 let backward_simplify_passive env (new_neg, new_pos) passive =
-  let new_pos = List.map (fun e -> Positive, e) new_pos in
-  let (nl, ns), (pl, ps) = passive in
+  let new_pos, new_table =
+    List.fold_left
+      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+      ([], Hashtbl.create (List.length new_pos)) new_pos
+  in
+  let (nl, ns), (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
-    match forward_simplify env (sign, equality) new_pos with
+    match forward_simplify env (sign, equality) (new_pos, new_table) with
     | None -> resl, EqualitySet.remove equality ress, newn
     | Some (s, e) ->
         if equality = e then
@@ -406,9 +435,13 @@ let backward_simplify_passive env (new_neg, new_pos) passive =
   in
   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+  let passive_table =
+    List.fold_left
+      (fun tbl e -> Indexing.index tbl e) (Hashtbl.create (List.length pl)) pl
+  in
   match newn, newp with
-  | [], [] -> ((nl, ns), (pl, ps)), None
-  | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
+  | [], [] -> ((nl, ns), (pl, ps), passive_table), None
+  | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 ;;
 
 
@@ -416,7 +449,7 @@ let backward_simplify env new' ?passive active =
   let active, newa = backward_simplify_active env new' active in
   match passive with
   | None ->
-      active, (([], EqualitySet.empty), ([], EqualitySet.empty)), newa, None
+      active, (make_passive [] []), newa, None
   | Some passive ->
       let passive, newp =
         backward_simplify_passive env new' passive in
@@ -424,26 +457,18 @@ let backward_simplify env new' ?passive active =
 ;;
 
 
+let infer_time = ref 0.;;
+let forward_simpl_time = ref 0.;;
+let backward_simpl_time = ref 0.;;
+
   
 let rec given_clause env passive active =
   match passive_is_empty passive with
   | true -> Failure
   | false ->
-(*       Printf.printf "before select\n"; *)
       let (sign, current), passive = select env passive active in
-(*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
-(*         (string_of_sign sign) (string_of_equality ~env current); *)
       match forward_simplify env (sign, current) ~passive active with
-(*       | None when sign = Negative -> *)
-(*           Printf.printf "OK!!! %s %s" (string_of_sign sign) *)
-(*             (string_of_equality ~env current); *)
-(*           print_newline (); *)
-(*           let proof, _, _, _ = current in *)
-(*           Success (Some proof, env) *)
       | None ->
-(*           Printf.printf "avanti... %s %s" (string_of_sign sign) *)
-(*             (string_of_equality ~env current); *)
-(*           print_newline (); *)
           given_clause env passive active
       | Some (sign, current) ->
           if (sign = Negative) && (is_identity env current) then (
@@ -458,32 +483,51 @@ let rec given_clause env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
+            
             let res, proof = contains_empty env new' in
             if res then
               Success (proof, env)
-            else
+            else 
+              let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' active in
+              let t2 = Unix.gettimeofday () in
+              let _ =
+                forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
+              in
               let active =
                 match sign with
                 | Negative -> active
                 | Positive ->
+                    let t1 = Unix.gettimeofday () in
                     let active, _, newa, _ =
                       backward_simplify env ([], [current]) active
                     in
+                    let t2 = Unix.gettimeofday () in
+                    backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
                     match newa with
                     | None -> active
                     | Some (n, p) ->
-                        let nn = List.map (fun e -> Negative, e) n
-                        and pp = List.map (fun e -> Positive, e) p in
-                        nn @ active @ pp
+                        let al, tbl = active in
+                        let nn = List.map (fun e -> Negative, e) n in
+                        let pp, tbl =
+                          List.fold_right
+                            (fun e (l, t) ->
+                               (Positive, e)::l,
+                               Indexing.index tbl e)
+                            p ([], tbl)
+                        in
+                        nn @ al @ pp, tbl
               in
               let _ =
                 Printf.printf "active:\n%s\n"
                   (String.concat "\n"
                      ((List.map
                          (fun (s, e) -> (string_of_sign s) ^ " " ^
-                            (string_of_equality ~env e)) active)));
+                            (string_of_equality ~env e)) (fst active))));
                 print_newline ();
               in
               let _ =
@@ -502,12 +546,14 @@ let rec given_clause env passive active =
               match contains_empty env new' with
               | false, _ -> 
                   let active =
+                    let al, tbl = active in
                     match sign with
-                    | Negative -> (sign, current)::active
-                    | Positive -> active @ [(sign, current)]
+                    | Negative -> (sign, current)::al, tbl
+                    | Positive ->
+                        al @ [(sign, current)], Indexing.index tbl current
                   in
                   let passive = add_to_passive passive new' in
-                  let (_, ns), (_, ps) = passive in
+                  let (_, ns), (_, ps), _ = passive in
                   Printf.printf "passive:\n%s\n"
                     (String.concat "\n"
                        ((List.map (fun e -> "Negative " ^
@@ -528,10 +574,7 @@ let rec given_clause_fullred env passive active =
   match passive_is_empty passive with
   | true -> Failure
   | false ->
-(*       Printf.printf "before select\n"; *)
       let (sign, current), passive = select env passive active in
-(*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
-(*         (string_of_sign sign) (string_of_equality ~env current); *)
       match forward_simplify env (sign, current) ~passive active with
       | None ->
           given_clause_fullred env passive active
@@ -548,33 +591,29 @@ let rec given_clause_fullred env passive active =
               (string_of_sign sign) (string_of_equality ~env current);
             print_newline ();
 
+            let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
+            let t2 = Unix.gettimeofday () in
+            infer_time := !infer_time +. (t2 -. t1);
 
             let active =
               if is_identity env current then active
               else
+                let al, tbl = active in
                 match sign with
-                | Negative -> (sign, current)::active
-                | Positive -> active @ [(sign, current)]
+                | Negative -> (sign, current)::al, tbl
+                | Positive -> al @ [(sign, current)], Indexing.index tbl current
             in
-(*             let _ = *)
-(*               match new' with *)
-(*               | neg, pos -> *)
-(*                   Printf.printf "new' before simpl:\n%s\n" *)
-(*                     (String.concat "\n" *)
-(*                        ((List.map *)
-(*                            (fun e -> "Negative " ^ *)
-(*                               (string_of_equality ~env e)) neg) @ *)
-(*                           (List.map *)
-(*                              (fun e -> "Positive " ^ *)
-(*                                 (string_of_equality ~env e)) pos))); *)
-(*                   print_newline (); *)
-(*             in *)
             let rec simplify new' active passive =
+              let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+              let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained =
-                backward_simplify env new' ~passive active
-              in
+                backward_simplify env new' ~passive active in
+              let t2 = Unix.gettimeofday () in
+              backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
               | None, None -> active, passive, new'
               | Some (n, p), None
@@ -591,7 +630,7 @@ let rec given_clause_fullred env passive active =
                 (String.concat "\n"
                    ((List.map
                        (fun (s, e) -> (string_of_sign s) ^ " " ^
-                          (string_of_equality ~env e)) active)));
+                          (string_of_equality ~env e)) (fst active))));
               print_newline ();
             in
             let _ =
@@ -610,16 +649,6 @@ let rec given_clause_fullred env passive active =
             match contains_empty env new' with
             | false, _ -> 
                 let passive = add_to_passive passive new' in
-(*                 let (_, ns), (_, ps) = passive in *)
-(*                 Printf.printf "passive:\n%s\n" *)
-(*                   (String.concat "\n" *)
-(*                      ((List.map (fun e -> "Negative " ^ *)
-(*                                    (string_of_equality ~env e)) *)
-(*                          (EqualitySet.elements ns)) @ *)
-(*                         (List.map (fun e -> "Positive " ^ *)
-(*                                      (string_of_equality ~env e)) *)
-(*                            (EqualitySet.elements ps)))); *)
-(*                 print_newline (); *)
                 given_clause_fullred env passive active
             | true, proof ->
                 Success (proof, env)
@@ -663,24 +692,18 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right), _, _ = term_equality in
-    let active = [] in
+    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let active = make_active () in
     let passive = make_passive [term_equality] equalities in
-    Printf.printf "\ncurrent goal: %s ={%s} %s\n"
-      (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
+    Printf.printf "\ncurrent goal: %s\n"
+      (string_of_equality ~env term_equality);
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
-    Printf.printf "\nequalities:\n";
-    List.iter
-      (function (_, (ty, t1, t2), _, _) ->
-         let w1 = weight_of_term t1 in
-         let w2 = weight_of_term t2 in
-         let res = !compare_terms t1 t2 in
-         Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
-           (PP.ppterm t1) (string_of_weight w1)
-           (string_of_comparison res)
-           (PP.ppterm t2) (string_of_weight w2))
-      equalities;
+    Printf.printf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (string_of_equality ~env)
+            equalities));
     print_endline "--------------------------------------------------";
     let start = Unix.gettimeofday () in
     print_endline "GO!";
@@ -690,8 +713,16 @@ let main () =
     | Failure ->
         Printf.printf "NO proof found! :-(\n\n"
     | Success (Some proof, env) ->
-        Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
+        Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
+          (PP.pp proof (names_of_context context))
           (finish -. start);
+        Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+                         "backward_simpl_time: %.9f\n")
+          !infer_time !forward_simpl_time !backward_simpl_time;
+        Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^
+                         "  demodulate: %.9f\n  subsumption: %.9f\n")
+          fs_time_info.build_all fs_time_info.demodulate
+          fs_time_info.subsumption;
     | Success (None, env) ->
         Printf.printf "Success, but no proof?!?\n\n"
   with exc ->
@@ -708,6 +739,7 @@ let _ =
   and set_lpo () = Utils.compare_terms := lpo
   and set_kbo () = Utils.compare_terms := nonrec_kbo
   and set_fullred () = given_clause_ref := given_clause_fullred
+  and set_use_index v = Indexing.use_index := v
   in
   Arg.parse [
     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
@@ -722,6 +754,8 @@ let _ =
     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 
     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
+
+    "-i", Arg.Bool set_use_index, "Use indexing yes/no (default: yes)";
   ] (fun a -> ()) "Usage:"
 in
 Helm_registry.load_from !configuration_file;