diff options
author | lduboisd <lduboisd@inria.fr> | 2021-12-10 17:55:46 +0100 |
---|---|---|
committer | lduboisd <lduboisd@inria.fr> | 2021-12-10 17:55:46 +0100 |
commit | 15ab2869ab700d21c59c5a272721b5bba1d2b8ee (patch) | |
tree | 0505e07b4f05ea392ea25a78295d61b40bd7ef26 /src/Tactics.v | |
parent | 2c3b041073910c7d84d7995992e014e56aaed1fb (diff) | |
download | smtcoq-15ab2869ab700d21c59c5a272721b5bba1d2b8ee.tar.gz smtcoq-15ab2869ab700d21c59c5a272721b5bba1d2b8ee.zip |
verit timeout
Diffstat (limited to 'src/Tactics.v')
-rw-r--r-- | src/Tactics.v | 71 |
1 files changed, 71 insertions, 0 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 ]. |