From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 30 Jun 2009 13:07:35 +0000 (+0000)
Subject: attempt of using 2 different orderings
X-Git-Tag: make_still_working~3765
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f5f3f5c96fd3ab0c466b828a731b8517a91bbd0;p=helm.git

attempt of using 2 different orderings
---

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 2e69e08d7..d615d18ca 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -65,11 +65,12 @@ in the current directory only.
 usage: matitaprover [options] problemfile";
   let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
   let goal = match goals with [x] -> x | _ -> assert false in
+  let leaf_compare = ref (fun ((a,_) : leaf) ((b,_) : leaf) -> Pervasives.compare a b) in
   let module B : Terms.Blob 
   with type t = leaf and type input = Ast.term = struct
         type t = leaf
         let eq a b = a == b
-        let compare (a,_) (b,_) = Pervasives.compare a b
+        let compare a b = !leaf_compare a b
         let eqP = hash "=="
         let pp (_,a) =  a 
         type input = Ast.term
@@ -97,8 +98,20 @@ usage: matitaprover [options] problemfile";
 
   end
   in
-  let module P = Paramod.Paramod(B) in
   let module Pp = Pp.Pp(B) in
+  let module P = Paramod.Paramod(B) in
+  let success_msg bag l (pp : ?margin:int -> B.t Terms.unit_clause -> string)=
+    print_endline ("% SZS status Unsatisfiable for " ^ 
+      Filename.basename !problem_file);
+    print_endline ("% SZS output start CNFRefutation for " ^ 
+      Filename.basename !problem_file);
+    flush stdout;
+    List.iter (fun x ->
+      print_endline (pp ~margin:max_int 
+        (fst(Terms.M.find x bag)))) l;
+    print_endline ("% SZS output end CNFRefutation for " ^ 
+      Filename.basename !problem_file)
+  in
   let bag = Terms.M.empty, 0 in
   let bag, g_passives = P.mk_goal bag goal in
   let bag, passives = 
@@ -111,20 +124,22 @@ usage: matitaprover [options] problemfile";
   List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives;
   prerr_endline "Goal";
   prerr_endline (" " ^ Pp.pp_unit_clause g_passives);
-  (* let _ = Unix.alarm !seconds in *)
-  match P.paramod ~timeout:(Unix.gettimeofday () +. float_of_int !seconds) ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with
-  | [] -> fail_msg ()
-  | (bag,_,l)::_ ->
-      print_endline ("% SZS status Unsatisfiable for " ^ 
-        Filename.basename !problem_file);
-      print_endline ("% SZS output start CNFRefutation for " ^ 
-        Filename.basename !problem_file);
-      flush stdout;
-      List.iter (fun x ->
-        print_endline (Pp.pp_unit_clause ~margin:max_int 
-          (fst(Terms.M.find x bag)))) l;
-      print_endline ("% SZS output end CNFRefutation for " ^ 
-        Filename.basename !problem_file);
+  let _ = Unix.alarm !seconds in
+  match 
+    P.paramod 
+     ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) )
+     ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
+  with
+  | [] -> 
+      leaf_compare := (fun (_,a) (_,b) -> Pervasives.compare a b);
+      (match 
+       P.paramod 
+        ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) )
+        ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
+      with
+      | [] -> fail_msg ()
+      | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause)
+  | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause
 ;;
 
 main ()