X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=1d5d9783fb3bdf4a7df250f67f5b3691e6990183;hb=2b635ef37ea18619199fbadcdab61fc9184995dd;hp=021afb5abdf0ed36f61450e6119d7fdc2230173c;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 021afb5ab..1d5d9783f 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -70,15 +70,6 @@ let maxmeta = ref 0;;
 let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
-type new_proof = 
-  Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
-type result =
-  | ParamodulationFailure of string
-  | ParamodulationSuccess of new_proof
-;;
-
-(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *)
-
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
 let symbols_of_equality equality = 
@@ -117,22 +108,25 @@ end
 
 module EqualitySet = Set.Make(OrderedEquality);;
 
-exception Empty_list;;
-
-type passives = Equality.equality list * EqualitySet.t;;
-type actives = Equality.equality list * Indexing.Index.t;;
-
-(* initializes the passive set of equalities 
- * XXX I think EqualitySet.elements should be ok (to eliminate duplicates)
- *)
-let make_passive pos =
+type passive_table = Equality.equality list * EqualitySet.t
+type active_table = Equality.equality list * Indexing.Index.t
+type new_proof = 
+  Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
+type result =
+  | ParamodulationFailure of string * active_table * passive_table
+  | ParamodulationSuccess of new_proof * active_table * passive_table
+;;
+let make_passive eq_list =
   let set =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty pos
+    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements*) pos, set
+  (*EqualitySet.elements set*) eq_list, set
+;;
+let make_empty_active () = [], Indexing.empty ;;
+let make_active eq_list = 
+  eq_list, List.fold_left Indexing.index Indexing.empty eq_list
 ;;
 
-let make_active () = [], Indexing.empty ;;
 let size_of_passive (passive_list, _) = List.length passive_list;;
 let size_of_active (active_list, _) = List.length active_list;;
 let passive_is_empty = function
@@ -256,12 +250,12 @@ let rec select env g passive =
 ;;
 
 
-let filter_dependent passive id =
+let filter_dependent bag passive id =
   let pos_list, pos_set = passive in
   let passive,no_pruned =
     List.fold_right
       (fun eq ((list,set),no) ->
-         if Equality.depend eq id then
+         if Equality.depend bag eq id then
            (list, EqualitySet.remove eq set), no + 1
          else 
            (eq::list, set), no)
@@ -288,7 +282,6 @@ let add_to_passive passive new_pos preferred =
       (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)  
       pos 
   in
-  assert(pos_head = []);
   pos_head @ pos_list @ pos_tail, add pos_set pos
 ;;
 
@@ -350,30 +343,30 @@ let prune_passive howmany (active, _) passive =
 
 
 (** inference of new equalities between current and some in active *)
-let infer eq_uri env current (active_list, active_table) =
+let infer bag eq_uri env current (active_list, active_table) =
   let (_,c,_) = env in 
   if Utils.debug_metas then
-    (ignore(Indexing.check_target c current "infer1");
-     ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); 
+    (ignore(Indexing.check_target bag c current "infer1");
+     ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list)); 
   let new_pos = 
-      let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+      let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in
         maxmeta := maxm;
       let active_table =  Indexing.index active_table copy_of_current in
 (*       let _ = <:start<current contro active>> in *)
       let maxm, res =
-        Indexing.superposition_right eq_uri !maxmeta env active_table current 
+        Indexing.superposition_right bag eq_uri !maxmeta env active_table current 
       in
 (*       let _ = <:stop<current contro active>> in *)
       if Utils.debug_metas then
         ignore(List.map 
                  (function current -> 
-                    Indexing.check_target c current "sup0") res);
+                    Indexing.check_target bag c current "sup0") res);
       maxmeta := maxm;
       let rec infer_positive table = function
         | [] -> []
         | equality::tl ->
             let maxm, res =
-              Indexing.superposition_right 
+              Indexing.superposition_right bag 
                 ~subterms_only:true eq_uri !maxmeta env table equality 
             in
               maxmeta := maxm;
@@ -381,7 +374,7 @@ let infer eq_uri env current (active_list, active_table) =
                 ignore
                   (List.map 
                      (function current -> 
-                        Indexing.check_target c current "sup2") res);
+                        Indexing.check_target bag c current "sup2") res);
               let pos = infer_positive table tl in
               res @ pos
       in
@@ -396,7 +389,7 @@ let infer eq_uri env current (active_list, active_table) =
       if Utils.debug_metas then 
         ignore(List.map 
                  (function current -> 
-                    Indexing.check_target c current "sup3") pos);
+                    Indexing.check_target bag c current "sup3") pos);
       res @ pos
   in
   derived_clauses := !derived_clauses + (List.length new_pos);
@@ -444,22 +437,22 @@ let check_for_deep_subsumption env active_table eq =
 ;;
 
 (** simplifies current using active and passive *)
-let forward_simplify eq_uri env current (active_list, active_table) =
+let forward_simplify bag eq_uri env current (active_list, active_table) =
   let _, context, _ = env in
   let demodulate table current = 
     let newmeta, newcurrent =
-      Indexing.demodulation_equality eq_uri !maxmeta env table current
+      Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
-    if Equality.is_identity env newcurrent then None else Some newcurrent
+    if Equality.is_weak_identity newcurrent then None else Some newcurrent
   in
-  let rec demod current =
+  let demod current =
     if Utils.debug_metas then
-      ignore (Indexing.check_target context current "demod0");
+      ignore (Indexing.check_target bag context current "demod0");
     let res = demodulate active_table current in
-      if Utils.debug_metas then
-        ignore ((function None -> () | Some x -> 
-                   ignore (Indexing.check_target context x "demod1");()) res);
+    if Utils.debug_metas then
+      ignore ((function None -> () | Some x -> 
+      ignore (Indexing.check_target bag context x "demod1");()) res);
     res
   in 
   let res = demod current in
