From: denes <??>
Date: Tue, 30 Jun 2009 10:20:40 +0000 (+0000)
Subject: Enabled age selection (ratio 1/5)
X-Git-Tag: make_still_working~3769
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d4dc2f5ea9651ac93c9df478bf1298ed876b518;p=helm.git

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 a970bb6f0..9daefe305 100644
--- 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 6c3c5118d..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)
@@ -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)