X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=25314a100794c5fda5094dabd49c6d432f6ca309;hb=c1edc2a802659d79c41590f1edb29845f4bcb63c;hp=dbc85261b87385771cc457f5407ed14a1ccf6984;hpb=975da98810a335a759a3b5e5f96b1beb96c932d2;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index dbc85261b..25314a100 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -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) -> (
@@ -131,16 +127,19 @@ let select env passive active =
             (others + (abs (common - card))), e1
           in
           let _, current = EqualitySet.fold f pos_set initial in
-          Printf.printf "\nsymbols-based selection: %s\n\n"
-            (string_of_equality ~env current);
+(*           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,144 +246,185 @@ let contains_empty env (negative, positive) =
 ;;
 
 
-let forward_simplify env ?(active=[]) ?passive (sign, current) =
-  (* first step, remove already present equalities *)
-  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 duplicate =
-    let rec aux = function
-      | [] -> false
-      | (s, eq)::tl when s = sign ->
-          if meta_convertibility_eq current eq then true
-          else aux tl
-      | _::tl -> aux tl
-    in
-    aux all
+  let all = active_list @ pl in
+  let rec find_duplicate sign current = function
+    | [] -> false
+    | (s, eq)::tl when s = sign ->
+        if meta_convertibility_eq current eq then true
+        else find_duplicate sign current tl
+    | _::tl -> find_duplicate sign current tl
   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
-            None
-          else if newcurrent <> current then
-            aux env (sign, newcurrent) active
-          else
-            aux env (sign, newcurrent) tl
-    in
-    aux env (sign, current) all
+  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
+  match res with
+  | None -> None
+  | Some (s, c) ->
+      if find_duplicate s c all then
+        None
+      else
+        let pred (sign, eq) =
+          if sign <> s then false
+          else subsumption env c eq
+        in
+        if List.exists pred all then None
+        else res
 ;;
 
+type fs_time_info_t = {
+  mutable build_all: float;
+  mutable demodulate: float;
+  mutable subsumption: float;
+};;
 
-let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) =
-  let pn, pp =
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
+
+
+let forward_simplify_new env (new_neg, new_pos) ?passive active =
+  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 new_pos_set =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
+
+  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
-  new_neg, EqualitySet.elements new_pos_set
-;;
 
+  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 backward_simplify_active env (sign, current) active =
-  match sign with
-  | Negative -> active
-  | Positive ->
-      let active = 
-        List.map
-          (fun (s, equality) ->
-             (*            match s with *)
-             (*            | Negative -> s, equality *)
-             (*            | Positive -> *)
-             let newmeta, equality =
-               demodulation !maxmeta env equality current in
-             maxmeta := newmeta;
-             s, equality)
-          active
-      in
-      let active =
-        List.filter (fun (s, eq) -> not (is_identity env eq)) active
-      in
-      let find eq1 where =
-        List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
-      in
-      List.fold_right
-        (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
-        active []
+  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 ->
+         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
+  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 = 
+  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 ->
-         match forward_simplify env ~active:new_pos (s, equality) with
-         | None -> res
-         | Some e -> e::res)
-      active []
+      (fun (s, equality) (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 
+               res, (s, e)::newn)
+      active_list ([], [])
   in
   let find eq1 where =
     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
   in
-  List.fold_right
-    (fun (s, eq) res ->
-       if (is_identity env eq) || (find eq res) then
-         res
-       else
-         (s, eq)::res)
-    active []
+  let active, newa =
+    List.fold_right
+      (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
+           (n, p)
+         else
+           if s = Negative then eq::n, p
+           else n, eq::p)
+      newa ([], [])
+  in
+  match newa with
+  | [], [] -> active, None
+  | _ -> active, Some newa
 ;;
 
 
 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 ~active:new_pos (sign, equality) 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
@@ -392,77 +435,202 @@ 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)
 ;;
 
 
-let backward_simplify env ?(active=[]) ?passive new' =
-  let active = backward_simplify_active env new' active in
+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)), None
+      active, (make_passive [] []), newa, None
   | Some passive ->
-      let passive, new' =
+      let passive, newp =
         backward_simplify_passive env new' passive in
-      active, passive, new'
+      active, passive, newa, newp
 ;;
 
 
+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) ~active ~passive 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)
+      match forward_simplify env (sign, current) ~passive active with
       | 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) ->
