From 07fb52e761b192a97c6fe00c657e670b2d1fc2f1 Mon Sep 17 00:00:00 2001 From: denes Date: Mon, 29 Jun 2009 13:33:42 +0000 Subject: [PATCH] First attempt for refined goal selection strategy --- .../components/ng_paramodulation/foUtils.ml | 4 ++++ .../components/ng_paramodulation/foUtils.mli | 3 +++ .../components/ng_paramodulation/orderings.ml | 17 ++++++++++++++ .../ng_paramodulation/orderings.mli | 3 +++ .../components/ng_paramodulation/paramod.ml | 22 ++++++++++++++++--- 5 files changed, 46 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 4c99f5b9c..a970bb6f0 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -140,6 +140,10 @@ module Utils (B : Terms.Blob) = struct (Order.compute_unit_clause_weight cl, cl) ;; + let mk_passive_goal g = + (Order.compute_goal_weight g, g) + ;; + let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) = if w1 = w2 then id1 - id2 else w1 - w2 diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 5cbe461a0..139e81f2e 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -29,6 +29,9 @@ module Utils (B : Terms.Blob) : val mk_passive_clause : B.t Terms.unit_clause -> B.t Terms.passive_clause + val mk_passive_goal : + B.t Terms.unit_clause -> B.t Terms.passive_clause + val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 51b48a4c3..5c42090c4 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -68,6 +68,23 @@ module Orderings (B : Terms.Blob) = struct let wr, mr = weight_of_term r in weight_of_polynomial (wl+wr) (ml@mr) ;; + +let compute_goal_weight (_,l, _, _) = + let weight_of_polynomial w m = + let factor = 2 in + w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m + in + match l with + | Terms.Predicate t -> + let w, m = weight_of_term t in + weight_of_polynomial w m + | Terms.Equation (l,r,_,_) -> + let wl, ml = weight_of_term l in + let wr, mr = weight_of_term r in + let wl = weight_of_polynomial wl ml in + let wr = weight_of_polynomial wr mr in + - (abs (wl-wr)) + ;; (* Riazanov: 3.1.5 pag 38 *) (* Compare weights normalized in a new way : diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index 7586d41ac..ab5c1897b 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -25,4 +25,7 @@ module Orderings (B : Terms.Blob) : val compute_unit_clause_weight : B.t Terms.unit_clause -> int + val compute_goal_weight : + B.t Terms.unit_clause -> int + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 43b57b6cd..435c95024 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -45,6 +45,12 @@ module Paramod (B : Terms.Blob) = struct WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a ;; + let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g = + let g = if no_weight then (0,g) + else Utils.mk_passive_goal g in + WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a + ;; + let remove_passive_clause (passives_w,passives_a) cl = let passives_w = WeightPassiveSet.remove cl passives_w in let passives_a = AgePassiveSet.remove cl passives_a in @@ -61,6 +67,16 @@ module Paramod (B : Terms.Blob) = struct AgePassiveSet.union new_clauses_a passives_a) ;; + let add_passive_goals ?(no_weight=false) + (passives_w,passives_a) new_clauses = + let new_clauses_w,new_clauses_a = + List.fold_left (add_passive_goal ~no_weight) + (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses + in + (WeightPassiveSet.union new_clauses_w passives_w, + AgePassiveSet.union new_clauses_a passives_a) + ;; + let is_passive_set_empty (passives_w,passives_a) = if (WeightPassiveSet.is_empty passives_w) then begin assert (AgePassiveSet.is_empty passives_a); true @@ -117,7 +133,7 @@ module Paramod (B : Terms.Blob) = struct in debug "Performed infer_left step"; bag, maxvar, actives, passives, g_current::g_actives, - (add_passive_clauses g_passives new_goals) + (add_passive_goals g_passives new_goals) ;; let forward_infer_step bag maxvar actives passives g_actives @@ -159,7 +175,7 @@ module Paramod (B : Terms.Blob) = struct in bag, maxvar, actives, add_passive_clauses passives new_clauses, g_actives, - add_passive_clauses g_passives new_goals + add_passive_goals g_passives new_goals ;; let rec given_clause ~noinfer @@ -293,7 +309,7 @@ module Paramod (B : Terms.Blob) = struct add_passive_clauses ~no_weight:true passive_empty_set passives in let g_passives = - add_passive_clauses ~no_weight:true passive_empty_set g_passives + add_passive_goals ~no_weight:true passive_empty_set g_passives in let g_actives = [] in let actives = [], IDX.DT.empty in -- 2.39.2