X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fmatitaprover%2Fmatitaprover.ml;h=f8a74014ae347f8802e5f2c0b489d347cdade90b;hb=341c09ae53c5b432015dbd95ac099d824609e626;hp=1172bbb5d3438f752eb44c1fedcea6f903330892;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 1172bbb5d..f8a74014a 100644
--- 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
 
@@ -106,7 +107,7 @@ let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_cla
   List.iter (fun x -> prerr_endline (" " ^ pp x)) passives;
   prerr_endline "Goal:";
   prerr_endline (" " ^ pp g_passives);
-  prerr_endline "Order:";
+(*  prerr_endline "Order:";
   prerr_endline ("  " ^ oname);
   prerr_endline "Leaf order:";
   List.iter (fun ((_,name), (a,b,c,gp,l)) ->
@@ -114,22 +115,22 @@ let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_cla
        string_of_int b ^ " " ^
        string_of_int c ^ " " ^
        String.concat "," (List.map string_of_int gp) ^ 
-       String.concat "," (List.map snd l))) stats;
+       String.concat "," (List.map snd l))) stats;*)
 ;;
 
 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_unit_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_unit_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
@@ -163,10 +164,24 @@ end
           name, (n_occ, arity, n_gocc, g_pos, Stats.dependencies name passives))
        data
    in
-   List.sort Pervasives.compare data
+   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,_)) ((_,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
@@ -180,13 +195,13 @@ let worker order goal hypotheses =
         if List.length raw = 
            List.length (HExtlib.list_uniq raw)
         then
-          (prerr_endline "NO CLASH, using fixed ground order";
+          ((*prerr_endline "NO CLASH, using fixed ground order";*)
            fun a b ->
             Pervasives.compare 
               (pos a stats)
               (pos b stats))
         else
-          (prerr_endline "CLASH, statistics insufficient";
+          ((*prerr_endline "CLASH, statistics insufficient";*)
             fun (a,_) (b,_) -> Pervasives.compare a b)
       ;;
      end
@@ -197,19 +212,19 @@ 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_unit_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_unit_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_unit_clause O.name
 ;;
 
 let print_status p = 
-  let print_endline s = prerr_endline (string_of_int p ^ ": " ^ s) in
+  let print_endline s = () in (* prerr_endline (string_of_int p ^ ": " ^ s) in*)
     function
     | Unix.WEXITED 0 -> 
         print_endline ("status Unsatisfiable for " ^ 
@@ -270,13 +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 ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `LPO goal hypotheses)
-*)
+      (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
     ];
   let rec aux () =
     if List.length !childs = 0 then