-          print_endline "\n================================================";
-          Printf.printf "selected: %s %s"
-            (string_of_sign sign) (string_of_equality ~env current);
-          print_newline ();
-
-          let new' = infer env sign current active in
-
-          let res, proof = contains_empty env new' in
-          if res then
-            Success (proof, env)
-          else
-            let new' = forward_simplify_new env new' ~active in
+          if (sign = Negative) && (is_identity env current) then (
+            Printf.printf "OK!!! %s %s" (string_of_sign sign)
+              (string_of_equality ~env current);
+            print_newline ();
+            let proof, _, _, _ = current in
+            Success (Some proof, env)
+          ) else (            
+            print_endline "\n================================================";
+            Printf.printf "selected: %s %s"
+              (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, passive, retained = *)
-            (*             backward_simplify env [(sign, current)] ~active ~passive *)
-            (*           in *)
-            let active =
-              match sign with
-              | Negative -> active
-              | Positive ->
-                  let active, _, _ =
-                    backward_simplify env ([], [current]) ~active
+            let res, proof = contains_empty env new' in
+            if res then
+              Success (proof, env)
+            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 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)) (fst active))));
+                print_newline ();
+              in
+              let _ =
+                match new' with
+                | neg, pos ->
+                    Printf.printf "new':\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
+              match contains_empty env new' with
+              | false, _ -> 
+                  let active =
+                    let al, tbl = active in
+                    match sign with
+                    | Negative -> (sign, current)::al, tbl
+                    | Positive ->
+                        al @ [(sign, current)], Indexing.index tbl current
                   in
-                  active
+                  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 env passive active
+              | true, proof ->
+                  Success (proof, env)
+          )
+;;
+
+
+let rec given_clause_fullred env passive active =
+  match passive_is_empty passive with
+  | true -> Failure
+  | false ->
+      let (sign, current), passive = select env passive active in
+      match forward_simplify env (sign, current) ~passive active with
+      | None ->
+          given_clause_fullred env passive active
+      | Some (sign, current) ->
+          if (sign = Negative) && (is_identity env current) then (
+            Printf.printf "OK!!! %s %s" (string_of_sign sign)
+              (string_of_equality ~env current);
+            print_newline ();
+            let proof, _, _, _ = current in
+            Success (Some proof, env)
+          ) else (
+            print_endline "\n================================================";
+            Printf.printf "selected: %s %s"
+              (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)::al, tbl
+                | Positive -> al @ [(sign, current)], Indexing.index tbl current
+            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
+              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
+              | None, Some (n, p) ->
+                  let nn, np = new' in
+                  simplify (nn @ n, np @ p) active passive
+              | Some (n, p), Some (rn, rp) ->
+                  let nn, np = new' in
+                  simplify (nn @ n @ rn, np @ p @ rp) active passive
             in
+            let active, passive, new' = simplify new' active passive 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 _ =
@@ -480,102 +648,14 @@ let rec given_clause env passive active =
             in
             match contains_empty env new' with
             | false, _ -> 
-                let active =
-                  match sign with
-                  | Negative -> (sign, current)::active
-                  | Positive -> active @ [(sign, current)]
-                in
                 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 env passive active
+                given_clause_fullred env passive active
             | true, proof ->
                 Success (proof, env)
+          )
 ;;
 
 
-(*
-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); *)
-      print_endline "\n================================================";
-      Printf.printf "selected: %s %s"
-        (string_of_sign sign) (string_of_equality ~env current);
-      print_newline ();
-
-      let new' = infer env sign current active in
-
-      let rec simplify new' active passive =
-        let new' = forward_simplify_new env new' ~active ~passive in
-        let active, passive, retained =
-          backward_simplify env new' ~active ~passive
-        in
-        match retained with
-        | None -> active, passive, new'
-        | Some (rn, rp) ->
-            let nn, np = new' in
-            simplify (nn @ rn, np @ rp) active passive
-      in
-      let active, passive, new' = simplify new' active passive 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)));
-        print_newline ();
-      in
-      let _ =
-        match new' with
-        | neg, pos ->
-            Printf.printf "new':\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
-      match contains_empty env new' with
-      | false, _ -> 
-          let active =
-            match sign with
-            | Negative -> (sign, current)::active
-            | Positive -> active @ [(sign, current)]
-          in
-          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 env passive active
-      | true, proof ->
-          Success (proof, env)
-;;
-*)
-
-
 let get_from_user () =
   let dbd = Mysql.quick_connect
     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
@@ -592,6 +672,9 @@ let get_from_user () =
 ;;
 
 
+let given_clause_ref = ref given_clause;;
+
+
 let main () =
   let module C = Cic in
   let module T = CicTypeChecker in
@@ -609,35 +692,37 @@ 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!";
-    let res = given_clause env passive active in
+    let res = !given_clause_ref env passive active in
     let finish = Unix.gettimeofday () in
     match res with
     | 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 ->
@@ -653,8 +738,12 @@ let _ =
   and set_conf f = configuration_file := f
   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";
+    
     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 
     "-s", Arg.Int set_sel,
@@ -665,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;