@@ -475,18 +468,18 @@ let forward_simplify eq_uri env current (active_list, active_table) =
 ;;
 
 (** simplifies new using active and passive *)
-let forward_simplify_new eq_uri env new_pos active =
+let forward_simplify_new bag eq_uri env new_pos active =
   if Utils.debug_metas then
     begin
       let m,c,u = env in
         ignore(List.map 
-        (fun current -> Indexing.check_target c current "forward new pos") 
+        (fun current -> Indexing.check_target bag c current "forward new pos") 
       new_pos;)
     end;
   let active_list, active_table = active in
   let demodulate table target =
     let newmeta, newtarget =
-      Indexing.demodulation_equality eq_uri !maxmeta env table target 
+      Indexing.demodulation_equality bag eq_uri !maxmeta env table target 
     in
     maxmeta := newmeta;
     newtarget
@@ -496,7 +489,7 @@ let forward_simplify_new eq_uri env new_pos active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Equality.is_identity env e) then
+         if not (Equality.is_weak_identity e) then
            EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
@@ -510,27 +503,29 @@ let forward_simplify_new eq_uri env new_pos active =
 
 
 (** simplifies a goal with equalities in active and passive *)  
-let rec simplify_goal env goal (active_list, active_table) =
-  let demodulate table goal = Indexing.demodulation_goal env table goal in
+let rec simplify_goal bag env goal (active_list, active_table) =
+  let demodulate table goal = Indexing.demodulation_goal bag env table goal in
   let changed, goal = demodulate active_table goal in
   changed,
   if not changed then 
     goal 
   else 
-    snd (simplify_goal env goal (active_list, active_table)) 
+    snd (simplify_goal bag env goal (active_list, active_table)) 
 ;;
 
 
-let simplify_goals env goals active =
+let simplify_goals bag env goals active =
   let a_goals, p_goals = goals in
-  let p_goals = List.map (fun g -> snd (simplify_goal env g active)) p_goals in
-  let a_goals = List.map (fun g -> snd (simplify_goal env g active)) a_goals in
+  let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in
+  let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in
   a_goals, p_goals
 ;;
 
 
 (** simplifies active usign new *)
-let backward_simplify_active eq_uri env new_pos new_table min_weight active =
+let backward_simplify_active 
+  bag eq_uri env new_pos new_table min_weight active 
+=
   let active_list, active_table = active in
   let active_list, newa, pruned = 
     List.fold_right
@@ -540,7 +535,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
            equality::res, newn,pruned
          else
            match 
-             forward_simplify eq_uri env equality (new_pos, new_table) 
+             forward_simplify bag eq_uri env equality (new_pos, new_table) 
            with
            | None -> res, newn, id::pruned
            | Some e ->
