]> matita.cs.unibo.it Git - helm.git/commitdiff
- new given_clause
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 May 2006 14:54:35 +0000 (14:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 May 2006 14:54:35 +0000 (14:54 +0000)
- support for a set of goals in OR
- restored superposition_left (even if not called)

components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/saturation.ml

index b921f78c1984bfed44701c202e20deede6d77ecd..b6c3dc66a6625ec2e2ba92043e5108d6375f501d 100644 (file)
@@ -146,7 +146,7 @@ let rec depend eq id =
     | Step (_,(_,id1,(_,id2),_)) ->
         let eq1 = Hashtbl.find id_to_eq id1 in
         let eq2 = Hashtbl.find id_to_eq id2 in  
-        depend eq1 id || depend eq2 id
+        depend eq1 id || depend eq2 id
 ;;
 
 let ppsubst = Subst.ppsubst ~names:[];;
@@ -475,7 +475,8 @@ let build_goal_proof l initial ty =
         build_proof_step subst current_proof p pos l r pred)
    initial l
   in
-  canonical (contextualize_rewrites proof ty)
+  proof 
+  (*canonical (contextualize_rewrites proof ty)*)
 ;;
 
 let refl_proof ty term = 
index e3ef59d9b54f538ebd50ca4cc8d70d01d065e1f0..d68c6d65164573f1d320b1bab4058448cfb23db6 100644 (file)
@@ -25,6 +25,8 @@
 
 (* $Id$ *)
 
