Added the computation of max_weight for equations in proofs.

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d4ccf8f42bbcc71f172f6b69085c273437541f36..c40b4a9ac238de328366c0c49fa9ec6e067dc23b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -153,11 +153,13 @@ let age_factor = 0.01;;
    of weight, age and goal-similarity
 *)
 
-let rec select env (goals,_) passive =
+let rec select env g passive =
   processed_clauses := !processed_clauses + 1;
+(*
   let goal =
     match (List.rev goals) with goal::_ -> goal | _ -> assert false
   in
+*)
   let pos_list, pos_set = passive in
   let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
   if !weight_age_ratio > 0 then
@@ -165,20 +167,38 @@ let rec select env (goals,_) passive =
   match !weight_age_counter with
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
+      let skip_giant pos_list pos_set =
+        match pos_list with
+          | (hd:EqualitySet.elt)::tl ->
+              let w,_,_,_,_ = Equality.open_equality hd in
+                if w < 30 then
+                  hd, (tl, EqualitySet.remove hd pos_set)
+                else
+                  (prerr_endline 
+                    ("+++ skipping giant of size "^string_of_int w^" +++");
+                  select env g (tl@[hd],pos_set))
+          | _ -> assert false
+                  in
+                   skip_giant pos_list pos_set)
+
+(*
       let rec skip_giant pos_list pos_set =
         match pos_list with
           | (hd:EqualitySet.elt)::tl ->
               let w,_,_,_,_ = Equality.open_equality hd in
               let pos_set = EqualitySet.remove hd pos_set in
-                if w < 500 then
+                if w < 30 then
                   hd, (tl, pos_set)
                 else
                   (prerr_endline 
                     ("+++ skipping giant of size "^string_of_int w^" +++");
                   skip_giant tl pos_set)
           | _ -> assert false
-      in
-        skip_giant pos_list pos_set)
+      in        
+  skip_giant pos_list pos_set)
+
+*)
+(*
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
@@ -216,6 +236,7 @@ let rec select env (goals,_) passive =
       let _, current = EqualitySet.fold f pos_set initial in
         current,
       (remove current pos_list, EqualitySet.remove current pos_set))
+*)
   | _ ->
       symbols_counter := !symbols_ratio;
       let my_min e1 e2 =
@@ -843,6 +864,10 @@ let simplify_goal_set env goals active =
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
   in
+    (* prova:tengo le passive semplificate 
+  let passive_goals = 
+    List.map (fun g -> snd (simplify_goal env g active)) passive_goals 
+  in *)
     List.fold_left
       (fun (acc_a,acc_p) goal -> 
         match simplify_goal env goal active with 
@@ -864,6 +889,7 @@ let check_if_goals_set_is_solved env active goals =
           check goal [
             check_if_goal_is_identity env;
             check_if_goal_is_subsumed env (snd active)])
+(* provare active and passive?*)
     None active_goals
 ;;
 
@@ -958,7 +984,6 @@ let given_clause
     int_of_float iterations_left 
   in
   let rec step goals theorems passive active iterno =
-    pp_goals "xxx" goals context;
     if iterno > max_iterations then
       (ParamodulationFailure "No more iterations to spend")
     else if Unix.gettimeofday () > max_time then
@@ -989,7 +1014,8 @@ let given_clause
           passive
       in
       kept_clauses := (size_of_passive passive) + (size_of_active active);
-      let goals = infer_goal_set env active goals in
+      let goals = infer_goal_set env active goals 
+      in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
           prerr_endline 
@@ -1267,7 +1293,9 @@ let saturate
       prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline "ENDOFPROOFS";
+      prerr_endline "ENDOFPROOFS___";
+      prerr_endline ("max weight: " ^ 
+       (string_of_int (Equality.max_weight goalproof newproof)));
       (* generation of the CIC proof *)
       let side_effects = 
         List.filter (fun i -> i <> goalno)