From: Enrico Tassi Date: Thu, 2 Jul 2009 10:57:00 +0000 (+0000) Subject: return type of paramod fixed according to the SZSOntology X-Git-Tag: make_still_working~3758 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ec39afa1b8aaad13d8f5460bccf7119f45788c5;p=helm.git return type of paramod fixed according to the SZSOntology --- diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 379aca1dc..79ea569a2 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -32,10 +32,12 @@ let nparamod rdb metasenv subst context t table = let (bag,maxvar), goals = HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t] in - let solutions = + match P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) ~g_passives:goals ~passives (bag,maxvar) - in + with + | P.Error _ | P.GaveUp | P.Timeout _ -> [] + | P.Unsatisfiable solutions -> List.map (fun (bag,i,l) -> (* List.iter (fun x -> diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index a6f3a93c7..0dafc864e 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -17,7 +17,12 @@ let debug _ = ();; let monster = 100;; module Paramod (B : Terms.Blob) = struct - exception Failure of string * B.t Terms.bag * int * int + type szsontology = + | Unsatisfiable of (B.t Terms.bag * int * int list) list + | GaveUp + | Error of string + | Timeout of int * B.t Terms.bag + exception Stop of szsontology type bag = B.t Terms.bag * int module Pp = Pp.Pp (B) module FU = FoUnif.Founif(B) @@ -109,8 +114,10 @@ module Paramod (B : Terms.Blob) = struct (* 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 - assert (not (is_passive_set_empty g_passives)); - let g_cl = pick_min_passive ~use_age:use_age g_passives in + if (is_passive_set_empty g_passives) then + raise (Stop GaveUp) (* we say we are incomplete *) + else + let g_cl = pick_min_passive ~use_age:use_age g_passives in (true,g_cl,passives,remove_passive_clause g_passives g_cl) end else let cl = pick_min_passive ~use_age:use_age passives in @@ -186,8 +193,7 @@ module Paramod (B : Terms.Blob) = struct actives passives g_actives g_passives = let iterno = iterno + 1 in - if iterno = max_steps then - raise (Failure ("No iterations left !",bag,maxvar,iterno)); + if iterno = max_steps then raise (Stop (Timeout (maxvar,bag))); (* timeout check: gettimeofday called only if timeout set *) if timeout <> None && (match timeout with @@ -208,9 +214,7 @@ module Paramod (B : Terms.Blob) = struct (); x::acc,i+1) ([],0) g_actives); - raise (Failure (("Last chance: failed over " ^ - string_of_int maxgoals^ " goal " ^ - string_of_float (Unix.gettimeofday())),bag,maxvar,0)); + raise (Stop (Timeout (maxvar,bag))) end else if false then (* activates last chance strategy *) begin @@ -218,9 +222,9 @@ module Paramod (B : Terms.Blob) = struct given_clause ~noinfer:true bag maxvar iterno max_steps (Some (Unix.gettimeofday () +. 20.)) actives passives g_actives g_passives; - raise (Failure ("Timeout !",bag,maxvar,iterno)) + raise (Stop (Timeout (maxvar,bag))); end - else raise (Failure ("Timeout !",bag,maxvar,iterno)); + else raise (Stop (Timeout (maxvar,bag))); let use_age = iterno mod 5 = 0 in @@ -357,11 +361,9 @@ module Paramod (B : Terms.Blob) = struct List.iter (fun x -> prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l; *) - [ bag, i, l ] - | Failure (msg,_bag,_maxvar,iterno) -> - prerr_endline msg; - prerr_endline (Printf.sprintf "FAILURE in %d iterations" iterno); - [] + Unsatisfiable [ bag, i, l ] + | Stop (Unsatisfiable _) -> Error "stop bug solution found!" + | Stop o -> o ;; end diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index c8ba6cad9..fa914ef61 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -13,6 +13,11 @@ module Paramod ( B : Terms.Blob ) : sig + type szsontology = + | Unsatisfiable of (B.t Terms.bag * int * int list) list + | GaveUp + | Error of string + | Timeout of int * B.t Terms.bag type bag = B.t Terms.bag * int val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause @@ -21,6 +26,5 @@ module Paramod ( B : Terms.Blob ) : ?timeout:float -> bag -> g_passives:B.t Terms.unit_clause list -> - passives:B.t Terms.unit_clause list -> - (B.t Terms.bag * int * int list) list + passives:B.t Terms.unit_clause list -> szsontology end