X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=197ceffbbbb6e06e48bd13cec42bba11eba34f34;hb=b75631eb92b06591c86cd4563d753cd8ed7e11b7;hp=f56b8946f0e248d305c8ca2927a01c459543d5be;hpb=cb983fed69f0d209e19e22f3abcac5041f5f4a63;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index f56b8946f..197ceffbb 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -23,11 +23,14 @@ 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_ratio = ref (* 5 *) 4;; (* settable by the user *)
 let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref 2;;
+let symbols_ratio = ref (* 0 *) 3;;
 let symbols_counter = ref 0;;
 
+(* non-recursive Knuth-Bendix term ordering by default *)
+Utils.compare_terms := Utils.nonrec_kbo;; 
+
 (* statistics... *)
 let derived_clauses = ref 0;;
 let kept_clauses = ref 0;;
@@ -37,8 +40,8 @@ let maxmeta = ref 0;;
 
 
 type result =
-  | Failure
-  | Success of Inference.equality option * environment
+  | ParamodulationFailure
+  | ParamodulationSuccess of Inference.equality option * environment
 ;;
 
 
@@ -87,7 +90,7 @@ module OrderedEquality = struct
               try
                 let res = Pervasives.compare (List.hd a) (List.hd a') in
                 if res <> 0 then res else Pervasives.compare eq1 eq2
-              with _ -> 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 *)
@@ -279,9 +282,13 @@ 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 round v =
+    let t = ceil v in 
+    int_of_float (if t -. v < 0.5 then t else v)
+  in
+  let in_weight = round (howmany *. ratio /. (ratio +. 1.))
+  and in_age = round (howmany /. (ratio +. 1.)) in 
+  debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
   let symbols, card =
     match active with
     | (Negative, e)::_ ->
@@ -362,7 +369,7 @@ let prune_passive howmany (active, _) passive =
   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);
+    maximal_retained_equality := Some (EqualitySet.max_elt ps); 
   let tbl =
     EqualitySet.fold
       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
@@ -409,11 +416,52 @@ let infer env sign current (active_list, active_table) =
   in
   derived_clauses := !derived_clauses + (List.length new_neg) +
     (List.length new_pos);
-  match (* !maximal_weight *)!maximal_retained_equality with
+  match !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
+  | Some eq ->
+      (* if we have a maximal_retained_equality, we can discard all equalities
+         "greater" than it, as they will never be reached...  An equality is
+         greater than maximal_retained_equality if it is bigger
+         wrt. OrderedEquality.compare and it is less similar than
+         maximal_retained_equality to the current goal *)
+      let symbols, card =
+        match active_list 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 new_pos = 
+        match symbols with
+        | None ->
+            List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
+        | Some symbols ->
+            let filterfun e =
+              if OrderedEquality.compare e eq <= 0 then
+                true
+              else
+                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 initial =
+                  let common, others =
+                    TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
+                  others + (abs (common - card))
+                in
+                let common, others =
+                  TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
+                let c = others + (abs (common - card)) in
+                if c < initial then true else false 
+            in
+            List.filter filterfun new_pos
+      in
       new_neg, new_pos
 ;;
 
@@ -444,7 +492,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   in
   let all = if pl = [] then active_list else active_list @ pl in
 
-(*   let rec find_duplicate sign current = function *)
+  (*   let rec find_duplicate sign current = function *)
 (*     | [] -> false *)
 (*     | (s, eq)::tl when s = sign -> *)
 (*         if meta_convertibility_eq current eq then true *)
@@ -633,18 +681,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 ;;
 
 
-let backward_simplify_active env new_pos new_table active =
+let backward_simplify_active env new_pos new_table min_weight 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)
+         let ew, _, _, _, _ = equality in
+         if ew < min_weight then
+           (s, equality)::res, newn
+         else
+           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 =
@@ -677,17 +729,22 @@ let backward_simplify_active env new_pos new_table active =
 ;;
 
 
