X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=4a1b2f6c72ea32be73696c725e225e22c604caf0;hb=1eb00eff3c3a5f67c3a200a82098c97f4fbe0c5e;hp=435c95024416b3f232ce280855605de6e0cc1fb1;hpb=07fb52e761b192a97c6fe00c657e670b2d1fc2f1;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 435c95024..4a1b2f6c7 100644
--- 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)
@@ -168,8 +172,7 @@ module Paramod (B : Terms.Blob) = struct
       let bag, maxvar, new_goals = 
         List.fold_left 
           (fun (bag,m,acc) g -> 
-             let bag, m, ng = Sup.infer_left bag m g
-               ([current],ctable) in
+             let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
                bag,m,ng@acc) 
           (bag,maxvar,[]) g_actives 
       in
@@ -219,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)