Now using age selection

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b898d353babce559769c77239d630d1bae9b404b..105f5c86b11ad6ecb0a2f46d8d5f8b11f795684f 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,8 +11,8 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline s ;;
-(* let debug _ = ();; *)
+(* let debug s = prerr_endline s ;;*)
+ let debug _ = ();;
     
 let max_nb_iter = 999999999 ;;
 let amount_of_time = 300.0 ;;
@@ -74,7 +74,7 @@ module Paramod (B : Terms.Blob) = struct
     (WeightPassiveSet.empty,AgePassiveSet.empty)
   ;;
 
-  let pick_min_passive use_age (passives_w,passives_a) =
+  let pick_min_passive ~use_age (passives_w,passives_a) =
     if use_age then AgePassiveSet.min_elt passives_a
     else WeightPassiveSet.min_elt passives_w
   ;;
@@ -90,17 +90,17 @@ module Paramod (B : Terms.Blob) = struct
   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
 
   (* TODO : global age over facts and goals (without comparing weights) *)
-  let select passives g_passives =
+  let select ~use_age passives g_passives =
     if is_passive_set_empty passives then begin
       assert (not (is_passive_set_empty g_passives));
-      let g_cl = pick_min_passive false g_passives in
+      let g_cl = pick_min_passive ~use_age:use_age g_passives in
        (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
     end
-    else let cl = pick_min_passive false passives in
+    else let cl = pick_min_passive ~use_age:use_age passives in
       if is_passive_set_empty g_passives then
        (false,snd cl,remove_passive_clause passives cl,g_passives)
       else
-       let g_cl = pick_min_passive false g_passives in
+       let g_cl = pick_min_passive ~use_age:use_age g_passives in
          if (fst cl <= fst g_cl) then
            (false,snd cl,remove_passive_clause passives cl,g_passives)
          else
@@ -132,9 +132,6 @@ module Paramod (B : Terms.Blob) = struct
      * new'= demod A'' new    *
      * P' = P + new'          *)
     debug "Forward infer step...";
-    debug "Selected and simplified";
-    (* debug ("Fact after simplification :"
-       ^ Pp.pp_unit_clause current); *)
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
@@ -173,8 +170,12 @@ module Paramod (B : Terms.Blob) = struct
     if Unix.gettimeofday () > timeout then
       raise (Failure ("Timeout !",bag,maxvar,nb_iter));
 
+    let use_age = nb_iter mod 10 = 0 in
+
     let rec aux_select passives g_passives =
-      let backward,current,passives,g_passives = select passives g_passives in
+      let backward,current,passives,g_passives =
+       select ~use_age passives g_passives
+      in
        if backward then
         match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
            | None -> aux_select passives g_passives