]> matita.cs.unibo.it Git - helm.git/commitdiff
some experiments
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 19 Jun 2006 13:06:10 +0000 (13:06 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 19 Jun 2006 13:06:10 +0000 (13:06 +0000)
helm/software/components/tactics/paramodulation/saturation.ml

index b50e0a49f09fdafdaea42c51db772a880a58422c..67a328275b2d68b543ef16d2c079a566a5f8043b 100644 (file)
@@ -213,7 +213,17 @@ let rec select env (goals,_) passive =
        passive_table))
   | _ ->
       symbols_counter := !symbols_ratio;
-      let current = EqualitySet.min_elt pos_set in
+      let my_min e1 e2 =
+        let w1,_,_,_,_ = Equality.open_equality e1 in
+       let w2,_,_,_,_ = Equality.open_equality e2 in
+       if w1 < w2 then e1 else e2
+      in
+      let rec my_min_elt min = function
+        | [] -> min
+       | hd::tl -> my_min_elt (my_min hd min) tl
+      in
+      (* let current = EqualitySet.min_elt pos_set in *)
+      let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in
       let passive_table =
         Indexing.remove_index passive_table current
       in
@@ -958,7 +968,9 @@ let simplify_goal_set env goals passive active =
     List.fold_left
       (fun acc goal -> 
         match simplify_goal env goal ~passive active with 
-        | _, g -> if find g acc then acc else g::acc)
+        | changed, g -> 
+            if changed then prerr_endline "???????????????cambiato ancora";
+            if find g acc then acc else g::acc)
       (* active_goals active_goals *)
       [] active_goals
   in
@@ -973,7 +985,7 @@ let simplify_goal_set env goals passive active =
 ;;
 
 let check_if_goals_set_is_solved env active goals =
-  let active_goals, passive_goals = goals in 
+  let active_goals, passive_goals = goals in
   List.fold_left 
     (fun proof goal ->
       match proof with
@@ -985,29 +997,59 @@ let check_if_goals_set_is_solved env active goals =
     None active_goals
 ;;
 
+let infer_goal_set env active goals = 
+  let active_goals, passive_goals = goals in
+  let rec aux = function
+    | [] -> 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'
+        in
+        selected::active_goals, new_passive_goals
+  in 
+  aux passive_goals
+;;
+
+(* old
 let infer_goal_set env active goals = 
   let active_goals, passive_goals = goals in
   let rec aux = function
     | [] -> goals
     | ((_,_,t1) as hd)::tl when 
-       not (List.exists 
-             (fun (_,_,t) -> Equality.meta_convertibility t t1) 
-             active_goals)
+        not (List.exists 
+              (fun (_,_,t) -> 
+                 Equality.meta_convertibility t t1) 
+              active_goals)
        -> 
         let selected = hd in
         let passive_goals = tl in
-        let _,_,ty = selected in 
-        let new' = 
-          if CicUtil.is_meta_closed ty then
-            []
-          else
-            Indexing.superposition_left env (snd active) selected 
+        let new_passive_goals =
+          if CicUtil.is_meta_closed t1 then 
+           passive_goals
+          else 
+            let new' = Indexing.superposition_left env (snd active) selected in
+            passive_goals @ new'
         in
-        selected::active_goals, passive_goals @ new'
+        selected::active_goals, new_passive_goals
     | _::tl -> aux tl
   in 
   aux passive_goals
 ;;
+*)
 
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
@@ -1048,10 +1090,12 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
+      (* 
       let _ = prerr_endline "simpl goal with active" in
       let _ = <:start<simplify goal set active>> in
-      let goals = simplify_goal_set env goals passive active in  
+      let goals = simplify_goal_set env goals passive active in 
       let _ = <:stop<simplify goal set active>> in
+      *)
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
           prerr_endline 
@@ -1064,7 +1108,8 @@ let given_clause
             (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
             iterno (size_of_active active) (size_of_passive passive)
             (size_of_goal_set_a goals) (size_of_goal_set_p goals));
-          (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)  
+          (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
+          (*
           let passive =
             let selection_estimate = iterations_left iterno in
             let kept = size_of_passive passive in
@@ -1077,6 +1122,7 @@ let given_clause
               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! *)
@@ -1084,9 +1130,11 @@ let given_clause
             begin
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
-              let _,_,goaltype = List.hd (fst goals) in                
-              prerr_endline (Printf.sprintf  "Current goal = %s\n"
-                (CicPp.pp goaltype names));
+              let _,_,goaltype = List.hd (fst goals) in
+              List.iter                 
+                 (fun _,_,g -> 
+                    prerr_endline (Printf.sprintf  "Current goal = %s\n"
+                      (CicPp.pp g names))) (fst goals);
               prerr_endline (Printf.sprintf  "Selected = %s\n"
                 (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
@@ -1098,6 +1146,7 @@ let given_clause
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
                   prerr_endline "infer";
+                 let _,_,_,_,id = Equality.open_equality current in
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
@@ -1404,7 +1453,8 @@ let saturate
   let eq_indexes, equalities, maxm = 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, type_of_goal in
+  let cleaned_goal = Utils.remove_local_context type_of_goal 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 =