Final version, submitted to CASC-22.

diff --git a/helm/software/components/binaries/matitaprover/Makefile b/helm/software/components/binaries/matitaprover/Makefile
index c5a65b032ce300f12d56a71418730fb4278f7947..2b35935d95b5a8e7de4b5aabd8a9f8d1dc26391f 100644 (file)
--- a/helm/software/components/binaries/matitaprover/Makefile
+++ b/helm/software/components/binaries/matitaprover/Makefile
@@ -1,5 +1,5 @@
 DATE=$(shell date +%y%m%d)
-VERSION=1.0.0-rc1
+VERSION=1.0.0
 DIST=matitaprover---$(VERSION)
 
 all:

diff --git a/helm/software/components/binaries/matitaprover/hTopoSort.ml b/helm/software/components/binaries/matitaprover/hTopoSort.ml
new file mode 120000 (symlink)
index 0000000..32bae99
--- /dev/null
+++ b/helm/software/components/binaries/matitaprover/hTopoSort.ml
@@ -0,0 +1 @@
+../../extlib/hTopoSort.ml
\ No newline at end of file

diff --git a/helm/software/components/binaries/matitaprover/hTopoSort.mli b/helm/software/components/binaries/matitaprover/hTopoSort.mli
new file mode 120000 (symlink)
index 0000000..d3f754d
--- /dev/null
+++ b/helm/software/components/binaries/matitaprover/hTopoSort.mli
@@ -0,0 +1 @@
+../../extlib/hTopoSort.mli
\ No newline at end of file

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 627f2604b6c2ea0c36cfc3187b4598c4d42ab999..7f9046eb3519f168abe6a58cf999493f7b169aa7 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
 
@@ -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,14 +115,14 @@ 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 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 = 
@@ -129,7 +130,7 @@ module Main(P : Paramod.Paramod with type t = leaf) = struct
    in
    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,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 goal hypotheses =
    let stats = compute_stats goal hypotheses in
    let module C = 
      struct
@@ -184,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
@@ -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 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 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 stats goal hypotheses Pp.pp_unit_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 goal hypotheses)
     ;
-      (fun () -> worker `KBO goal hypotheses)
+      (fun () -> worker `KBO ~useage:true goal hypotheses)
     ;
-      (fun () -> worker `LPO goal hypotheses)
+      (fun () -> worker `LPO ~useage:true goal hypotheses)
+    ;
+      (fun () -> worker `NRKBO ~useage:false goal hypotheses)
     ];
   let rec aux () =
     if List.length !childs = 0 then