From 9d4dc2f5ea9651ac93c9df478bf1298ed876b518 Mon Sep 17 00:00:00 2001 From: denes Date: Tue, 30 Jun 2009 10:20:40 +0000 Subject: [PATCH] Enabled age selection (ratio 1/5) --- .../components/ng_paramodulation/foUtils.ml | 2 +- .../components/ng_paramodulation/paramod.ml | 20 +++++++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) 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) -- 2.39.2