+type goal = Equality.goal_proof * Cic.metasenv * Cic.term
+
 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
 (*
 module Index = Equality_indexing.DT (* path tree based indexing *)
@@ -406,7 +408,7 @@ let find_all_matches
 (*
   returns true if target is subsumed by some equality in table
 *)
-let subsumption env table target = 
+let subsumption_aux use_unification env table target = 
   (* 
   let print_res l =
     prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
@@ -435,7 +437,10 @@ let subsumption env table target =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching metasenv m context what other ugraph
+                if use_unification then
+                  Inference.unification metasenv m context what other ugraph
+                else
+                  Inference.matching metasenv m context what other ugraph
               in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
@@ -471,6 +476,9 @@ let subsumption env table target =
 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 ;;
 
+let subsumption = subsumption_aux false;;
+let unification = subsumption_aux true;;
+
 let rec demodulation_aux ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
@@ -905,107 +913,63 @@ let sup_l_counter = ref 1;;
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
-let superposition_left newmeta (metasenv, context, ugraph) table target = 
-  assert false
-(*
-let superposition_left newmeta (metasenv, context, ugraph) table target =
+  
+let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
+  let pos, equality = eq_found in
+  let (_, proof', (ty, what, other, _), menv',id) = 
+    Equality.open_equality equality in
+  let what, other = if pos = Utils.Left then what, other else other, what in
+  let newterm, newgoalproof =
+    let bo = 
+      Utils.guarded_simpl context 
+        (apply_subst subst (CicSubstitution.subst other t)) 
+    in
+    let bo' = (*apply_subst subst*) t in 
+    let name = Cic.Name "x" in
+    let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    bo, (newgoalproofstep::goalproof)
+  in
+  let newmetasenv = (* Inference.filter subst *) menv in
+  (newgoalproof, newmetasenv, newterm)
+;;
+
+let superposition_left 
+  (metasenv, context, ugraph) table (proof,menv,ty)
+= 
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), menv, id = 
-    Equality.open_equality target 
+  let big,small,pos,eq,ty = 
+    match ty with
+    | Cic.Appl [eq;ty;l;r] ->
+       let c = 
+         Utils.compare_weights ~normalize:true
+           (Utils.weight_of_term l) (Utils.weight_of_term r)
+       in
+       (match c with 
+       | Utils.Gt -> l,r,Utils.Right,eq,ty
+       | _ -> r,l,Utils.Left,eq,ty)
+    | _ -> assert false
   in
-  if Utils.debug_metas then
-    ignore(check_target context target "superpositionleft");
-  let expansions, _ =
-    let term = if ordering = U.Gt then left else right in
-    betaexpand_term metasenv context ugraph table 0 term
-  in
-  let maxmeta = ref newmeta in
-  let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
-(*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
-    let time1 = Unix.gettimeofday () in
-    
-    let pos, equality = eq_found in
-    let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
-    let proof'_new, proof'_old = proof' in
-    let what, other = if pos = Utils.Left then what, other else other, what in
-    let newgoal, newproof =
-      let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
-      let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
-      incr sup_l_counter;
-      let bo'' = 
-        let l, r =
-          if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
-                S.lift 1 eq_ty; l; r]
-      in
-      incr maxmeta;
-      let metaproof =
-        let irl =
-          CicMkImplicit.identity_relocation_list_for_metavariable context in
-        C.Meta (!maxmeta, irl)
-      in
-      let eq_found =
-        let proof' =
-          let termlist =
-            if pos = Utils.Left then [ty; what; other]
-            else [ty; other; what]
-          in
-          proof'_new, (* MAH????? *)
-          Equality.ProofSymBlock (termlist, proof'_old)
-        in
-        let what, other =
-          if pos = Utils.Left then what, other else other, what
-        in
-        pos, 
-          Equality.mk_equality 
-            (0, proof', (ty, other, what, Utils.Incomparable), menv')
-      in
-      let target_proof = assert false (*
-        let pb =
-          Equality.ProofBlock 
-            (s, eq_URI, (name, ty), bo'', eq_found,
-            Equality.BasicProof (Equality.empty_subst,metaproof))
-        in
-        match proof with
-        | Equality.BasicProof _ ->
-(*             debug_print (lazy "replacing a BasicProof"); *)
-            pb
-        | Equality.ProofGoalBlock (_, parent_proof) ->
-(*             debug_print (lazy "replacing another ProofGoalBlock"); *)
-            Equality.ProofGoalBlock (pb, parent_proof)
-        | _ -> assert false*)
-      in
-      let refl =
-        C.Appl [C.MutConstruct (* reflexivity *)
-                  (LibraryObjects.eq_URI (), 0, 1, []);
-                eq_ty; if ordering = U.Gt then right else left]
-      in
-      (bo',
-       (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
-         assert false), (* il predicato della beta expand non viene tenuto? *) 
-       Equality.ProofGoalBlock 
-        (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
+  let small = CicSubstitution.lift 1 small in
+  let ty = CicSubstitution.lift 1 ty in
+  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+  let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) = 
+    let pred = 
+      match pos with
+      | Utils.Left -> 
+          Cic.Appl [eq;ty;small;t]
+      | Utils.Right -> 
+          Cic.Appl [eq;ty;t;small]
     in
-    let left, right =
-      if ordering = U.Gt then newgoal, right else left, newgoal in
-    let neworder = !Utils.compare_terms left right in
-    let stat = (eq_ty, left, right, neworder) in
-    let newmenv = (* Inference.filter s *) menv in  
-    let time2 = Unix.gettimeofday () in
-    build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
-    let w = Utils.compute_equality_weight stat in
-    Equality.mk_equality (w, newproof, stat, newmenv) 
-
+    (pred, subst, menv, ug, (eq_found, eq_URI))
   in
-  !maxmeta, List.map build_new expansions
+  List.map (build_newgoal context proof) 
+    (List.map fix_preds expansions)
 ;;
-*)
 
 let sup_r_counter = ref 1;;
 
@@ -1130,8 +1094,10 @@ let rec demodulation_goal newmeta env table goal =
       Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
-      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
-      with CicUtil.Meta_not_found _ -> ty
+      try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
+      with 
+      | CicUtil.Meta_not_found _ 
+      | Invalid_argument("List.fold_left2") -> ty
     in
     let newterm, newgoalproof =
       let bo = 
index 8af265f907f945c4a597b24e299e64b5da29dc22..f3f23e6f18fdcca82a3d6398da526c23579bf9f0 100644 (file)
@@ -25,6 +25,8 @@
 
 (* $Id$ *)
 
+type goal = Equality.goal_proof * Cic.metasenv * Cic.term
+
 module Index :
   sig
     module PosEqSet : Set.S 
@@ -43,17 +45,21 @@ val match_unif_time_no : float ref
 val indexing_retrieval_time : float ref
 val init_index : unit -> unit
 val build_newtarget_time : float ref
+val unification :
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.equality ->
+  (Subst.substitution * Equality.equality) option
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
   (Subst.substitution * Equality.equality) option
 val superposition_left :
-  int ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Equality.equality ->
-   int * Equality.equality list
+  goal ->
+   goal list
 
 val superposition_right :
   int ->
@@ -72,9 +78,8 @@ val demodulation_goal :
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Equality.goal_proof * Cic.metasenv * Index.key ->
-  bool * int * 
-   (Equality.goal_proof * Cic.metasenv * Index.key)
+  goal ->
+  bool * int * goal
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
index f8c20d0e3b61250633e5dc4841fabe932b911470..351bc11bd0b88f67def8add7000da426cb418c4a 100644 (file)
@@ -25,6 +25,8 @@
 
 (* $Id$ *)
 
+(* <:profiler<"saturation">> *)
+
 open Inference;;
 open Utils;;
 
@@ -73,8 +75,8 @@ let maxwidth = ref 3;;
 type new_proof = 
   Equality.goal_proof * Equality.proof * Subst.substitution * Cic.metasenv
 type result =
-  | ParamodulationFailure
-  | ParamodulationSuccess of new_proof option
+  | ParamodulationFailure of string
+  | ParamodulationSuccess of new_proof
 ;;
 
 type goal = Equality.goal_proof * Cic.metasenv * Cic.term;;
@@ -153,21 +155,21 @@ let rec select env goals passive =
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
       let rec skip_giant pos_list pos_set passive_table =
-       match pos_list with
-         | (hd:EqualitySet.elt)::tl ->
-             let w,_,_,_,_ = Equality.open_equality hd in
+        match pos_list with
+          | (hd:EqualitySet.elt)::tl ->
+              let w,_,_,_,_ = Equality.open_equality hd in
               let passive_table =
-               Indexing.remove_index passive_table hd
+                Indexing.remove_index passive_table hd
               in 
-             let pos_set = EqualitySet.remove hd pos_set in
-               if w < 50 then
-                 hd, ((tl, pos_set), passive_table)
-               else
-                 (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n");
-                 skip_giant tl pos_set passive_table)
-         | _ -> assert false
+              let pos_set = EqualitySet.remove hd pos_set in
+                if w < 500 then
+                  hd, ((tl, pos_set), passive_table)
+                else
+                  (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n");
+                  skip_giant tl pos_set passive_table)
+          | _ -> assert false
       in
-       skip_giant pos_list pos_set passive_table)
+        skip_giant pos_list pos_set passive_table)
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
@@ -222,22 +224,23 @@ let rec select env goals passive =
 
 let filter_dependent passive id =
   prerr_endline ("+++++++++++++++passives "^
-                  ( string_of_int (size_of_passive passive)));
+                   ( string_of_int (size_of_passive passive)));
   let (pos_list, pos_set), passive_table = passive in
   let passive =
     List.fold_right
       (fun eq ((list,set),table) ->
-        if Equality.depend eq id then
+         if Equality.depend eq id then
            (let _,_,_,_,id_eq = Equality.open_equality eq in
-             if id_eq = 9228 then 
-               prerr_endline ("\n\n--------filtering "^(string_of_int id_eq));
-          ((list, 
-            EqualitySet.remove eq set),
-           Indexing.remove_index table eq))
-        else ((eq::list, set),table))
+              if id_eq = 9228 then 
+                prerr_endline ("\n\n--------filtering "^(string_of_int id_eq));
+           ((list, 
+             EqualitySet.remove eq set),
+            Indexing.remove_index table eq))
+         else 
+              ((eq::list, set),table))
       pos_list (([],pos_set),passive_table) in
   prerr_endline ("+++++++++++++++passives "^
-                  ( string_of_int (size_of_passive passive)));  
+                   ( string_of_int (size_of_passive passive)));  
   passive
 ;;
 
