From: Enrico Tassi <enrico.tassi@inria.fr>
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