]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/matitaprover/matitaprover.ml
update in delayed_updating
[helm.git] / matita / components / binaries / matitaprover / matitaprover.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
13
14 module OT = struct type t = string  let compare = Pervasives.compare end 
15 module HC = Map.Make(OT)
16 module TS = HTopoSort.Make(OT)
17
18 type leaf = int * string
19
20 let cache = ref HC.empty 
21 let num = ref 100
22
23 let hash s = 
24   try HC.find s !cache
25   with Not_found ->
26           cache := HC.add s (!num,s) !cache;
27           decr num;
28           HC.find s !cache
29 ;;
30
31 hash "==";;
32 hash "_";;
33
34 let problem_file = ref "no-file-given";;
35 let tptppath = ref "/";;
36 let seconds = ref 0;;
37
38 let fail_msg () =
39       print_endline ("% SZS status Timeout for " ^ 
40         Filename.basename !problem_file)
41 ;;
42   
43 module type LeafComparer =
44   sig
45     val cmp : leaf -> leaf -> int
46   end
47 ;;
48
49 module MakeBlob(C:LeafComparer) : Terms.Blob 
50   with type t = leaf and type input = Ast.term = struct
51         type t = leaf
52         let eq a b = a == b
53         let compare a b = C.cmp a b
54         let eqP = hash "=="
55         let pp (_,a) =  a 
56         type input = Ast.term
57         let rec embed m = function
58             | Ast.Variable name ->
59                 (try m, List.assoc name m
60                  with Not_found -> 
61                     let t = Terms.Var ~-(List.length m) in
62                     (name,t)::m, t)
63             | Ast.Constant name -> m, Terms.Leaf (hash name)
64             | Ast.Function (name,args) -> 
65                 let m, args = 
66                   HExtlib.list_mapi_acc 
67                     (fun x _ m -> embed m x) m args
68                 in
69                 m, Terms.Node (Terms.Leaf (hash name):: args) 
70         let is_eq = function
71           | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
72               Some (ty,l,r) 
73           | _ -> None
74         let saturate bo ty = 
75           let vars, ty = embed [] ty in
76           let _, bo = embed vars bo in
77           let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
78           bo, ty
79         ;;
80         let embed t = snd(embed [] t);;
81
82   end
83 ;;
84
85 let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord =
86   (* TODO: do some sort of poor man lock (open + OEXCL) so that
87    *       just one thread at a time prints the proof *)
88   print_endline ("% SZS status Unsatisfiable for " ^ 
89     Filename.basename !problem_file);
90   print_endline ("% SZS output start CNFRefutation for " ^ 
91     Filename.basename !problem_file);
92   flush stdout;
93   List.iter (fun x ->
94     let (cl,_,_) = Terms.get_from_bag x bag in
95     print_endline (pp ~margin:max_int 
96       cl)) l;
97   print_endline ("% SZS output end CNFRefutation for " ^ 
98     Filename.basename !problem_file);
99   let prefix = string_of_int (Unix.getpid ()) in
100   let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in
101   let times = Unix.times () in
102   prerr_endline ("solved " ^ !problem_file ^ " in " ^ string_of_float
103     (times.Unix.tms_utime +. times.Unix.tms_stime) ^ "(Process Time) using " ^ ord);
104 ;;
105
106 let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_clause -> string) oname =
107   let prefix = string_of_int (Unix.getpid ()) in
108   let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in
109   prerr_endline "Facts:";
110   List.iter (fun x -> prerr_endline (" " ^ pp x)) passives;
111   prerr_endline "Goal:";
112   prerr_endline (" " ^ pp g_passives);
113 (*  prerr_endline "Order:";
114   prerr_endline ("  " ^ oname);
115   prerr_endline "Leaf order:";
116   List.iter (fun ((_,name), (a,b,c,gp,l)) ->
117      prerr_endline (" " ^name ^ " " ^ string_of_int a ^ " " ^
118        string_of_int b ^ " " ^
119        string_of_int c ^ " " ^
120        String.concat "," (List.map string_of_int gp) ^ 
121        String.concat "," (List.map snd l))) stats;*)
122 ;;
123
124 let report_error s =  prerr_endline (string_of_int (Unix.getpid())^": "^s);;
125
126
127 module Main(P : Paramod.Paramod with type t = leaf) = struct
128
129   (*let mk_clause bag maxvar (t,ty) =
130     let (proof,ty) = B.saturate t ty in
131     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
132     let bag, c = Terms.add_to_bag c bag in
133       (bag, maxvar), c
134   ;;
135   
136   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
137   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;*)
138
139  let run ~useage ~printmsg stats goal hypotheses pp_unit_clause name = 
140    let bag = Terms.empty_bag, 0 in
141    let bag, g_passives = P.mk_goal bag goal in
142    let bag, passives = 
143      HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
144    in
145    if printmsg then start_msg stats passives g_passives pp_unit_clause name;
146    match
147      P.paramod ~useage
148       ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
149    with
150    | P.Error s -> report_error s; 3
151    | P.Unsatisfiable ((bag,_,_,l)::_) -> 
152          success_msg bag l pp_unit_clause name; 0
153    | P.Unsatisfiable ([]) -> 
154          report_error "Unsatisfiable but no solution output"; 3
155    | P.GaveUp -> 2
156    | P.Timeout _ -> 1
157  ;;
158 end
159
160  let compute_stats goal hypotheses =
161    let module C = 
162      struct type t = leaf let cmp (a,_) (b,_) = Pervasives.compare a b end 
163    in
164    let module B = MakeBlob(C) in
165    let module Pp = Pp.Pp(B) in
166    let module O = Orderings.NRKBO(B) in
167    let module P = Paramod.Paramod(O) in
168    let module Stats = Stats.Stats(O) in
169    let bag = Terms.empty_bag, 0 in
170    let bag, g_passives = P.mk_goal bag goal in
171    let bag, passives = 
172      HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
173    in
174    let data = Stats.parse_symbols passives g_passives in
175    let data = 
176      List.map
177        (fun (name, n_occ, arity, n_gocc, g_pos) ->
178           name, (n_occ, arity, n_gocc, g_pos, Stats.dependencies name passives))
179        data
180    in
181    let oplist = List.map (fun ((_,x),_) -> x) data in
182    let deps op = 
183      (let _,(_,_,_,_,d) = List.find (fun ((_,op'),_) -> op = op') data 
184       in List.map snd d)
185    in 
186    let oplist = TS.topological_sort oplist deps in
187    List.sort 
188      (fun ((_,n1),(o1,a1,go1,p1,_)) ((_,n2),(o2,a2,go2,p2,_)) ->
189         if a1 = 0 && a2 = 0 then 0
190         else if a1 = 0 then -1
191         else if a2 = 0 then 1
192         else let res = Pervasives.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2)
193              in if res = 0 then Pervasives.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist)
194                 else res)
195      data
196  ;;
197
198 let worker order ~useage ~printmsg goal hypotheses =
199    let stats = compute_stats goal hypotheses in
200    let module C = 
201      struct
202       let cmp =
203         let raw = List.map snd stats in
204         let rec pos x = function
205           | ((y,_)::tl) when y = x -> 0
206           | _::tl -> 1 + pos x tl
207           | [] -> assert false
208         in
209         if List.length raw = 
210            List.length (HExtlib.list_uniq raw)
211         then
212           ((*prerr_endline "NO CLASH, using fixed ground order";*)
213            fun a b ->
214             Pervasives.compare 
215               (pos a stats)
216               (pos b stats))
217         else
218           ((*prerr_endline "CLASH, statistics insufficient";*)
219             fun (a,_) (b,_) -> Pervasives.compare a b)
220       ;;
221      end
222    in
223    let module B = MakeBlob(C) in
224    let module Pp = Pp.Pp(B) in
225    match order with
226    | `NRKBO ->
227        let module O = Orderings.NRKBO(B) in
228        let module Main = Main(Paramod.Paramod(O)) in
229        Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
230    | `KBO ->
231        let module O = Orderings.KBO(B) in
232        let module Main = Main(Paramod.Paramod(O)) in
233        Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
234    | `LPO ->
235        let module O = Orderings.LPO(B) in
236        let module Main = Main(Paramod.Paramod(O)) in
237        Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
238 ;;
239
240 let print_status p = 
241   let print_endline s = () in (* prerr_endline (string_of_int p ^ ": " ^ s) in*)
242     function
243     | Unix.WEXITED 0 -> 
244         print_endline ("status Unsatisfiable for " ^ 
245           Filename.basename !problem_file);
246     | Unix.WEXITED 1 -> 
247         print_endline ("status Timeout for " ^ 
248           Filename.basename !problem_file);
249     | Unix.WEXITED 2 -> 
250         print_endline ("status GaveUp for " ^ 
251           Filename.basename !problem_file);
252     | Unix.WEXITED 3 ->
253         print_endline ("status Error for " ^ 
254           Filename.basename !problem_file);
255     | Unix.WEXITED _ -> assert false
256     | Unix.WSIGNALED s -> print_endline ("killed by signal " ^ string_of_int s)
257     | Unix.WSTOPPED _ -> print_endline "stopped"
258  ;;
259
260 let killall l = 
261   List.iter (fun pid -> try Unix.kill pid 9 with _ -> ()) l
262 ;;
263
264 let main () =
265   let childs = ref [] in
266   let _ =
267     Sys.signal 24 (Sys.Signal_handle 
268       (fun _ -> fail_msg (); killall !childs; exit 1)) 
269   in
270   let _ =
271     Sys.signal Sys.sigalrm 
272       (Sys.Signal_handle (fun _ -> prerr_endline "Alarm!"; fail_msg (); killall !childs; exit 1)) 
273   in
274   Arg.parse [
275    "--tptppath", Arg.String (fun p -> tptppath := p), 
276      ("[path]  TPTP lib root, default " ^ !tptppath);
277    "--timeout", Arg.Int (fun p -> seconds := p), 
278      ("[seconds]  timeout, default none");
279    ] (fun x -> problem_file := x) "
280 Matitaprover is the first order automatic prover that equips the 
281 Matita interactive theorem prover (http://matita.cs.unibo.it).
282
283 Developed by A.Asperti, M.Denes and E.Tassi, released under GPL version 2
284 or at your option any later version.
285
286 If --tptppath is given, instead of the problem file you can just give the 
287 problem name with the .p suffix (e.g. BOO001-1.p)
288
289 If --tptppath is not given, included files (i.e. axiom sets) are searched 
290 in the current directory only.
291
292 usage: matitaprover [options] problemfile";
293   let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
294   let goal = match goals with [x] -> x | _ -> assert false in
295   let _ = if !seconds > 0 then Unix.alarm !seconds else 0 in
296   childs := 
297     List.map 
298       (fun f -> 
299          let pid = Unix.fork () in 
300          if pid = 0 then (exit (f ())) else pid)
301     [ 
302       (fun () -> worker `NRKBO ~useage:true ~printmsg:true goal hypotheses)
303     ;
304       (fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses)
305     ;
306       (fun () -> worker `LPO ~useage:true ~printmsg:false goal hypotheses)
307     ;
308       (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
309     ];
310   let rec aux () =
311     if List.length !childs = 0 then
312       (fail_msg (); exit 1)
313     else 
314      match Unix.wait () with
315      | p, (Unix.WEXITED 0 as s) -> 
316          print_status p s;            
317          killall !childs; exit 0;
318      | p, s -> 
319          print_status p s;            
320          childs := List.filter ((<>)p) !childs; aux ()
321   in
322    aux ()
323 ;;
324
325 main ()