summaryrefslogtreecommitdiff
path: root/contrib/omega
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/omega
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/omega')
-rw-r--r--[-rwxr-xr-x]contrib/omega/Omega.v2
-rw-r--r--contrib/omega/OmegaLemmas.v202
-rw-r--r--contrib/omega/coq_omega.ml344
-rw-r--r--contrib/omega/g_omega.ml46
-rw-r--r--[-rwxr-xr-x]contrib/omega/omega.ml469
5 files changed, 534 insertions, 489 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index e72dcec2..66f86a49 100755..100644
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -13,7 +13,7 @@
(* *)
(**************************************************************************)
-(* $Id: Omega.v,v 1.10.2.1 2004/07/16 19:30:12 herbelin Exp $ *)
+(* $Id: Omega.v 8642 2006-03-17 10:09:02Z notin $ *)
(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
Require Export ZArith_base.
diff --git a/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v
index 6f0ea2c6..ae642a3e 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/contrib/omega/OmegaLemmas.v
@@ -1,45 +1,45 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
-(*i $Id: OmegaLemmas.v,v 1.4.2.1 2004/07/16 19:30:12 herbelin Exp $ i*)
+(*i $Id: OmegaLemmas.v 7727 2005-12-25 13:42:20Z herbelin $ i*)
Require Import ZArith_base.
+Open Local Scope Z_scope.
(** These are specific variants of theorems dedicated for the Omega tactic *)
-Lemma new_var : forall x:Z, exists y : Z, x = y.
+Lemma new_var : forall x : Z, exists y : Z, x = y.
intros x; exists x; trivial with arith.
Qed.
-Lemma OMEGA1 : forall x y:Z, x = y -> (0 <= x)%Z -> (0 <= y)%Z.
+Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.
intros x y H; rewrite H; auto with arith.
Qed.
-Lemma OMEGA2 : forall x y:Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z.
+Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.
exact Zplus_le_0_compat.
Qed.
-Lemma OMEGA3 :
- forall x y k:Z, (k > 0)%Z -> x = (y * k)%Z -> x = 0%Z -> y = 0%Z.
+Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.
intros x y k H1 H2 H3; apply (Zmult_integral_l k);
- [ unfold not in |- *; intros H4; absurd (k > 0)%Z;
+ [ unfold not in |- *; intros H4; absurd (k > 0);
[ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate
| assumption ]
| rewrite <- H2; assumption ].
Qed.
-Lemma OMEGA4 : forall x y z:Z, (x > 0)%Z -> (y > x)%Z -> (z * y + x)%Z <> 0%Z.
+Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0.
-unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0)%Z;
- [ intros H4; cut (0 <= z * y + x)%Z;
+unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0);
+ [ intros H4; cut (0 <= z * y + x);
[ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6;
- absurd (z * y + x > 0)%Z;
+ absurd (z * y + x > 0);
[ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
| apply Zle_gt_trans with x;
[ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
@@ -55,48 +55,44 @@ unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0)%Z;
| apply Zgt_trans with x; [ assumption | assumption ] ].
Qed.
-Lemma OMEGA5 : forall x y z:Z, x = 0%Z -> y = 0%Z -> (x + y * z)%Z = 0%Z.
+Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0.
intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith.
Qed.
-Lemma OMEGA6 : forall x y z:Z, (0 <= x)%Z -> y = 0%Z -> (0 <= x + y * z)%Z.
+Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z.
intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption.
Qed.
Lemma OMEGA7 :
- forall x y z t:Z,
- (z > 0)%Z ->
- (t > 0)%Z -> (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * z + y * t)%Z.
+ forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.
intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat;
apply Zmult_gt_0_le_0_compat; assumption.
Qed.
-Lemma OMEGA8 :
- forall x y:Z, (0 <= x)%Z -> (0 <= y)%Z -> x = (- y)%Z -> x = 0%Z.
+Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.
intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
- [ intros H4; absurd (0 < x)%Z;
- [ change (0 >= x)%Z in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
+ [ intros H4; absurd (0 < x);
+ [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r;
assumption
| assumption ]
| intros H4; rewrite H4; trivial with arith ].
Qed.
-Lemma OMEGA9 :
- forall x y z t:Z, y = 0%Z -> x = z -> (y + (- x + z) * t)%Z = 0%Z.
+Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0.
intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l;
rewrite Zplus_0_r; assumption.
Qed.
Lemma OMEGA10 :
- forall v c1 c2 l1 l2 k1 k2:Z,
- ((v * c1 + l1) * k1 + (v * c2 + l2) * k2)%Z =
- (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))%Z.
+ forall v c1 c2 l1 l2 k1 k2 : Z,
+ (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
+ v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
@@ -104,8 +100,8 @@ intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
Qed.
Lemma OMEGA11 :
- forall v1 c1 l1 l2 k1:Z,
- ((v1 * c1 + l1) * k1 + l2)%Z = (v1 * (c1 * k1) + (l1 * k1 + l2))%Z.
+ forall v1 c1 l1 l2 k1 : Z,
+ (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
@@ -113,8 +109,8 @@ intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
Qed.
Lemma OMEGA12 :
- forall v2 c2 l1 l2 k2:Z,
- (l1 + (v2 * c2 + l2) * k2)%Z = (v2 * (c2 * k2) + (l1 + l2 * k2))%Z.
+ forall v2 c2 l1 l2 k2 : Z,
+ l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
@@ -122,8 +118,8 @@ intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
Qed.
Lemma OMEGA13 :
- forall (v l1 l2:Z) (x:positive),
- (v * Zpos x + l1 + (v * Zneg x + l2))%Z = (l1 + l2)%Z.
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
@@ -133,8 +129,8 @@ intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
Qed.
Lemma OMEGA14 :
- forall (v l1 l2:Z) (x:positive),
- (v * Zneg x + l1 + (v * Zpos x + l2))%Z = (l1 + l2)%Z.
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
@@ -142,128 +138,126 @@ intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
rewrite Zplus_0_r; trivial with arith.
Qed.
Lemma OMEGA15 :
- forall v c1 c2 l1 l2 k2:Z,
- (v * c1 + l1 + (v * c2 + l2) * k2)%Z =
- (v * (c1 + c2 * k2) + (l1 + l2 * k2))%Z.
+ forall v c1 c2 l1 l2 k2 : Z,
+ v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith.
Qed.
-Lemma OMEGA16 :
- forall v c l k:Z, ((v * c + l) * k)%Z = (v * (c * k) + l * k)%Z.
+Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.
intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
trivial with arith.
Qed.
-Lemma OMEGA17 : forall x y z:Z, Zne x 0 -> y = 0%Z -> Zne (x + y * z) 0.
+Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
- apply Zplus_reg_l with (y * z)%Z; rewrite Zplus_comm;
+ apply Zplus_reg_l with (y * z); rewrite Zplus_comm;
rewrite H3; rewrite H2; auto with arith.
Qed.
-Lemma OMEGA18 : forall x y k:Z, x = (y * k)%Z -> Zne x 0 -> Zne y 0.
+Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0.
unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1;
rewrite H3; auto with arith.
Qed.
-Lemma OMEGA19 :
- forall x:Z, Zne x 0 -> (0 <= x + -1)%Z \/ (0 <= x * -1 + -1)%Z.
+Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
[ intros H1; elim Zle_lt_or_eq with (1 := H1);
- [ intros H2; left; change (0 <= Zpred x)%Z in |- *; apply Zsucc_le_reg;
+ [ intros H2; left; change (0 <= Zpred x) in |- *; apply Zsucc_le_reg;
rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
- | intros H2; absurd (x = 0%Z); auto with arith ]
+ | intros H2; absurd (x = 0); auto with arith ]
| intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
apply Zle_left; apply Zsucc_le_reg; simpl in |- *;
apply Zlt_le_succ; auto with arith ].
Qed.
-Lemma OMEGA20 : forall x y z:Z, Zne x 0 -> y = 0%Z -> Zne (x + y * z) 0.
+Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3;
simpl in H3; rewrite Zplus_0_r in H3; trivial with arith.
Qed.
-Definition fast_Zplus_sym (x y:Z) (P:Z -> Prop) (H:P (y + x)%Z) :=
- eq_ind_r P H (Zplus_comm x y).
+Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
+ (H : P (y + x)) := eq_ind_r P H (Zplus_comm x y).
-Definition fast_Zplus_assoc_r (n m p:Z) (P:Z -> Prop)
- (H:P (n + (m + p))%Z) := eq_ind_r P H (Zplus_assoc_reverse n m p).
+Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
+ (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).
-Definition fast_Zplus_assoc_l (n m p:Z) (P:Z -> Prop)
- (H:P (n + m + p)%Z) := eq_ind_r P H (Zplus_assoc n m p).
+Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
+ (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).
-Definition fast_Zplus_permute (n m p:Z) (P:Z -> Prop)
- (H:P (m + (n + p))%Z) := eq_ind_r P H (Zplus_permute n m p).
+Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
+ (H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p).
-Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2:Z) (P:Z -> Prop)
- (H:P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))%Z) :=
+Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop)
+ (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) :=
eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).
-Definition fast_OMEGA11 (v1 c1 l1 l2 k1:Z) (P:Z -> Prop)
- (H:P (v1 * (c1 * k1) + (l1 * k1 + l2))%Z) :=
+Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop)
+ (H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) :=
eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
-Definition fast_OMEGA12 (v2 c2 l1 l2 k2:Z) (P:Z -> Prop)
- (H:P (v2 * (c2 * k2) + (l1 + l2 * k2))%Z) :=
+Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+ (H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) :=
eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).
-Definition fast_OMEGA15 (v c1 c2 l1 l2 k2:Z) (P:Z -> Prop)
- (H:P (v * (c1 + c2 * k2) + (l1 + l2 * k2))%Z) :=
+Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+ (H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) :=
eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
-Definition fast_OMEGA16 (v c l k:Z) (P:Z -> Prop)
- (H:P (v * (c * k) + l * k)%Z) := eq_ind_r P H (OMEGA16 v c l k).
+Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop)
+ (H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k).
-Definition fast_OMEGA13 (v l1 l2:Z) (x:positive) (P:Z -> Prop)
- (H:P (l1 + l2)%Z) := eq_ind_r P H (OMEGA13 v l1 l2 x).
+Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+ (H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x).
-Definition fast_OMEGA14 (v l1 l2:Z) (x:positive) (P:Z -> Prop)
- (H:P (l1 + l2)%Z) := eq_ind_r P H (OMEGA14 v l1 l2 x).
-Definition fast_Zred_factor0 (x:Z) (P:Z -> Prop) (H:P (x * 1)%Z) :=
- eq_ind_r P H (Zred_factor0 x).
+Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+ (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
+Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
+ (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).
-Definition fast_Zopp_one (x:Z) (P:Z -> Prop) (H:P (x * -1)%Z) :=
- eq_ind_r P H (Zopp_eq_mult_neg_1 x).
+Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
+ (H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x).
-Definition fast_Zmult_sym (x y:Z) (P:Z -> Prop) (H:P (y * x)%Z) :=
- eq_ind_r P H (Zmult_comm x y).
+Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
+ (H : P (y * x)) := eq_ind_r P H (Zmult_comm x y).
-Definition fast_Zopp_Zplus (x y:Z) (P:Z -> Prop) (H:P (- x + - y)%Z) :=
- eq_ind_r P H (Zopp_plus_distr x y).
+Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
+ (H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y).
-Definition fast_Zopp_Zopp (x:Z) (P:Z -> Prop) (H:P x) :=
+Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
eq_ind_r P H (Zopp_involutive x).
-Definition fast_Zopp_Zmult_r (x y:Z) (P:Z -> Prop)
- (H:P (x * - y)%Z) := eq_ind_r P H (Zopp_mult_distr_r x y).
+Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
+ (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
-Definition fast_Zmult_plus_distr (n m p:Z) (P:Z -> Prop)
- (H:P (n * p + m * p)%Z) := eq_ind_r P H (Zmult_plus_distr_l n m p).
-Definition fast_Zmult_Zopp_left (x y:Z) (P:Z -> Prop)
- (H:P (x * - y)%Z) := eq_ind_r P H (Zmult_opp_comm x y).
+Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
+ (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
+Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
+ (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).
-Definition fast_Zmult_assoc_r (n m p:Z) (P:Z -> Prop)
- (H:P (n * (m * p))%Z) := eq_ind_r P H (Zmult_assoc_reverse n m p).
+Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
+ (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
-Definition fast_Zred_factor1 (x:Z) (P:Z -> Prop) (H:P (x * 2)%Z) :=
- eq_ind_r P H (Zred_factor1 x).
+Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
+ (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).
-Definition fast_Zred_factor2 (x y:Z) (P:Z -> Prop)
- (H:P (x * (1 + y))%Z) := eq_ind_r P H (Zred_factor2 x y).
-Definition fast_Zred_factor3 (x y:Z) (P:Z -> Prop)
- (H:P (x * (1 + y))%Z) := eq_ind_r P H (Zred_factor3 x y).
+Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
+ (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y).
-Definition fast_Zred_factor4 (x y z:Z) (P:Z -> Prop)
- (H:P (x * (y + z))%Z) := eq_ind_r P H (Zred_factor4 x y z).
+Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
+ (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y).
-Definition fast_Zred_factor5 (x y:Z) (P:Z -> Prop)
- (H:P y) := eq_ind_r P H (Zred_factor5 x y).
+Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
+ (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).
-Definition fast_Zred_factor6 (x:Z) (P:Z -> Prop) (H:P (x + 0)%Z) :=
- eq_ind_r P H (Zred_factor6 x).
+Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
+ (H : P y) := eq_ind_r P H (Zred_factor5 x y).
+
+Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
+ (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 7a20aeb6..ee3301d7 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -13,13 +13,12 @@
(* *)
(**************************************************************************)
-(* $Id: coq_omega.ml,v 1.59.2.3 2004/07/16 19:30:12 herbelin Exp $ *)
+(* $Id: coq_omega.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
open Util
open Pp
open Reduction
open Proof_type
-open Ast
open Names
open Nameops
open Term
@@ -36,9 +35,11 @@ open Clenv
open Logic
open Libnames
open Nametab
-open Omega
open Contradiction
+module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+open OmegaSolver
+
(* Added by JCF, 09/03/98 *)
let elim_id id gl = simplest_elim (pf_global gl id) gl
@@ -56,16 +57,6 @@ let write f x = f:=x
open Goptions
-(* Obsolete, subsumed by Time Omega
-let _ =
- declare_bool_option
- { optsync = false;
- optname = "Omega time displaying flag";
- optkey = SecondaryTable ("Omega","Time");
- optread = read display_time_flag;
- optwrite = write display_time_flag }
-*)
-
let _ =
declare_bool_option
{ optsync = false;
@@ -110,6 +101,31 @@ let new_identifier_var =
let cpt = ref 0 in
(fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s)
+let new_id =
+ let cpt = ref 0 in fun () -> incr cpt; !cpt
+
+let new_var_num =
+ let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+
+let new_var =
+ let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+
+let display_var i = Printf.sprintf "X%d" i
+
+let intern_id,unintern_id =
+ let cpt = ref 0 in
+ let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
+ (fun (name : identifier) ->
+ try Hashtbl.find table name with Not_found ->
+ let idx = !cpt in
+ Hashtbl.add table name idx;
+ Hashtbl.add co_table idx name;
+ incr cpt; idx),
+ (fun idx ->
+ try Hashtbl.find co_table idx with Not_found ->
+ let v = new_var () in
+ Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+
let mk_then = tclTHENLIST
let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
@@ -156,22 +172,22 @@ let constant = gen_constant_in_modules "Omega" coq_modules
let coq_xH = lazy (constant "xH")
let coq_xO = lazy (constant "xO")
let coq_xI = lazy (constant "xI")
-let coq_ZERO = lazy (constant (if !Options.v7 then "ZERO" else "Z0"))
-let coq_POS = lazy (constant (if !Options.v7 then "POS" else "Zpos"))
-let coq_NEG = lazy (constant (if !Options.v7 then "NEG" else "Zneg"))
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
let coq_Z = lazy (constant "Z")
-let coq_relation = lazy (constant (if !Options.v7 then "relation" else "comparison"))
-let coq_SUPERIEUR = lazy (constant "SUPERIEUR")
-let coq_INFEEIEUR = lazy (constant "INFERIEUR")
-let coq_EGAL = lazy (constant "EGAL")
+let coq_comparison = lazy (constant "comparison")
+let coq_Gt = lazy (constant "Gt")
+let coq_INFEEIEUR = lazy (constant "Lt")
+let coq_Eq = lazy (constant "Eq")
let coq_Zplus = lazy (constant "Zplus")
let coq_Zmult = lazy (constant "Zmult")
let coq_Zopp = lazy (constant "Zopp")
let coq_Zminus = lazy (constant "Zminus")
-let coq_Zs = lazy (constant "Zs")
+let coq_Zsucc = lazy (constant "Zsucc")
let coq_Zgt = lazy (constant "Zgt")
let coq_Zle = lazy (constant "Zle")
-let coq_inject_nat = lazy (constant "inject_nat")
+let coq_Z_of_nat = lazy (constant "Z_of_nat")
let coq_inj_plus = lazy (constant "inj_plus")
let coq_inj_mult = lazy (constant "inj_mult")
let coq_inj_minus1 = lazy (constant "inj_minus1")
@@ -183,12 +199,12 @@ let coq_inj_ge = lazy (constant "inj_ge")
let coq_inj_gt = lazy (constant "inj_gt")
let coq_inj_neq = lazy (constant "inj_neq")
let coq_inj_eq = lazy (constant "inj_eq")
-let coq_fast_Zplus_assoc_r = lazy (constant "fast_Zplus_assoc_r")
-let coq_fast_Zplus_assoc_l = lazy (constant "fast_Zplus_assoc_l")
-let coq_fast_Zmult_assoc_r = lazy (constant "fast_Zmult_assoc_r")
+let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
+let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
+let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
-let coq_fast_Zplus_sym = lazy (constant "fast_Zplus_sym")
-let coq_fast_Zmult_sym = lazy (constant "fast_Zmult_sym")
+let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm")
+let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm")
let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx")
let coq_OMEGA1 = lazy (constant "OMEGA1")
let coq_OMEGA2 = lazy (constant "OMEGA2")
@@ -217,12 +233,12 @@ let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3")
let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4")
let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5")
let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6")
-let coq_fast_Zmult_plus_distr = lazy (constant "fast_Zmult_plus_distr")
-let coq_fast_Zmult_Zopp_left = lazy (constant "fast_Zmult_Zopp_left")
-let coq_fast_Zopp_Zplus = lazy (constant "fast_Zopp_Zplus")
-let coq_fast_Zopp_Zmult_r = lazy (constant "fast_Zopp_Zmult_r")
-let coq_fast_Zopp_one = lazy (constant "fast_Zopp_one")
-let coq_fast_Zopp_Zopp = lazy (constant "fast_Zopp_Zopp")
+let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l")
+let coq_fast_Zmult_opp_comm = lazy (constant "fast_Zmult_opp_comm")
+let coq_fast_Zopp_plus_distr = lazy (constant "fast_Zopp_plus_distr")
+let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r")
+let coq_fast_Zopp_eq_mult_neg_1 = lazy (constant "fast_Zopp_eq_mult_neg_1")
+let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive")
let coq_Zegal_left = lazy (constant "Zegal_left")
let coq_Zne_left = lazy (constant "Zne_left")
let coq_Zlt_left = lazy (constant "Zlt_left")
@@ -240,10 +256,10 @@ let coq_dec_Zgt = lazy (constant "dec_Zgt")
let coq_dec_Zge = lazy (constant "dec_Zge")
let coq_not_Zeq = lazy (constant "not_Zeq")
-let coq_not_Zle = lazy (constant "not_Zle")
-let coq_not_Zlt = lazy (constant "not_Zlt")
-let coq_not_Zge = lazy (constant "not_Zge")
-let coq_not_Zgt = lazy (constant "not_Zgt")
+let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
+let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
+let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
+let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
let coq_neq = lazy (constant "neq")
let coq_Zne = lazy (constant "Zne")
let coq_Zle = lazy (constant "Zle")
@@ -304,7 +320,7 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
EvalConstRef kn
| _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
-let sp_Zs = lazy (evaluable_ref_of_constr "Zs" coq_Zs)
+let sp_Zsucc = lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
@@ -324,23 +340,23 @@ let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |])
let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |])
let mk_not t = mkApp (build_coq_not (), [| t |])
let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
- [| Lazy.force coq_relation; t1; t2 |])
-let mk_inj t = mkApp (Lazy.force coq_inject_nat, [| t |])
+ [| Lazy.force coq_comparison; t1; t2 |])
+let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
let mk_integer n =
let rec loop n =
- if n=1 then Lazy.force coq_xH else
- mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI),
- [| loop (n/2) |])
+ if n =? one then Lazy.force coq_xH else
+ mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI),
+ [| loop (n/two) |])
in
- if n = 0 then Lazy.force coq_ZERO
- else mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG),
+ if n =? zero then Lazy.force coq_Z0
+ else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg),
[| loop (abs n) |])
type omega_constant =
- | Zplus | Zmult | Zminus | Zs | Zopp
+ | Zplus | Zmult | Zminus | Zsucc | Zopp
| Plus | Mult | Minus | Pred | S | O
- | POS | NEG | ZERO | Inject_nat
+ | Zpos | Zneg | Z0 | Z_of_nat
| Eq | Neq
| Zne | Zle | Zlt | Zge | Zgt
| Z | Nat
@@ -401,7 +417,7 @@ let destructurate_term t =
| _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
| _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
| _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
- | _, [_] when c = Lazy.force coq_Zs -> Kapp (Zs,args)
+ | _, [_] when c = Lazy.force coq_Zsucc -> Kapp (Zsucc,args)
| _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
| _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
| _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
@@ -409,25 +425,25 @@ let destructurate_term t =
| _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
| _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
| _, [] when c = Lazy.force coq_O -> Kapp (O,args)
- | _, [_] when c = Lazy.force coq_POS -> Kapp (NEG,args)
- | _, [_] when c = Lazy.force coq_NEG -> Kapp (POS,args)
- | _, [] when c = Lazy.force coq_ZERO -> Kapp (ZERO,args)
- | _, [_] when c = Lazy.force coq_inject_nat -> Kapp (Inject_nat,args)
+ | _, [_] when c = Lazy.force coq_Zpos -> Kapp (Zneg,args)
+ | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
+ | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
+ | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_nat,args)
| Var id,[] -> Kvar id
| _ -> Kufo
let recognize_number t =
let rec loop t =
match decompose_app t with
- | f, [t] when f = Lazy.force coq_xI -> 1 + 2 * loop t
- | f, [t] when f = Lazy.force coq_xO -> 2 * loop t
- | f, [] when f = Lazy.force coq_xH -> 1
+ | f, [t] when f = Lazy.force coq_xI -> one + two * loop t
+ | f, [t] when f = Lazy.force coq_xO -> two * loop t
+ | f, [] when f = Lazy.force coq_xH -> one
| _ -> failwith "not a number"
in
match decompose_app t with
- | f, [t] when f = Lazy.force coq_POS -> loop t
- | f, [t] when f = Lazy.force coq_NEG -> - (loop t)
- | f, [] when f = Lazy.force coq_ZERO -> 0
+ | f, [t] when f = Lazy.force coq_Zpos -> loop t
+ | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
+ | f, [] when f = Lazy.force coq_Z0 -> zero
| _ -> failwith "not a number"
type constr_path =
@@ -443,13 +459,11 @@ type constr_path =
let context operation path (t : constr) =
let rec loop i p0 t =
match (p0,kind_of_term t) with
- | (p, Cast (c,t)) -> mkCast (loop i p c,t)
+ | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
| ([], _) -> operation i t
| ((P_APP n :: p), App (f,v)) ->
-(* let f,l = get_applist t in NECESSAIRE ??
- let v' = Array.of_list (f::l) in *)
let v' = Array.copy v in
- v'.(n-1) <- loop i p v'.(n-1); mkApp (f, v')
+ v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v')
| ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
(* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
let v' = Array.copy v in
@@ -462,13 +476,13 @@ let context operation path (t : constr) =
| (p, Fix ((_,n as ln),(tys,lna,v))) ->
let l = Array.length v in
let v' = Array.copy v in
- v'.(n) <- loop (i+l) p v.(n); (mkFix (ln,(tys,lna,v')))
+ v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
| ((P_BODY :: p), Prod (n,t,c)) ->
- (mkProd (n,t,loop (i+1) p c))
+ (mkProd (n,t,loop (succ i) p c))
| ((P_BODY :: p), Lambda (n,t,c)) ->
- (mkLambda (n,t,loop (i+1) p c))
+ (mkLambda (n,t,loop (succ i) p c))
| ((P_BODY :: p), LetIn (n,b,t,c)) ->
- (mkLetIn (n,b,t,loop (i+1) p c))
+ (mkLetIn (n,b,t,loop (succ i) p c))
| ((P_TYPE :: p), Prod (n,t,c)) ->
(mkProd (n,loop i p t,c))
| ((P_TYPE :: p), Lambda (n,t,c)) ->
@@ -476,16 +490,16 @@ let context operation path (t : constr) =
| ((P_TYPE :: p), LetIn (n,b,t,c)) ->
(mkLetIn (n,b,loop i p t,c))
| (p, _) ->
- ppnl (Printer.prterm t);
+ ppnl (Printer.pr_lconstr t);
failwith ("abstract_path " ^ string_of_int(List.length p))
in
loop 1 path t
let occurence path (t : constr) =
let rec loop p0 t = match (p0,kind_of_term t) with
- | (p, Cast (c,t)) -> loop p c
+ | (p, Cast (c,_,_)) -> loop p c
| ([], _) -> t
- | ((P_APP n :: p), App (f,v)) -> loop p v.(n-1)
+ | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n)
| ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
| ((P_ARITY :: p), App (f,_)) -> loop p f
| ((P_ARG :: p), App (f,v)) -> loop p v.(0)
@@ -497,7 +511,7 @@ let occurence path (t : constr) =
| ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
| ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
| (p, _) ->
- ppnl (Printer.prterm t);
+ ppnl (Printer.pr_lconstr t);
failwith ("occurence " ^ string_of_int(List.length p))
in
loop path t
@@ -509,7 +523,7 @@ let abstract_path typ path t =
let focused_simpl path gl =
let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
- convert_concl_no_check newc gl
+ convert_concl_no_check newc DEFAULTcast gl
let focused_simpl path = simpl_time (focused_simpl path)
@@ -518,7 +532,7 @@ type oformula =
| Oinv of oformula
| Otimes of oformula * oformula
| Oatom of identifier
- | Oz of int
+ | Oz of bigint
| Oufo of constr
let rec oprint = function
@@ -530,7 +544,7 @@ let rec oprint = function
print_string "("; oprint t1; print_string "*";
oprint t2; print_string ")"
| Oatom s -> print_string (string_of_id s)
- | Oz i -> print_int i
+ | Oz i -> print_string (string_of_bigint i)
| Oufo f -> print_string "?"
let rec weight = function
@@ -567,7 +581,7 @@ let rec decompile af =
in
loop af.body
-let mkNewMeta () = mkMeta (Clenv.new_meta())
+let mkNewMeta () = mkMeta (Evarutil.new_meta())
let clever_rewrite_base_poly typ p result theorem gl =
let full = pf_concl gl in
@@ -606,7 +620,7 @@ let clever_rewrite p vpath t gl =
let vargs = List.map (fun p -> occurence p occ) vpath in
let t' = applist(t, (vargs @ [abstracted])) in
exact (applist(t',[mkNewMeta()])) gl
-
+
let rec shuffle p (t1,t2) =
match t1,t2 with
| Oplus(l1,r1), Oplus(l2,r2) ->
@@ -614,7 +628,7 @@ let rec shuffle p (t1,t2) =
let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
(clever_rewrite p [[P_APP 1;P_APP 1];
[P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_r)
+ (Lazy.force coq_fast_Zplus_assoc_reverse)
:: tac,
Oplus(l1,t'))
else
@@ -627,12 +641,12 @@ let rec shuffle p (t1,t2) =
if weight l1 > weight t2 then
let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_r)
+ (Lazy.force coq_fast_Zplus_assoc_reverse)
:: tac,
Oplus(l1, t')
else
[clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_sym)],
+ (Lazy.force coq_fast_Zplus_comm)],
Oplus(t2,t1)
| t1,Oplus(l2,r2) ->
if weight l2 > weight t1 then
@@ -643,11 +657,11 @@ let rec shuffle p (t1,t2) =
Oplus(l2,t')
else [],Oplus(t1,t2)
| Oz t1,Oz t2 ->
- [focused_simpl p], Oz(t1+t2)
+ [focused_simpl p], Oz(Bigint.add t1 t2)
| t1,t2 ->
if weight t1 < weight t2 then
[clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_sym)],
+ (Lazy.force coq_fast_Zplus_comm)],
Oplus(t2,t1)
else [],Oplus(t1,t2)
@@ -665,7 +679,7 @@ let rec shuffle_mult p_init k1 e1 k2 e2 =
[P_APP 2; P_APP 2]]
(Lazy.force coq_fast_OMEGA10)
in
- if k1*c1 + k2 * c2 = 0 then
+ if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then
let tac' =
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
(Lazy.force coq_fast_Zred_factor5) in
@@ -722,7 +736,7 @@ let rec shuffle_mult_right p_init e1 k2 e2 =
[P_APP 2; P_APP 2]]
(Lazy.force coq_fast_OMEGA15)
in
- if c1 + k2 * c2 = 0 then
+ if Bigint.add c1 (Bigint.mult k2 c2) =? zero then
let tac' =
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
(Lazy.force coq_fast_Zred_factor5)
@@ -732,7 +746,7 @@ let rec shuffle_mult_right p_init e1 k2 e2 =
else tac :: loop (P_APP 2 :: p) (l1,l2)
else if v1 > v2 then
clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_r) ::
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
loop (P_APP 2 :: p) (l1,l2')
else
clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
@@ -744,7 +758,7 @@ let rec shuffle_mult_right p_init e1 k2 e2 =
loop (P_APP 2 :: p) (l1',l2)
| ({c=c1;v=v1}::l1), [] ->
clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_r) ::
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
loop (P_APP 2 :: p) (l1,[])
| [],({c=c2;v=v2}::l2) ->
clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
@@ -765,7 +779,7 @@ let rec shuffle_cancel p = function
clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2];
[P_APP 2; P_APP 2];
[P_APP 1; P_APP 1; P_APP 2; P_APP 1]]
- (if c1 > 0 then
+ (if c1 >? zero then
(Lazy.force coq_fast_OMEGA13)
else
(Lazy.force coq_fast_OMEGA14))
@@ -777,15 +791,15 @@ let rec scalar p n = function
let tac1,t1' = scalar (P_APP 1 :: p) n t1 and
tac2,t2' = scalar (P_APP 2 :: p) n t2 in
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_plus_distr) ::
+ (Lazy.force coq_fast_Zmult_plus_distr_l) ::
(tac1 @ tac2), Oplus(t1',t2')
| Oinv t ->
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_Zopp_left);
- focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(-n))
+ (Lazy.force coq_fast_Zmult_opp_comm);
+ focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n))
| Otimes(t1,Oz x) ->
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_assoc_r);
+ (Lazy.force coq_fast_Zmult_assoc_reverse);
focused_simpl (P_APP 2 :: p)],
Otimes(t1,Oz (n*x))
| Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
@@ -809,7 +823,7 @@ let rec norm_add p_init =
| [] -> [focused_simpl p_init]
| _:: l ->
clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_r) ::
+ (Lazy.force coq_fast_Zplus_assoc_reverse) ::
loop (P_APP 2 :: p) l
in
loop p_init
@@ -831,31 +845,31 @@ let rec negate p = function
let tac1,t1' = negate (P_APP 1 :: p) t1 and
tac2,t2' = negate (P_APP 2 :: p) t2 in
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
- (Lazy.force coq_fast_Zopp_Zplus) ::
+ (Lazy.force coq_fast_Zopp_plus_distr) ::
(tac1 @ tac2),
Oplus(t1',t2')
| Oinv t ->
- [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_Zopp)], t
+ [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t
| Otimes(t1,Oz x) ->
[clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
- (Lazy.force coq_fast_Zopp_Zmult_r);
- focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (-x))
+ (Lazy.force coq_fast_Zopp_mult_distr_r);
+ focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
| Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
| (Oatom _ as t) ->
- let r = Otimes(t,Oz(-1)) in
- [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_one)], r
- | Oz i -> [focused_simpl p],Oz(-i)
+ let r = Otimes(t,Oz(negone)) in
+ [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
+ | Oz i -> [focused_simpl p],Oz(neg i)
| Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
let rec transform p t =
- let default () =
+ let default isnat t' =
try
- let v,th,_ = find_constr t in
+ let v,th,_ = find_constr t' in
[clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
with _ ->
let v = new_identifier_var ()
and th = new_identifier () in
- hide_constr t v th false;
+ hide_constr t' v th isnat;
[clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
in
try match destructurate_term t with
@@ -870,10 +884,10 @@ let rec transform p t =
(mkApp (Lazy.force coq_Zplus,
[| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
unfold sp_Zminus :: tac,t
- | Kapp(Zs,[t1]) ->
+ | Kapp(Zsucc,[t1]) ->
let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
- [| t1; mk_integer 1 |])) in
- unfold sp_Zs :: tac,t
+ [| t1; mk_integer one |])) in
+ unfold sp_Zsucc :: tac,t
| Kapp(Zmult,[t1;t2]) ->
let tac1,t1' = transform (P_APP 1 :: p) t1
and tac2,t2' = transform (P_APP 2 :: p) t2 in
@@ -882,40 +896,32 @@ let rec transform p t =
| (Oz n,_) ->
let sym =
clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_sym) in
+ (Lazy.force coq_fast_Zmult_comm) in
let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
- | _ -> default ()
+ | _ -> default false t
end
- | Kapp((POS|NEG|ZERO),_) ->
- (try ([],Oz(recognize_number t)) with _ -> default ())
+ | Kapp((Zpos|Zneg|Z0),_) ->
+ (try ([],Oz(recognize_number t)) with _ -> default false t)
| Kvar s -> [],Oatom s
| Kapp(Zopp,[t]) ->
let tac,t' = transform (P_APP 1 :: p) t in
let tac',t'' = negate p t' in
tac @ tac', t''
- | Kapp(Inject_nat,[t']) ->
- begin try
- let v,th,_ = find_constr t' in
- [clever_rewrite_base p (mkVar v) (mkVar th)],Oatom v
- with _ ->
- let v = new_identifier_var () and th = new_identifier () in
- hide_constr t' v th true;
- [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
- end
- | _ -> default ()
- with e when catchable_exception e -> default ()
+ | Kapp(Z_of_nat,[t']) -> default true t'
+ | _ -> default false t
+ with e when catchable_exception e -> default false t
let shrink_pair p f1 f2 =
match f1,f2 with
| Oatom v,Oatom _ ->
- let r = Otimes(Oatom v,Oz 2) in
+ let r = Otimes(Oatom v,Oz two) in
clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r
| Oatom v, Otimes(_,c2) ->
- let r = Otimes(Oatom v,Oplus(c2,Oz 1)) in
+ let r = Otimes(Oatom v,Oplus(c2,Oz one)) in
clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]]
(Lazy.force coq_fast_Zred_factor2), r
| Otimes (v1,c1),Oatom v ->
- let r = Otimes(Oatom v,Oplus(c1,Oz 1)) in
+ let r = Otimes(Oatom v,Oplus(c1,Oz one)) in
clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]]
(Lazy.force coq_fast_Zred_factor3), r
| Otimes (Oatom v,c1),Otimes (v2,c2) ->
@@ -931,13 +937,13 @@ let shrink_pair p f1 f2 =
let reduce_factor p = function
| Oatom v ->
- let r = Otimes(Oatom v,Oz 1) in
+ let r = Otimes(Oatom v,Oz one) in
[clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r
| Otimes(Oatom v,Oz n) as f -> [],f
| Otimes(Oatom v,c) ->
let rec compute = function
| Oz n -> n
- | Oplus(t1,t2) -> compute t1 + compute t2
+ | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
| _ -> error "condense.1"
in
[focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
@@ -950,7 +956,7 @@ let rec condense p = function
let assoc_tac =
clever_rewrite p
[[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_l) in
+ (Lazy.force coq_fast_Zplus_assoc) in
let tac_list,t' = condense p (Oplus(t,r)) in
(assoc_tac :: shrink_tac :: tac_list), t'
end else begin
@@ -958,7 +964,7 @@ let rec condense p = function
let tac',t' = condense (P_APP 2 :: p) t in
(tac @ tac'), Oplus(f,t')
end
- | Oplus(f1,Oz n) as t ->
+ | Oplus(f1,Oz n) ->
let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
| Oplus(f1,f2) ->
if weight f1 = weight f2 then begin
@@ -973,12 +979,12 @@ let rec condense p = function
| Oz _ as t -> [],t
| t ->
let tac,t' = reduce_factor p t in
- let final = Oplus(t',Oz 0) in
+ let final = Oplus(t',Oz zero) in
let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in
tac @ [tac'], final
let rec clear_zero p = function
- | Oplus(Otimes(Oatom v,Oz 0),r) ->
+ | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero ->
let tac =
clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
(Lazy.force coq_fast_Zred_factor5) in
@@ -992,7 +998,7 @@ let replay_history tactic_normalisation =
let aux = id_of_string "auxiliary" in
let aux1 = id_of_string "auxiliary_1" in
let aux2 = id_of_string "auxiliary_2" in
- let zero = mk_integer 0 in
+ let izero = mk_integer zero in
let rec loop t =
match t with
| HYP e :: l ->
@@ -1007,7 +1013,7 @@ let replay_history tactic_normalisation =
and eq2 = decompile e2 in
let id1 = hyp_of_tag e1.id
and id2 = hyp_of_tag e2.id in
- let k = if b then (-1) else 1 in
+ let k = if b then negone else one in
let p_initial = [P_APP 1;P_TYPE] in
let tac= shuffle_mult_right p_initial e1.body k e2.body in
tclTHENLIST [
@@ -1028,11 +1034,10 @@ let replay_history tactic_normalisation =
let p_initial = [P_APP 2;P_TYPE] in
let tac = shuffle_cancel p_initial e1.body in
let solve_le =
- let superieur = Lazy.force coq_SUPERIEUR in
let not_sup_sup = mkApp (build_coq_eq (), [|
- Lazy.force coq_relation;
- Lazy.force coq_SUPERIEUR;
- Lazy.force coq_SUPERIEUR |])
+ Lazy.force coq_comparison;
+ Lazy.force coq_Gt;
+ Lazy.force coq_Gt |])
in
tclTHENS
(tclTHENLIST [
@@ -1070,7 +1075,7 @@ let replay_history tactic_normalisation =
(intros_using [id]);
(cut (mk_gt kk dd)) ])
[ tclTHENS
- (cut (mk_gt kk zero))
+ (cut (mk_gt kk izero))
[ tclTHENLIST [
(intros_using [aux1; aux2]);
(generalize_tac
@@ -1088,20 +1093,16 @@ let replay_history tactic_normalisation =
tclTHEN (mk_then tac) reflexivity ]
| NOT_EXACT_DIVIDE (e1,k) :: l ->
- let id = hyp_of_tag e1.id in
let c = floor_div e1.constant k in
- let d = e1.constant - c * k in
+ let d = Bigint.sub e1.constant (Bigint.mult c k) in
let e2 = {id=e1.id; kind=EQUA;constant = c;
body = map_eq_linear (fun c -> c / k) e1.body } in
- let eq1 = val_of(decompile e1)
- and eq2 = val_of(decompile e2) in
+ let eq2 = val_of(decompile e2) in
let kk = mk_integer k
and dd = mk_integer d in
- let rhs = mk_plus (mk_times eq2 kk) dd in
- let state_eq = mk_eq eq1 rhs in
let tac = scalar_norm_add [P_APP 2] e2.body in
tclTHENS
- (cut (mk_gt dd zero))
+ (cut (mk_gt dd izero))
[ tclTHENS (cut (mk_gt kk dd))
[tclTHENLIST [
(intros_using [aux2;aux1]);
@@ -1147,7 +1148,7 @@ let replay_history tactic_normalisation =
tclTHENS (cut state_eq)
[
tclTHENS
- (cut (mk_gt kk zero))
+ (cut (mk_gt kk izero))
[tclTHENLIST [
(intros_using [aux2;aux1]);
(generalize_tac
@@ -1170,7 +1171,7 @@ let replay_history tactic_normalisation =
and eq2 = val_of (decompile (negate_eq e1)) in
let tac =
clever_rewrite [P_APP 3] [[P_APP 1]]
- (Lazy.force coq_fast_Zopp_one) ::
+ (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
scalar_norm [P_APP 3] e1.body
in
tclTHENS
@@ -1184,13 +1185,13 @@ let replay_history tactic_normalisation =
(loop l) ];
tclTHEN (mk_then tac) reflexivity]
- | STATE(new_eq,def,orig,m,sigma) :: l ->
+ | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
let id = new_identifier ()
and id2 = hyp_of_tag orig.id in
- tag_hypothesis id new_eq.id;
+ tag_hypothesis id e.id;
let eq1 = val_of(decompile def)
and eq2 = val_of(decompile orig) in
- let vid = unintern_id sigma in
+ let vid = unintern_id v in
let theorem =
mkApp (build_coq_ex (), [|
Lazy.force coq_Z;
@@ -1201,12 +1202,11 @@ let replay_history tactic_normalisation =
in
let mm = mk_integer m in
let p_initial = [P_APP 2;P_TYPE] in
- let r = mk_plus eq2 (mk_times (mk_plus (mk_inv (mkVar vid)) eq1) mm) in
let tac =
clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial)
- [[P_APP 1]] (Lazy.force coq_fast_Zopp_one) ::
+ [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
shuffle_mult_right p_initial
- orig.body m ({c= -1;v=sigma}::def.body) in
+ orig.body m ({c= negone;v= v}::def.body) in
tclTHENS
(cut theorem)
[tclTHENLIST [
@@ -1241,7 +1241,7 @@ let replay_history tactic_normalisation =
and id2 = hyp_of_tag e2.id in
let eq1 = val_of(decompile e1)
and eq2 = val_of(decompile e2) in
- if k1 = 1 & e2.kind = EQUA then
+ if k1 =? one & e2.kind = EQUA then
let tac_thm =
match e1.kind with
| EQUA -> Lazy.force coq_OMEGA5
@@ -1264,9 +1264,9 @@ let replay_history tactic_normalisation =
and kk2 = mk_integer k2 in
let p_initial = [P_APP 2;P_TYPE] in
let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
- tclTHENS (cut (mk_gt kk1 zero))
+ tclTHENS (cut (mk_gt kk1 izero))
[tclTHENS
- (cut (mk_gt kk2 zero))
+ (cut (mk_gt kk2 izero))
[tclTHENLIST [
(intros_using [aux2;aux1]);
(generalize_tac
@@ -1345,7 +1345,7 @@ let destructure_omega gl tac_def (id,c) =
normalize_equation
id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
| Kapp(Zlt,[t1;t2]) ->
- let t = mk_plus (mk_plus t2 (mk_integer (-1))) (mk_inv t1) in
+ let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
normalize_equation
id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
| Kapp(Zge,[t1;t2]) ->
@@ -1353,7 +1353,7 @@ let destructure_omega gl tac_def (id,c) =
normalize_equation
id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
| Kapp(Zgt,[t1;t2]) ->
- let t = mk_plus (mk_plus t1 (mk_integer (-1))) (mk_inv t2) in
+ let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
normalize_equation
id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
| _ -> tac_def
@@ -1362,7 +1362,7 @@ let destructure_omega gl tac_def (id,c) =
let reintroduce id =
(* [id] cannot be cleared if dependent: protect it by a try *)
tclTHEN (tclTRY (clear [id])) (intro_using id)
-
+
let coq_omega gl =
clear_tables ();
let tactic_normalisation, system =
@@ -1382,8 +1382,8 @@ let coq_omega gl =
(intros_using [th;id]);
tac ]),
{kind = INEQ;
- body = [{v=intern_id v; c=1}];
- constant = 0; id = i} :: sys
+ body = [{v=intern_id v; c=one}];
+ constant = zero; id = i} :: sys
else
(tclTHENLIST [
(simplest_elim (applist (Lazy.force coq_new_var, [t])));
@@ -1393,17 +1393,19 @@ let coq_omega gl =
(tclIDTAC,[]) (dump_tables ())
in
let system = system @ sys in
- if !display_system_flag then display_system system;
+ if !display_system_flag then display_system display_var system;
if !old_style_flag then begin
- try let _ = simplify false system in tclIDTAC gl
+ try
+ let _ = simplify (new_id,new_var_num,display_var) false system in
+ tclIDTAC gl
with UNSOLVABLE ->
let _,path = depend [] [] (history ()) in
- if !display_action_flag then display_action path;
+ if !display_action_flag then display_action display_var path;
(tclTHEN prelude (replay_history tactic_normalisation path)) gl
end else begin
try
- let path = simplify_strong system in
- if !display_action_flag then display_action path;
+ let path = simplify_strong (new_id,new_var_num,display_var) system in
+ if !display_action_flag then display_action display_var path;
(tclTHEN prelude (replay_history tactic_normalisation path)) gl
with NO_CONTRADICTION -> error "Omega can't solve this system"
end
@@ -1411,8 +1413,6 @@ let coq_omega gl =
let coq_omega = solver_time coq_omega
let nat_inject gl =
- let aux = id_of_string "auxiliary" in
- let table = Hashtbl.create 7 in
let rec explore p t =
try match destructurate_term t with
| Kapp(Plus,[t1;t2]) ->
@@ -1444,7 +1444,7 @@ let nat_inject gl =
(explore (P_APP 1 :: p) t1);
(explore (P_APP 2 :: p) t2) ];
(tclTHEN
- (clever_rewrite_gen p (mk_integer 0)
+ (clever_rewrite_gen p (mk_integer zero)
((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
(loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
]
@@ -1461,7 +1461,7 @@ let nat_inject gl =
Kapp(S,[t]) ->
(tclTHEN
(clever_rewrite_gen p
- (mkApp (Lazy.force coq_Zs, [| mk_inj t |]))
+ (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
((Lazy.force coq_inj_S),[t]))
(loop (P_APP 1 :: p) t))
| _ -> explore p t
@@ -1564,7 +1564,7 @@ let rec decidability gl t =
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
| _ -> errorlabstrm "decidability"
(str "Omega: Can't solve a goal with equality on " ++
- Printer.prterm typ)
+ Printer.pr_lconstr typ)
end
| Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
| Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
@@ -1665,25 +1665,25 @@ let destructure_hyps gl =
| Kapp(Zle, [t1;t2]) ->
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_Zle, [| t1;t2;mkVar i|])]);
+ [mkApp (Lazy.force coq_Znot_le_gt, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Zge, [t1;t2]) ->
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_Zge, [| t1;t2;mkVar i|])]);
+ [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Zlt, [t1;t2]) ->
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_Zlt, [| t1;t2;mkVar i|])]);
+ [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Zgt, [t1;t2]) ->
tclTHENLIST [
(generalize_tac
- [mkApp (Lazy.force coq_not_Zgt, [| t1;t2;mkVar i|])]);
+ [mkApp (Lazy.force coq_Znot_gt_le, [| t1;t2;mkVar i|])]);
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Le, [t1;t2]) ->
@@ -1776,7 +1776,7 @@ let destructure_goal gl =
let destructure_goal = all_time (destructure_goal)
let omega_solver gl =
- Library.check_required_library ["Coq";"omega";"Omega"];
+ Coqlib.check_required_library ["Coq";"omega";"Omega"];
let result = destructure_goal gl in
(* if !display_time_flag then begin text_time ();
flush Pervasives.stdout end; *)
diff --git a/contrib/omega/g_omega.ml4 b/contrib/omega/g_omega.ml4
index 726cf8bc..01592ebe 100644
--- a/contrib/omega/g_omega.ml4
+++ b/contrib/omega/g_omega.ml4
@@ -15,10 +15,10 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_omega.ml4,v 1.1.12.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: g_omega.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
open Coq_omega
-TACTIC EXTEND Omega
- [ "Omega" ] -> [ omega_solver ]
+TACTIC EXTEND omega
+ [ "omega" ] -> [ omega_solver ]
END
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index f0eb1e78..fd774c16 100755..100644
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -11,52 +11,75 @@
(* *)
(* Pierre Crégut (CNET, Lannion, France) *)
(* *)
+(* 13/10/2002 : modified to cope with an external numbering of equations *)
+(* and hypothesis. Its use for Omega is not more complex and it makes *)
+(* things much simpler for the reflexive version where we should limit *)
+(* the number of source of numbering. *)
(**************************************************************************)
-(* $Id: omega.ml,v 1.7.2.2 2005/02/17 18:25:20 herbelin Exp $ *)
-
-open Util
-open Hashtbl
open Names
-let flat_map f =
- let rec flat_map_f = function
- | [] -> []
- | x :: l -> f x @ flat_map_f l
- in
- flat_map_f
-
-let pp i = print_int i; print_newline (); flush stdout
+module type INT = sig
+ type bigint
+ val less_than : bigint -> bigint -> bool
+ val add : bigint -> bigint -> bigint
+ val sub : bigint -> bigint -> bigint
+ val mult : bigint -> bigint -> bigint
+ val euclid : bigint -> bigint -> bigint * bigint
+ val neg : bigint -> bigint
+ val zero : bigint
+ val one : bigint
+ val to_string : bigint -> string
+end
let debug = ref false
-let filter = List.partition
+module MakeOmegaSolver (Int:INT) = struct
+
+type bigint = Int.bigint
+let (<?) = Int.less_than
+let (<=?) x y = Int.less_than x y or x = y
+let (>?) x y = Int.less_than y x
+let (>=?) x y = Int.less_than y x or x = y
+let (=?) = (=)
+let (+) = Int.add
+let (-) = Int.sub
+let ( * ) = Int.mult
+let (/) x y = fst (Int.euclid x y)
+let (mod) x y = snd (Int.euclid x y)
+let zero = Int.zero
+let one = Int.one
+let two = one + one
+let negone = Int.neg one
+let abs x = if Int.less_than x zero then Int.neg x else x
+let string_of_bigint = Int.to_string
+let neg = Int.neg
+
+(* To ensure that polymorphic (<) is not used mistakenly on big integers *)
+(* Warning: do not use (=) either on big int *)
+let (<) = ((<) : int -> int -> bool)
+let (>) = ((>) : int -> int -> bool)
+let (<=) = ((<=) : int -> int -> bool)
+let (>=) = ((>=) : int -> int -> bool)
+
+let pp i = print_int i; print_newline (); flush stdout
let push v l = l := v :: !l
-let rec pgcd x y = if y = 0 then x else pgcd y (x mod y)
+let rec pgcd x y = if y =? zero then x else pgcd y (x mod y)
let pgcd_l = function
| [] -> failwith "pgcd_l"
| x :: l -> List.fold_left pgcd x l
let floor_div a b =
- match a >=0 , b > 0 with
+ match a >=? zero , b >? zero with
| true,true -> a / b
| false,false -> a / b
- | true, false -> (a-1) / b - 1
- | false,true -> (a+1) / b - 1
+ | true, false -> (a-one) / b - one
+ | false,true -> (a+one) / b - one
-let new_id =
- let cpt = ref 0 in fun () -> incr cpt; ! cpt
-
-let new_var =
- let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
-
-let new_var_num =
- let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
-
-type coeff = {c: int ; v: int}
+type coeff = {c: bigint ; v: int}
type linear = coeff list
@@ -70,60 +93,63 @@ type afine = {
(* the variables and their coefficient *)
body: coeff list;
(* a constant *)
- constant: int }
+ constant: bigint }
+
+type state_action = {
+ st_new_eq : afine;
+ st_def : afine;
+ st_orig : afine;
+ st_coef : bigint;
+ st_var : int }
type action =
- | DIVIDE_AND_APPROX of afine * afine * int * int
- | NOT_EXACT_DIVIDE of afine * int
+ | DIVIDE_AND_APPROX of afine * afine * bigint * bigint
+ | NOT_EXACT_DIVIDE of afine * bigint
| FORGET_C of int
- | EXACT_DIVIDE of afine * int
- | SUM of int * (int * afine) * (int * afine)
- | STATE of afine * afine * afine * int * int
+ | EXACT_DIVIDE of afine * bigint
+ | SUM of int * (bigint * afine) * (bigint * afine)
+ | STATE of state_action
| HYP of afine
| FORGET of int * int
| FORGET_I of int * int
| CONTRADICTION of afine * afine
| NEGATE_CONTRADICT of afine * afine * bool
- | MERGE_EQ of int * afine * int
- | CONSTANT_NOT_NUL of int * int
+ | MERGE_EQ of int * afine * int
+ | CONSTANT_NOT_NUL of int * bigint
| CONSTANT_NUL of int
- | CONSTANT_NEG of int * int
+ | CONSTANT_NEG of int * bigint
| SPLIT_INEQ of afine * (int * action list) * (int * action list)
- | WEAKEN of int * int
+ | WEAKEN of int * bigint
exception UNSOLVABLE
exception NO_CONTRADICTION
-let intern_id,unintern_id =
- let cpt = ref 0 in
- let table = create 7 and co_table = create 7 in
- (fun (name : identifier) ->
- try find table name with Not_found ->
- let idx = !cpt in
- add table name idx; add co_table idx name; incr cpt; idx),
- (fun idx ->
- try find co_table idx with Not_found ->
- let v = new_var () in add table v idx; add co_table idx v; v)
-
-let display_eq (l,e) =
+let display_eq print_var (l,e) =
let _ =
List.fold_left
(fun not_first f ->
print_string
- (if f.c < 0 then "- " else if not_first then "+ " else "");
+ (if f.c <? zero then "- " else if not_first then "+ " else "");
let c = abs f.c in
- if c = 1 then
- Printf.printf "%s " (string_of_id (unintern_id f.v))
+ if c =? one then
+ Printf.printf "%s " (print_var f.v)
else
- Printf.printf "%d %s " c (string_of_id (unintern_id f.v));
+ Printf.printf "%s %s " (string_of_bigint c) (print_var f.v);
true)
false l
in
- if e > 0 then
- Printf.printf "+ %d " e
- else if e < 0 then
- Printf.printf "- %d " (abs e)
+ if e >? zero then
+ Printf.printf "+ %s " (string_of_bigint e)
+ else if e <? zero then
+ Printf.printf "- %s " (string_of_bigint (abs e))
+
+let rec trace_length l =
+ let action_length accu = function
+ | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
+ accu + one + trace_length l1 + trace_length l2
+ | _ -> accu + one in
+ List.fold_left action_length zero l
let operator_of_eq = function
| EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
@@ -131,49 +157,51 @@ let operator_of_eq = function
let kind_of = function
| EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
-let display_system l =
+let display_system print_var l =
List.iter
(fun { kind=b; body=e; constant=c; id=id} ->
- print_int id; print_string ": ";
- display_eq (e,c); print_string (operator_of_eq b);
- print_string "0\n")
+ Printf.printf "E%d: " id;
+ display_eq print_var (e,c);
+ Printf.printf "%s 0\n" (operator_of_eq b))
l;
print_string "------------------------\n\n"
-let display_inequations l =
- List.iter (fun e -> display_eq e;print_string ">= 0\n") l;
+let display_inequations print_var l =
+ List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
print_string "------------------------\n\n"
-let rec display_action = function
+let sbi = string_of_bigint
+
+let rec display_action print_var = function
| act :: l -> begin match act with
| DIVIDE_AND_APPROX (e1,e2,k,d) ->
Printf.printf
- "Inequation E%d is divided by %d and the constant coefficient is \
- rounded by substracting %d.\n" e1.id k d
+ "Inequation E%d is divided by %s and the constant coefficient is \
+ rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
| NOT_EXACT_DIVIDE (e,k) ->
Printf.printf
"Constant in equation E%d is not divisible by the pgcd \
- %d of its other coefficients.\n" e.id k
+ %s of its other coefficients.\n" e.id (sbi k)
| EXACT_DIVIDE (e,k) ->
Printf.printf
"Equation E%d is divided by the pgcd \
- %d of its coefficients.\n" e.id k
+ %s of its coefficients.\n" e.id (sbi k)
| WEAKEN (e,k) ->
Printf.printf
"To ensure a solution in the dark shadow \
- the equation E%d is weakened by %d.\n" e k
+ the equation E%d is weakened by %s.\n" e (sbi k)
| SUM (e,(c1,e1),(c2,e2)) ->
Printf.printf
- "We state %s E%d = %d %s E%d + %d %s E%d.\n"
- (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2
+ "We state %s E%d = %s %s E%d + %s %s E%d.\n"
+ (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2)
(kind_of e2.kind) e2.id
- | STATE (e,_,_,x,_) ->
- Printf.printf "We define a new equation %d :" e.id;
- display_eq (e.body,e.constant);
- print_string (operator_of_eq e.kind); print_string " 0\n"
+ | STATE { st_new_eq = e } ->
+ Printf.printf "We define a new equation E%d: " e.id;
+ display_eq print_var (e.body,e.constant);
+ print_string (operator_of_eq e.kind); print_string " 0"
| HYP e ->
- Printf.printf "We define %d :" e.id;
- display_eq (e.body,e.constant);
+ Printf.printf "We define E%d: " e.id;
+ display_eq print_var (e.body,e.constant);
print_string (operator_of_eq e.kind); print_string " 0\n"
| FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e
| FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
@@ -182,33 +210,34 @@ let rec display_action = function
Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
| CONTRADICTION (e1,e2) ->
Printf.printf
- "equations E%d and E%d implie a contradiction on their \
+ "Equations E%d and E%d imply a contradiction on their \
constant factors.\n" e1.id e2.id
| NEGATE_CONTRADICT(e1,e2,b) ->
Printf.printf
- "Eqations E%d and E%d state that their body is at the same time
+ "Equations E%d and E%d state that their body is at the same time
equal and different\n" e1.id e2.id
| CONSTANT_NOT_NUL (e,k) ->
- Printf.printf "equation E%d states %d=0.\n" e k
+ Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
| CONSTANT_NEG(e,k) ->
- Printf.printf "equation E%d states %d >= 0.\n" e k
+ Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k)
| CONSTANT_NUL e ->
- Printf.printf "inequation E%d states 0 != 0.\n" e
+ Printf.printf "Inequation E%d states 0 != 0.\n" e
| SPLIT_INEQ (e,(e1,l1),(e2,l2)) ->
- Printf.printf "equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
- display_action l1;
+ Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
+ display_action print_var l1;
print_newline ();
- display_action l2;
+ display_action print_var l2;
print_newline ()
- end; display_action l
+ end; display_action print_var l
| [] ->
flush stdout
-(*""*)
+let default_print_var v = Printf.sprintf "X%d" v (* For debugging *)
+(*""*)
let add_event, history, clear_history =
let accu = ref [] in
- (fun (v : action) -> if !debug then display_action [v]; push v accu),
+ (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
(fun () -> !accu),
(fun () -> accu := [])
@@ -218,7 +247,7 @@ let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
let map_eq_linear f =
let rec loop = function
- | x :: l -> let c = f x.c in if c=0 then loop l else {v=x.v; c=c} :: loop l
+ | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l
| [] -> []
in
loop
@@ -227,28 +256,28 @@ let map_eq_afine f e =
{ id = e.id; kind = e.kind; body = map_eq_linear f e.body;
constant = f e.constant }
-let negate_eq = map_eq_afine (fun x -> -x)
+let negate_eq = map_eq_afine (fun x -> neg x)
let rec sum p0 p1 = match (p0,p1) with
| ([], l) -> l | (l, []) -> l
| (((x1::l1) as l1'), ((x2::l2) as l2')) ->
if x1.v = x2.v then
let c = x1.c + x2.c in
- if c = 0 then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
+ if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
else if x1.v > x2.v then
x1 :: sum l1 l2'
else
x2 :: sum l1' l2
-let sum_afine eq1 eq2 =
- { kind = eq1.kind; id = new_id ();
+let sum_afine new_eq_id eq1 eq2 =
+ { kind = eq1.kind; id = new_eq_id ();
body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
exception FACTOR1
let rec chop_factor_1 = function
| x :: l ->
- if abs x.c = 1 then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
+ if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
| [] -> raise FACTOR1
exception CHOPVAR
@@ -261,24 +290,24 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
if e = [] then begin
match eq_flag with
| EQUA ->
- if x =0 then [] else begin
+ if x =? zero then [] else begin
add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
end
| DISE ->
- if x <> 0 then [] else begin
+ if x <> zero then [] else begin
add_event (CONSTANT_NUL id); raise UNSOLVABLE
end
| INEQ ->
- if x >= 0 then [] else begin
+ if x >=? zero then [] else begin
add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
end
end else
let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
- if eq_flag=EQUA & x mod gcd <> 0 then begin
+ if eq_flag=EQUA & x mod gcd <> zero then begin
add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
- end else if eq_flag=DISE & x mod gcd <> 0 then begin
+ end else if eq_flag=DISE & x mod gcd <> zero then begin
add_event (FORGET_C eq.id); []
- end else if gcd <> 1 then begin
+ end else if gcd <> one then begin
let c = floor_div x gcd in
let d = x - c * gcd in
let new_eq = {id=id; kind=eq_flag; constant=c;
@@ -288,97 +317,107 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
[new_eq]
end else [eq]
-let eliminate_with_in {v=v;c=c_unite} eq2
+let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
({body=e1; constant=c1} as eq1) =
try
let (f,_) = chop_var v e1 in
- let coeff = if c_unite=1 then -f.c else if c_unite= -1 then f.c
+ let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c
else failwith "eliminate_with_in" in
- let res = sum_afine eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
- add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res
+ let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
+ add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res
with CHOPVAR -> eq1
-let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b)
-let banerjee_step original l1 l2 =
+let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
+let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
let e = original.body in
- let sigma = new_var_num () in
+ let sigma = new_var_id () in
let smallest,var =
try
- List.fold_left (fun (v,p) c -> if v > (abs c.c) then abs c.c,c.v else (v,p))
+ List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
(abs (List.hd e).c, (List.hd e).v) (List.tl e)
- with Failure "tl" -> display_system [original] ; failwith "TL" in
- let m = smallest + 1 in
+ with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+ let m = smallest + one in
let new_eq =
{ constant = omega_mod original.constant m;
- body = {c= -m;v=sigma} ::
+ body = {c= neg m;v=sigma} ::
map_eq_linear (fun a -> omega_mod a m) original.body;
- id = new_id (); kind = EQUA } in
+ id = new_eq_id (); kind = EQUA } in
let definition =
- { constant = - floor_div (2 * original.constant + m) (2 * m);
- body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m))
+ { constant = neg (floor_div (two * original.constant + m) (two * m));
+ body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m)))
original.body;
- id = new_id (); kind = EQUA } in
- add_event (STATE (new_eq,definition,original,m,sigma));
+ id = new_eq_id (); kind = EQUA } in
+ add_event (STATE {st_new_eq = new_eq; st_def = definition;
+ st_orig = original; st_coef = m; st_var = sigma});
let new_eq = List.hd (normalize new_eq) in
let eliminated_var, def = chop_var var new_eq.body in
let other_equations =
- flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e))
- l1 in
+ Util.list_map_append
+ (fun e ->
+ normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in
let inequations =
- flat_map (fun e -> normalize (eliminate_with_in eliminated_var new_eq e))
- l2 in
- let original' = eliminate_with_in eliminated_var new_eq original in
+ Util.list_map_append
+ (fun e ->
+ normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in
+ let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
let mod_original = map_eq_afine (fun c -> c / m) original' in
add_event (EXACT_DIVIDE (original',m));
List.hd (normalize mod_original),other_equations,inequations
-let rec eliminate_one_equation (e,other,ineqs) =
- if !debug then display_system (e::other);
+let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) =
+ if !debug then display_system print_var (e::other);
try
let v,def = chop_factor_1 e.body in
- (flat_map (fun e' -> normalize (eliminate_with_in v e e')) other,
- flat_map (fun e' -> normalize (eliminate_with_in v e e')) ineqs)
- with FACTOR1 -> eliminate_one_equation (banerjee_step e other ineqs)
-
-let rec banerjee (sys_eq,sys_ineq) =
+ (Util.list_map_append
+ (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
+ Util.list_map_append
+ (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
+ with FACTOR1 ->
+ eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
+
+let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
let rec fst_eq_1 = function
(eq::l) ->
- if List.exists (fun x -> abs x.c = 1) eq.body then eq,l
+ if List.exists (fun x -> abs x.c =? one) eq.body then eq,l
else let (eq',l') = fst_eq_1 l in (eq',eq::l')
| [] -> raise Not_found in
match sys_eq with
- [] -> if !debug then display_system sys_ineq; sys_ineq
+ [] -> if !debug then display_system print_var sys_ineq; sys_ineq
| (e1::rest) ->
let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
if eq.body = [] then
- if eq.constant = 0 then begin
- add_event (FORGET_C eq.id); banerjee (other,sys_ineq)
+ if eq.constant =? zero then begin
+ add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
end else begin
add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
end
- else banerjee (eliminate_one_equation (eq,other,sys_ineq))
+ else
+ banerjee new_ids
+ (eliminate_one_equation new_ids (eq,other,sys_ineq))
+
type kind = INVERTED | NORMAL
-let redundancy_elimination system =
+
+let redundancy_elimination new_eq_id system =
let normal = function
- ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED
+ ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
| e -> e,NORMAL in
- let table = create 7 in
+ let table = Hashtbl.create 7 in
List.iter
(fun e ->
let ({body=ne} as nx) ,kind = normal e in
if ne = [] then
- if nx.constant < 0 then begin
+ if nx.constant <? zero then begin
add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
end else add_event (FORGET_C nx.id)
else
try
- let (optnormal,optinvert) = find table ne in
+ let (optnormal,optinvert) = Hashtbl.find table ne in
let final =
if kind = NORMAL then begin
match optnormal with
Some v ->
let kept =
- if v.constant < nx.constant
+ if v.constant <? nx.constant
then begin add_event (FORGET (v.id,nx.id));v end
else begin add_event (FORGET (nx.id,v.id));nx end in
(Some(kept),optinvert)
@@ -386,32 +425,32 @@ let redundancy_elimination system =
end else begin
match optinvert with
Some v ->
- let kept =
- if v.constant > nx.constant
+ let _kept =
+ if v.constant >? nx.constant
then begin add_event (FORGET_I (v.id,nx.id));v end
else begin add_event (FORGET_I (nx.id,v.id));nx end in
- (optnormal,Some(if v.constant > nx.constant then v else nx))
+ (optnormal,Some(if v.constant >? nx.constant then v else nx))
| None -> optnormal,Some nx
end in
begin match final with
(Some high, Some low) ->
- if high.constant < low.constant then begin
+ if high.constant <? low.constant then begin
add_event(CONTRADICTION (high,negate_eq low));
raise UNSOLVABLE
end
| _ -> () end;
- remove table ne;
- add table ne final
+ Hashtbl.remove table ne;
+ Hashtbl.add table ne final
with Not_found ->
- add table ne
+ Hashtbl.add table ne
(if kind = NORMAL then (Some nx,None) else (None,Some nx)))
system;
let accu_eq = ref [] in
let accu_ineq = ref [] in
- iter
+ Hashtbl.iter
(fun p0 p1 -> match (p0,p1) with
- | (e, (Some x, Some y)) when x.constant = y.constant ->
- let id=new_id () in
+ | (e, (Some x, Some y)) when x.constant =? y.constant ->
+ let id=new_eq_id () in
add_event (MERGE_EQ(id,x,y.id));
push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
| (e, (optnorm,optinvert)) ->
@@ -425,17 +464,17 @@ let redundancy_elimination system =
exception SOLVED_SYSTEM
let select_variable system =
- let table = create 7 in
+ let table = Hashtbl.create 7 in
let push v c=
- try let r = find table v in r := max !r (abs c)
- with Not_found -> add table v (ref (abs c)) in
+ try let r = Hashtbl.find table v in r := max !r (abs c)
+ with Not_found -> Hashtbl.add table v (ref (abs c)) in
List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
- let vmin,cmin = ref (-1), ref 0 in
+ let vmin,cmin = ref (-1), ref zero in
let var_cpt = ref 0 in
- iter
+ Hashtbl.iter
(fun v ({contents = c}) ->
incr var_cpt;
- if c < !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
+ if c <? !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
table;
if !var_cpt < 1 then raise SOLVED_SYSTEM;
!vmin
@@ -444,25 +483,25 @@ let classify v system =
List.fold_left
(fun (not_occ,below,over) eq ->
try let f,eq' = chop_var v eq.body in
- if f.c >= 0 then (not_occ,((f.c,eq) :: below),over)
- else (not_occ,below,((-f.c,eq) :: over))
+ if f.c >=? zero then (not_occ,((f.c,eq) :: below),over)
+ else (not_occ,below,((neg f.c,eq) :: over))
with CHOPVAR -> (eq::not_occ,below,over))
([],[],[]) system
-let product dark_shadow low high =
+let product new_eq_id dark_shadow low high =
List.fold_left
(fun accu (a,eq1) ->
List.fold_left
(fun accu (b,eq2) ->
let eq =
- sum_afine (map_eq_afine (fun c -> c * b) eq1)
+ sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
(map_eq_afine (fun c -> c * a) eq2) in
add_event(SUM(eq.id,(b,eq1),(a,eq2)));
match normalize eq with
| [eq] ->
let final_eq =
if dark_shadow then
- let delta = (a - 1) * (b - 1) in
+ let delta = (a - one) * (b - one) in
add_event(WEAKEN(eq.id,delta));
{id = eq.id; kind=INEQ; body = eq.body;
constant = eq.constant - delta}
@@ -473,33 +512,34 @@ let product dark_shadow low high =
accu high)
[] low
-let fourier_motzkin dark_shadow system =
+let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system =
let v = select_variable system in
let (ineq_out, ineq_low,ineq_high) = classify v system in
- let expanded = ineq_out @ product dark_shadow ineq_low ineq_high in
- if !debug then display_system expanded; expanded
+ let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
+ if !debug then display_system print_var expanded; expanded
-let simplify dark_shadow system =
+let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
if List.exists (fun e -> e.kind = DISE) system then
failwith "disequation in simplify";
clear_history ();
List.iter (fun e -> add_event (HYP e)) system;
- let system = flat_map normalize system in
- let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
- let simp_eq,simp_ineq = redundancy_elimination ineqs in
+ let system = Util.list_map_append normalize system in
+ let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
let system = (eqs @ simp_eq,simp_ineq) in
let rec loop1a system =
- let sys_ineq = banerjee system in
+ let sys_ineq = banerjee new_ids system in
loop1b sys_ineq
and loop1b sys_ineq =
- let simp_eq,simp_ineq = redundancy_elimination sys_ineq in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq)
in
let rec loop2 system =
try
- let expanded = fourier_motzkin dark_shadow system in
+ let expanded = fourier_motzkin new_ids dark_shadow system in
loop2 (loop1b expanded)
- with SOLVED_SYSTEM -> if !debug then display_system system; system
+ with SOLVED_SYSTEM ->
+ if !debug then display_system print_var system; system
in
loop2 (loop1a system)
@@ -520,11 +560,9 @@ let rec depend relie_on accu = function
depend (e1.id::e2.id::relie_on) (act::accu) l
else
depend relie_on accu l
- | STATE (e,_,o,_,_) ->
- if List.mem e.id relie_on then
- depend (o.id::relie_on) (act::accu) l
- else
- depend relie_on accu l
+ | STATE {st_new_eq=e;st_orig=o} ->
+ if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
+ else depend relie_on accu l
| HYP e ->
if List.mem e.id relie_on then depend relie_on (act::accu) l
else depend relie_on accu l
@@ -548,59 +586,68 @@ let rec depend relie_on accu = function
end
| [] -> relie_on, accu
-let solve system =
- try let _ = simplify false system in failwith "no contradiction"
- with UNSOLVABLE -> display_action (snd (depend [] [] (history ())))
+(*
+let depend relie_on accu trace =
+ Printf.printf "Longueur de la trace initiale : %d\n"
+ (trace_length trace + trace_length accu);
+ let rel',trace' = depend relie_on accu trace in
+ Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
+ rel',trace'
+*)
+
+let solve (new_eq_id,new_eq_var,print_var) system =
+ try let _ = simplify new_eq_id false system in failwith "no contradiction"
+ with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
let negation (eqs,ineqs) =
- let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in
+ let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
let normal = function
- | ({body=f::_} as e) when f.c < 0 -> negate_eq e, INVERTED
+ | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
| e -> e,NORMAL in
- let table = create 7 in
+ let table = Hashtbl.create 7 in
List.iter (fun e ->
let {body=ne;constant=c} ,kind = normal e in
- add table (ne,c) (kind,e)) diseq;
+ Hashtbl.add table (ne,c) (kind,e)) diseq;
List.iter (fun e ->
- if e.kind <> EQUA then pp 9999;
+ assert (e.kind = EQUA);
let {body=ne;constant=c},kind = normal e in
try
- let (kind',e') = find table (ne,c) in
+ let (kind',e') = Hashtbl.find table (ne,c) in
add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
raise UNSOLVABLE
with Not_found -> ()) eqs
exception FULL_SOLUTION of action list * int list
-let simplify_strong system =
+let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
clear_history ();
List.iter (fun e -> add_event (HYP e)) system;
(* Initial simplification phase *)
let rec loop1a system =
negation system;
- let sys_ineq = banerjee system in
+ let sys_ineq = banerjee new_ids system in
loop1b sys_ineq
and loop1b sys_ineq =
- let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in
- let simp_eq,simp_ineq = redundancy_elimination ine in
+ let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
if simp_eq = [] then dise @ simp_ineq
else loop1a (simp_eq,dise @ simp_ineq)
in
let rec loop2 system =
try
- let expanded = fourier_motzkin false system in
+ let expanded = fourier_motzkin new_ids false system in
loop2 (loop1b expanded)
- with SOLVED_SYSTEM -> if !debug then display_system system; system
+ with SOLVED_SYSTEM -> if !debug then display_system print_var system; system
in
let rec explode_diseq = function
| (de::diseq,ineqs,expl_map) ->
- let id1 = new_id ()
- and id2 = new_id () in
+ let id1 = new_eq_id ()
+ and id2 = new_eq_id () in
let e1 =
- {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in
+ {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in
let e2 =
- {id = id2; kind=INEQ; body = map_eq_linear (fun x -> -x) de.body;
- constant = - de.constant - 1} in
+ {id = id2; kind=INEQ; body = map_eq_linear neg de.body;
+ constant = neg de.constant - one} in
let new_sys =
List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys))
ineqs @
@@ -611,13 +658,13 @@ let simplify_strong system =
| ([],ineqs,expl_map) -> ineqs,expl_map
in
try
- let system = flat_map normalize system in
- let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
- let dise,ine = filter (fun e -> e.kind = DISE) ineqs in
- let simp_eq,simp_ineq = redundancy_elimination ine in
+ let system = Util.list_map_append normalize system in
+ let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+ let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in
+ let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
let system = (eqs @ simp_eq,simp_ineq @ dise) in
let system' = loop1a system in
- let diseq,ineq = filter (fun e -> e.kind = DISE) system' in
+ let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in
let first_segment = history () in
let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
let all_solutions =
@@ -627,20 +674,21 @@ let simplify_strong system =
try let _ = loop2 sys in raise NO_CONTRADICTION
with UNSOLVABLE ->
let relie_on,path = depend [] [] (history ()) in
- let dc,_ = filter (fun (_,id,_) -> List.mem id relie_on) decomp in
+ let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in
let red = List.map (fun (x,_,_) -> x) dc in
(red,relie_on,decomp,path))
sys_exploded
in
let max_count sys =
- let tbl = create 7 in
+ let tbl = Hashtbl.create 7 in
let augment x =
- try incr (find tbl x) with Not_found -> add tbl x (ref 1) in
+ try incr (Hashtbl.find tbl x)
+ with Not_found -> Hashtbl.add tbl x (ref 1) in
let eq = ref (-1) and c = ref 0 in
List.iter (function
| ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
| (l,_,_,_) -> List.iter augment l) sys;
- iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
+ Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
!eq
in
let rec solve systems =
@@ -649,17 +697,20 @@ let simplify_strong system =
let rec sign = function
| ((id',_,b)::l) -> if id=id' then b else sign l
| [] -> failwith "solve" in
- let s1,s2 = filter (fun (_,_,decomp,_) -> sign decomp) systems in
+ let s1,s2 =
+ List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
let s1' =
- List.map (fun (dep,ro,dc,pa) -> (list_except id dep,ro,dc,pa)) s1 in
+ List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
let s2' =
- List.map (fun (dep,ro,dc,pa) -> (list_except id dep,ro,dc,pa)) s2 in
+ List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
let (r1,relie1) = solve s1'
and (r2,relie2) = solve s2' in
let (eq,id1,id2) = List.assoc id explode_map in
- [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: list_union relie1 relie2
+ [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
with FULL_SOLUTION (x0,x1) -> (x0,x1)
in
let act,relie_on = solve all_solutions in
snd(depend relie_on act first_segment)
with UNSOLVABLE -> snd (depend [] [] (history ()))
+
+end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 20:54:23 +0000