From: Enrico Tassi Date: Thu, 9 Jul 2009 13:41:20 +0000 (+0000) Subject: New functorialization: paramod is abstracted over a Orderings.Blob, that is like... X-Git-Tag: make_still_working~3713 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2bcf927f58bac034b8758173cdbd16cb7475de36 New functorialization: paramod is abstracted over a Orderings.Blob, that is like Terms.Blob but adds the compare_terms function. This allows an easy instantiation of the main loop with differend orderings --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index c029cfa22..1c837f18d 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -78,7 +78,7 @@ module MakeBlob(C:LeafComparer) : Terms.Blob end ;; -let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) = +let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord = print_endline ("% SZS status Unsatisfiable for " ^ Filename.basename !problem_file); print_endline ("% SZS output start CNFRefutation for " ^ @@ -89,10 +89,15 @@ let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) = print_endline (pp ~margin:max_int cl)) l; print_endline ("% SZS output end CNFRefutation for " ^ - Filename.basename !problem_file) + Filename.basename !problem_file); + let prefix = string_of_int (Unix.getpid ()) in + let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in + let times = Unix.times () in + prerr_endline ("solved " ^ !problem_file ^ " in " ^ string_of_float + (times.Unix.tms_utime +. times.Unix.tms_stime) ^ " using " ^ ord); ;; -let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) = +let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname = let prefix = string_of_int (Unix.getpid ()) in let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in prerr_endline "Facts:"; @@ -100,16 +105,14 @@ let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) = prerr_endline "Goal:"; prerr_endline (" " ^ pp g_passives); prerr_endline "Order:"; - prerr_endline " ...fixme..."; - prerr_endline "Strategy:"; - prerr_endline " ...fixme..."; + prerr_endline (" " ^ oname); ;; let report_error s = prerr_endline (string_of_int (Unix.getpid())^": "^s);; -module Main(C:LeafComparer) = struct +module Main(C:Orderings.Blob with type t = leaf) = struct let main goal hypotheses = - let module B = MakeBlob(C) in + let module B = C in let module Pp = Pp.Pp(B) in let module P = Paramod.Paramod(B) in let bag = Terms.empty_bag, 0 in @@ -117,14 +120,14 @@ module Main(C:LeafComparer) = struct let bag, passives = HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses in - start_msg passives g_passives Pp.pp_unit_clause; + start_msg passives g_passives Pp.pp_unit_clause C.name; match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with | P.Error s -> report_error s; 3 | P.Unsatisfiable ((bag,_,l)::_) -> - success_msg bag l Pp.pp_unit_clause; 0 + success_msg bag l Pp.pp_unit_clause C.name; 0 | P.Unsatisfiable ([]) -> report_error "Unsatisfiable but no solution output"; 3 | P.GaveUp -> 2 @@ -175,7 +178,8 @@ let main () = Matitaprover is the first order automatic prover that equips the Matita interactive theorem prover (http://matita.cs.unibo.it). -Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1 +Developed by A.Asperti, M.Denes and E.Tassi, released under GPL version 2 +or at your option any later version. If --tptppath is given, instead of the problem file you can just give the problem name with the .p suffix (e.g. BOO001-1.p) @@ -194,14 +198,16 @@ usage: matitaprover [options] problemfile"; if pid = 0 then (exit (f ())) else pid) [ (fun () -> - let module M = Main(struct let cmp (a,_) (b,_) = compare a b end) in + let module M = Main(Orderings.NRKBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in + M.main goal hypotheses) + ; + (fun () -> + let module M = Main(Orderings.KBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in M.main goal hypotheses) ; -(* (fun () -> - let module M = Main(struct let cmp (a,_) (b,_) = compare b a end) in + let module M = Main(Orderings.LPO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in M.main goal hypotheses) -*) ]; let rec aux () = if List.length !childs = 0 then diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 3d43409fe..dc8ab7011 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,11 +1,11 @@ pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi -index.cmi: terms.cmi -foUnif.cmi: terms.cmi -superposition.cmi: terms.cmi index.cmi -paramod.cmi: terms.cmi +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 +paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi @@ -19,10 +19,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 foUtils.cmi index.cmi -index.cmx: terms.cmx foUtils.cmx index.cmi -foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi +index.cmx: terms.cmx orderings.cmx foUtils.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 \ foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ @@ -37,7 +37,7 @@ cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.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 pp.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \ - nCicParamod.cmi +nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ + nCicBlob.cmi nCicParamod.cmi +nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ + nCicBlob.cmx nCicParamod.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 3d43409fe..dc8ab7011 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,11 +1,11 @@ pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi -index.cmi: terms.cmi -foUnif.cmi: terms.cmi -superposition.cmi: terms.cmi index.cmi -paramod.cmi: terms.cmi +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 +paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi @@ -19,10 +19,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 foUtils.cmi index.cmi -index.cmx: terms.cmx foUtils.cmx index.cmi -foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi +index.cmx: terms.cmx orderings.cmx foUtils.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 \ foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ @@ -37,7 +37,7 @@ cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.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 pp.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \ - nCicParamod.cmi +nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ + nCicBlob.cmi nCicParamod.cmi +nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ + nCicBlob.cmx nCicParamod.cmi diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml index 05fdbe37c..427db4f95 100644 --- a/helm/software/components/ng_paramodulation/foUnif.ml +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -25,8 +25,8 @@ let mem2 a b l = aux false false l ;; -module Founif (B : Terms.Blob) = struct - module Subst = FoSubst (*.Subst(B)*) +module Founif (B : Orderings.Blob) = struct + module Subst = FoSubst module U = FoUtils.Utils(B) let unification vars locked_vars t1 t2 = diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli index 4b5e23a48..87b57ae70 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 : Terms.Blob) : +module Founif (B : Orderings.Blob) : sig val unification: diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 10c96f543..7b57e5bb3 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -21,9 +21,9 @@ let rec lexicograph f l1 l2 = | _,[] -> 1 ;; -module Utils (B : Terms.Blob) = struct - module Subst = FoSubst;; (*.Subst(B) ;;*) - module Order = Orderings.Orderings(B) ;; +module Utils (B : Orderings.Blob) = struct + module Subst = FoSubst;; + module Order = B;; let rec eq_foterm x y = x == y || diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 8a3b1739b..d725d3c7f 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 : Terms.Blob) : +module Utils (B : Orderings.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 diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 3c203d3a7..889e1e7ef 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -11,7 +11,7 @@ (* $Id$ *) -module Index(B : Terms.Blob) = struct +module Index(B : Orderings.Blob) = struct module U = FoUtils.Utils(B) module ClauseOT = diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli index 5d496d936..7d75f2837 100644 --- a/helm/software/components/ng_paramodulation/index.mli +++ b/helm/software/components/ng_paramodulation/index.mli @@ -11,7 +11,7 @@ (* $Id$ *) -module Index (B : Terms.Blob) : +module Index (B : Orderings.Blob) : sig module ClauseSet : Set.S with type elt = Terms.direction * B.t Terms.unit_clause diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 79ea569a2..be7e140f3 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -19,9 +19,9 @@ let nparamod rdb metasenv subst context t table = let context = context end in - let module B : Terms.Blob + let module B : Orderings.Blob with type t = NCic.term and type input = NCic.term - = NCicBlob.NCicBlob(C) + = Orderings.NRKBO(NCicBlob.NCicBlob(C)) in let module P = Paramod.Paramod(B) in let module Pp = Pp.Pp(B) in diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 27b3ac647..ba6969aeb 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -13,30 +13,46 @@ type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE -module Orderings (B : Terms.Blob) = struct +module type Blob = + sig + include Terms.Blob - module Pp = Pp.Pp(B) + (* This order relation should be: + * - stable for instantiation + * - total on ground terms + * + *) + val compare_terms : + t Terms.foterm -> t Terms.foterm -> Terms.comparison + + val compute_unit_clause_weight : 't Terms.unit_clause -> int - type weight = int * (int * int) list;; + val compute_goal_weight : 't Terms.unit_clause -> int -let rec eq_foterm x y = + val name : string + + end + +type weight = int * (int * int) list;; + +let rec eq_foterm f x y = x == y || match x, y with - | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2 + | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2 | Terms.Var i, Terms.Var j -> i = j - | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2 + | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2 | _ -> false - ;; +;; - let string_of_weight (cw, mw) = - let s = - String.concat ", " - (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) - in - Printf.sprintf "[%d; %s]" cw s - ;; +let string_of_weight (cw, mw) = + let s = + String.concat ", " + (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) + in + Printf.sprintf "[%d; %s]" cw s +;; - let weight_of_term term = +let weight_of_term term = let vars_dict = Hashtbl.create 5 in let rec aux = function | Terms.Var i -> @@ -58,9 +74,9 @@ let rec eq_foterm x y = | (m1, _), (m2, _) -> m1 - m2 in (w, List.sort compare l) (* from the smallest meta to the bigest *) - ;; +;; - let compute_unit_clause_weight (_,l, _, _) = +let compute_unit_clause_weight (_,l, _, _) = let weight_of_polynomial w m = let factor = 2 in w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m @@ -78,7 +94,7 @@ let rec eq_foterm x y = let wl, ml = weight_of_term l in 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 = @@ -97,81 +113,101 @@ let compute_goal_weight (_,l, _, _) = - (abs (wl-wr)) ;; - (* Riazanov: 3.1.5 pag 38 *) +(* Riazanov: 3.1.5 pag 38 *) (* Compare weights normalized in a new way : * Variables should be sorted from the lowest index to the highest * Variables which do not occur in the term should not be present * in the normalized polynomial *) - let compare_weights (h1, w1) (h2, w2) = - let rec aux hdiff (lt, gt) diffs w1 w2 = - match w1, w2 with - | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) -> - if var1 = var2 then - let diffs = (w1 - w2) + diffs in - let r = compare w1 w2 in - let lt = lt or (r < 0) in - let gt = gt or (r > 0) in - if lt && gt then XINCOMPARABLE else - aux hdiff (lt, gt) diffs tl1 tl2 - else if var1 < var2 then - if lt then XINCOMPARABLE else - aux hdiff (false,true) (diffs+w1) tl1 l2 - else - if gt then XINCOMPARABLE else - aux hdiff (true,false) (diffs-w2) l1 tl2 - | [], (_,w2)::tl2 -> - if gt then XINCOMPARABLE else - aux hdiff (true,false) (diffs-w2) [] tl2 - | (_,w1)::tl1, [] -> +let compare_weights (h1, w1) (h2, w2) = + let rec aux hdiff (lt, gt) diffs w1 w2 = + match w1, w2 with + | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) -> + if var1 = var2 then + let diffs = (w1 - w2) + diffs in + let r = Pervasives.compare w1 w2 in + let lt = lt or (r < 0) in + let gt = gt or (r > 0) in + if lt && gt then XINCOMPARABLE else + aux hdiff (lt, gt) diffs tl1 tl2 + else if var1 < var2 then if lt then XINCOMPARABLE else - aux hdiff (false,true) (diffs+w1) tl1 [] - | [], [] -> - if lt then - if hdiff <= 0 then XLT - else if (- diffs) >= hdiff then XLE else XINCOMPARABLE - else if gt then - if hdiff >= 0 then XGT - else if diffs >= (- hdiff) then XGE else XINCOMPARABLE - else - if hdiff < 0 then XLT - else if hdiff > 0 then XGT - else XEQ - in - aux (h1-h2) (false,false) 0 w1 w2 - ;; + aux hdiff (false,true) (diffs+w1) tl1 l2 + else + if gt then XINCOMPARABLE else + aux hdiff (true,false) (diffs-w2) l1 tl2 + | [], (_,w2)::tl2 -> + if gt then XINCOMPARABLE else + aux hdiff (true,false) (diffs-w2) [] tl2 + | (_,w1)::tl1, [] -> + if lt then XINCOMPARABLE else + aux hdiff (false,true) (diffs+w1) tl1 [] + | [], [] -> + if lt then + if hdiff <= 0 then XLT + else if (- diffs) >= hdiff then XLE else XINCOMPARABLE + else if gt then + if hdiff >= 0 then XGT + else if diffs >= (- hdiff) then XGE else XINCOMPARABLE + else + if hdiff < 0 then XLT + else if hdiff > 0 then XGT + else XEQ + in + aux (h1-h2) (false,false) 0 w1 w2 +;; + +(* Riazanov: p. 40, relation >>> + * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *) +let rec aux_ordering b_compare ?(head_only=false) t1 t2 = + match t1, t2 with + (* We want to discard any identity equality. * + * If we give back XEQ, no inference rule * + * will be applied on this equality *) + | Terms.Var i, Terms.Var j when i = j -> + XEQ + (* 1. *) + | Terms.Var _, _ + | _, Terms.Var _ -> XINCOMPARABLE + (* 2.a *) + | Terms.Leaf a1, Terms.Leaf a2 -> + let cmp = b_compare a1 a2 in + if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT + | Terms.Leaf _, Terms.Node _ -> XLT + | Terms.Node _, Terms.Leaf _ -> XGT + (* 2.b *) + | Terms.Node l1, Terms.Node l2 -> + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> XEQ + | _, [] -> (* XGT *) assert false (* hd symbols were eq *) + | [], _ -> (* XLT *) assert false (* hd symbols were eq *) + | hd1::tl1, hd2::tl2 -> + let o = aux_ordering b_compare ~head_only hd1 hd2 in + if o = XEQ && not head_only then cmp tl1 tl2 else o + in + cmp l1 l2 +;; - (* Riazanov: p. 40, relation >>> - * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *) - let rec aux_ordering ?(head_only=false) t1 t2 = - match t1, t2 with - (* We want to discard any identity equality. * - * If we give back XEQ, no inference rule * - * will be applied on this equality *) - | Terms.Var i, Terms.Var j when i = j -> - XEQ - (* 1. *) - | Terms.Var _, _ - | _, Terms.Var _ -> XINCOMPARABLE - (* 2.a *) - | Terms.Leaf a1, Terms.Leaf a2 -> - let cmp = B.compare a1 a2 in - if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT - | Terms.Leaf _, Terms.Node _ -> XLT - | Terms.Node _, Terms.Leaf _ -> XGT - (* 2.b *) - | Terms.Node l1, Terms.Node l2 -> - let rec cmp t1 t2 = - match t1, t2 with - | [], [] -> XEQ - | _, [] -> (* XGT *) assert false (* hd symbols were eq *) - | [], _ -> (* XLT *) assert false (* hd symbols were eq *) - | hd1::tl1, hd2::tl2 -> - let o = aux_ordering ~head_only hd1 hd2 in - if o = XEQ && not head_only then cmp tl1 tl2 else o - in - cmp l1 l2 - ;; +let compare_terms o x y = + match o x y with + | XINCOMPARABLE -> Terms.Incomparable + | XGT -> Terms.Gt + | XLT -> Terms.Lt + | XEQ -> Terms.Eq + | _ -> assert false +;; + +module NRKBO (B : Terms.Blob) = struct + let name = "nrkbo" + include B + + module Pp = Pp.Pp(B) + + let eq_foterm = eq_foterm B.eq;; + + let compute_unit_clause_weight = compute_unit_clause_weight;; + let compute_goal_weight = compute_goal_weight;; (* Riazanov: p. 40, relation >_n *) let nonrec_kbo t1 t2 = @@ -179,16 +215,36 @@ let compute_goal_weight (_,l, _, _) = let w2 = weight_of_term t2 in match compare_weights w1 w2 with | XLE -> (* this is .> *) - if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE + if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE | XGE -> - if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE - | XEQ -> aux_ordering t1 t2 + if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE + | XEQ -> aux_ordering B.compare t1 t2 | res -> res ;; + + let compare_terms = compare_terms nonrec_kbo;; + + let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";; + let compare_terms x y = + profiler.HExtlib.profile (compare_terms x) y + ;; + +end +module KBO (B : Terms.Blob) = struct + let name = "kbo" + include B + + module Pp = Pp.Pp(B) + + let eq_foterm = eq_foterm B.eq;; + + let compute_unit_clause_weight = compute_unit_clause_weight;; + let compute_goal_weight = compute_goal_weight;; + (* Riazanov: p. 38, relation > *) let rec kbo t1 t2 = - let aux = aux_ordering ~head_only:true in + let aux = aux_ordering B.compare ~head_only:true in let rec cmp t1 t2 = match t1, t2 with | [], [] -> XEQ @@ -231,6 +287,26 @@ let compute_goal_weight (_,l, _, _) = | res -> res ;; + let compare_terms = compare_terms kbo;; + + let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";; + let compare_terms x y = + profiler.HExtlib.profile (compare_terms x) y + ;; + +end + +module LPO (B : Terms.Blob) = struct + let name = "lpo" + include B + + module Pp = Pp.Pp(B) + + let eq_foterm = eq_foterm B.eq;; + + let compute_unit_clause_weight = compute_unit_clause_weight;; + let compute_goal_weight = compute_goal_weight;; + let rec lpo s t = match s,t with | s, t when eq_foterm s t -> @@ -266,7 +342,7 @@ let compute_goal_weight (_,l, _, _) = if lpo x t = XLT then check_subterms t ([],tl) else false in - match aux_ordering hd1 hd2 with + match aux_ordering B.compare hd1 hd2 with | XGT -> if check_subterms s (r_ol,tl2) then XGT else XINCOMPARABLE | XLT -> if check_subterms t (l_ol,tl1) then XLT @@ -287,22 +363,16 @@ let compute_goal_weight (_,l, _, _) = | XINCOMPARABLE -> XINCOMPARABLE | _ -> assert false end - | _,_ -> aux_ordering s t + | _,_ -> aux_ordering B.compare s t ;; - let compare_terms x y = - match nonrec_kbo x y with - | XINCOMPARABLE -> Terms.Incomparable - | XGT -> Terms.Gt - | XLT -> Terms.Lt - | XEQ -> Terms.Eq - | _ -> assert false - ;; + let compare_terms = compare_terms lpo;; - let profiler = HExtlib.profile ~enable:true "compare_terms";; + let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";; let compare_terms x y = profiler.HExtlib.profile (compare_terms x) y ;; end + diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index ab5c1897b..a6d1a8743 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -11,8 +11,9 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -module Orderings (B : Terms.Blob) : +module type Blob = sig + include Terms.Blob (* This order relation should be: * - stable for instantiation @@ -20,12 +21,22 @@ module Orderings (B : Terms.Blob) : * *) val compare_terms : - B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison + t Terms.foterm -> t Terms.foterm -> Terms.comparison - val compute_unit_clause_weight : - B.t Terms.unit_clause -> int + (* these could be outside the module, but to ease experimentation + * we allow them to be tied with the ordering *) + val compute_unit_clause_weight : 't Terms.unit_clause -> int + val compute_goal_weight : 't Terms.unit_clause -> int - val compute_goal_weight : - B.t Terms.unit_clause -> int + val name : string end + +module NRKBO (B : Terms.Blob) : Blob +with type t = B.t and type input = B.input + +module KBO (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 and type input = B.input diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index f156ff0ff..1cdb9eb5c 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -16,7 +16,7 @@ let debug _ = ();; let monster = 100;; -module Paramod (B : Terms.Blob) = struct +module Paramod (B : Orderings.Blob) = struct type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list | GaveUp @@ -29,7 +29,7 @@ module Paramod (B : Terms.Blob) = struct module IDX = Index.Index(B) module Sup = Superposition.Superposition(B) module Utils = FoUtils.Utils(B) - module Order = Orderings.Orderings(B) + module Order = B module WeightOrderedPassives = struct type t = B.t Terms.passive_clause diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index fa914ef61..13fe56fc5 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -module Paramod ( B : Terms.Blob ) : +module Paramod ( B : Orderings.Blob ) : sig type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 1a5880434..f86d4d36e 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -11,12 +11,12 @@ (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) -module Superposition (B : Terms.Blob) = +module Superposition (B : Orderings.Blob) = struct module IDX = Index.Index(B) module Unif = FoUnif.Founif(B) module Subst = FoSubst - module Order = Orderings.Orderings(B) + module Order = B module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 149bbb048..30d32d540 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -11,7 +11,7 @@ (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) -module Superposition (B : Terms.Blob) : +module Superposition (B : Orderings.Blob) : sig (* bag, maxvar, meeting point *)