From: Wilmer Ricciotti Date: Mon, 20 Jul 2009 17:07:00 +0000 (+0000) Subject: added a flag for age selection X-Git-Tag: make_still_working~3652 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9450b36b5e385818adbcda257fa74260c2979fcd;p=helm.git added a flag for age selection --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index c0099a604..6dc4150c1 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -5,7 +5,7 @@ foUtils.cmi: terms.cmi orderings.cmi index.cmi: terms.cmi orderings.cmi foUnif.cmi: terms.cmi orderings.cmi superposition.cmi: terms.cmi orderings.cmi index.cmi -stats.cmi: orderings.cmi +stats.cmi: terms.cmi orderings.cmi paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi @@ -20,8 +20,10 @@ orderings.cmo: terms.cmi pp.cmi orderings.cmi orderings.cmx: terms.cmx pp.cmx orderings.cmi foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi -index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi +index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \ + index.cmi +index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \ + index.cmi foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 5c085c518..3179f0000 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -93,11 +93,11 @@ module Index(B : Orderings.Blob) = struct | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> DT.index t r (Terms.Right2Left, c) | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c -> - if are_invertible maxvar vl l r then +(* if are_invertible maxvar vl l r then (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^ (Pp.pp_foterm r)); DT.index t l (Terms.Left2Right, c)) - else + else *) DT.index (DT.index t l (Terms.Left2Right, c)) r (Terms.Right2Left, c) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index be7e140f3..8c740a0e4 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -33,7 +33,7 @@ let nparamod rdb metasenv subst context t table = HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t] in match - P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) + P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) ~g_passives:goals ~passives (bag,maxvar) with | P.Error _ | P.GaveUp | P.Timeout _ -> [] diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 06d3251f7..ac73df2d0 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -28,7 +28,8 @@ module type Paramod = type bag = t Terms.bag * int val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause - val paramod : + val paramod : + useage:bool -> max_steps:int -> ?timeout:float -> bag -> @@ -213,7 +214,7 @@ module Paramod (B : Orderings.Blob) = struct add_passive_goals g_passives new_goals ;; - let rec given_clause ~noinfer + let rec given_clause ~useage ~noinfer bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives = @@ -244,14 +245,14 @@ module Paramod (B : Orderings.Blob) = struct else if false then (* activates last chance strategy *) begin debug("Last chance: "^string_of_float (Unix.gettimeofday())); - given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps + given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps (Some (Unix.gettimeofday () +. 20.)) actives passives g_actives g_passives; raise (Stop (Timeout (maxvar,bag))); end else raise (Stop (Timeout (maxvar,bag))); - let use_age = false && (weight_picks = (iterno / 6 + 1)) in + let use_age = useage && (weight_picks = (iterno / 6 + 1)) in let weight_picks = if use_age then 0 else weight_picks+1 in @@ -341,12 +342,12 @@ module Paramod (B : Orderings.Blob) = struct debug (Printf.sprintf "Number of passives : %d" (passive_set_cardinal passives)); - given_clause ~noinfer + given_clause ~useage ~noinfer bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives ;; - let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = let initial_timestamp = Unix.gettimeofday () in let passives = add_passive_clauses ~no_weight:true passive_empty_set passives @@ -357,7 +358,7 @@ module Paramod (B : Orderings.Blob) = struct let g_actives = [] in let actives = [], IDX.DT.empty in try - given_clause ~noinfer:false + given_clause ~useage ~noinfer:false bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives with | Sup.Success (bag, _, (i,_,_,_)) -> diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index e133036af..9cffd9d28 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -24,6 +24,7 @@ module type Paramod = val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause val paramod : + useage:bool -> max_steps:int -> ?timeout:float -> bag -> diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml index 0f9f45d96..fd68f0fe7 100644 --- a/helm/software/components/ng_paramodulation/stats.ml +++ b/helm/software/components/ng_paramodulation/stats.ml @@ -83,6 +83,12 @@ module Stats (B : Terms.Blob) = (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res [] ;; + let rec leaf_count = function + | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l + | Terms.Leaf _ -> 1 + | _ -> 0 + ;; + let rec dependencies op clauses acc = match clauses with | [] -> acc @@ -109,10 +115,21 @@ module Stats (B : Terms.Blob) = else dependencies op tl acc else dependencies op tl acc + | ((Terms.Node (Terms.Leaf op1::t) as x),y) + | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y -> + let rec term_leaves = function + | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l + | Terms.Leaf x -> [x] + | _ -> [] + in + if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then + dependencies op tl (op1::acc) + else + dependencies op tl acc | _ -> dependencies op tl acc ;; - let dependencies op clauses = dependencies op clauses [];; + let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));; (* let max_weight_hyp = *)