diff options
Diffstat (limited to 'contrib/omega')
| -rw-r--r--[-rwxr-xr-x] | contrib/omega/Omega.v | 2 | ||||
| -rw-r--r-- | contrib/omega/OmegaLemmas.v | 202 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 344 | ||||
| -rw-r--r-- | contrib/omega/g_omega.ml4 | 6 | ||||
| -rw-r--r--[-rwxr-xr-x] | contrib/omega/omega.ml | 469 |
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 |