]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/saturation.ml
profiling experiments...
[helm.git] / helm / ocaml / paramodulation / saturation.ml
index 405ba15a632307b773a22a1b68d20a1615344450..25314a100794c5fda5094dabd49c6d432f6ca309 100644 (file)
@@ -7,29 +7,29 @@ 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 string_of_equality ?env =
-  match env with
-  | None -> (
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
-              (CicPp.ppterm left) (CicPp.ppterm right)
-    )
-  | Some (_, context, _) -> (
-      let names = names_of_context context in
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
-              (CicPp.pp left names) (CicPp.pp right names)
-    )
+let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+  let m1 = symbols_of_term left in
+  let m = 
+    TermMap.fold
+      (fun k v res ->
+         try
+           let c = TermMap.find k res in
+           TermMap.add k (c+v) res
+         with Not_found ->
+           TermMap.add k v res)
+      (symbols_of_term right) m1
+  in
+(*   Printf.printf "symbols_of_equality %s:\n" *)
+(*     (string_of_equality equality); *)
+(*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
+(*   print_newline (); *)
+  m
 ;;
 
 
@@ -40,70 +40,194 @@ struct
   let compare eq1 eq2 =
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
-    | false -> Pervasives.compare eq1 eq2
+    | false ->
+        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
+        match Pervasives.compare w1 w2 with
+        | 0 -> Pervasives.compare eq1 eq2
+        | res -> res
 end
 
 module EqualitySet = Set.Make(OrderedEquality);;
-    
 
 
-let select env passive =
-  match passive with
-  | hd::tl, pos -> (Negative, hd), (tl, pos)
-  | [], hd::tl -> (Positive, hd), ([], tl)
-  | _, _ -> assert false
+let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
+let weight_age_counter = ref !weight_age_ratio;;
+
+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_table = passive in
+  let remove eq l =
+    List.filter (fun e -> e <> eq) l
+  in
+  if !weight_age_ratio > 0 then
+    weight_age_counter := !weight_age_counter - 1;
+  match !weight_age_counter with
+  | 0 -> (
+      weight_age_counter := !weight_age_ratio;
+      match neg_list, pos_list with
+      | hd::tl, pos ->
+          (* Negatives aren't indexed, no need to remove them... *)
+          (Negative, hd),
+          ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
+      | [], hd::tl ->
+          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) -> (
+      symbols_counter := !symbols_counter - 1;
+      let cardinality map =
+        TermMap.fold (fun k v res -> res + v) map 0
+      in
+      match active with
+      | (Negative, e)::_ ->
+          let symbols = symbols_of_equality e in
+          let card = cardinality symbols in
+          let f equality (i, e) =
+            let common, others =
+              TermMap.fold
+                (fun k v (r1, r2) ->
+                   if TermMap.mem k symbols then
+                     let c = TermMap.find k symbols in
+                     let c1 = abs (c - v) in
+                     let c2 = v - c1 in
+                     r1 + c2, r2 + c1
+                   else
+                     r1, r2 + v)
+                (symbols_of_equality equality) (0, 0)
+            in
+(*             Printf.printf "equality: %s, common: %d, others: %d\n" *)
+(*               (string_of_equality ~env equality) common others; *)
+            let c = others + (abs (common - card)) in
+            if c < i then (c, equality)
+            else (i, e)
+          in
+          let e1 = EqualitySet.min_elt pos_set in
+          let initial =
+            let common, others = 
+              TermMap.fold
+                (fun k v (r1, r2) ->
+                   if TermMap.mem k symbols then
+                     let c = TermMap.find k symbols in
+                     let c1 = abs (c - v) in
+                     let c2 = v - (abs (c - v)) in
+                     r1 + c1, r2 + c2
+                   else
+                     r1, r2 + v)
+                (symbols_of_equality e1) (0, 0)
+            in
+            (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); *)
+          let passive_table = Indexing.remove_index passive_table current in
+          (Positive, current),
+          (([], neg_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),
+            Indexing.remove_index passive_table current
+          in
+          (Positive, current), passive
+    )
+  | _ ->
+      symbols_counter := !symbols_ratio;
+      let set_selection set = EqualitySet.min_elt set in
+      if EqualitySet.is_empty neg_set then
+        let current = set_selection pos_set in
+        let passive =
+          (neg_list, neg_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),
+          passive_table
+        in
+        (Negative, current), passive
 ;;
 
 
-(*
-let select env passive =
-  match passive with
-  | neg, pos when EqualitySet.is_empty neg ->
-      let elem = EqualitySet.min_elt pos in
-      (Positive, elem), (neg, EqualitySet.remove elem pos)
-  | neg, pos ->
-      let elem = EqualitySet.min_elt neg in
-      (Negative, elem), (EqualitySet.remove elem neg, pos)
+let make_passive neg pos =
+  let set_of equalities =
+    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
+  in
+  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), 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),
+  List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+;;
+
+
+let passive_is_empty = function
+  | ([], _), ([], _), _ -> true
+  | _ -> false
 ;;
-*)
 
 
 (* 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
 ;;
 
 
@@ -112,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
@@ -122,187 +246,413 @@ let contains_empty env (negative, positive) =
 ;;
 
 
-let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
-  let find sign eq1 eq2 =
-    if meta_convertibility_eq eq1 eq2 then (
-(*       Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *)
-(*         (string_of_sign sign) (string_of_equality eq1); *)
-      true
-    ) else
-      false
+let forward_simplify env (sign, current) ?passive (active_list, active_table) =
+  let pl, passive_table =
+    match passive with
+    | 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_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
-  let ok sign equalities equality =
-    not (List.exists (find sign equality) equalities)
+  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 neg = List.filter (ok Negative passive_neg) new_neg in
-  let pos = List.filter (ok Positive passive_pos) new_pos in
-(*   let neg, pos = new_neg, new_pos in *)
-  (neg @ passive_neg, passive_pos @ pos)
+  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 is_identity ((_, context, ugraph) as env) = function
-  | ((_, (ty, left, right), _, _) as equality) ->
-      let res =
-        (left = right ||
-            (fst (CicReduction.are_convertible context left right ugraph)))
-      in
-(*       if res then ( *)
-(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(*         print_newline (); *)
-(*       ); *)
-      res
-;;
+let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 
 
-let forward_simplify env (sign, current) active =
-(*   if sign = Negative then *)
-(*     Some (sign, current) *)
-(*   else *)
-    let rec aux env (sign, current) =
-      function
-        | [] -> Some (sign, current)
-        | (Negative, _)::tl -> aux env (sign, current) tl
-        | (Positive, equality)::tl ->
-            let newmeta, current = demodulation !maxmeta env current equality in
-            maxmeta := newmeta;
-            if is_identity env current then
-              None
-            else
-              aux env (sign, current) tl
-    in
-    aux env (sign, current) active
+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 -> [], 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_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 f sign' target (sign, eq) =
+    if sign <> sign' then false
+    else subsumption env target eq 
+  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 ->
+         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 forward_simplify_new env (new_neg, new_pos) active =
-  let remove_identities equalities =
-    let ok eq = not (is_identity env eq) in
-    List.filter ok equalities
+let backward_simplify_active env (new_neg, new_pos) 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, 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
-  let rec simpl active target =
-    match active with
-    | [] -> target
-    | (Negative, _)::tl -> simpl tl target
-    | (Positive, source)::tl ->
-        let newmeta, target = demodulation !maxmeta env target source in
-        maxmeta := newmeta;
-        if is_identity env target then target
-        else simpl tl target
+  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
-  let new_neg = List.map (simpl active) new_neg
-  and new_pos = List.map (simpl active) new_pos in
-  new_neg, remove_identities new_pos
+  match newa with
+  | [], [] -> active, None
+  | _ -> active, Some newa
 ;;
 
 
-let backward_simplify 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 backward_simplify_passive env (new_neg, new_pos) passive =
+  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, new_table) with
+    | None -> resl, EqualitySet.remove equality ress, newn
+    | Some (s, e) ->
+        if equality = e then
+          equality::resl, ress, newn
+        else
+          let ress = EqualitySet.remove equality ress in
+          resl, ress, e::newn
+  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), passive_table), None
+  | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 ;;
-      
 
