From e61a54d7581b42259d726389250e1cb63682d8d8 Mon Sep 17 00:00:00 2001 From: lduboisd Date: Mon, 11 Apr 2022 11:29:23 +0200 Subject: verit_timeout takes an integer as parameter --- examples/Example.v | 23 ++++++++++++++++++++++- examples/foo.v | 28 ---------------------------- src/Tactics.v | 48 ++++++++++++++++++++++++------------------------ src/g_smtcoq.mlg | 4 ++-- 4 files changed, 48 insertions(+), 55 deletions(-) delete mode 100644 examples/foo.v diff --git a/examples/Example.v b/examples/Example.v index b949740..9fcb555 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/examples/foo.v b/examples/foo.v deleted file mode 100644 index c2162df..0000000 --- a/examples/foo.v +++ /dev/null @@ -1,28 +0,0 @@ -Add Rec LoadPath "../src" as SMTCoq. -Require Import SMTCoq.SMTCoq. -Require Import ZArith. - -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. -Qed. - -Tactic Notation "verit_timeout2" := - prop2bool; - [ .. | get_hyps ltac:(fun Hs => - lazymatch Hs with - | Some ?Hs => idtac 1 ; - prop2bool_hyps Hs; idtac 2 ; - [ .. | idtac 3 ; verit_bool_base_auto_timeout (Some Hs) ] - | None => idtac 4 ; verit_bool_base_auto_timeout (@None nat) - end) - ]. - -Goal true -> P 1000000000. -intro H. -verit_timeout2. constructor. \ No newline at end of file diff --git a/src/Tactics.v b/src/Tactics.v index c44af14..316fcc1 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -91,28 +91,28 @@ Tactic Notation "verit_bool_no_check" := (** 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_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) := +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)) - | None => verit_bool_base_auto_timeout (Some h) + | 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" := - get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; 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) := +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)) - | None => verit_bool_no_check_base_auto_timeout (Some h) + | 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" := - get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; 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 **) @@ -165,48 +165,48 @@ Tactic Notation "verit_no_check" := end; vauto) ]. -Tactic Notation "verit_timeout" constr(h) := +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)) ] - | None => verit_bool_base_auto_timeout (Some h) + [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout] + | None => verit_bool_base_auto_timeout (Some h) timeout end; vauto) ] ]. -Tactic Notation "verit_timeout" := +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) ] - | None => verit_bool_base_auto_timeout (@None nat) + [ .. | 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) := +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)) ] - | None => verit_bool_no_check_base_auto_timeout (Some h) + [ .. | 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" := +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) ] - | None => verit_bool_no_check_base_auto_timeout (@None nat) + [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout] + | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout end; vauto) ]. diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg index 19298f4..1d8f146 100644 --- a/src/g_smtcoq.mlg +++ b/src/g_smtcoq.mlg @@ -115,8 +115,8 @@ END TACTIC EXTEND Tactic_verit | [ "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 ()) } +| [ "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 -- cgit