From a872dba2b03e27967d5b9b51e950e85967340e52 Mon Sep 17 00:00:00 2001 From: denes Date: Tue, 30 Jun 2009 14:12:52 +0000 Subject: [PATCH] Moved ID management inside the bag --- .../components/ng_paramodulation/.depend | 12 +++++------ .../components/ng_paramodulation/foUtils.ml | 16 +------------- .../components/ng_paramodulation/foUtils.mli | 7 ------- .../ng_paramodulation/nCicParamod.ml | 2 +- .../components/ng_paramodulation/nCicProof.ml | 2 +- .../components/ng_paramodulation/paramod.ml | 16 +++++++------- .../components/ng_paramodulation/pp.ml | 6 +++--- .../ng_paramodulation/superposition.ml | 10 ++++----- .../components/ng_paramodulation/terms.ml | 21 ++++++++++++++++++- .../components/ng_paramodulation/terms.mli | 17 ++++++++++++++- 10 files changed, 61 insertions(+), 48 deletions(-) diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 2a989273b..ead11bcc5 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -11,8 +11,8 @@ cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi -pp.cmo: terms.cmi pp.cmi -pp.cmx: terms.cmx pp.cmi +pp.cmo: terms.cmi foUtils.cmi pp.cmi +pp.cmx: terms.cmx foUtils.cmx pp.cmi foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi orderings.cmo: terms.cmi orderings.cmi @@ -35,9 +35,9 @@ nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi -nCicProof.cmo: terms.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx: terms.cmx foSubst.cmx nCicProof.cmi -nCicParamod.cmo: terms.cmi paramod.cmi nCicProof.cmi nCicBlob.cmi \ +nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi +nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi +nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi nCicProof.cmi nCicBlob.cmi \ nCicParamod.cmi -nCicParamod.cmx: terms.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \ +nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \ nCicParamod.cmi diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 9daefe305..454432ec4 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -21,11 +21,6 @@ let rec lexicograph f l1 l2 = | _,[] -> 1 ;; -let mk_id = - let id = ref 0 in - fun () -> incr id; !id -;; - module Utils (B : Terms.Blob) = struct module Subst = FoSubst;; (*.Subst(B) ;;*) module Order = Orderings.Orderings(B) ;; @@ -124,18 +119,9 @@ module Utils (B : Terms.Blob) = struct | t -> Terms.Predicate t in let proof = Terms.Exact proofterm in - fresh_unit_clause maxvar (mk_id (), lit, varlist, proof) + fresh_unit_clause maxvar (0, lit, varlist, proof) ;; - let add_to_bag bag (_,lit,vl,proof) = - let id = mk_id () in - let clause = (id, lit, vl, proof) in - let bag = Terms.M.add id (clause,false) bag in - bag, clause - ;; - - let empty_bag = Terms.M.empty ;; - let mk_passive_clause cl = (Order.compute_unit_clause_weight cl, cl) ;; diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 139e81f2e..c23779bde 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -42,13 +42,6 @@ module Utils (B : Terms.Blob) : (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *) val relocate : int -> int list -> int * int list * B.t Terms.substitution - (* also gives a fresh ID to the clause *) - val add_to_bag : - B.t Terms.bag -> B.t Terms.unit_clause -> - B.t Terms.bag * B.t Terms.unit_clause - - val empty_bag : B.t Terms.bag - val compare_passive_clauses_weight : B.t Terms.passive_clause -> B.t Terms.passive_clause -> int diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 6c1aa695e..379aca1dc 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -25,7 +25,7 @@ let nparamod rdb metasenv subst context t table = in let module P = Paramod.Paramod(B) in let module Pp = Pp.Pp(B) in - let bag, maxvar = Terms.M.empty, 0 in + let bag, maxvar = Terms.empty_bag, 0 in let (bag,maxvar), passives = HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table in diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 37abd6edf..0dbaa1a8f 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -120,7 +120,7 @@ t vl in let get_literal id = - let (_, lit, vl, proof),_ = Terms.M.find id bag in + let (_, lit, vl, proof),_ = Terms.get_from_bag id bag in let lit =match lit with | Terms.Predicate t -> assert false | Terms.Equation (l,r,ty,_) -> diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 4a1b2f6c7..a6f3a93c7 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,9 +12,9 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let debug s = prerr_endline s ;; -(* let debug _ = ();;*) +let debug _ = ();; -let monster = 500;; +let monster = 100;; module Paramod (B : Terms.Blob) = struct exception Failure of string * B.t Terms.bag * int * int @@ -99,7 +99,7 @@ module Paramod (B : Terms.Blob) = struct let mk_clause bag maxvar (t,ty) = let (proof,ty) = B.saturate t ty in let c, maxvar = Utils.mk_unit_clause maxvar ty proof in - let bag, c = Utils.add_to_bag bag c in + let bag, c = Terms.add_to_bag c bag in (bag, maxvar), c ;; @@ -226,10 +226,10 @@ module Paramod (B : Terms.Blob) = struct let rec aux_select bag passives g_passives = let backward,(weight,current),passives,g_passives = - select ~use_age passives g_passives + select ~use_age:false passives g_passives in if use_age && weight > monster then - let bag,cl = Utils.add_to_bag bag current in + let bag,cl = Terms.add_to_bag current bag in if backward then aux_select bag passives (add_passive_clause g_passives cl) else @@ -260,8 +260,8 @@ module Paramod (B : Terms.Blob) = struct if weight > monster then bag,None else bag, Some (current,actives) else if Sup.orphan_murder bag (fst actives) current then - let (id,_,_,_) = current in - let bag = Terms.M.add id (current,true) bag in + let _ = debug "Orphan murdered" in + let bag = Terms.replace_in_bag (current,true) bag in bag, None else Sup.keep_simplified current actives bag maxvar with @@ -331,7 +331,7 @@ module Paramod (B : Terms.Blob) = struct | Sup.Success (bag, _, (i,_,_,_)) -> let l = let rec traverse ongoal (accg,acce) i = - match Terms.M.find i bag with + match Terms.get_from_bag i bag with | (id,_,_,Terms.Exact _),_ -> if ongoal then [i],acce else if (List.mem i acce) then accg,acce else accg,acce@[i] diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index cb971ea74..1c9fb2fc6 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -68,8 +68,8 @@ let pp_proof bag ~formatter:f p = eq (string_of_rule rule); Format.fprintf f "|%d with %d dir %s))" eq1 eq2 (string_of_direction dir); - let (_, _, _, proof1),_ = Terms.M.find eq1 bag in - let (_, _, _, proof2),_ = Terms.M.find eq2 bag in + let (_, _, _, proof1),_ = Terms.get_from_bag eq1 bag in + let (_, _, _, proof2),_ = Terms.get_from_bag eq2 bag in Format.fprintf f "@["; aux eq1 proof1; aux eq2 proof2; @@ -120,7 +120,7 @@ let pp_unit_clause ~formatter:f c = Format.fprintf f "@]" ;; -let pp_bag ~formatter:f bag = +let pp_bag ~formatter:f (_,bag) = Format.fprintf f "@["; Terms.M.iter (fun _ (c,d) -> pp_unit_clause ~formatter:f c; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index d3e6000b7..96b16bb07 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -92,7 +92,7 @@ module Superposition (B : Terms.Blob) = | t -> Terms.Predicate t in let bag, uc = - Utils.add_to_bag bag (0, literal, vars_of_term t, proof) + Terms.add_to_bag (0, literal, vars_of_term t, proof) bag in Some (bag, uc) else @@ -302,7 +302,7 @@ module Superposition (B : Terms.Blob) = ;; let rec orphan_murder bag acc i = - match Terms.M.find i bag with + match Terms.get_from_bag i bag with | (_,_,_,Terms.Exact _),discarded -> (discarded,acc) | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc) | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false -> @@ -335,8 +335,8 @@ module Superposition (B : Terms.Blob) = let simplify table maxvar bag clause = match simplify table maxvar bag clause with - | bag, None -> let (id,_,_,_) = clause in - Terms.M.add id (clause,true) bag, None + | bag, None -> + Terms.replace_in_bag (clause,true) bag, None | bag, Some clause -> bag, Some clause (*let (id,_,_,_) = clause in if orphan_murder bag clause then @@ -573,7 +573,7 @@ module Superposition (B : Terms.Blob) = let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in (* We need to put fresh_current into the bag so that all * * variables clauses refer to are known. *) - let bag, fresh_current = Utils.add_to_bag bag fresh_current in + let bag, fresh_current = Terms.add_to_bag fresh_current bag in (* We superpose current with active clauses *) let bag, maxvar, additional_new_clauses = superposition_with_table bag maxvar fresh_current atable diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 1d1465f9e..aefbc01a8 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -56,7 +56,26 @@ module OT = module M : Map.S with type key = int = Map.Make(OT) -type 'a bag = ('a unit_clause * bool) M.t +type 'a bag = int + * (('a unit_clause * bool) M.t) + + let add_to_bag (_,lit,vl,proof) (id,bag) = + let id = id+1 in + let clause = (id, lit, vl, proof) in + let bag = M.add id (clause,false) bag in + (id,bag), clause + ;; + + let replace_in_bag ((id,_,_,_),_ as cl) (max_id,bag) = + let bag = M.add id cl bag in + (max_id,bag) + ;; + + let get_from_bag id (_,bag) = + M.find id bag + ;; + + let empty_bag = (0,M.empty);; module type Blob = sig diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index e0576d1f3..89d6993d9 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -54,7 +54,22 @@ type 'a passive_clause = int * 'a unit_clause (* weight * equation *) module M : Map.S with type key = int -type 'a bag = ('a unit_clause * bool) M.t +type 'a bag = int (* max ID *) + * (('a unit_clause * bool) M.t) + +(* also gives a fresh ID to the clause *) + val add_to_bag : + 'a unit_clause -> 'a bag -> + 'a bag * 'a unit_clause + + val replace_in_bag : + 'a unit_clause * bool -> 'a bag -> + 'a bag + + val get_from_bag : + int -> 'a bag -> 'a unit_clause * bool + + val empty_bag : 'a bag module type Blob = sig -- 2.39.2