verit timeout

4 files changed, 87 insertions, 8 deletions

diff --git a/src/Tactics.v b/src/Tactics.v
index f79b253..e41b0f5 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -89,6 +89,31 @@ Tactic Notation "verit_bool_no_check" constr(h) :=
 Tactic Notation "verit_bool_no_check"           :=
   get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto).
 
+(** Tactics in bool with timeout **)
+
+Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances.
+Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances.
+
+Tactic Notation "verit_bool_timeout" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs))
+                   | None => verit_bool_base_auto_timeout (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool_timeout"           :=
+  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto).
+
+Tactic Notation "verit_bool_no_check_timeout" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs))
+                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool_no_check_timeout"           :=
+  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; vauto).
+
 
 (** Tactics in Prop **)
 
@@ -140,6 +165,52 @@ Tactic Notation "verit_no_check"           :=
                           end; vauto)
   ].
 
+Tactic Notation "verit_timeout" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) ]
+                                   | None => verit_bool_base_auto_timeout (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit_timeout"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_base_auto_timeout (Some Hs) ]
+                          | None => verit_bool_base_auto_timeout (@None nat)
+                          end; vauto)
+  ].
+Tactic Notation "verit_no_check_timeout" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) ]
+                                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit_no_check_timeout"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) ]
+                          | None => verit_bool_no_check_base_auto_timeout (@None nat)
+                          end; vauto)
+  ].
+
+
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg
index c8d38db..19298f4 100644
--- a/src/g_smtcoq.mlg
+++ b/src/g_smtcoq.mlg
@@ -113,8 +113,10 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic lpl (get_lemmas ()) }
-| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check lpl (get_lemmas ()) }
+| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) }
+| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) }
 END
 
 TACTIC EXTEND Tactic_cvc4
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 7f89943..b0c75a7 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -169,7 +169,7 @@ let export out_channel rt ro lsmt =
 
 exception Unknown
 
-let call_verit _ rt ro ra_quant rf_quant first lsmt =
+let call_verit timeout _ rt ro ra_quant rf_quant first lsmt =
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro lsmt;
   close_out outchan;
@@ -177,6 +177,11 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
   let wname, woc = Filename.open_temp_file "warnings_verit" ".log" in
   close_out woc;
   let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename ^ " 2> " ^ wname in
+  let command = 
+    match timeout with
+      | Some i -> "timeout "^(string_of_int i)^" "^command
+      | None -> command
+  in
   Format.eprintf "%s@." command;
   let t0 = Sys.time () in
   let exit_code = Sys.command command in
@@ -202,7 +207,7 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
           CoqInterface.error ("veriT failed with the error: " ^ l)
       done
     with End_of_file -> () in
-
+  if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = failwith "veriT timed out" in ());
   try
     if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();
@@ -217,7 +222,7 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
 let verit_logic =
   SL.of_list [LUF; LLia]
 
-let tactic_gen vm_cast lcpl lcepl =
+let tactic_gen vm_cast timeout lcpl lcepl =
   (* Transform the tuple of lemmas given by the user into a list *)
   let lcpl =
     let lcpl = EConstr.Unsafe.to_constr lcpl in
@@ -235,6 +240,7 @@ let tactic_gen vm_cast lcpl lcepl =
   let rf = VeritSyntax.rf in
   let ra_quant = VeritSyntax.ra_quant in
   let rf_quant = VeritSyntax.rf_quant in
-  SmtCommands.tactic call_verit verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl
+  SmtCommands.tactic (call_verit timeout) verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl
 let tactic = tactic_gen vm_cast_true
 let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check)
+
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index f0acd0c..654de07 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
 val theorem : CoqInterface.id -> string -> string -> unit
-val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
-val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic_no_check : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic