"
;;
+let p_to_ma ?timeout ~tptppath ~filename () =
+ let data =
+ Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath
+ ~raw_preamble ()
+ in
+ data
+;;
+
let main () =
MatitaInit.fill_registry ();
let tptppath = ref "./" in
+ let timeout = ref 600 in
MatitaInit.add_cmdline_spec
["-tptppath",Arg.String (fun s -> tptppath:= s),
- "Where to find the Axioms/ and Problems/ directory"];
+ "Where to find the Axioms/ and Problems/ directory";
+ "-timeout", Arg.Int (fun x -> timeout := x),
+ "Timeout in seconds"];
MatitaInit.parse_cmdline ();
MatitaInit.load_configuration_file ();
Helm_registry.set_bool "db.nodb" true;
| _ -> prerr_endline "You must specify exactly one .p file."; exit 1
in
let data =
- Tptp2grafite.tptp2grafite ~filename:inputfile ~tptppath:!tptppath
- ~raw_preamble ()
+ p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath ()
in
(* prerr_endline data; *)
let is = Ulexing.from_utf8_string data in