aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/Example.v23
-rw-r--r--src/PropToBool.v10
-rw-r--r--src/Tactics.v73
-rw-r--r--src/g_smtcoq.mlg6
-rw-r--r--src/verit/verit.ml14
-rw-r--r--src/verit/verit.mli4
6 files changed, 115 insertions, 15 deletions
diff --git a/examples/Example.v b/examples/Example.v
index cd53212..0cd1477 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -14,7 +14,6 @@
If you are using native-coq instead of Coq 8.11, replace it with:
Require Import SMTCoq.
*)
-
Require Import SMTCoq.SMTCoq.
Require Import Bool.
@@ -425,3 +424,25 @@ Section CompCert.
Qed.
End CompCert.
+
+
+(** The verit solver can be called with an integer (the timeout in seconds).
+If the goal cannot be solved within timeout seconds, then an anomaly is raised **)
+
+Section test_timeout.
+
+Variable P : Z -> bool.
+Variable H0 : P 0.
+Variable HInd : forall n, implb (P n) (P (n + 1)).
+
+Goal P 3.
+(* verit_timeout 3. *) verit.
+Qed.
+
+Goal true -> P 1000000000.
+intro H.
+(* Fail verit_timeout 1.
+Fail verit_timeout 5. *)
+Abort.
+
+End test_timeout.
diff --git a/src/PropToBool.v b/src/PropToBool.v
index d71c81c..5a7bf53 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -164,10 +164,10 @@ Ltac prop2bool_hyp H :=
destruct HFalse
| ];
clear H';
- match (eval compute in prop2bool_comp) with
+ lazymatch (eval compute in prop2bool_comp) with
| true =>
let A := eval cbv in prop2bool_t in
- match goal with
+ lazymatch goal with
| [ _ : CompDec A |- _ ] => idtac
| _ =>
let Hcompdec := fresh "Hcompdec" in
@@ -195,7 +195,7 @@ Ltac prop2bool_hyp H :=
| _ => prop2bool
end in
tac_rec;
- match goal with
+ lazymatch goal with
| [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
end;
destruct HFalse
@@ -213,9 +213,9 @@ Ltac prop2bool_hyp H :=
Ltac remove_compdec_hyp H :=
let TH := type of H in
- match TH with
+ lazymatch TH with
| forall p : CompDec ?A, _ =>
- match goal with
+ lazymatch goal with
| [ p' : CompDec A |- _ ] =>
let H1 := fresh in
assert (H1 := H p'); clear H; assert (H := H1); clear H1;
diff --git a/src/Tactics.v b/src/Tactics.v
index 14b984b..727e0b7 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -29,7 +29,7 @@ Ltac get_hyps_acc acc :=
| id _ => fail
| _ =>
let _ := match goal with _ => change P with (id P) in H end in
- match acc with
+ lazymatch acc with
| Some ?t => get_hyps_acc (Some (H, t))
| None => get_hyps_acc (Some H)
end
@@ -94,6 +94,31 @@ Tactic Notation "verit_bool_no_check" :=
let Hs := get_hyps in
fun Hs => verit_bool_no_check_base_auto Hs; vauto.
+(** Tactics in bool with timeout **)
+
+Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances.
+Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances.
+
+Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) :=
+ get_hyps ltac:(fun Hs =>
+ match Hs with
+ | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
+ | None => verit_bool_base_auto_timeout (Some h) timeout
+ end;
+ vauto).
+Tactic Notation "verit_bool_timeout" int_or_var(timeout) :=
+ get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto).
+
+Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) :=
+ get_hyps ltac:(fun Hs =>
+ match Hs with
+ | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
+ | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+ end;
+ vauto).
+Tactic Notation "verit_bool_no_check_timeout" int_or_var(timeout) :=
+ get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto).
+
(** Tactics in Prop **)
@@ -145,6 +170,52 @@ Tactic Notation "verit_no_check" :=
end; vauto
].
+Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=
+ 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)) timeout]
+ | None => verit_bool_base_auto_timeout (Some h) timeout
+ end; vauto)
+ ]
+ ].
+Tactic Notation "verit_timeout" int_or_var(timeout) :=
+ prop2bool;
+ [ .. | get_hyps ltac:(fun Hs =>
+ match Hs with
+ | Some ?Hs =>
+ prop2bool_hyps Hs;
+ [ .. | verit_bool_base_auto_timeout (Some Hs) timeout]
+ | None => verit_bool_base_auto_timeout (@None nat) timeout
+ end; vauto)
+ ].
+Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) :=
+ 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)) timeout ]
+ | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+ end; vauto)
+ ]
+ ].
+Tactic Notation "verit_no_check_timeout" int_or_var(timeout) :=
+ prop2bool;
+ [ .. | get_hyps ltac:(fun Hs =>
+ match Hs with
+ | Some ?Hs =>
+ prop2bool_hyps Hs;
+ [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
+ | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
+ 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 7b8093b..cd0233f 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) int_or_var(timeout) ] -> { Verit.tactic (Some timeout) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic_no_check (Some timeout) lpl (get_lemmas ()) }
END
TACTIC EXTEND Tactic_cvc4
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index c2fb186..eb8c5cc 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 _ = CErrors.anomaly (Pp.str "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 72566d2..d67051f 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
generated by cgit (git 2.34.1) at 2024-06-12 19:14:48 +0000