X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=e7ef6fa7c2b9def7764a18273fef1981eaf91baa;hb=a0cb7cf4ac234997157aac20a1a68a4a88e805e1;hp=bb1b3a853515d22c49fecc0e9b43e944e0b55d17;hpb=a67679766c06b41ec29e695eb52091229dbba282;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index bb1b3a853..e7ef6fa7c 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -901,6 +901,17 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
               
+let pp_goal_set msg goals names = 
+  let active_goals, passive_goals = goals in
+  prerr_endline ("////" ^ msg);
+  prerr_endline ("ACTIVE G: " ^
+    (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+    active_goals)));
+  prerr_endline ("PASSIVE G: " ^
+    (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+    passive_goals)))
+;;
+
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*
   let names = names_of_context ctx in
@@ -959,7 +970,7 @@ let rec check goal = function
       | (Some p) as ok  -> ok
 ;;
   
-let simplify_goal_set env goals passive active = 
+let simplify_goal_set env goals ?passive active = 
   let active_goals, passive_goals = goals in 
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
@@ -967,7 +978,7 @@ let simplify_goal_set env goals passive active =
   let simplified =
     List.fold_left
       (fun acc goal -> 
-        match simplify_goal env goal ~passive active with 
+        match simplify_goal env goal ?passive active with 
         | changed, g -> 
             if changed then prerr_endline "???????????????cambiato ancora";
             if find g acc then acc else g::acc)
@@ -1000,26 +1011,28 @@ let check_if_goals_set_is_solved env active goals =
 let infer_goal_set env active goals = 
   let active_goals, passive_goals = goals in
   let rec aux = function
-    | [] -> goals
+    | [] -> active_goals, []
     | hd::tl ->
         let changed,selected = simplify_goal env hd active in
         if changed then
           prerr_endline ("--------------- goal semplificato");
         let (_,_,t1) = selected in
-        if (List.exists 
-             (fun (_,_,t) -> 
-	 	 Equality.meta_convertibility t t1) 
-              active_goals) then aux tl
-        else
-        let passive_goals = tl in
-        let new_passive_goals =
-          if Utils.metas_of_term t1 = [] then passive_goals
-          else 
-            let new' = 
-               Indexing.superposition_left env (snd active) selected in
-            passive_goals @ new'
+        let already_in = 
+          List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
+              active_goals
         in
-        selected::active_goals, new_passive_goals
+        if already_in then 
+             aux tl
+          else
+            let passive_goals = tl in
+            let new_passive_goals =
+              if Utils.metas_of_term t1 = [] then passive_goals
+              else 
+                let new' = 
+                   Indexing.superposition_left env (snd active) selected in
+                passive_goals @ new'
+            in
+            selected::active_goals, new_passive_goals
   in 
   aux passive_goals
 ;;
@@ -1053,8 +1066,11 @@ let infer_goal_set env active goals =
 
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
-  let _,table,_ = build_table [current] in
-  active_goals,
+  let l,table,_  = build_table [current] in
+  let active_goals, _ = 
+    simplify_goal_set env goals (l,table)
+  in
+  active_goals, 
   List.fold_left 
     (fun acc g ->
       let new' = Indexing.superposition_left env table g in
@@ -1152,6 +1168,11 @@ let given_clause
                    prerr_endline (Printf.sprintf  "Current goal = %s\n"
                     (CicPp.pp g names))) 
                  (fst goals);
+                List.iter                 
+                 (fun _,_,g -> 
+                   prerr_endline (Printf.sprintf  "Passive goal = %s\n"
+                    (CicPp.pp g names))) 
+                 (snd goals);
                 prerr_endline (Printf.sprintf  "Selected = %s\n"
                   (Equality.string_of_equality ~env current))
               in
@@ -1167,6 +1188,15 @@ let given_clause
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
+(*
+      match check_if_goals_set_is_solved env active goals with
+      | Some p -> 
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+          ParamodulationSuccess p
+      | None -> 
+*)
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
@@ -1194,7 +1224,7 @@ let given_clause
                   let goals = 
                     let a,b,_ = build_table new' in
                     let _ = <:start<simplify_goal_set new>> in
-                    let rc = simplify_goal_set env goals passive (a,b) in
+                    let rc = simplify_goal_set env goals ~passive (a,b) in
                     let _ = <:stop<simplify_goal_set new>> in
                     rc
                   in
@@ -1225,6 +1255,8 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
             let al, tbl = active in
             al @ [current], Indexing.index tbl current
         in
+        (* 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' ~passive active in
           let active, passive, newa, retained, pruned =
@@ -1461,6 +1493,7 @@ let eq_and_ty_of_goal = function
 ;;
 
 let saturate 
+    caso_strano 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
   reset_refs ();
@@ -1481,7 +1514,7 @@ let saturate
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
-      find_library_equalities dbd context (proof, goalno) (maxm+2)
+      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
@@ -1531,7 +1564,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in
@@ -1675,7 +1708,7 @@ let retrieve_and_print dbd term metasenv ugraph =
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
   let lib_eq_uris, library_equalities, maxm =
-    find_library_equalities dbd context (proof, goal') (maxm+2) in
+    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
@@ -1753,7 +1786,7 @@ let main_demod_equalities dbd term metasenv ugraph =
   let eq_uri = eq_of_goal goal in 
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let lib_eq_uris, library_equalities, maxm =
-    find_library_equalities dbd context (proof, goal') (maxm+2)
+    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!! *)
@@ -1832,7 +1865,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
     Inference.find_equalities context proof 
   in
   let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in
+    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