Enabled age selection (ratio 1/5)

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index a970bb6f0c51ee67870e6577b9797daf45b1abca..9daefe305a215e3eca30939c4cd458488fc5f704 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -141,7 +141,7 @@ module Utils (B : Terms.Blob) = struct
   ;;
 
   let mk_passive_goal g =
-    (Order.compute_goal_weight g, g)
+    (Order.compute_unit_clause_weight g, g)
   ;;
 
   let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 6c3c5118d62362eadc982fa63ecfbd9672b635cc..4a1b2f6c72ea32be73696c725e225e22c604caf0 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let debug s = prerr_endline s ;;
-let debug _ = ();;
+(* let debug _ = ();;*)
 
 let monster = 500;;
     
@@ -118,7 +118,11 @@ module Paramod (B : Terms.Blob) = struct
         (false,cl,remove_passive_clause passives cl,g_passives)
       else
         let g_cl = pick_min_passive ~use_age:use_age g_passives in
-          if (fst cl <= fst g_cl) then
+       let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
+       let cmp = if use_age then id1 <= id2
+       else fst cl <= fst g_cl
+       in
+          if cmp then
             (false,cl,remove_passive_clause passives cl,g_passives)
           else
             (true,g_cl,passives,remove_passive_clause g_passives g_cl)
@@ -218,13 +222,21 @@ module Paramod (B : Terms.Blob) = struct
           end
         else raise (Failure ("Timeout !",bag,maxvar,iterno));
 
-    (* let use_age = iterno mod 10 = 0 in *)
+    let use_age = iterno mod 5 = 0 in
 
     let rec aux_select bag passives g_passives =
       let backward,(weight,current),passives,g_passives =
-        select ~use_age:false passives g_passives
+        select ~use_age passives g_passives
       in
+       if use_age && weight > monster then
+         let bag,cl = Utils.add_to_bag bag current in
+           if backward then
+             aux_select bag passives (add_passive_clause g_passives cl)
+           else
+             aux_select bag (add_passive_clause passives cl) g_passives
+       else
         if backward then
+          let _ = debug ("Selected goal : " ^ Pp.pp_unit_clause current) in
          match 
            if noinfer then 
              if weight > monster then None else Some (bag,current)