X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=413c7b15ea7bd760ed301b64f46d025336c3a646;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=6508e75dac896900d9941f3a486685b7c463757b;hpb=6cce91267c785d7790e9377717a13d0546bb68e1;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 6508e75da..413c7b15e 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -1,369 +1,1214 @@
 open Inference;;
 open Utils;;
 
+
+(* set to false to disable paramodulation inside auto_tac *)
+let connect_to_auto = true;;
+
+
+(* profiling statistics... *)
+let infer_time = ref 0.;;
+let forward_simpl_time = ref 0.;;
+let forward_simpl_new_time = ref 0.;;
+let backward_simpl_time = ref 0.;;
+let passive_maintainance_time = ref 0.;;
+
+(* limited-resource-strategy related globals *)
+let processed_clauses = ref 0;; (* number of equalities selected so far... *)
+let time_limit = ref 0.;; (* in seconds, settable by the user... *)
+let start_time = ref 0.;; (* time at which the execution started *)
+let elapsed_time = ref 0.;;
+(* let maximal_weight = ref None;; *)
+let maximal_retained_equality = ref None;;
+
+(* equality-selection related globals *)
+let use_fullred = ref true;;
+let weight_age_ratio = ref 3;; (* settable by the user from the command line *)
+let weight_age_counter = ref !weight_age_ratio;;
+let symbols_ratio = ref 2;;
+let symbols_counter = ref 0;;
+
+(* statistics... *)
+let derived_clauses = ref 0;;
+let kept_clauses = ref 0;;
+
+(* index of the greatest Cic.Meta created - TODO: find a better way! *)
+let maxmeta = ref 0;;
+
+
 type result =
-  | Failure
-  | Success of Cic.term option * environment
+  | ParamodulationFailure
+  | ParamodulationSuccess of Inference.equality option * environment
 ;;
 
 
-type equality_sign = Negative | Positive;;
+(*
+let symbols_of_equality (_, (_, left, right), _, _) =
+  TermSet.union (symbols_of_term left) (symbols_of_term right)
+;;
+*)
 
-let string_of_sign = function
-  | Negative -> "Negative"
-  | Positive -> "Positive"
+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
 ;;
 
 