-let backward_simplify_passive env new_pos new_table passive =
+let backward_simplify_passive env new_pos new_table min_weight 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
+    let ew, _, _, _, _ = equality in
+    if ew < min_weight then
+(*       let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *)
+      equality::resl, ress, newn
+    else
+      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
@@ -702,18 +759,21 @@ let backward_simplify_passive env new_pos new_table passive =
 
 
 let backward_simplify env new' ?passive active =
-  let new_pos, new_table =
+  let new_pos, new_table, min_weight =
     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
+      (fun (l, t, w) e ->
+         let ew, _, _, _, _ = e in
+         (Positive, e)::l, Indexing.index t e, min ew w)
+      ([], Indexing.empty_table (), 1000000) (snd new')
+  in
+  let active, newa =
+    backward_simplify_active env new_pos new_table min_weight 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
+        backward_simplify_passive env new_pos new_table min_weight passive in
       active, passive, newa, newp
 ;;
 
@@ -736,13 +796,13 @@ let rec given_clause env passive active =
     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);
+      debug_print (lazy (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..." ^^
+      debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
                                      "(kept: %d, selection_estimate: %d)\n")
-                     kept selection_estimate);
+                     kept selection_estimate));
       prune_passive selection_estimate active passive
     ) else
       passive
@@ -754,7 +814,7 @@ let rec given_clause env passive active =
   kept_clauses := (size_of_passive passive) + (size_of_active active);
     
   match passive_is_empty passive with
-  | true -> Failure
+  | true -> ParamodulationFailure
   | false ->
       let (sign, current), passive = select env passive active in
       let time1 = Unix.gettimeofday () in
@@ -766,14 +826,14 @@ let rec given_clause env passive active =
           given_clause 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));
-            Success (Some current, env)
+            debug_print (lazy (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"
+            debug_print (lazy "\n================================================");
+            debug_print (lazy (Printf.sprintf "selected: %s %s"
                            (string_of_sign sign)
-                           (string_of_equality ~env current));
+                           (string_of_equality ~env current)));
 
             let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
@@ -782,7 +842,7 @@ let rec given_clause env passive active =
             
             let res, goal = contains_empty env new' in
             if res then
-              Success (goal, env)
+              ParamodulationSuccess (goal, env)
             else 
               let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' (* ~passive *) active in
@@ -857,7 +917,7 @@ let rec given_clause env passive active =
 (*                   print_newline (); *)
                   given_clause env passive active
               | true, goal ->
-                  Success (goal, env)
+                  ParamodulationSuccess (goal, env)
           )
 ;;
 
@@ -871,13 +931,13 @@ let rec given_clause_fullred env passive active =
     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);
+      debug_print (lazy (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..." ^^
+      debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
                                      "(kept: %d, selection_estimate: %d)\n")
-                     kept selection_estimate);
+                     kept selection_estimate));
       prune_passive selection_estimate active passive
     ) else
       passive
@@ -889,7 +949,7 @@ let rec given_clause_fullred env passive active =
   kept_clauses := (size_of_passive passive) + (size_of_active active);
 
   match passive_is_empty passive with
-  | true -> Failure
+  | true -> ParamodulationFailure
   | false ->
       let (sign, current), passive = select env passive active in
       let time1 = Unix.gettimeofday () in
@@ -901,14 +961,14 @@ let rec given_clause_fullred env passive active =
           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));
-            Success (Some current, env)
+            debug_print (lazy (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"
+            debug_print (lazy "\n================================================");
+            debug_print (lazy (Printf.sprintf "selected: %s %s"
                            (string_of_sign sign)
-                           (string_of_equality ~env current));
+                           (string_of_equality ~env current)));
 
             let t1 = Unix.gettimeofday () in
             let new' = infer env sign current active in
@@ -950,17 +1010,17 @@ let rec given_clause_fullred env passive active =
               processed_clauses := !processed_clauses + (kept - 1 - k);
             
             let _ =
-              debug_print (
+              debug_print (lazy (
                 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)))))
+                            (string_of_equality ~env e)) (fst active))))))
             in
             let _ =
               match new' with
               | neg, pos ->