@@ -561,7 +556,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
       (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
            (res, (id_of_eq eq)::pruned),tbl 
-         else if (Equality.is_identity env eq) || (find eq res) then (
+         else if (Equality.is_weak_identity eq) || (find eq res) then (
            (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
@@ -569,7 +564,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
       active_list (([],pruned), Indexing.empty),
     List.fold_right
       (fun eq p ->
-         if (Equality.is_identity env eq) then p
+         if (Equality.is_weak_identity eq) then p
          else eq::p)
       newa []
   in
@@ -580,7 +575,9 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
 
 
 (** simplifies passive using new *)
-let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
+let backward_simplify_passive 
+  bag eq_uri env new_pos new_table min_weight passive 
+=
   let (pl, ps), passive_table = passive in
   let f equality (resl, ress, newn) =
     let ew, _, _, _ , _ = Equality.open_equality equality in
@@ -588,7 +585,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
       equality::resl, ress, newn
     else
       match 
-        forward_simplify eq_uri env equality (new_pos, new_table) 
+        forward_simplify bag eq_uri env equality (new_pos, new_table) 
       with
       | None -> resl, EqualitySet.remove equality ress, newn
       | Some e ->
@@ -617,15 +614,15 @@ let build_table equations =
 ;;
   
 
-let backward_simplify eq_uri env new' active =
+let backward_simplify bag eq_uri env new' active =
   let new_pos, new_table, min_weight = build_table new' in
   let active, newa, pruned =
-    backward_simplify_active eq_uri env new_pos new_table min_weight active 
+    backward_simplify_active bag eq_uri env new_pos new_table min_weight active 
   in
-  active, newa, None, pruned
+  active, newa, pruned
 ;;
 
-let close eq_uri env new' given =
+let close bag eq_uri env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
@@ -635,7 +632,7 @@ let close eq_uri env new' given =
   in
   List.fold_left
     (fun p c ->
-       let pos = infer eq_uri env c (new_pos,new_table) in
+       let pos = infer bag eq_uri env c (new_pos,new_table) in
          pos@p)
     [] given 
 ;;
@@ -651,7 +648,7 @@ let is_commutative_law eq =
       | _ -> false
 ;;
 
-let prova eq_uri env new' active = 
+let prova bag eq_uri env new' active = 
   let given = List.filter is_commutative_law (fst active) in
   let _ =
     Utils.debug_print
@@ -661,7 +658,7 @@ let prova eq_uri env new' active =
                (List.map
                   (fun e -> Equality.string_of_equality ~env e)
                    given)))) in
-    close eq_uri env new' given
+    close bag eq_uri env new' given
 ;;
 
 (* returns an estimation of how many equalities in passive can be activated
@@ -710,7 +707,7 @@ let activate_theorem (active, passive) =
 
 
 
-let simplify_theorems env theorems ?passive (active_list, active_table) =
+let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
     | None -> [], None
@@ -719,7 +716,7 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
   let a_theorems, p_theorems = theorems in
   let demodulate table theorem =
     let newmeta, newthm =
-      Indexing.demodulation_theorem !maxmeta env table theorem in
+      Indexing.demodulation_theorem bag !maxmeta env table theorem in
     maxmeta := newmeta;
     theorem != newthm, newthm
   in
@@ -741,19 +738,22 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
 ;;
 
 
-let rec simpl eq_uri env e others others_simpl =
+let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in
   let tbl =
     List.fold_left
-      (fun t e -> Indexing.index t e)
+      (fun t e -> 
+         if Equality.is_weak_identity e then t else Indexing.index t e) 
       Indexing.empty active
   in
-  let res = forward_simplify eq_uri env e (active, tbl) in
+  let res = 
+      forward_simplify bag eq_uri env e (active, tbl) 
+  in
     match others with
       | hd::tl -> (
           match res with
-            | None -> simpl eq_uri env hd tl others_simpl
-            | Some e -> simpl eq_uri env hd tl (e::others_simpl)
+            | None -> simpl bag eq_uri env hd tl others_simpl
+            | Some e -> simpl bag eq_uri env hd tl (e::others_simpl)
         )
       | [] -> (
           match res with
@@ -762,7 +762,7 @@ let rec simpl eq_uri env e others others_simpl =
         )
 ;;
 
-let simplify_equalities eq_uri env equalities =
+let simplify_equalities bag eq_uri env equalities =
   Utils.debug_print
     (lazy 
        (Printf.sprintf "equalities:\n%s\n"
@@ -773,7 +773,7 @@ let simplify_equalities eq_uri env equalities =
     | [] -> []
     | hd::tl ->
         let res =
-          List.rev (simpl eq_uri env hd tl [])
+          List.rev (simpl bag eq_uri env hd tl [])
         in
           Utils.debug_print
             (lazy
@@ -806,13 +806,13 @@ let pp_goal_set msg goals names =
     passive_goals)))
 ;;
 
-let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-  let names = Utils.names_of_context ctx in
+let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
+(*   let names = Utils.names_of_context ctx in *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when LibraryObjects.is_eq_URI uri ->
       (let goal_equation = 
-         Equality.mk_equality
+         Equality.mk_equality bag
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
 (*      match Indexing.subsumption env table goal_equation with*)
@@ -829,7 +829,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
               if swapped then
-                Equality.symmetric eq_ty l id uri m
+                Equality.symmetric bag eq_ty l id uri m
               else
                 p
             in
@@ -848,7 +848,7 @@ let check_if_goal_is_identity env = function
     (let _,context,_ = env in
     try 
      let s,m,_ = 
-       Inference.unification m m context left right CicUniv.empty_ugraph 
+       Founif.unification m m context left right CicUniv.empty_ugraph 
      in
       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
@@ -865,7 +865,7 @@ let rec check goal = function
       | (Some p) as ok  -> ok
 ;;
   
-let simplify_goal_set env goals active = 
+let simplify_goal_set bag env goals active = 
   let active_goals, passive_goals = goals in 
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
@@ -876,7 +876,7 @@ let simplify_goal_set env goals active =
   in *)
     List.fold_left
       (fun (acc_a,acc_p) goal -> 
-        match simplify_goal env goal active with 
+        match simplify_goal bag env goal active with 
         | changed, g -> 
             if changed then 
               if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
@@ -885,7 +885,7 @@ let simplify_goal_set env goals active =
       ([],passive_goals) active_goals
 ;;
 
-let check_if_goals_set_is_solved env active goals =
+let check_if_goals_set_is_solved bag env active goals =
   let active_goals, passive_goals = goals in
   List.fold_left 
     (fun proof goal ->
@@ -894,17 +894,17 @@ let check_if_goals_set_is_solved env active goals =
       | None -> 
           check goal [
             check_if_goal_is_identity env;
-            check_if_goal_is_subsumed env (snd active)])
+            check_if_goal_is_subsumed bag env (snd active)])
 (* provare active and passive?*)
     None active_goals
 ;;
 
-let infer_goal_set env active goals = 
+let infer_goal_set bag env active goals = 
   let active_goals, passive_goals = goals in
   let rec aux = function
     | [] -> active_goals, []
     | hd::tl ->
-        let changed,selected = simplify_goal env hd active in
+        let changed,selected = simplify_goal bag env hd active in
 (*
         if changed then
           prerr_endline ("--------------- goal semplificato");
@@ -922,7 +922,7 @@ let infer_goal_set env active goals =
               if Utils.metas_of_term t1 = [] then passive_goals
               else 
                 let newmaxmeta,new' = 
-                   Indexing.superposition_left env (snd active) selected
+                   Indexing.superposition_left bag env (snd active) selected
                    !maxmeta 
                 in
                 maxmeta := newmaxmeta;
@@ -933,15 +933,13 @@ let infer_goal_set env active goals =
   aux passive_goals
 ;;
 
-let infer_goal_set_with_current env current goals active = 
-  let active_goals, passive_goals = 
-    simplify_goal_set env goals active
-  in
+let infer_goal_set_with_current bag env current goals active = 
+  let active_goals, passive_goals = simplify_goal_set bag env goals active in
   let l,table,_  = build_table [current] in
   active_goals, 
   List.fold_left 
     (fun acc g ->
-      let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+      let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in
       maxmeta := newmaxmeta;
       acc @ new')
     passive_goals active_goals
@@ -976,7 +974,7 @@ let pp_goals label goals context =
 ;;
 
 let print_status iterno goals active passive =
-  print_endline 
+  prerr_endline 
     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
       iterno (size_of_active active) (size_of_passive passive)
       (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
@@ -985,7 +983,8 @@ let print_status iterno goals active passive =
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
 let given_clause 
-  eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
+  bag eq_uri ((_,context,_) as env) goals passive active 
+  goal_steps saturation_steps max_time
 = 
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
@@ -998,19 +997,19 @@ let given_clause
     let iterations_left = time_left /. iteration_medium_cost in
     int_of_float iterations_left 
   in
-  let rec step goals theorems passive active iterno =
-    if iterno > max_iterations then
-      (ParamodulationFailure "No more iterations to spend")
+  let rec step goals passive active g_iterno s_iterno =
+    if g_iterno > goal_steps && s_iterno > saturation_steps then
+      (ParamodulationFailure ("No more iterations to spend",active,passive))
     else if Unix.gettimeofday () > max_time then
-      (ParamodulationFailure "No more time to spend")
+      (ParamodulationFailure ("No more time to spend",active,passive))
     else
       let _ = 
-(*         print_status iterno goals active passive  *)
-        Printf.printf ".%!";
+         print_status (max g_iterno s_iterno) goals active passive  
+(*         Printf.eprintf ".%!"; *)
       in
       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
       let passive =
-        let selection_estimate = iterations_left iterno in
+        let selection_estimate = iterations_left (max g_iterno s_iterno) in
         let kept = size_of_passive passive in
         if kept > selection_estimate then 
           begin
@@ -1021,49 +1020,55 @@ let given_clause
           passive
       in
       kept_clauses := (size_of_passive passive) + (size_of_active active);
-      let goals = infer_goal_set env active goals 
+      let goals = 
+        if g_iterno < goal_steps then
+          infer_goal_set bag env active goals 
+        else
+          goals
       in
-      match check_if_goals_set_is_solved env active goals with
+      match check_if_goals_set_is_solved bag env active goals with
       | Some p -> 
-          print_endline 
+          prerr_endline 
             (Printf.sprintf "\nFound a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
-          ParamodulationSuccess p
+          ParamodulationSuccess (p,active,passive)
       | None -> 
           (* SELECTION *)
           if passive_is_empty passive then
             if no_more_passive_goals goals then 
-              ParamodulationFailure "No more passive equations/goals"
+              ParamodulationFailure 
+                ("No more passive equations/goals",active,passive)
               (*maybe this is a success! *)
             else
-              step goals theorems passive active (iterno+1)
+              step goals passive active (g_iterno+1) (s_iterno+1)
           else
             begin
               (* COLLECTION OF GARBAGED EQUALITIES *)
-              if iterno mod 40 = 0 then
+              if max g_iterno s_iterno mod 40 = 0 then
                 begin
-                  print_status iterno goals active passive;
+                  print_status (max g_iterno s_iterno) goals active passive;
                   let active = List.map Equality.id_of (fst active) in
                   let passive = List.map Equality.id_of (fst passive) in
                   let goal = ids_of_goal_set goals in
-                  Equality.collect active passive goal
+                  Equality.collect bag active passive goal
                 end;
-              let current, passive = select env goals passive in
-              (* SIMPLIFICATION OF CURRENT *)
-(*
-              prerr_endline
-                    ("Selected : " ^ 
-                      Equality.string_of_equality ~env  current);
-*)
-              let res = 
-                forward_simplify eq_uri env current active 
+              let res, passive = 
+                if s_iterno < saturation_steps then
+                  let current, passive = select env goals passive in
+                  (* SIMPLIFICATION OF CURRENT *)
+                  prerr_endline
+                        ("Selected : " ^ 
+                          Equality.string_of_equality ~env  current);
+                  forward_simplify bag eq_uri env current active, passive
+                else
+                  None, passive
               in
               match res with
-              | None -> step goals theorems passive active (iterno+1)
+              | None -> step goals passive active (g_iterno+1) (s_iterno+1)
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
 (*                   prerr_endline "infer"; *)
-                  let new' = infer eq_uri env current active in
+                  let new' = infer bag eq_uri env current active in
 (*                   prerr_endline "infer goal"; *)
 (*
       match check_if_goals_set_is_solved env active goals with
@@ -1074,66 +1079,66 @@ let given_clause
           ParamodulationSuccess p
       | None -> 
 *)
+
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
                   in
                   let goals = 
-                    infer_goal_set_with_current env current goals active 
+                    infer_goal_set_with_current bag env current goals active 
                   in
+
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
 (*                   prerr_endline "fwd/back simpl"; *)
-                  let rec simplify new' active passive head =
+                  let rec simplify new' active passive =
                     let new' = 
-                      forward_simplify_new eq_uri env new' active 
+                      forward_simplify_new bag eq_uri env new' active 
                     in
-                    let active, newa, retained, pruned =
-                      backward_simplify eq_uri env new' active 
+                    let active, newa, pruned =
+                      backward_simplify bag eq_uri env new' active 
                     in
                     let passive = 
-                      List.fold_left filter_dependent passive pruned 
+                      List.fold_left (filter_dependent bag) passive pruned 
                     in
-                    match newa, retained with
-                    | None, None -> active, passive, new', head
-                    | Some p, None 
-                    | None, Some p -> simplify (new' @ p) active passive head
-                    | Some p, Some rp -> 
-                        simplify (new' @ p @ rp) active passive (head @ p)
+                    match newa with
+                    | None -> active, passive, new'
+                    | Some p -> simplify (new' @ p) active passive 
                   in
-                  let active, passive, new', head = 
-                    simplify new' active passive []
+                  let active, passive, new' = 
+                    simplify new' active passive
                   in
+
 (*                   prerr_endline "simpl goal with new"; *)
                   let goals = 
                     let a,b,_ = build_table new' in
 (*                     let _ = <:start<simplify_goal_set new>> in *)
-                    let rc = simplify_goal_set env goals (a,b) in
+                    let rc = simplify_goal_set bag env goals (a,b) in
 (*                     let _ = <:stop<simplify_goal_set new>> in *)
                     rc
                   in
-                  let passive = add_to_passive passive new' head in
-                  step goals theorems passive active (iterno+1)
+                  let passive = add_to_passive passive new' [] in
+                  step goals passive active (g_iterno+1) (s_iterno+1)
             end
   in
-    step goals theorems passive active 1
+    step goals passive active 1 1
 ;;
 
-let rec saturate_equations eq_uri env goal accept_fun passive active =
+let rec saturate_equations bag eq_uri env goal accept_fun passive active =
   elapsed_time := Unix.gettimeofday () -. !start_time;
   if !elapsed_time > !time_limit then
     (active, passive)
   else
     let current, passive = select env ([goal],[]) passive in
-    let res = forward_simplify eq_uri env current active in
+    let res = forward_simplify bag eq_uri env current active in
     match res with
     | None ->
-        saturate_equations eq_uri env goal accept_fun passive active
+        saturate_equations bag eq_uri env goal accept_fun passive active
     | Some current ->
         Utils.debug_print (lazy (Printf.sprintf "selected: %s"
                              (Equality.string_of_equality ~env current)));
-        let new' = infer eq_uri env current active in
+        let new' = infer bag eq_uri env current active in
         let active =
-          if Equality.is_identity env current then active
+          if Equality.is_weak_identity (*env*) current then active
           else
             let al, tbl = active in
             al @ [current], Indexing.index tbl current
@@ -1141,16 +1146,14 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         (* alla fine new' contiene anche le attive semplificate!
          * quindi le aggiungo alle passive insieme alle new *)
         let rec simplify new' active passive =
-          let new' = forward_simplify_new eq_uri env new' active in
-          let active, newa, retained, pruned =
-            backward_simplify eq_uri env new' active in
+          let new' = forward_simplify_new bag eq_uri env new' active in
+          let active, newa, pruned =
+            backward_simplify bag eq_uri env new' active in
           let passive = 
-            List.fold_left filter_dependent passive pruned in
-          match newa, retained with
-          | None, None -> active, passive, new'
-          | Some p, None
-          | None, Some p -> simplify (new' @ p) active passive
-          | Some p, Some rp -> simplify (new' @ p @ rp) active passive
+            List.fold_left (filter_dependent bag) passive pruned in
+          match newa with
+          | None -> active, passive, new'
+          | Some p -> simplify (new' @ p) active passive
         in
         let active, passive, new' = simplify new' active passive in
         let _ =
@@ -1173,7 +1176,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         in
         let new' = List.filter accept_fun new' in
         let passive = add_to_passive passive new' [] in
-        saturate_equations eq_uri env goal accept_fun passive active
+        saturate_equations bag eq_uri env goal accept_fun passive active
 ;;
   
 let default_depth = !maxdepth
@@ -1194,7 +1197,6 @@ let reset_refs () =
   passive_maintainance_time := 0.;
   derived_clauses := 0;
   kept_clauses := 0;
-  Equality.reset ();
 ;;
 
 let eq_of_goal = function
@@ -1209,94 +1211,26 @@ let eq_and_ty_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
-let saturate 
-    caso_strano 
-    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
-  let module C = Cic in
-  reset_refs ();
-  Indexing.init_index ();
-  maxdepth := depth;
-  maxwidth := width;
-(*  CicUnification.unif_ty := false;*)
+(* status: input proof status
+ * goalproof: forward steps on goal
+ * newproof: backward steps
+ * subsumption_id: the equation used if goal is closed by subsumption
+ *   (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
+ * subsumption_subst: subst to make newproof and goalproof match
+ * proof_menv: final metasenv
+ *)
+let build_proof 
+  bag status  
+  goalproof newproof subsumption_id subsumption_subst proof_menv
+=
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let cleaned_goal = Utils.remove_local_context type_of_goal in
-  Utils.set_goal_symbols cleaned_goal;
-  let names = Utils.names_of_context context in
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in 
-  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
-  let res, time =
-    let t1 = Unix.gettimeofday () in
-    let lib_eq_uris, library_equalities, maxm =
-      Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
-    in
-    let library_equalities = List.map snd library_equalities in
-    let t2 = Unix.gettimeofday () in
-    maxmeta := maxm+2;
-    let equalities = 
-      simplify_equalities eq_uri env (equalities@library_equalities) 
-    in 
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
-    let t1 = Unix.gettimeofday () in
-    let theorems =
-      if full then
-        let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in
-        let context_hyp = Inference.find_context_hypotheses env eq_indexes in
-        context_hyp @ thms, []
-      else
-        let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
-        let t = CicUtil.term_of_uri refl_equal in
-        let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-        [(t, ty, [])], []
-    in
-    let t2 = Unix.gettimeofday () in
-    let _ =
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf
-              "Theorems:\n-------------------------------------\n%s\n"
-              (String.concat "\n"
-                 (List.map
-                    (fun (t, ty, _) ->
-                       Printf.sprintf
-                         "Term: %s, type: %s"
-                         (CicPp.ppterm t) (CicPp.ppterm ty))
-                    (fst theorems)))));
-      Utils.debug_print
-        (lazy
-           (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
-    in
-    let active = make_active () in
-    let passive = make_passive equalities in
-    let start = Unix.gettimeofday () in
-    let res =
-(*
-      let goals = make_goals goal in
-      given_clause_fullred dbd env goals theorems passive active
-*)
-      let goals = make_goal_set goal in
-      let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
-      given_clause 
-        eq_uri env goals theorems passive active max_iterations max_time 
-    in
-    let finish = Unix.gettimeofday () in
-    (res, finish -. start)
-  in
-  match res with
-  | ParamodulationFailure s ->
-      raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
-  | ParamodulationSuccess 
-    (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
-      print_endline "Proof:";
-      print_endline 
-        (Equality.pp_proof names goalproof newproof subsumption_subst
+      let names = Utils.names_of_context context in
+      prerr_endline "Proof:";
+      prerr_endline 
+        (Equality.pp_proof bag names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
 (*       prerr_endline "ENDOFPROOFS"; *)
 (*
@@ -1311,34 +1245,37 @@ let saturate
       in
       let goal_proof, side_effects_t = 
         let initial = Equality.add_subst subsumption_subst newproof in
-        Equality.build_goal_proof 
+        Equality.build_goal_proof bag
           eq_uri goalproof initial type_of_goal side_effects
           context proof_menv
       in
-(*       prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+      (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
-(*prerr_endline (CicPp.pp goal_proof names);*)
-      (* ?? *)
+      (* prerr_endline (CicPp.pp goal_proof names); *)
       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
       in
       (* replacing fake mets with real ones *)
-(*       prerr_endline "replacing metas..."; *)
+      (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
       let goal_proof_menv, what, with_what,free_meta = 
         List.fold_left 
           (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
              match uniq with
                | Some m -> 
-                   acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq
+(*                     acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq  *)
+                   (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2,
+                     (Cic.Meta(i,irl))::acc3, uniq
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) 
           (List.filter 
-           (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
+           (fun (i,_,_) -> 
+             List.mem i metas_still_open_in_proof
+             (*&& not(List.mem i metas_still_open_in_goal)*)) 
            proof_menv)
       in
       let replace where = 
@@ -1358,8 +1295,9 @@ let saturate
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
-(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int
- * free_metas) ); *)
+      (* prerr_endline 
+       *   ("freemetas: " ^ 
+       *   String.concat "," (List.map string_of_int free_metas) ); *)
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1372,6 +1310,12 @@ let saturate
         let free_metas_menv = 
           List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas
         in
+(*
+        prerr_endline ("XX type_of_goal  " ^ CicPp.ppterm type_of_goal);
+        prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
+        prerr_endline ("XX metasenv      " ^ 
+        CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
+*)
         try
           CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv)
            replaced_goal type_of_goal CicUniv.empty_ugraph
@@ -1399,13 +1343,20 @@ let saturate
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
             raise exn
       in
+
+      let metas_of_proof = Utils.metas_of_term goal_proof in
+
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
       let open_goals = 
+        HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) 
+      in
+(*
         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
+*)
 (*
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
@@ -1413,193 +1364,212 @@ let saturate
           (CicMetaSubst.ppmetasenv [] metasenv)
           (CicMetaSubst.ppmetasenv [] real_metasenv);
 *)
-      print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
-      proof, open_goals
+      final_subst, proof, open_goals
 ;;
 
-let main _ _ _ _ _ = () ;;
-
-let retrieve_and_print 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 proof = None, (1, [], term)::metasenv, C.Meta (1, []), term 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 uri, metasenv, meta_proof, term_to_prove = proof in
-  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+let find_equalities dbd status smart_flag ?auto cache =
+  let proof, goalno = status in
+  let _, metasenv,_,_ = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
-  let ugraph = CicUniv.empty_ugraph in
-  let env = (metasenv, context, ugraph) in
-  let t1 = Unix.gettimeofday () in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in
-  let t2 = Unix.gettimeofday () in
-  maxmeta := maxm+2;
-  let equalities = (* equalities @ *) library_equalities in
-  Utils.debug_print
-     (lazy
-        (Printf.sprintf "\n\nequalities:\n%s\n"
-           (String.concat "\n"
-              (List.map 
-          (fun (u, e) ->
-(*                  Printf.sprintf "%s: %s" *)
-                   (UriManager.string_of_uri u)
-(*                    (string_of_equality e) *)
-                     )
-          equalities))));
-  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
-  let rec simpl e others others_simpl =
-    let (u, e) = e in
-    let active = (others @ others_simpl) in
-    let tbl =
-      List.fold_left
-        (fun t (_, e) -> Indexing.index t e)
-        Indexing.empty active
-    in
-    let res = forward_simplify eq_uri env e (active, tbl) in
-    match others with
-        | hd::tl -> (
-            match res with
-              | None -> simpl hd tl others_simpl
-              | Some e -> simpl hd tl ((u, e)::others_simpl)
-          )
-        | [] -> (
-            match res with
-              | None -> others_simpl
-              | Some e -> (u, e)::others_simpl
-          ) 
+  let env = (metasenv, context, CicUniv.empty_ugraph) in 
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm, cache = 
+    Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
   in
-  let _equalities =
-    match equalities with
-      | [] -> []
-      | hd::tl ->
-          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
-          let res =
-            List.rev (simpl (*(Positive,*) hd others [])
-          in
-            Utils.debug_print
-              (lazy
-                 (Printf.sprintf "\nequalities AFTER:\n%s\n"
-                    (String.concat "\n"
-                       (List.map
-                          (fun (u, e) ->
-                             Printf.sprintf "%s: %s"
-                               (UriManager.string_of_uri u)
-                               (Equality.string_of_equality e)
-                          )
-                          res))));
-            res in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+  prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Equality_retrieval.find_library_equalities bag
+      ?auto smart_flag dbd context (proof, goalno) (maxm+2)
+      cache
+  in
+  prerr_endline (">>>>>>>>>>  gained from the library >>>>>>>>>>>>" ^
+    string_of_int maxm);
+  List.iter
+    (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) 
+    library_equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let equalities = List.map snd library_equalities @ equalities in
+  let equalities = 
+    simplify_equalities bag eq_uri env equalities
+  in 
+  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+  bag, equalities, cache, maxm
 ;;
 
+let saturate_more bag active maxmeta status smart_flag ?auto cache =
+  let proof, goalno = status in
+  let _, metasenv,_,_ = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let env = (metasenv, context, CicUniv.empty_ugraph) in 
+  let eq_indexes, equalities, maxm, cache = 
+    Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
+  in
+  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+    string_of_int maxm);
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) 
+    equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+  let equalities = 
+    HExtlib.filter_map 
+      (fun e -> forward_simplify bag eq_uri env e active)
+    equalities
+  in
+  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
+  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+  bag, equalities, cache, maxm
 
-let main_demod_equalities dbd term metasenv ugraph =
+let saturate 
+    smart_flag 
+    dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
+    ?(timeout=600.) ?auto status = 
   let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term 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 eq_uri = eq_of_goal goal in 
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2)
-  in
-  let library_equalities = List.map snd library_equalities 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
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
-            (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
+  reset_refs ();
+  maxdepth := depth;
+  maxwidth := width;
+(*  CicUnification.unif_ty := false;*)
+  let proof, goalno = status in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
+  let ugraph = CicUniv.empty_ugraph in
+  let env = (metasenv, context, ugraph) in 
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
+  let bag, equalities, cache, maxm = 
+    find_equalities dbd status smart_flag ?auto AutoCache.cache_empty 
   in
-  let env = (metasenv, context, ugraph) in
-  (*try*)
-    let goal = [], [], goal 
+  let res, time =
+    maxmeta := maxm+2;
+    let t1 = Unix.gettimeofday () in
+    let theorems =
+      let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
+      let t = CicUtil.term_of_uri refl_equal in
+      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+      [(t, ty, [])], []
     in
-    let equalities = 
-      simplify_equalities eq_uri env (equalities@library_equalities) 
+    let t2 = Unix.gettimeofday () in
+    let _ =
+      Utils.debug_print
+        (lazy
+           (Printf.sprintf
+              "Theorems:\n-------------------------------------\n%s\n"
+              (String.concat "\n"
+                 (List.map
+                    (fun (t, ty, _) ->
+                       Printf.sprintf
+                         "Term: %s, type: %s"
+                         (CicPp.ppterm t) (CicPp.ppterm ty))
+                    (fst theorems)))));
+      Utils.debug_print
+        (lazy
+           (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
     in
-    let active = make_active () in
+    let active = make_empty_active () in
     let passive = make_passive equalities in
-    Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.printf "\nequalities:\n%s\n"
-      (String.concat "\n"
-         (List.map
-            (Equality.string_of_equality ~env) equalities));
-    print_endline "--------------------------------------------------";
-    print_endline "GO!";
-    start_time := Unix.gettimeofday ();
-    if !time_limit < 1. then time_limit := 60.;    
-    let ra, rp =
-      saturate_equations eq_uri env goal (fun e -> true) passive active
-    in
-
-    let initial =
-      List.fold_left (fun s e -> EqualitySet.add e s)
-        EqualitySet.empty equalities
+    let start = Unix.gettimeofday () in
+    let res =
+(*
+      let goals = make_goals goal in
+      given_clause_fullred dbd env goals theorems passive active
+*)
+      let goals = make_goal_set goal in
+      let max_iterations = 10000 in
+      let max_time = Unix.gettimeofday () +.  timeout (* minutes *) in
+      given_clause bag
+        eq_uri env goals passive active max_iterations max_iterations max_time 
     in
-    let addfun s e = 
-      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    let finish = Unix.gettimeofday () in
+    (res, finish -. start)
+  in
+  match res with
+  | ParamodulationFailure (s,_,_) ->
+      raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
+  | ParamodulationSuccess 
+    ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),_,_) ->
+      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+    let _,p,gl = 
+      build_proof bag
+        status goalproof newproof subsumption_id subsumption_subst proof_menv
     in
+    p,gl
+;;
+(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
 
-    let passive =
-      match rp with
-      | p, _ ->
-          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
-    in
-    let active =
-      let l = fst ra in
-      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+(* exported version of given_clause *)
+let given_clause 
+  bag maxm status active passive goal_steps saturation_steps max_time 
+=
+  reset_refs();
+  maxmeta := maxm;
+  let max_l l = 
+    List.fold_left 
+     (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
+      List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
+     0 l
+  in
+  let active_l = fst active in
+  let passive_l = fst passive in
+  let ma = max_l active_l in
+  let mp = max_l passive_l in
+  assert (maxm > max ma mp);
+  let proof, goalno = status in
+  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri = eq_of_goal type_of_goal in 
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
+  let env = metasenv,context,CicUniv.empty_ugraph in
+  prerr_endline ">>>>>> ACTIVES >>>>>>>>"; 
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+  active_l;
+  prerr_endline ">>>>>>>>>>>>>>"; 
+  let goals = make_goal_set goal in
+  match 
+    given_clause bag eq_uri env goals passive active 
+      goal_steps saturation_steps max_time
+  with
+  | ParamodulationFailure (_,a,p) ->
+      None, a, p, !maxmeta
+  | ParamodulationSuccess 
+    ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) ->
+    let subst, proof, gl =
+      build_proof bag
+        status goalproof newproof subsumption_id subsumption_subst proof_menv
     in
-    Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
-     (*  (String.concat "\n"
-         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
-(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
-      (String.concat "\n"
-         (List.map 
-           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
-          passive));
-    print_newline ();
-(*
-  with e ->
-    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
-*)
+    Some (subst, proof,gl),a,p, !maxmeta
 ;;
 
 let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let eq_uri = eq_of_goal ty in 
-  let eq_indexes, equalities, maxm = 
-    Inference.find_equalities context proof 
+  let eq_uri = eq_of_goal ty in
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm, cache = 
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
+  in
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Equality_retrieval.find_library_equalities bag 
+      false dbd context (proof, goal) (maxm+2)  cache 
   in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
   let initgoal = [], [], ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let equalities = 
-    simplify_equalities eq_uri env (equalities@library_equalities) 
+    simplify_equalities bag eq_uri env (equalities@library_equalities) 
   in   
   let table = 
     List.fold_left 
@@ -1607,14 +1577,14 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
       Indexing.empty equalities 
   in
   let changed,(newproof,newmetasenv, newty) = 
-    Indexing.demodulation_goal 
+    Indexing.demodulation_goal bag
       (metasenv,context,CicUniv.empty_ugraph) table initgoal 
   in
   if changed then
     begin
       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
       let proofterm,_ = 
-        Equality.build_goal_proof 
+        Equality.build_goal_proof bag
           eq_uri newproof opengoal ty [] context metasenv
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
@@ -1660,14 +1630,16 @@ let rec position_of i x = function
 
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   reset_refs();
-  Indexing.init_index ();
   let proof,goalno = status in 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let names = Utils.names_of_context context in
-  let eq_index, equalities, maxm = Inference.find_equalities context proof in
+  let bag = Equality.mk_equality_bag () in
+  let eq_index, equalities, maxm,cache  = 
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty 
+  in
   let eq_what = 
     let what = find_in_ctx 1 target context in
     List.nth equalities (position_of 0 what eq_index)
@@ -1687,7 +1659,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let index = List.fold_left Indexing.index Indexing.empty eq_other in
   let maxm, eql = 
     if table = "" then maxm,[eq_what] else 
-    Indexing.superposition_right 
+    Indexing.superposition_right bag
       ~subterms_only eq_uri maxm env index eq_what
   in
   prerr_endline ("Superposition right:");
@@ -1707,7 +1679,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
     prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
     Subst.ppsubst s ^ "\n" ^ 
-    CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
+    CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
       let eql = 
@@ -1727,7 +1699,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
         List.fold_left 
           (fun (maxm,acc) e -> 
             let maxm,eq = 
-              Indexing.demodulation_equality eq_uri maxm env table e
+              Indexing.demodulation_equality bag eq_uri maxm env table e
             in
             maxm,eq::acc) 
           (maxm,[]) eql
@@ -1748,8 +1720,191 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
 
 let get_stats () = "" 
 (*
-  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+  <:show<Saturation.>> ^ Indexing.get_stats () ^ Founif.get_stats () ^
   Equality.get_stats ()
 ;;
 *)
 
+(* THINGS USED ONLY BY saturate_main.ml *)
+
+let main _ _ _ _ _ = () ;;
+
+let retrieve_and_print 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 proof = None, (1, [], term)::metasenv, C.Meta (1, []), term 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 uri, metasenv, meta_proof, term_to_prove = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_uri = eq_of_goal type_of_goal in
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm,cache = 
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+  let ugraph = CicUniv.empty_ugraph in
+  let env = (metasenv, context, ugraph) in
+  let t1 = Unix.gettimeofday () in
+  let lib_eq_uris, library_equalities, maxm, cache =
+    Equality_retrieval.find_library_equalities bag
+      false dbd context (proof, goal') (maxm+2)  cache
+  in 
+  let t2 = Unix.gettimeofday () in
+  maxmeta := maxm+2;
+  let equalities = (* equalities @ *) library_equalities in
+  Utils.debug_print
+     (lazy
+        (Printf.sprintf "\n\nequalities:\n%s\n"
+           (String.concat "\n"
+              (List.map 
+          (fun (u, e) ->
+(*                  Printf.sprintf "%s: %s" *)
+                   (UriManager.string_of_uri u)
+(*                    (string_of_equality e) *)
+                     )
+          equalities))));
+  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+  let rec simpl e others others_simpl =
+    let (u, e) = e in
+    let active = (others @ others_simpl) in
+    let tbl =
+      List.fold_left
+        (fun t (_, e) -> Indexing.index t e)
+        Indexing.empty active
+    in
+    let res = forward_simplify bag eq_uri env e (active, tbl) in
+    match others with
+        | hd::tl -> (
+            match res with
+              | None -> simpl hd tl others_simpl
+              | Some e -> simpl hd tl ((u, e)::others_simpl)
+          )
+        | [] -> (
+            match res with
+              | None -> others_simpl
+              | Some e -> (u, e)::others_simpl
+          ) 
+  in
+  let _equalities =
+    match equalities with
+      | [] -> []
+      | hd::tl ->
+          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
+          let res =
+            List.rev (simpl (*(Positive,*) hd others [])
+          in
+            Utils.debug_print
+              (lazy
+                 (Printf.sprintf "\nequalities AFTER:\n%s\n"
+                    (String.concat "\n"
+                       (List.map
+                          (fun (u, e) ->
+                             Printf.sprintf "%s: %s"
+                               (UriManager.string_of_uri u)
+                               (Equality.string_of_equality e)
+                          )
+                          res))));
+            res in
+    Utils.debug_print
+      (lazy
+         (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+;;
+
+
+let main_demod_equalities 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 proof = None, (1, [], term)::metasenv, C.Meta (1, []), term 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 eq_uri = eq_of_goal goal in 
+  let bag = Equality.mk_equality_bag () in
+  let eq_indexes, equalities, maxm,  cache = 
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+  let lib_eq_uris, library_equalities, maxm,cache =
+    Equality_retrieval.find_library_equalities bag
+      false dbd context (proof, goal') (maxm+2)  cache
+  in
+  let library_equalities = List.map snd library_equalities 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
+    Utils.debug_print
+      (lazy
+         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+            (CicPp.ppterm ty)));
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+  let env = (metasenv, context, ugraph) in
+  (*try*)
+    let goal = [], [], goal 
+    in
+    let equalities = 
+      simplify_equalities bag eq_uri env (equalities@library_equalities) 
+    in
+    let active = make_empty_active () in
+    let passive = make_passive equalities in
+    Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+    Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+    Printf.eprintf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (Equality.string_of_equality ~env) equalities));
+    prerr_endline "--------------------------------------------------";
+    prerr_endline "GO!";
+    start_time := Unix.gettimeofday ();
+    if !time_limit < 1. then time_limit := 60.;    
+    let ra, rp =
+      saturate_equations bag eq_uri env goal (fun e -> true) passive active
+    in
+
+    let initial =
+      List.fold_left (fun s e -> EqualitySet.add e s)
+        EqualitySet.empty equalities
+    in
+    let addfun s e = 
+      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    in
+
+    let passive =
+      match rp with
+      | p, _ ->
+          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+    in
+    let active =
+      let l = fst ra in
+      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+    in
+    Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
+     (*  (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
+(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+      (String.concat "\n"
+         (List.map 
+           (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e)) 
+          passive));
+    print_newline ();
+(*
+  with e ->
+    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+*)
+;;
+let saturate_equations eq_uri env goal accept_fun passive active =
+  let bag = Equality.mk_equality_bag () in
+  saturate_equations bag eq_uri env goal accept_fun passive active
+;;
+
+let add_to_passive eql passives = 
+  add_to_passive passives eql eql
+;;