From 38c54dd8e2234836d5f3e8011c478daf7d59fa25 Mon Sep 17 00:00:00 2001 From: denes Date: Tue, 28 Jul 2009 17:50:37 +0000 Subject: [PATCH 1/1] Various architectural changes --- .../components/ng_paramodulation/nCicBlob.ml | 32 +------------- .../components/ng_paramodulation/nCicBlob.mli | 2 +- .../ng_paramodulation/nCicParamod.ml | 42 +++++++++++++++--- .../components/ng_paramodulation/nCicProof.ml | 3 +- .../ng_paramodulation/orderings.mli | 8 ++-- .../components/ng_paramodulation/paramod.ml | 43 ++++++++++--------- .../components/ng_paramodulation/paramod.mli | 12 ++---- .../components/ng_paramodulation/stats.ml | 14 +++--- .../ng_paramodulation/superposition.ml | 4 +- .../components/ng_paramodulation/terms.ml | 4 +- .../components/ng_paramodulation/terms.mli | 5 --- 11 files changed, 81 insertions(+), 88 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 2ed7eef23..3383e01f2 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -19,7 +19,7 @@ module type NCicContext = end module NCicBlob(C : NCicContext) : Terms.Blob -with type t = NCic.term and type input = NCic.term = struct +with type t = NCic.term = struct type t = NCic.term @@ -48,36 +48,6 @@ with type t = NCic.term and type input = NCic.term = struct let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; - type input = NCic.term - - let rec embed = function - | NCic.Meta (i,_) -> Terms.Var i, [i] - | NCic.Appl l -> - let rec aux acc l = function - |[] -> acc@l - |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl - in - let res,vars = List.fold_left - (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l - in (Terms.Node (List.rev res)), vars - | t -> Terms.Leaf t, [] - ;; - - let embed t = fst (embed t) ;; - - let saturate t ty = - let sty, _, args = - NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context - ty 0 - in - let proof = - if args = [] then Terms.Leaf t - else Terms.Node (Terms.Leaf t :: List.map embed args) - in - let sty = embed sty in - proof, sty - ;; - let eqP = let r = OCic2NCic.reference_of_oxuri diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli index 16a8c33a2..87e12c950 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.mli +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -19,5 +19,5 @@ module type NCicContext = end module NCicBlob(C : NCicContext) : Terms.Blob -with type t = NCic.term and type input = NCic.term +with type t = NCic.term diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 8c740a0e4..ff34709e9 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -let nparamod rdb metasenv subst context t table = +let nparamod rdb metasenv subst context (g_t,g_ty) table = let module C = struct let metasenv = metasenv @@ -20,21 +20,49 @@ let nparamod rdb metasenv subst context t table = end in let module B : Orderings.Blob - with type t = NCic.term and type input = NCic.term + with type t = NCic.term = Orderings.NRKBO(NCicBlob.NCicBlob(C)) in let module P = Paramod.Paramod(B) in let module Pp = Pp.Pp(B) in - let bag, maxvar = Terms.empty_bag, 0 in - let (bag,maxvar), passives = + + let rec embed = function + | NCic.Meta (i,_) -> Terms.Var i, [i] + | NCic.Appl l -> + let rec aux acc l = function + |[] -> acc@l + |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl + in + let res,vars = List.fold_left + (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l + in (Terms.Node (List.rev res)), vars + | t -> Terms.Leaf t, [] + in + + let embed t = fst (embed t) in + + let saturate ~is_goal t ty = + let sty, _, args = + NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context ty 0 + in + let proof = + if args = [] then Terms.Leaf t + else Terms.Node (Terms.Leaf t :: List.map embed args) + in + let sty = embed sty in + proof, if is_goal then [sty],[] else [],[sty] + in + let goal = saturate ~is_goal:true g_t g_ty in + let hypotheses = List.map (fun (t,ty) -> saturate ~is_goal:false t ty) table in + (*let (bag,maxvar), passives = HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table in let (bag,maxvar), goals = HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t] - in + in*) match - P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) - ~g_passives:goals ~passives (bag,maxvar) + P.paramod ~useage:true ~max_steps:max_int ~print_problem:true + goal hypotheses with | P.Error _ | P.GaveUp | P.Timeout _ -> [] | P.Unsatisfiable solutions -> diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index b1373819c..aadaafb5a 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -122,7 +122,8 @@ let get_literal id = let (_, nlit, plit, vl, proof),_,_ = Terms.get_from_bag id bag in let lit = match nlit,plit with - | [],[Terms.Equation (l,r,ty,_),_] -> + | [Terms.Equation (l,r,ty,_),_],[] + | [],[Terms.Equation (l,r,ty,_),_] -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] | _ -> assert false in diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index 7c66cc40b..84a3cf9f5 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -32,10 +32,10 @@ module type Blob = end module NRKBO (B : Terms.Blob) : Blob -with type t = B.t and type input = B.input +with type t = B.t module KBO (B : Terms.Blob) : Blob -with type t = B.t and type input = B.input +with type t = B.t -module LPO (B : Terms.Blob) : Blob -with type t = B.t and type input = B.input +module LPO (B : Terms.Blob) : Blob +with type t = B.t diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 48811239b..8024dbba0 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -19,27 +19,22 @@ let monster = 100;; module type Paramod = sig type t - type input type szsontology = | Unsatisfiable of (t Terms.bag * int * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag - type bag = t Terms.bag * int - val mk_passive : bag -> input * input -> bag * t Terms.clause - val mk_goal : bag -> input * input -> bag * t Terms.clause val paramod : useage:bool -> max_steps:int -> + print_problem:bool -> ?timeout:float -> - bag -> - g_passives:t Terms.clause list -> - passives:t Terms.clause list -> szsontology + t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) -> + (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology end module Paramod (B : Orderings.Blob) = struct type t = B.t - type input = B.input type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list | GaveUp @@ -125,16 +120,6 @@ module Paramod (B : Orderings.Blob) = struct else WeightPassiveSet.min_elt passives_w ;; - let mk_clause bag maxvar (t,ty) = - let (proof,ty) = B.saturate t ty in - let c, maxvar = Utils.mk_clause maxvar [] [ty] proof in - let bag, c = Terms.add_to_bag c bag in - (bag, maxvar), c - ;; - - let mk_passive (bag,maxvar) = mk_clause bag maxvar;; - let mk_goal (bag,maxvar) = mk_clause bag maxvar;; - (* TODO : global age over facts and goals (without comparing weights) *) let select ~use_age passives g_passives = if is_passive_set_empty passives then begin @@ -347,16 +332,32 @@ module Paramod (B : Orderings.Blob) = struct actives passives g_actives g_passives ;; - let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses = let initial_timestamp = Unix.gettimeofday () in + 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 bag,c = Terms.add_to_bag c bag in + (bag,maxvar,c::l) + in + let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in + let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in + let goal = match goals with | [g] -> g | _ -> assert false in let passives = - add_passive_clauses ~no_weight:true passive_empty_set passives + add_passive_clauses ~no_weight:true passive_empty_set hypotheses in let g_passives = - add_passive_goals ~no_weight:true passive_empty_set g_passives + add_passive_goal ~no_weight:true passive_empty_set goal in let g_actives = [] in let actives = [], IDX.DT.empty in + if print_problem then begin + prerr_endline "Facts:"; + List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses; + prerr_endline "Goal:"; + prerr_endline (" " ^ Pp.pp_clause goal); + end; try given_clause ~useage ~noinfer:false bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 8376b256b..0aa990d52 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -14,23 +14,19 @@ module type Paramod = sig type t - type input type szsontology = | Unsatisfiable of (t Terms.bag * int * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag - type bag = t Terms.bag * int - val mk_passive : bag -> input * input -> bag * t Terms.clause - val mk_goal : bag -> input * input -> bag * t Terms.clause val paramod : useage:bool -> max_steps:int -> + print_problem:bool -> ?timeout:float -> - bag -> - g_passives:t Terms.clause list -> - passives:t Terms.clause list -> szsontology + t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) -> + (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology end module Paramod ( B : Orderings.Blob ) : Paramod -with type t = B.t and type input = B.input +with type t = B.t diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml index 04aaa75f5..b6fe753d3 100644 --- a/helm/software/components/ng_paramodulation/stats.ml +++ b/helm/software/components/ng_paramodulation/stats.ml @@ -15,6 +15,7 @@ module Stats (B : Terms.Blob) = struct module SymbMap = Map.Make(B) + module Pp = Pp.Pp(B) let rec occ_nbr t acc = function | Terms.Leaf u when B.eq t u -> 1+acc @@ -49,10 +50,13 @@ module Stats (B : Terms.Blob) = match l with | [] -> acc | (_,nlit,plit,_,_)::tl -> - match nlit,plit with - | [],[Terms.Equation (l,r,_,_),_] -> - parse_symbols (aux (aux acc l) r) tl - | _ -> assert false; + let acc = List.fold_left (fun acc t -> + match t with + | Terms.Equation (l,r,_,_),_ -> + (aux (aux acc l) r) + | _ -> assert false) acc (nlit@plit) + in + parse_symbols acc tl ;; let goal_pos t goal = @@ -127,7 +131,7 @@ module Stats (B : Terms.Blob) = else dependencies op tl acc | _ -> dependencies op tl acc) - | _ -> assert false + | _ -> [] (* TODO : compute dependencies for clauses *) ;; let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 67df0654e..306104658 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -194,6 +194,7 @@ module Superposition (B : Orderings.Blob) = let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table = match nlit,plit with + |[literal,_], [] |[],[literal,_] -> (match literal with | Terms.Predicate t -> assert false @@ -259,8 +260,7 @@ module Superposition (B : Orderings.Blob) = | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify -> (try ignore(Unif.unification (* vl *) [] l r); true with FoUnif.UnificationFailure _ -> false) - | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false - | _ -> assert false + | _ -> false ;; let build_new_clause bag maxvar filter rule t subst id id2 pos dir = diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 0e69cace9..d963d55ca 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -101,8 +101,6 @@ module type Blob = val compare : t -> t -> int val eqP : t val pp : t -> string - type input - val embed : input -> t foterm - val saturate : input -> input -> t foterm * t foterm + end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 90ccaf591..c15c85af2 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -97,10 +97,5 @@ module type Blob = * *) val pp : t -> string - type input - val embed : input -> t foterm - (* saturate [proof] [type] -> [proof] * [type] *) - val saturate : input -> input -> t foterm * t foterm - end -- 2.39.2