From 2041f4fefe300f77338f6aea598f025f84db1bbc Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 29 Jul 2009 16:17:28 +0000 Subject: [PATCH] Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertible (in orderings) --- .../components/ng_paramodulation/.depend | 29 ++++----- .../components/ng_paramodulation/Makefile | 3 +- .../components/ng_paramodulation/foUnif.ml | 2 +- .../components/ng_paramodulation/foUnif.mli | 2 +- .../components/ng_paramodulation/foUtils.ml | 63 +------------------ .../components/ng_paramodulation/foUtils.mli | 35 +---------- .../components/ng_paramodulation/index.ml | 3 +- .../components/ng_paramodulation/orderings.ml | 63 ++++++------------- .../components/ng_paramodulation/paramod.ml | 13 ++-- .../ng_paramodulation/superposition.ml | 5 +- 10 files changed, 54 insertions(+), 164 deletions(-) diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 6dc4150c1..489a80a1a 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,9 +1,10 @@ pp.cmi: terms.cmi foSubst.cmi: terms.cmi +foUtils.cmi: terms.cmi +foUnif.cmi: terms.cmi orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi orderings.cmi +clauses.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: terms.cmi orderings.cmi paramod.cmi: terms.cmi orderings.cmi @@ -16,22 +17,22 @@ pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi -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 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 +foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +orderings.cmo: terms.cmi pp.cmi foUnif.cmi foSubst.cmi orderings.cmi +orderings.cmx: terms.cmx pp.cmx foUnif.cmx foSubst.cmx orderings.cmi +clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi clauses.cmi +clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx clauses.cmi +index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi +index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo: terms.cmi stats.cmi -stats.cmx: terms.cmx stats.cmi +stats.cmo: terms.cmi pp.cmi stats.cmi +stats.cmx: terms.cmx pp.cmx stats.cmi paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ foUtils.cmi foUnif.cmi paramod.cmi paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index 6196ab1f9..0d2eef103 100644 --- a/helm/software/components/ng_paramodulation/Makefile +++ b/helm/software/components/ng_paramodulation/Makefile @@ -2,7 +2,8 @@ PACKAGE = ng_paramodulation INTERFACE_FILES = \ terms.mli pp.mli foSubst.mli \ - orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \ + foUtils.mli foUnif.mli orderings.mli \ + clauses.mli index.mli superposition.mli \ stats.mli paramod.mli nCicBlob.mli cicBlob.mli nCicProof.mli \ nCicParamod.mli diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml index 61bbdcd8b..916e33ca8 100644 --- a/helm/software/components/ng_paramodulation/foUnif.ml +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -25,7 +25,7 @@ let mem2 a b l = aux false false l ;; -module Founif (B : Orderings.Blob) = struct +module FoUnif (B : Terms.Blob) = struct module Subst = FoSubst module U = FoUtils.Utils(B) diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli index 2371f2180..87792ec8c 100644 --- a/helm/software/components/ng_paramodulation/foUnif.mli +++ b/helm/software/components/ng_paramodulation/foUnif.mli @@ -13,7 +13,7 @@ exception UnificationFailure of string Lazy.t;; -module Founif (B : Orderings.Blob) : +module FoUnif (B : Terms.Blob) : sig val unification: diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 7b192579d..5dd1268b0 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -21,9 +21,8 @@ let rec lexicograph f l1 l2 = | _,[] -> 1 ;; -module Utils (B : Orderings.Blob) = struct +module Utils (B : Terms.Blob) = struct module Subst = FoSubst;; - module Order = B;; let rec eq_foterm x y = x == y || @@ -69,9 +68,6 @@ module Utils (B : Orderings.Blob) = struct | Terms.Equation _, Terms.Predicate _ -> 1 ;; - let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2 - let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2 - let relocate maxvar varlist subst = List.fold_right (fun i (maxvar, varlist, s) -> @@ -79,61 +75,4 @@ module Utils (B : Orderings.Blob) = struct varlist (maxvar+1, [], subst) ;; - let fresh_clause maxvar (id, nlit, plit, varlist, proof) = - let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in - let apply_subst_on_lit = function - | Terms.Equation (l,r,ty,o) -> - let l = Subst.apply_subst subst l in - let r = Subst.apply_subst subst r in - let ty = Subst.apply_subst subst ty in - Terms.Equation (l,r,ty,o) - | Terms.Predicate p -> - let p = Subst.apply_subst subst p in - Terms.Predicate p - in - let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in - let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in - let proof = - match proof with - | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t) - | Terms.Step (rule,c1,c2,dir,pos,s) -> - Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s) - in - (id, nlit, plit, varlist, proof), maxvar - ;; - - (* may be moved inside the bag *) - let mk_clause maxvar nlit plit proofterm = - let foterm_to_lit (acc,literals) ty = - let vars = Terms.vars_of_term ~start_acc:acc ty in - match ty with - | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> - let o = Order.compare_terms l r in - (vars,(Terms.Equation (l, r, ty, o),true)::literals) - | _ -> (vars,(Terms.Predicate ty,true)::literals) - in - let varlist = Terms.vars_of_term proofterm in - let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in - let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in - let proof = Terms.Exact proofterm in - fresh_clause maxvar (0, nlit, plit, varlist, proof) - ;; - - let mk_passive_clause cl = - (Order.compute_clause_weight cl, cl) - ;; - - let mk_passive_goal g = - (Order.compute_clause_weight g, g) - ;; - - let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) = - if w1 = w2 then id1 - id2 - else w1 - w2 - ;; - - let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) = - id1 - id2 - ;; - end diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 48ef1d90b..fcb94c22e 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -13,7 +13,7 @@ val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int -module Utils (B : Orderings.Blob) : +module Utils (B : Terms.Blob) : sig val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int @@ -21,36 +21,7 @@ module Utils (B : Orderings.Blob) : val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int - (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *) - val mk_clause : - int -> - B.t Terms.foterm list -> (* negative literals in clause *) - B.t Terms.foterm list -> (* positive literals in clause *) - B.t Terms.foterm -> - B.t Terms.clause * int - - val mk_passive_clause : - B.t Terms.clause -> B.t Terms.passive_clause - - val mk_passive_goal : - B.t Terms.clause -> B.t Terms.passive_clause - - val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool - val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int - - - val fresh_clause : - int -> B.t Terms.clause -> B.t Terms.clause * int - - (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *) - val relocate : - int -> int list -> B.t Terms.substitution -> - int * int list * B.t Terms.substitution - - val compare_passive_clauses_weight : - B.t Terms.passive_clause -> B.t Terms.passive_clause -> int - - val compare_passive_clauses_age : - B.t Terms.passive_clause -> B.t Terms.passive_clause -> int + val relocate : int -> int list -> B.t Terms.substitution + -> int * int list * B.t Terms.substitution end diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index beb3aed86..e44d79131 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -13,6 +13,7 @@ module Index(B : Orderings.Blob) = struct module U = FoUtils.Utils(B) + module Clauses = Clauses.Clauses(B) module ClauseOT = struct @@ -23,7 +24,7 @@ module Index(B : Orderings.Blob) = struct let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in - if c <> 0 then c else U.compare_clause uc1 uc2 + if c <> 0 then c else Clauses.compare_clause uc1 uc2 ;; end diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 47f6b4512..89b390b07 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -186,58 +186,25 @@ let compare_terms o x y = | _ -> assert false ;; +let are_invertible relocate alpha_eq l r = + let varlist = Terms.vars_of_term l in + let maxvar = List.fold_left max 0 varlist in + let _,_,subst = relocate maxvar varlist FoSubst.id_subst in + let l = FoSubst.apply_subst subst l in + try (ignore(alpha_eq l r);true) with + FoUnif.UnificationFailure _ -> false;; + module NRKBO (B : Terms.Blob) = struct let name = "nrkbo" include B module Pp = Pp.Pp(B) + module Unif = FoUnif.FoUnif(B) + module Utils = FoUtils.Utils(B) let eq_foterm = eq_foterm B.eq;; -exception UnificationFailure of string Lazy.t;; - - -(* DUPLICATE CODE FOR TESTS (see FoUnif) *) - let alpha_eq s t = - let rec equiv subst s t = - let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s - and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t - - in - match s, t with - | s, t when eq_foterm s t -> subst - | Terms.Var i, Terms.Var j - when (not (List.exists (fun (_,k) -> k=t) subst)) -> - let subst = FoSubst.build_subst i t subst in - subst - | Terms.Node l1, Terms.Node l2 -> ( - try - List.fold_left2 - (fun subst' s t -> equiv subst' s t) - subst l1 l2 - with Invalid_argument _ -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - ) - | _, _ -> - raise (UnificationFailure (lazy "Inference.unification.unif")) - in - equiv FoSubst.id_subst s t -;; - -let relocate maxvar varlist subst = - List.fold_right - (fun i (maxvar, varlist, s) -> - maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s) - varlist (maxvar+1, [], subst) - ;; - - let are_invertible l r = - let varlist = Terms.vars_of_term l in - let maxvar = List.fold_left max 0 varlist in - let _,_,subst = relocate maxvar varlist FoSubst.id_subst in - let l = FoSubst.apply_subst subst l in - try (ignore(alpha_eq l r);true) with - UnificationFailure _ -> false + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; let compute_clause_weight = compute_clause_weight;; @@ -270,9 +237,13 @@ module KBO (B : Terms.Blob) = struct include B module Pp = Pp.Pp(B) + module Unif = FoUnif.FoUnif(B) + module Utils = FoUtils.Utils(B) let eq_foterm = eq_foterm B.eq;; + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; + let compute_clause_weight = compute_clause_weight;; let compute_goal_weight = compute_goal_weight;; @@ -336,9 +307,13 @@ module LPO (B : Terms.Blob) = struct include B module Pp = Pp.Pp(B) + module Unif = FoUnif.FoUnif(B) + module Utils = FoUtils.Utils(B) let eq_foterm = eq_foterm B.eq;; + let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;; + let compute_clause_weight = compute_clause_weight;; let compute_goal_weight = compute_goal_weight;; diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 8024dbba0..1f64314c9 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -43,21 +43,22 @@ module Paramod (B : Orderings.Blob) = struct exception Stop of szsontology type bag = B.t Terms.bag * int module Pp = Pp.Pp (B) - module FU = FoUnif.Founif(B) + module FU = FoUnif.FoUnif(B) module IDX = Index.Index(B) module Sup = Superposition.Superposition(B) module Utils = FoUtils.Utils(B) module Order = B + module Clauses = Clauses.Clauses(B) module WeightOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses_weight + let compare = Clauses.compare_passive_clauses_weight end module AgeOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses_age + let compare = Clauses.compare_passive_clauses_age end module WeightPassiveSet = Set.Make(WeightOrderedPassives) @@ -65,13 +66,13 @@ module Paramod (B : Orderings.Blob) = struct let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl = let cl = if no_weight then (0,cl) - else Utils.mk_passive_clause cl in + else Clauses.mk_passive_clause cl in 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 + else Clauses.mk_passive_goal g in WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; @@ -337,7 +338,7 @@ module Paramod (B : Orderings.Blob) = struct let bag = Terms.empty_bag in let maxvar = 0 in let build_clause (bag,maxvar,l) (t,(nlit,plit)) = - let c,maxvar = Utils.mk_clause maxvar nlit plit t in + let c,maxvar = Clauses.mk_clause maxvar nlit plit t in let bag,c = Terms.add_to_bag c bag in (bag,maxvar,c::l) in diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 306104658..47119d477 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -14,11 +14,12 @@ module Superposition (B : Orderings.Blob) = struct module IDX = Index.Index(B) - module Unif = FoUnif.Founif(B) + module Unif = FoUnif.FoUnif(B) module Subst = FoSubst module Order = B module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) + module Clauses = Clauses.Clauses(B) exception Success of B.t Terms.bag * int * B.t Terms.clause @@ -688,7 +689,7 @@ module Superposition (B : Orderings.Blob) = current :: alist, IDX.index_clause atable current in debug (lazy "Indexed"); - let fresh_current, maxvar = Utils.fresh_clause maxvar current in + let fresh_current, maxvar = Clauses.fresh_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 = Terms.add_to_bag fresh_current bag in -- 2.39.2