-(*
-let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
-  let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in
-  add_all passive_neg new_neg, add_all passive_pos new_pos
+
+let backward_simplify env new' ?passive active =
+  let active, newa = backward_simplify_active env new' active in
+  match passive with
+  | None ->
+      active, (make_passive [] []), newa, None
+  | Some passive ->
+      let passive, newp =
+        backward_simplify_passive env new' passive in
+      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 with
-(*   | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *)
-(*       Failure *)
-  | [], [] -> Failure
-  | passive ->
-(*       Printf.printf "before select\n"; *)
-      let (sign, current), passive = select env passive 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 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 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 ->
-          Printf.printf "avanti... %s %s" (string_of_sign sign)
-            (string_of_equality ~env current);
-          print_newline ();
           given_clause env passive active
       | Some (sign, current) ->
-(*           Printf.printf "sign: %s\ncurrent: %s\n" *)
-(*             (string_of_sign sign) (string_of_equality ~env current); *)
-(*           print_newline (); *)
+          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 new' = infer env sign current active in
+            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 
+              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
+                  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 active =
-            backward_simplify env (sign, current) active
-(*             match new' with *)
-(*             | [], [] -> backward_simplify env (sign, current) active *)
-(*             | _ -> active *)
-          in
 
-          let new' = forward_simplify_new env new' active in
-          
-          print_endline "\n================================================";
-          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)));
+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 ();
-          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 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)::active
-                | Positive -> active @ [(sign, current)]
-              in
-              let passive = add_to_passive passive new' in
-              given_clause env passive active
-          | true, proof ->
-              Success (proof, env)
+                | 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)) (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 passive = add_to_passive passive new' in
+                given_clause_fullred env passive active
+            | true, proof ->
+                Success (proof, env)
+          )
 ;;
 
 
@@ -322,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
@@ -339,40 +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 passive = *)
-(*       (EqualitySet.singleton term_equality, *)
-(*        List.fold_left *)
-(*          (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *)
-(*     in *)
-    let passive = [term_equality], equalities in
-    Printf.printf "\ncurrent goal: %s ={%s} %s\n"
-      (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
+    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\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 = nonrec_kbo 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 = Sys.time () in
+    let start = Unix.gettimeofday () in
     print_endline "GO!";
-    let res = given_clause env passive active in
-    let finish = Sys.time () 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 ->
@@ -380,8 +730,33 @@ let main () =
 ;;
 
 
+let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
+
 let _ =
-  let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in
-  Helm_registry.load_from configuration_file
+  let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
+  and set_sel v = symbols_ratio := v; symbols_counter := v;
+  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,
+    "symbols-based selection ratio (relative to the weight ratio)";
+
+    "-c", Arg.String set_conf, "Configuration file (for the db connection)";
+
+    "-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;
 main ()