-                  debug_print (
+                  debug_print (lazy (
                     Printf.sprintf "new':\n%s\n"
                       (String.concat "\n"
                          ((List.map
@@ -968,7 +1028,7 @@ let rec given_clause_fullred env passive active =
                                 (string_of_equality ~env e)) neg) @
                             (List.map
                                (fun e -> "Positive " ^
-                                  (string_of_equality ~env e)) pos))))
+                                  (string_of_equality ~env e)) pos)))))
             in
             match contains_empty env new' with
             | false, _ -> 
@@ -985,7 +1045,7 @@ let rec given_clause_fullred env passive active =
 (*                 print_newline (); *)
                 given_clause_fullred env passive active
             | true, goal ->
-                Success (goal, env)
+                ParamodulationSuccess (goal, env)
           )
 ;;
 
@@ -1006,7 +1066,7 @@ let main dbd term metasenv ugraph =
   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+1)
+    find_library_equalities ~dbd context (proof, goal') (maxm+2)
   in
   maxmeta := maxm+2; (* TODO ugly!! *)
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
@@ -1023,92 +1083,161 @@ let main dbd term metasenv ugraph =
   try
     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%s\n"
-      (String.concat "\n"
-         (List.map
-            (string_of_equality ~env)
-            equalities));
-    print_endline "--------------------------------------------------";
-    let start = Unix.gettimeofday () in
-    print_endline "GO!";
-    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
-      | Failure ->
-          Printf.printf "NO proof found! :-(\n\n"
-      | Success (Some goal, env) ->
-          let proof = Inference.build_proof_term goal in         
-          let newmetasenv =
+    if is_identity env term_equality then
+      let proof =
+        Cic.Appl [Cic.MutConstruct (* reflexivity *)
+                    (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                  eq_ty; left]
+      in
+      let _ = 
+        Printf.printf "OK, found a proof!\n";
+        let names = names_of_context context in
+        print_endline (PP.pp proof names)
+      in
+      ()
+    else
+      let equalities =
+        let equalities = equalities @ library_equalities in
+        debug_print (lazy (
+          Printf.sprintf "equalities:\n%s\n"
+            (String.concat "\n"
+               (List.map string_of_equality equalities))));
+        debug_print (lazy "SIMPLYFYING EQUALITIES...");
+        let rec simpl e others others_simpl =
+          let active = others @ others_simpl in
+          let tbl =
             List.fold_left
-              (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+              (fun t (_, e) -> Indexing.index t e)
+              (Indexing.empty_table ()) active
           in
-          let _ =
-          try
-            let ty, ug =
-              CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+          let res = forward_simplify env e (active, tbl) in
+          match others with
+          | hd::tl -> (
+              match res with
+              | None -> simpl hd tl others_simpl
+              | Some e -> simpl hd tl (e::others_simpl)
+            )
+          | [] -> (
+              match res with
+              | None -> others_simpl
+              | Some e -> e::others_simpl
+            )
+        in
+        match equalities with
+        | [] -> []
+        | hd::tl ->
+            let others = List.map (fun e -> (Positive, e)) tl in
+            let res =
+              List.rev (List.map snd (simpl (Positive, hd) others []))
             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
-          ()
-            
-      | Success (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;
+            debug_print (lazy (
+              Printf.sprintf "equalities AFTER:\n%s\n"
+                (String.concat "\n"
+                   (List.map string_of_equality res))));
+            res
+      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%s\n"
+        (String.concat "\n"
+           (List.map
+              (string_of_equality ~env)
+              (equalities @ library_equalities)));
+      print_endline "--------------------------------------------------";
+      let start = Unix.gettimeofday () in
+      print_endline "GO!";
+      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 proof = *)
+(* (\*               let p = CicSubstitution.lift 1 proof in *\) *)
+(*               let rec repl i = function *)
+(*                 | C.Meta _ -> C.Rel i *)
+(*                 | C.Appl l -> C.Appl (List.map (repl i) l) *)
+(*                 | C.Prod (n, s, t) -> C.Prod (n, s, repl (i+1) t) *)
+(*                 | C.Lambda (n, s, t) -> C.Lambda (n, s, repl (i+1) t) *)
+(*                 | t -> t *)
+(*               in *)
+(*               let p = repl 1 proof in *)
+(*               p *)
+(* (\*               C.Lambda (C.Anonymous, C.Rel 9, p) *\) *)
+(*             in *)
+            let newmetasenv =
+              List.fold_left
+                (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+            in
+            let _ =
+              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);
+              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;
+                print_endline (string_of_float (finish -. start));
+            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
 ;;
 
 
-exception Failure of string
-
 let saturate dbd (proof, goal) =
   let module C = Cic in
   maxmeta := 0;
@@ -1116,15 +1245,11 @@ let saturate dbd (proof, goal) =
   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));
+    debug_print (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
     Cic.Meta (maxm+1, irl),
     (maxm+1, context, ty)::metasenv,
     ty
@@ -1132,22 +1257,80 @@ let saturate dbd (proof, goal) =
   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
-    | Success (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
+  let term_equality = equality_of_term new_meta_goal goal in
+  let res, time = 
+    if is_identity env term_equality then
+      let w, _, (eq_ty, left, right, o), m, a = term_equality in
+      let proof =
+        Cic.Appl [Cic.MutConstruct (* reflexivity *)
+                    (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                  eq_ty; left]
+      in
+      (ParamodulationSuccess
+         (Some (0, Inference.BasicProof proof,
+                (eq_ty, left, right, o), m, a), env), 0.)
+    else
+      let library_equalities, maxm =
+        find_library_equalities ~dbd context (proof, goal') (maxm+2)
+      in
+      maxmeta := maxm+2;
+      let equalities =
+        let equalities = equalities @ library_equalities in
+        debug_print (lazy (
+          Printf.sprintf "equalities:\n%s\n"
+            (String.concat "\n"
+               (List.map string_of_equality equalities))));
+        debug_print (lazy "SIMPLYFYING EQUALITIES...");
+        let rec simpl e others others_simpl =
+          let active = others @ others_simpl in
+          let tbl =
+            List.fold_left
+              (fun t (_, e) -> Indexing.index t e)
+              (Indexing.empty_table ()) active
           in
+          let res = forward_simplify env e (active, tbl) in
+          match others with
+          | hd::tl -> (
+              match res with
+              | None -> simpl hd tl others_simpl
+              | Some e -> simpl hd tl (e::others_simpl)
+            )
+          | [] -> (
+              match res with
+              | None -> others_simpl
+              | Some e -> e::others_simpl
+            )
+        in
+        match equalities with
+        | [] -> []
+        | hd::tl ->
+            let others = List.map (fun e -> (Positive, e)) tl in
+            let res =
+              List.rev (List.map snd (simpl (Positive, hd) others []))
+            in
+            debug_print (lazy (
+              Printf.sprintf "equalities AFTER:\n%s\n"
+                (String.concat "\n"
+                   (List.map string_of_equality res))));
+            res
+      in      
+      let active = make_active () in
+      let passive = make_passive [term_equality] equalities in
+      let start = Unix.gettimeofday () in
+      let res = given_clause_fullred env passive active in
+      let finish = Unix.gettimeofday () in
+      (res, finish -. start)
+  in
+  match res with
+  | ParamodulationSuccess (Some goal, env) ->
+      debug_print (lazy "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 *)
@@ -1157,48 +1340,50 @@ let saturate dbd (proof, 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 t1 i =
-              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 e ->
-            debug_print "THE PROOF DOESN'T TYPECHECK!!!";
-            debug_print (CicPp.pp proof names);
-            raise (Failure "Found a proof, but it doesn't typecheck")
-        in
-        newstatus          
-    | _ ->
-        raise (Failure "NO proof found")
+        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 (lazy (CicPp.pp proof [](* names *)));
+          debug_print (lazy
+            (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 (lazy (
+            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 (lazy "THE PROOF DOESN'T TYPECHECK!!!");
+          debug_print (lazy (CicPp.pp proof names));
+          raise (ProofEngineTypes.Fail
+                   "Found a proof, but it doesn't typecheck")
+      in
+      debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
+      newstatus          
+  | _ ->
+      raise (ProofEngineTypes.Fail "NO proof found")
 (*   with e -> *)
 (*     raise (Failure "saturation failed") *)
 ;;