From: denes <??>
Date: Thu, 25 Jun 2009 12:19:45 +0000 (+0000)
Subject: Now using age selection
X-Git-Tag: make_still_working~3801
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=51f49e56206b6b2388a8b30dc35e1011491966ee;p=helm.git

Now using age selection
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b898d353b..105f5c86b 100644
--- 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