-module OrderedEquality =
-struct
+module OrderedEquality = struct
   type t = Inference.equality
 
   let compare eq1 eq2 =
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
-    | false -> Pervasives.compare eq1 eq2
+    | false ->
+        let w1, _, (ty, left, right, _), _, a = eq1
+        and w2, _, (ty', left', right', _), _, a' = 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 ->
+            let res = (List.length a) - (List.length a') in
+            if res <> 0 then res else (
+              try
+                let res = Pervasives.compare (List.hd a) (List.hd a') in
+                if res <> 0 then res else Pervasives.compare eq1 eq2
+              with Failure "hd" -> Pervasives.compare eq1 eq2
+(*               match a, a' with *)
+(*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(*                   let res = Pervasives.compare i j in *)
+(*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(*               | _, _ -> 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 select env passive (active, _) =
+  processed_clauses := !processed_clauses + 1;
+  
+  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
+(*             if !use_fullred then Indexing.remove_index passive_table hd *)
+(*             else passive_table *)
+          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 foldfun 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
+          in
+          let f equality (i, e) =
+            let common, others =
+              TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+            in
+            let c = others + (abs (common - card)) in
+            if c < i then (c, equality)
+(*             else if c = i then *)
+(*               match OrderedEquality.compare equality e with *)
+(*               | -1 -> (c, equality) *)
+(*               | res -> (i, e) *)
+            else (i, e)
+          in
+          let e1 = EqualitySet.min_elt pos_set in
+          let initial =
+            let common, others = 
+              TermMap.fold foldfun (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
+(*             if !use_fullred then Indexing.remove_index passive_table current *)
+(*             else passive_table *)
+          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_table =
+            Indexing.remove_index passive_table current
+(*             if !use_fullred then Indexing.remove_index passive_table current *)
+(*             else passive_table *)
+          in
+          let passive =
+            (neg_list, neg_set),
+            (remove current pos_list, EqualitySet.remove current pos_set),
+            passive_table
+          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
+(*           if !use_fullred then Indexing.remove_index passive_table current *)
+(*           else passive_table *)
+        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 =
+      List.fold_left (fun tbl e -> Indexing.index tbl e)
+        (Indexing.empty_table ()) pos
+(*     if !use_fullred then *)
+(*       List.fold_left (fun tbl e -> Indexing.index tbl e) *)
+(*         (Indexing.empty_table ()) pos *)
+(*     else *)
+(*       Indexing.empty_table () *)
+  in
+  (neg, set_of neg),
+  (pos, set_of pos),
+  table
 ;;
-*)
 
 
-(* TODO: find a better way! *)
-let maxmeta = ref 0;;
+let make_active () =
+  [], Indexing.empty_table () 
+;;
+
+
+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 table =
+      List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+(*     if !use_fullred then *)
+(*       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
+(*     else *)
+(*       table *)
+  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),
+  table
+;;
+
+
+let passive_is_empty = function
+  | ([], _), ([], _), _ -> true
+  | _ -> false
+;;
 
-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
+
+let size_of_passive ((_, ns), (_, ps), _) =
+  (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
+;;
+
+
+let size_of_active (active_list, _) =
+  List.length active_list
+;;
+
+
+let prune_passive howmany (active, _) passive =
+  let (nl, ns), (pl, ps), tbl = passive in
+  let howmany = float_of_int howmany
+  and ratio = float_of_int !weight_age_ratio in
+  let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
+  and in_age = int_of_float (howmany /. (ratio +. 1.)) in 
+  debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
+  let symbols, card =
+    match active with
+    | (Negative, e)::_ ->
+        let symbols = symbols_of_equality e in
+        let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
+        Some symbols, card
+    | _ -> None, 0
+  in
+  let counter = ref !symbols_ratio in
+  let rec pickw w ns ps =
+    if w > 0 then
+      if not (EqualitySet.is_empty ns) then
+        let e = EqualitySet.min_elt ns in
+        let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
+        EqualitySet.add e ns', ps
+      else if !counter > 0 then
+        let _ =
+          counter := !counter - 1;
+          if !counter = 0 then counter := !symbols_ratio
+        in
+        match symbols with
+        | None ->
+            let e = EqualitySet.min_elt ps in
+            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+            ns, EqualitySet.add e ps'
+        | Some symbols ->
+            let foldfun 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
+            in
+            let f equality (i, e) =
+              let common, others =
+                TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+              in
+              let c = others + (abs (common - card)) in
+              if c < i then (c, equality)
+              else (i, e)
+            in
+            let e1 = EqualitySet.min_elt ps in
+            let initial =
+              let common, others = 
+                TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+              in
+              (others + (abs (common - card))), e1
+            in
+            let _, e = EqualitySet.fold f ps initial in
+            let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+            ns, EqualitySet.add e ps'
+      else
+        let e = EqualitySet.min_elt ps in
+        let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
+        ns, EqualitySet.add e ps'        
+    else
+      EqualitySet.empty, EqualitySet.empty
+  in
+(*   let in_weight, ns = pickw in_weight ns in *)
+(*   let _, ps = pickw in_weight ps in *)
+  let ns, ps = pickw in_weight ns ps in
+  let rec picka w s l =
+    if w > 0 then
+      match l with
+      | [] -> w, s, []
+      | hd::tl when not (EqualitySet.mem hd s) ->
+          let w, s, l = picka (w-1) s tl in
+          w, EqualitySet.add hd s, hd::l
+      | hd::tl ->
+          let w, s, l = picka w s tl in
+          w, s, hd::l
+    else
+      0, s, l
+  in
+  let in_age, ns, nl = picka in_age ns nl in
+  let _, ps, pl = picka in_age ps pl in
+  if not (EqualitySet.is_empty ps) then
+(*     maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
+    maximal_retained_equality := Some (EqualitySet.max_elt ps);
+  let tbl =
+    EqualitySet.fold
+      (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+(*     if !use_fullred then *)
+(*       EqualitySet.fold *)
+(*         (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
+(*     else *)
+(*       tbl *)
+  in
+  (nl, ns), (pl, ps), tbl  
+;;
+
+
+let infer env sign current (active_list, active_table) =
+  let new_neg, new_pos = 
+    match sign with
+    | Negative ->
+        let maxm, res = 
+          Indexing.superposition_left !maxmeta env active_table current in
+        maxmeta := maxm;
+        res, [] 
+    | Positive ->
+        let maxm, res =
+          Indexing.superposition_right !maxmeta env active_table 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
+        let rec infer_positive table = function
+          | [] -> [], []
+          | (Negative, equality)::tl ->
+              let maxm, res =
+                Indexing.superposition_left !maxmeta env table equality in
+              maxmeta := maxm;
+              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 (Indexing.empty_table ()) current in
+        let neg, pos = infer_positive curr_table active_list in
+        neg, res @ pos
   in
-  match sign with
-  | Negative -> infer_negative current active
-  | Positive -> infer_positive current active
+  derived_clauses := !derived_clauses + (List.length new_neg) +
+    (List.length new_pos);
+  match (* !maximal_weight *)!maximal_retained_equality with
+  | None -> new_neg, new_pos
+  | Some (* w *) eq ->
+      let new_pos =
+        List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
+      new_neg, new_pos
 ;;
 
 
 let contains_empty env (negative, positive) =
   let metasenv, context, ugraph = env in
   try
-    let (proof, _, _, _) =
+    let found =
       List.find
-        (fun (proof, (ty, left, right), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
-    true, Some proof
+    true, Some found
   with Not_found ->
     false, None
 ;;
 
 
-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
-  in
-  let ok sign equalities equality =
-    not (List.exists (find sign equality) equalities)
+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 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 all = if pl = [] then active_list else 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 is_identity ((_, context, ugraph) as env) = function
-  | ((_, (ty, left, right), _, _) as equality) ->
-      let res =
-        (left = right ||
-            (fst (CicReduction.are_convertible context left right ugraph)))
+(*   let res =  *)
+(*     if sign = Positive then *)
+(*       Indexing.subsumption env active_table current *)
+(*     else *)
+(*       false *)
+(*   in *)
+(*   if res then *)
+(*     None *)
+(*   else *)
+  
+  let demodulate table current = 
+    let newmeta, newcurrent =
+      Indexing.demodulation !maxmeta env table sign 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 (Negative, c) ->
+      let ok = not (
+        List.exists
+          (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
+          all)
       in
-(*       if res then ( *)
-(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(*         print_newline (); *)
-(*       ); *)
-      res
+      if ok then res else None
+  | Some (Positive, c) ->
+      if Indexing.in_index active_table c then
+        None
+      else
+        match passive_table with
+        | None -> res
+        | Some passive_table ->
+            if Indexing.in_index passive_table c then None
+            else res
+
+(*   | Some (s, c) -> if find_duplicate s c all then None else res *)
+
+(*         if s = Utils.Negative then *)
+(*           res *)
+(*         else *)
+(*           if Indexing.subsumption env active_table c then *)
+(*             None *)
+(*           else ( *)
+(*             match passive_table with *)
+(*             | None -> res *)
+(*             | Some passive_table -> *)
+(*                 if Indexing.subsumption env passive_table c then *)
+(*                   None *)
+(*                 else *)
+(*                   res *)
+(*           ) *)
+
+(*         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 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 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 -> [], 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 sign table target =
+    let newmeta, newtarget =
+      Indexing.demodulation !maxmeta env table sign 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 =
+    let new_neg = List.map (demodulate Negative active_table) new_neg
+    and new_pos = List.map (demodulate Positive active_table) new_pos in
+    match passive_table with
+    | None -> new_neg, new_pos
+    | Some passive_table ->
+        List.map (demodulate Negative passive_table) new_neg,
+        List.map (demodulate Positive 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
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
+      EqualitySet.empty new_pos
+  in
+  let new_pos = EqualitySet.elements new_pos_set in
+
+  let subs =
+    match passive_table with
+    | None ->
+        (fun e -> not (Indexing.subsumption env active_table e))
+    | Some passive_table ->
+        (fun e -> not ((Indexing.subsumption env active_table e) ||
+                         (Indexing.subsumption env passive_table e)))
+  in
+
+  let t1 = Unix.gettimeofday () in
+
+(*   let new_neg, new_pos = *)
+(*     List.filter subs new_neg, *)
+(*     List.filter subs new_pos *)
+(*   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 is_duplicate =
+    match passive_table with
+    | None ->
+        (fun e -> not (Indexing.in_index active_table e))
+    | Some passive_table ->
+        (fun e ->
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
+  in
+  new_neg, List.filter is_duplicate 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 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_pos new_table active =
+  let active_list, active_table = active 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 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 find eq1 where =
+    List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
+  in
+  let active, newa =
+    List.fold_right
+      (fun (s, eq) (res, tbl) ->
+         if List.mem (s, eq) res then
+           res, tbl
+         else if (is_identity env eq) || (find eq res) then (
+           res, tbl
+         ) (* else if (find eq res) then *)
+(*            res, tbl *)
+         else
+           (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
+      active_list ([], Indexing.empty_table ()),
+    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_pos new_table passive =
+  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) (Indexing.empty_table ()) 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 new_pos, new_table =
+    List.fold_left
+      (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+      ([], Indexing.empty_table ()) (snd new')
+  in    
+  let active, newa = backward_simplify_active env new_pos new_table active in
+  match passive with
+  | None ->
+      active, (make_passive [] []), newa, None
+  | Some passive ->
+      let passive, newp =
+        backward_simplify_passive env new_pos new_table passive in
+      active, passive, newa, newp
 ;;
-*)
 
 
+let get_selection_estimate () =
+  elapsed_time := (Unix.gettimeofday ()) -. !start_time;
+(*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
+  int_of_float (
+    ceil ((float_of_int !processed_clauses) *.
+            ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
+;;
+
+  
 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)
+  let time1 = Unix.gettimeofday () in
+
+  let selection_estimate = get_selection_estimate () in
+  let kept = size_of_passive passive in
+  let passive =
+    if !time_limit = 0. || !processed_clauses = 0 then
+      passive
+    else if !elapsed_time > !time_limit then (
+      debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
+                     !time_limit !elapsed_time);
+      make_passive [] []
+    ) else if kept > selection_estimate then (
+      debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
+                                     "(kept: %d, selection_estimate: %d)\n")
+                     kept selection_estimate);
+      prune_passive selection_estimate active passive
+    ) else
+      passive
+  in
+
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
+    
+  match passive_is_empty passive with
+  | true -> ParamodulationFailure
+  | false ->
+      let (sign, current), passive = select env passive active in
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res 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 (); *)
-
-          let new' = infer env sign current active in
+          if (sign = Negative) && (is_identity env current) then (
+            debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+                           (string_of_equality ~env current));
+            ParamodulationSuccess (Some current, env)
+          ) else (            
+            debug_print "\n================================================";
+            debug_print (Printf.sprintf "selected: %s %s"
+                           (string_of_sign sign)
+                           (string_of_equality ~env current));
 
-          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)));
-            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 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, goal = contains_empty env new' in
+            if res then
+              ParamodulationSuccess (goal, env)
+            else 
+              let t1 = Unix.gettimeofday () in
+              let new' = forward_simplify_new env new' (* ~passive *) active in
+              let t2 = Unix.gettimeofday () in
+              let _ =
+                forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
+              in
               let active =
                 match sign with
-                | Negative -> (sign, current)::active
-                | Positive -> active @ [(sign, current)]
+                | 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 passive = add_to_passive passive new' in
-              given_clause env passive active
-          | true, proof ->
-              Success (proof, env)
+(*               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, goal ->
+                  ParamodulationSuccess (goal, env)
+          )
 ;;
 
 
-let get_from_user () =
-  let dbd = Mysql.quick_connect
-    ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
-  let rec get () =
-    match read_line () with
-    | "" -> []
-    | t -> t::(get ())
-  in
-  let term_string = String.concat "\n" (get ()) in
-  let env, metasenv, term, ugraph =
-    List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
+let rec given_clause_fullred env passive active =
+  let time1 = Unix.gettimeofday () in
+  
+  let selection_estimate = get_selection_estimate () in
+  let kept = size_of_passive passive in
+  let passive =
+    if !time_limit = 0. || !processed_clauses = 0 then
+      passive
+    else if !elapsed_time > !time_limit then (
+      debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
+                     !time_limit !elapsed_time);
+      make_passive [] []
+    ) else if kept > selection_estimate then (
+      debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
+                                     "(kept: %d, selection_estimate: %d)\n")
+                     kept selection_estimate);
+      prune_passive selection_estimate active passive
+    ) else
+      passive
   in
-  term, metasenv, ugraph
+
+  let time2 = Unix.gettimeofday () in
+  passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+    
+  kept_clauses := (size_of_passive passive) + (size_of_active active);
+
+  match passive_is_empty passive with
+  | true -> ParamodulationFailure
+  | false ->
+      let (sign, current), passive = select env passive active in
+      let time1 = Unix.gettimeofday () in
+      let res = forward_simplify env (sign, current) ~passive active in
+      let time2 = Unix.gettimeofday () in
+      forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+      match res with
+      | None ->
+          given_clause_fullred env passive active
+      | Some (sign, current) ->
+          if (sign = Negative) && (is_identity env current) then (
+            debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
+                           (string_of_equality ~env current));
+            ParamodulationSuccess (Some current, env)
+          ) else (
+            debug_print "\n================================================";
+            debug_print (Printf.sprintf "selected: %s %s"
+                           (string_of_sign sign)
+                           (string_of_equality ~env current));
+
+            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_new_time := !forward_simpl_new_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 k = size_of_passive passive in
+            if k < (kept - 1) then
+              processed_clauses := !processed_clauses + (kept - 1 - k);
+            
+            let _ =
+              debug_print (
+                Printf.sprintf "active:\n%s\n"
+                  (String.concat "\n"
+                     ((List.map
+                         (fun (s, e) -> (string_of_sign s) ^ " " ^
+                            (string_of_equality ~env e)) (fst active)))))
+            in
+            let _ =
+              match new' with
+              | neg, pos ->
+                  debug_print (
+                    Printf.sprintf "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))))
+            in
+            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, goal ->
+                ParamodulationSuccess (goal, env)
+          )
 ;;
 
 
-let main () =
+let given_clause_ref = ref given_clause;;
+
+
+let main dbd term metasenv ugraph =
   let module C = Cic in
   let module T = CicTypeChecker in
   let module PET = ProofEngineTypes in
   let module PP = CicPp in
-  let term, metasenv, ugraph = get_from_user () in
   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let proof, goals =
-    PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let goal = List.nth goals 0 in
+  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+  let proof, goals = status in
+  let goal' = List.nth goals 0 in
   let _, metasenv, meta_proof, _ = proof in
-  let _, context, goal = CicUtil.lookup_meta goal metasenv in
+  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let equalities, maxm = find_equalities context proof in
-  maxmeta := maxm; (* TODO ugly!! *)
+(*   let library_equalities, maxm = *)
+(*     find_library_equalities ~dbd context (proof, goal') (maxm+1) *)
+(*   in *)
+  maxmeta := maxm+2; (* TODO ugly!! *)
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let new_meta_goal, metasenv, type_of_goal =
+    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+    Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+    print_newline ();
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+(*   let new_meta_goal = Cic.Meta (goal', irl) in *)
   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 term_equality = equality_of_term new_meta_goal goal in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let active = make_active () in
+    let passive =
+      make_passive [term_equality] (equalities (* @ library_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
-    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)
-          (finish -. start);
-    | Success (None, env) ->
-        Printf.printf "Success, but no proof?!?\n\n"
+    start_time := Unix.gettimeofday ();
+    let res =
+      (if !use_fullred then given_clause_fullred else given_clause)
+        env passive active
+    in
+    let finish = Unix.gettimeofday () in
+    let _ =
+      match res with
+      | ParamodulationFailure ->
+          Printf.printf "NO proof found! :-(\n\n"
+      | ParamodulationSuccess (Some goal, env) ->
+          let proof = Inference.build_proof_term goal in         
+          let newmetasenv =
+            List.fold_left
+              (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+          in
+          let _ =
+          try
+            let ty, ug =
+              CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+            in
+            Printf.printf "OK, found a proof!\n";
+            (* REMEMBER: we have to instantiate meta_proof, we should use
+               apply  the "apply" tactic to proof and status 
+            *)
+            let names = names_of_context context in
+            print_endline (PP.pp proof names);
+            (*           print_endline (PP.ppterm proof); *)
+            
+            print_endline (string_of_float (finish -. start));
+            Printf.printf
+              "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+              (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+              (string_of_bool
+                 (fst (CicReduction.are_convertible
+                         context type_of_goal ty ug)));
+          with e ->
+            Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
+            Printf.printf "MAXMETA USED: %d\n" !maxmeta;
+          in
+          ()
+            
+      | ParamodulationSuccess (None, env) ->
+          Printf.printf "Success, but no proof?!?\n\n"
+    in
+    Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+                     "forward_simpl_new_time: %.9f\n" ^^
+                     "backward_simpl_time: %.9f\n")
+      !infer_time !forward_simpl_time !forward_simpl_new_time
+      !backward_simpl_time;
+    Printf.printf "passive_maintainance_time: %.9f\n"
+      !passive_maintainance_time;
+    Printf.printf "    successful unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_ok;
+    Printf.printf "    failed unification/matching time: %.9f\n"
+      !Indexing.match_unif_time_no;
+    Printf.printf "    indexing retrieval time: %.9f\n"
+      !Indexing.indexing_retrieval_time;
+    Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
+      !Indexing.build_newtarget_time;
+    Printf.printf "derived %d clauses, kept %d clauses.\n"
+      !derived_clauses !kept_clauses;
   with exc ->
     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
+    raise exc
+;;
+
+
+let saturate dbd (proof, goal) =
+  let module C = Cic in
+  maxmeta := 0;
+  let goal' = goal in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let equalities, maxm = find_equalities context proof in
+  let library_equalities, maxm =
+    find_library_equalities ~dbd context (proof, goal') (maxm+2)
+  in
+  maxmeta := maxm+2;
+  let new_meta_goal, metasenv, type_of_goal =
+    let irl =
+      CicMkImplicit.identity_relocation_list_for_metavariable context in
+    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+    debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+  let ugraph = CicUniv.empty_ugraph in
+  let env = (metasenv, context, ugraph) in
+(*   try *)
+    let term_equality = equality_of_term new_meta_goal goal in
+    let active = make_active () in
+    let passive =
+      make_passive [term_equality] (equalities @ library_equalities)
+    in
+    let res = given_clause_fullred env passive active in
+    match res with
+    | ParamodulationSuccess (Some goal, env) ->
+        debug_print "OK, found a proof!";
+        let proof = Inference.build_proof_term goal in         
+        let names = names_of_context context in
+        let newmetasenv =
+          let i1 =
+            match new_meta_goal with
+            | C.Meta (i, _) -> i | _ -> assert false
+          in
+(*           let i2 = *)
+(*             match meta_proof with *)
+(*             | C.Meta (i, _) -> i *)
+(*             | t -> *)
+(*                 Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
+(*                   (CicPp.pp meta_proof names) (string_of_int goal'); *)
+(*                 print_newline (); *)
+(*                 assert false *)
+(*           in *)
+          List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
+        in
+        let newstatus =
+          try
+            let ty, ug =
+              CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+            in
+            debug_print (CicPp.pp proof [](* names *));
+            debug_print
+              (Printf.sprintf
+                 "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
+                 (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+                 (string_of_bool
+                    (fst (CicReduction.are_convertible
+                            context type_of_goal ty ug))));
+            let equality_for_replace i t1 =
+              match t1 with
+              | C.Meta (n, _) -> n = i
+              | _ -> false
+            in
+            let real_proof =
+              ProofEngineReduction.replace
+                ~equality:equality_for_replace
+                ~what:[goal'] ~with_what:[proof]
+                ~where:meta_proof
+            in
+            debug_print (
+              Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
+                (match uri with Some uri -> UriManager.string_of_uri uri
+                 | None -> "")
+                (print_metasenv newmetasenv)
+                (CicPp.pp real_proof [](* names *))
+                (CicPp.pp term_to_prove names));
+            ((uri, newmetasenv, real_proof, term_to_prove), [])
+          with CicTypeChecker.TypeCheckerFailure _ ->
+            debug_print "THE PROOF DOESN'T TYPECHECK!!!";
+            debug_print (CicPp.pp proof names);
+            raise
+              (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck")
+        in
+        newstatus          
+    | _ ->
+        raise (ProofEngineTypes.Fail "NO proof found")
+(*   with e -> *)
+(*     raise (Failure "saturation failed") *)
 ;;
 
 
-let _ =
-  let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in
-  Helm_registry.load_from configuration_file
-in
-main ()
+(* dummy function called within matita to trigger linkage *)
+let init () = ();;
+
+
+(* UGLY SIDE EFFECT... *)
+if connect_to_auto then ( 
+  AutoTactic.paramodulation_tactic := saturate;
+  AutoTactic.term_is_equality := Inference.term_is_equality;
+);;