@@ -394,10 +397,12 @@ let check_for_deep_subsumption env active_table eq =
     match Indexing.subsumption env active_table eqtmp with
     | None -> false
     | Some (s,eq') -> 
+(*
         prerr_endline 
           ("\n\n " ^ Equality.string_of_equality ~env eq ^ 
           "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ 
           Equality.string_of_equality ~env eq' ^ "\n\n");
+*)
         true        
   in 
   let rec aux b (ok_so_far, subsumption_used) t1 t2  = 
@@ -408,30 +413,30 @@ let check_for_deep_subsumption env active_table eq =
       | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
           let rc = check_subsumed b t1 t1 in 
             if rc then 
-             true, true
-           else if h1 = h2 then
+              true, true
+            else if h1 = h2 then
               (try 
-                List.fold_left2 
-                  (fun (ok_so_far, subsumption_used) t t' -> 
-                     aux true (ok_so_far, subsumption_used) t t')
-                  (ok_so_far, subsumption_used) l l'
+                 List.fold_left2 
+                   (fun (ok_so_far, subsumption_used) t t' -> 
+                      aux true (ok_so_far, subsumption_used) t t')
+                   (ok_so_far, subsumption_used) l l'
                with Invalid_argument _ -> false,subsumption_used)
-           else
-             false, subsumption_used
+            else
+              false, subsumption_used
       | _ -> false, subsumption_used *)
       | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
           let rc = check_subsumed b t1 t2 in 
             if rc then 
-             true, true
-           else if h1 = h2 then
+              true, true
+            else if h1 = h2 then
               (try 
-                List.fold_left2 
-                  (fun (ok_so_far, subsumption_used) t t' -> 
-                     aux true (ok_so_far, subsumption_used) t t')
-                  (ok_so_far, subsumption_used) l l'
+                 List.fold_left2 
+                   (fun (ok_so_far, subsumption_used) t t' -> 
+                      aux true (ok_so_far, subsumption_used) t t')
+                   (ok_so_far, subsumption_used) l l'
                with Invalid_argument _ -> false,subsumption_used)
-           else
-             false, subsumption_used
+            else
+              false, subsumption_used
     | _ -> false, subsumption_used 
   in
   fst (aux false (true,false) left right)
@@ -529,9 +534,9 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
                 (match Indexing.subsumption env passive_table c with
                 | None -> res
                 | Some (_,c') -> 
-                   None
-                   (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
-                   Some c'*))
+                    None
+                    (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
+                    Some c'*))
 (*
               else
                 None
@@ -951,8 +956,9 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
 
-let check_if_goal_is_subsumed env (goalproof,menv,ty) table =
-  prerr_endline "check_goal_subsumed";
+let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
+  let names = names_of_context ctx in
+  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
@@ -961,6 +967,7 @@ let check_if_goal_is_subsumed env (goalproof,menv,ty) table =
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
       in
       match Indexing.subsumption env table goal_equation with
+(*       match Indexing.unification env table goal_equation with *)
         | Some (subst, equality ) ->
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
@@ -1002,7 +1009,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
             let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
             true, Some (goalproof, reflproof, Subst.empty_subst,m)
         | (_, [goal])::_ ->
-            (match check_if_goal_is_subsumed env goal (snd active) with
+            (match check_if_goal_is_subsumed env (snd active) goal with
             | None -> false,None
             | Some p ->
                 prerr_endline "Proof found by subsumption!";
@@ -1025,7 +1032,9 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
                 (let x,y,_ = passive in (fst x)@(fst y)))) in
           prerr_endline s;
           prerr_endline sp; *)
-      ParamodulationSuccess (proof))
+        match proof with 
+        | None -> assert false 
+        | Some p ->  ParamodulationSuccess p)
     else
       given_clause_fullred_aux dbd env goals theorems passive active
   else
@@ -1042,7 +1051,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
 (*       else *)
 (*         given_clause_fullred_aux env goals theorems passive active *)
 (*     else *)
-      if (passive_is_empty passive) then ParamodulationFailure
+      if (passive_is_empty passive) then ParamodulationFailure ""
       else given_clause_fullred_aux dbd env goals theorems passive active
     
 and given_clause_fullred_aux dbd env goals theorems passive active =
@@ -1110,7 +1119,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
   
   kept_clauses := (size_of_passive passive) + (size_of_active active);
   match passive_is_empty passive with
-  | true -> ParamodulationFailure 
+  | true -> ParamodulationFailure ""
       (* given_clause_fullred dbd env goals theorems passive active  *)     
   | false ->
       let current, passive = select env (fst goals) passive in
@@ -1166,8 +1175,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               let t1 = Unix.gettimeofday () in
               let active, passive, newa, retained, pruned =
                 backward_simplify env new' ~passive  active in
-             let passive = 
-               List.fold_left filter_dependent passive pruned in
+              let passive = 
+                List.fold_left filter_dependent passive pruned in
               let t2 = Unix.gettimeofday () in
                 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
@@ -1242,6 +1251,154 @@ let given_clause_fullred dbd env goals theorems passive active =
     (given_clause_fullred dbd env goals theorems passive) active
 *)
 
+let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());;
+
+let check_if_goal_is_identity env = function
+  | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
+    when left = right && iseq uri ->
+      let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+      Some (goalproof, reflproof,Subst.empty_subst,m)
+  | _ -> None
+;;                              
+    
+let rec check goal = function
+  | [] -> None
+  | f::tl ->
+      match f goal with
+      | None -> check goal tl
+      | (Some p) as ok  -> ok
+;;
+  
+let simplify_goal_set env goals passive active = 
+  (*
+  let supl_goals = 
+     (List.flatten 
+       (List.map (Indexing.superposition_left env (snd active)) 
+         goals))
+  in
+  *)
+  let simplified =
+    HExtlib.filter_map 
+      (fun g -> 
+        match simplify_goal env g ~passive active with 
+        | true, g -> Some g
+        | false, g -> Some g)
+      goals
+  in
+  HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
+    (List.sort (fun (_,_,t1) (_,_,t2) -> compare t1 t1)
+      ((*goals @*) simplified))
+;;
+
+let check_if_goals_set_is_solved env active goals =
+  List.fold_left 
+    (fun proof goal ->
+      match proof with
+      | Some p -> proof
+      | None -> 
+          check goal [
+            check_if_goal_is_identity env;
+            check_if_goal_is_subsumed env (snd active)])
+    None goals
+;;
+
+let size_of_goal_set = List.length;;
+
+(** given-clause algorithm with full reduction strategy: NEW implementation *)
+(* here goals is a set of goals in OR *)
+let given_clause
+  ((_,context,_) as env) goals theorems passive active max_iterations max_time
+= 
+  let initial_time = Unix.gettimeofday () in
+  let iterations_left iterno = 
+    let now = Unix.gettimeofday () in
+    let time_left = max_time -. now in
+    let time_spent_until_now = now -. initial_time in
+    let iteration_medium_cost = 
+      time_spent_until_now /. (float_of_int iterno)
+    in
+    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")
+    else if Unix.gettimeofday () > max_time then
+      (ParamodulationFailure "No more time to spend")
+    else
+      let goals = simplify_goal_set env goals passive active in  
+      match check_if_goals_set_is_solved env active goals with
+      | Some p -> 
+          Printf.eprintf "Found a proof in: %f\n" 
+            (Unix.gettimeofday() -. initial_time);
+          ParamodulationSuccess p
+      | None -> 
+          prerr_endline 
+            (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d\n"
+            iterno (size_of_active active) (size_of_passive passive)
+            (size_of_goal_set goals));
+          (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)  
+          let passive =
+            let selection_estimate = iterations_left iterno in
+            let kept = size_of_passive passive in
+            if kept > selection_estimate then 
+              begin
+                (*Printf.eprintf "Too many passive equalities: pruning...";
+                prune_passive selection_estimate active*) passive
+              end
+            else
+              passive
+          in
+          kept_clauses := (size_of_passive passive) + (size_of_active active);
+          (* SELECTION *)
+          if passive_is_empty passive then
+            ParamodulationFailure "No more passive" (* maybe this is a success! *)
+          else
+            begin
+              let current, passive = select env [1,goals] passive in
+              Printf.eprintf  "Selected = %s\n"
+                (Equality.string_of_equality ~env current);
+              (* SIMPLIFICATION OF CURRENT *)
+              let res = 
+                forward_simplify env (Positive, current) ~passive active 
+              in
+              match res with
+              | None -> step goals theorems passive active (iterno+1)
+              | Some current ->
+                  (* GENERATION OF NEW EQUATIONS *)
+                  let new' = infer env current active in
+                  let active = 
+                    if Equality.is_identity env current then 
+                      assert false 
+                      (* nonsense code, check to se if it can be removed *)
+                    else
+                      let al, tbl = active in
+                      al @ [current], Indexing.index tbl current
+                  in
+                  (* FORWARD AND BACKWARD SIMPLIFICATION *)
+                  let rec simplify new' active passive =
+                    let new' = forward_simplify_new env new' ~passive active in
+                    let active, passive, newa, retained, pruned =
+                      backward_simplify env new' ~passive  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
+                  in
+                  let active, passive, new' = simplify new' active passive in
+                  let goals = 
+                    let a,b,_ = build_table new' in
+                    simplify_goal_set env goals passive (a,b)
+                  in
+                  let passive = add_to_passive passive new' in
+                  step goals theorems passive active (iterno+1)
+            end
+  in
+    step goals theorems passive active 1
+;;
 
 let rec saturate_equations env goal accept_fun passive active =
   elapsed_time := Unix.gettimeofday () -. !start_time;
@@ -1267,8 +1424,8 @@ let rec saturate_equations env goal accept_fun passive active =
           let new' = forward_simplify_new env new' ~passive active in
           let active, passive, newa, retained, pruned =
             backward_simplify env new' ~passive active in
-         let passive = 
-           List.fold_left filter_dependent passive pruned in
+          let passive = 
+            List.fold_left filter_dependent passive pruned in
           match newa, retained with
           | None, None -> active, passive, new'
           | Some p, None
@@ -1513,7 +1670,9 @@ let saturate
   in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let goal = [], [], goal in
+  prerr_endline 
+    ("METASENV DEL GOAL: " ^ CicMetaSubst.ppmetasenv [] metasenv );
+  let goal = [], metasenv, goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -1562,22 +1721,34 @@ let saturate
     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 = [goal] in
+      let max_iterations = 1000 in
+      let max_time = 
+        Unix.gettimeofday () +. 
+        600. (* minutes *)
+      in
+      given_clause 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 
-      (Some (goalproof,newproof,subsumption_subst, proof_menv))
-      ->
+    (goalproof,newproof,subsumption_subst, proof_menv) ->
       prerr_endline "OK, found a proof!";
 
       prerr_endline "NEWPROOF";
      (* prerr_endline (Equality.string_of_proof_new ~names newproof
       * goalproof);*)
       prerr_endline (Equality.pp_proof names goalproof newproof);
+
+(*       assert false; *)
       
       (* generation of the proof *)
       let cic_proof_new = 
@@ -1596,14 +1767,20 @@ let saturate
       in
       let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
       prerr_endline "replacing metas (new)";
-      let newproof_menv, what, with_what = 
+      let newproof_menv, what, with_what,_ = 
         let irl = mkirl context in
         List.fold_left 
-          (fun (acc1,acc2,acc3) (i,_,ty) -> 
-            (i,context,ty)::acc1, 
-            (Cic.Meta(i,[]))::acc2, 
-            (Cic.Meta(i,irl)) ::acc3) 
-          ([],[],[]) proof_menv 
+          (fun (acc1,acc2,acc3,uniq) (i,_,ty) -> 
+             match uniq with
+               | Some m -> 
+                   acc1, 
+                   (Cic.Meta(i,[]))::acc2, 
+                   m::acc3, uniq
+               | None ->
+                   [i,context,ty], 
+                   (Cic.Meta(i,[]))::acc2, 
+                   (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
+          ([],[],[],None) proof_menv 
       in
       let cic_proof_new = ProofEngineReduction.replace_lifting
               ~equality:(=)
@@ -1616,14 +1793,14 @@ let saturate
 (*      prerr_endline (CicPp.pp cic_proof_new names); *)
 
       (* generation of proof metasenv *)
-      let newmetasenv =
+      let newmetasenv_new = metasenv@newproof_menv in
+      let newmetasenv_new =
         let i1 =
           match new_meta_goal with
           | C.Meta (i, _) -> i | _ -> assert false
         in
-        List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
+        List.filter (fun (i, _, _) -> i <> i1 && i <> goal') newmetasenv_new
       in
-      let newmetasenv_new = newmetasenv@newproof_menv in
       (* check/refine/... build the new proof *)
       let newstatus =
         let cic_proof,newmetasenv,proof_menv,ty, ug =
@@ -1659,8 +1836,8 @@ let saturate
           cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
           (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
         in
-(*        prerr_endline "FINAL PROOF";*)
-(*        prerr_endline (CicPp.pp cic_proof names);*)
+        prerr_endline "FINAL PROOF";
+        prerr_endline (CicPp.pp cic_proof names);
         prerr_endline "ENDOFPROOFS";
         (*  
         debug_print
@@ -1712,15 +1889,8 @@ let saturate
                  !passive_maintainance_time))
         end;
       newstatus 
-  | ParamodulationSuccess None -> assert false
-  | ParamodulationFailure ->
-      raise (ProofEngineTypes.Fail (lazy "NO proof found"))
 ;;
 
-(* dummy function called within matita to trigger linkage *)
-let init () = ();;
-
-
 let retrieve_and_print dbd term metasenv ugraph = 
   let module C = Cic in
   let module T = CicTypeChecker in