Fixed useage

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 627f2604b6c2ea0c36cfc3187b4598c4d42ab999..aa77e0c5a454566708b6fd54f399a1761ce5d9a7 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -13,6 +13,7 @@
 
 module OT = struct type t = string  let compare = Pervasives.compare end 
 module HC = Map.Make(OT)
+module TS = HTopoSort.Make(OT)
 
 type leaf = int * string
 
@@ -78,7 +79,7 @@ module MakeBlob(C:LeafComparer) : Terms.Blob
   end
 ;;
 
-let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord =
+let success_msg bag l (pp : ?margin:int -> leaf Terms.clause -> string) ord =
   (* TODO: do some sort of poor man lock (open + OEXCL) so that
    *       just one thread at a time prints the proof *)
   print_endline ("% SZS status Unsatisfiable for " ^ 
@@ -99,7 +100,7 @@ let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord
     (times.Unix.tms_utime +. times.Unix.tms_stime) ^ " using " ^ ord);
 ;;
 
-let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_clause -> string) oname =
+let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.clause -> string) oname =
   let prefix = string_of_int (Unix.getpid ()) in
   let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in
   prerr_endline "Facts:";
@@ -121,20 +122,20 @@ let report_error s =  prerr_endline (string_of_int (Unix.getpid())^": "^s);;
 
 module Main(P : Paramod.Paramod with type t = leaf) = struct
 
- let run stats goal hypotheses pp_unit_clause name = 
+ let run ~useage ~printmsg stats goal hypotheses pp_clause name = 
    let bag = Terms.empty_bag, 0 in
    let bag, g_passives = P.mk_goal bag goal in
    let bag, passives = 
      HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
    in
-   start_msg stats passives g_passives pp_unit_clause name;
+   if printmsg then start_msg stats passives g_passives pp_clause name;
    match
-     P.paramod 
+     P.paramod ~useage
       ~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_unit_clause name; 0
+         success_msg bag l pp_clause name; 0
    | P.Unsatisfiable ([]) -> 
          report_error "Unsatisfiable but no solution output"; 3
    | P.GaveUp -> 2
@@ -163,14 +164,24 @@ end
           name, (n_occ, arity, n_gocc, g_pos, Stats.dependencies name passives))
        data
    in
+   let oplist = List.map (fun ((_,x),_) -> x) data in
+   let deps op = 
+     (let _,(_,_,_,_,d) = List.find (fun ((_,op'),_) -> op = op') data 
+      in List.map snd d)
+   in 
+   let oplist = TS.topological_sort oplist deps in
    List.sort 
-     (fun (n1,(o1,a1,go1,p1,d1)) (n2,(o2,a2,go2,p2,d2)) -> 
-        Pervasives.compare 
-          (a1,o1,go1,p1,d1) (a2,o2,go2,p2,d2))
+     (fun ((_,n1),(o1,a1,go1,p1,_)) ((_,n2),(o2,a2,go2,p2,_)) ->
+        if a1 = 0 && a2 = 0 then 0
+        else if a1 = 0 then -1
+        else if a2 = 0 then 1
+        else let res = Pervasives.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2)
+             in if res = 0 then Pervasives.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist)
+                else res)
      data
  ;;
 
-let worker order goal hypotheses =
+let worker order ~useage ~printmsg goal hypotheses =
    let stats = compute_stats goal hypotheses in
    let module C = 
      struct
@@ -201,15 +212,15 @@ let worker order goal hypotheses =
    | `NRKBO ->
        let module O = Orderings.NRKBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_clause O.name
    | `KBO ->
        let module O = Orderings.KBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_clause O.name
    | `LPO ->
        let module O = Orderings.LPO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_clause O.name
 ;;
 
 let print_status p = 
@@ -274,11 +285,13 @@ usage: matitaprover [options] problemfile";
          let pid = Unix.fork () in 
          if pid = 0 then (exit (f ())) else pid)
     [ 
-      (fun () -> worker `NRKBO goal hypotheses)
+      (fun () -> worker `NRKBO ~useage:true ~printmsg:true goal hypotheses)
     ;
-      (fun () -> worker `KBO goal hypotheses)
+      (fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `LPO goal hypotheses)
+      (fun () -> worker `LPO ~useage:true ~printmsg:true goal hypotheses)
+    ;
+      (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
     ];
   let rec aux () =
     if List.length !childs = 0 then