(* argument parsing *)
let depth = int "depth" params in
let width = int "width" params in
+ let timeout = string "timeout" params in
let paramodulation = bool "paramodulation" params in
let full = bool "full" params in
let superposition = bool "superposition" params in
let subterms_only = bool "subterms_only" params in
let caso_strano = bool "caso_strano" params in
let demod_table = string "demod_table" params in
+ let timeout =
+ try Some (float_of_string timeout) with Failure _ -> None
+ in
(* the real tactic *)
let auto_tac dbd (proof, goal) =
let normal_auto () =
debug_print (lazy "USO PARAMODULATION...");
(* try *)
try
- let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in
+ let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full
+ ?timeout (proof, goal) in
prerr_endline (Saturation.get_stats ());
rc
with exn ->