hash "_";;
let problem_file = ref "no-file-given";;
-let tptppath = ref "./";;
+let tptppath = ref "/";;
let seconds = ref 300;;
let fail_msg () =
("[path] TPTP lib root, default " ^ !tptppath);
"--timeout", Arg.Int (fun p -> seconds := p),
("[seconds] timeout, default " ^ string_of_int !seconds);
- ] (fun x -> problem_file := x) "matitaprover [problemfile]";
+ ] (fun x -> problem_file := x) "
+Matitaprover is the first order automatic prover that equips the
+Matita interactive theorem prover (http://matita.cs.unibo.it).
+
+Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
+
+If --tptppath is given, instead of the problem file you can just give the
+problem name with the .p suffix (e.g. BOO001-1.p)
+
+If --tptppath is not given, included files (i.e. axiom sets) are searched
+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 module B : Terms.Blob with type t = leaf and type input = Ast.term = struct
+ 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
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 ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with
+ (* 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 " ^