module A = Ast;;
let floc = HExtlib.dummy_floc;;
+let paramod_timeout = ref 600;;
+
let universe = "Univ" ;;
let kw = [
fv))
else [])@
[GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
- GA.Auto (floc,["paramodulation",""])),
+ GA.Auto (floc,["paramodulation","";"timeout",string_of_int !paramod_timeout])),
Some (GA.Dot(floc))));
GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
;;
(* MAIN *)
-let tptp2grafite ?raw_preamble ~tptppath ~filename () =
+let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () =
+ paramod_timeout := timeout;
let rec aux = function
| [] -> []
| ((A.Inclusion (file,_)) as hd) :: tl ->
in
CicNotationPp.set_pp_term term_pp;
let lazy_term_pp = fun x -> assert false in
- let obj_pp = CicNotationPp.pp_obj in
+ let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
in
let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in