diff options
author | 2017-06-12 17:50:18 +0200 | |
---|---|---|
committer | 2017-06-16 16:42:40 +0200 | |
commit | d7e85f575fe6a41a700da9cd50236bef8ab03cf8 (patch) | |
tree | 3c0b30c781ba10676878632afbeba7f5281a0244 | |
parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) |
romega: avoid potential slowdown when changing concl by reified version
On some benchmarks provided by Chantal Keller a long time ago,
romega was abnormally slow compared to omega (or lia).
It turned out that the change of concl by reified version was
triggering unnecessary unfolds of Z.add, instead of unfolding
ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
the various Parameter Inline : no more indirections, Z_as_Int.plus
is directly Z.add.
Also use Tactics.convert_concl_no_check for this "change", as
recommended by PMP.
-rw-r--r-- | plugins/romega/ReflOmegaCore.v | 20 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 2 | ||||
-rw-r--r-- | test-suite/success/ROmega3.v | 31 |
3 files changed, 42 insertions, 11 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index d242264a9..51b99b993 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -18,12 +18,12 @@ Module Type Int. Bind Scope Int_scope with t. - Parameter zero : t. - Parameter one : t. - Parameter plus : t -> t -> t. - Parameter opp : t -> t. - Parameter minus : t -> t -> t. - Parameter mult : t -> t -> t. + Parameter Inline zero : t. + Parameter Inline one : t. + Parameter Inline plus : t -> t -> t. + Parameter Inline opp : t -> t. + Parameter Inline minus : t -> t -> t. + Parameter Inline mult : t -> t -> t. Notation "0" := zero : Int_scope. Notation "1" := one : Int_scope. @@ -39,10 +39,10 @@ Module Type Int. (** Int should also be ordered: *) - Parameter le : t -> t -> Prop. - Parameter lt : t -> t -> Prop. - Parameter ge : t -> t -> Prop. - Parameter gt : t -> t -> Prop. + Parameter Inline le : t -> t -> Prop. + Parameter Inline lt : t -> t -> Prop. + Parameter Inline ge : t -> t -> Prop. + Parameter Inline gt : t -> t -> Prop. Notation "x <= y" := (le x y): Int_scope. Notation "x < y" := (lt x y) : Int_scope. Notation "x >= y" := (ge x y) : Int_scope. diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 1a53862ec..60e6e7de7 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1016,7 +1016,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = Tactics.generalize (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >> - Tactics.change_concl (EConstr.of_constr reified) >> + Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> show_goal >> (if unsafe then diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v new file mode 100644 index 000000000..fd4ff260b --- /dev/null +++ b/test-suite/success/ROmega3.v @@ -0,0 +1,31 @@ + +Require Import ZArith ROmega. +Local Open Scope Z_scope. + +(** Benchmark provided by Chantal Keller, that romega used to + solve far too slowly (compared to omega or lia). *) + +Parameter v4 : Z. +Parameter v3 : Z. +Parameter o4 : Z. +Parameter s5 : Z. +Parameter v2 : Z. +Parameter o5 : Z. +Parameter s6 : Z. +Parameter v1 : Z. +Parameter o6 : Z. +Parameter s7 : Z. +Parameter v0 : Z. +Parameter o7 : Z. + +Lemma lemma_5833 : + ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192 +\/ + 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. +Proof. +Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 Qed. (* ditto *) |