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 ->