diff options
author | 2011-05-09 08:12:59 +0000 | |
---|---|---|
committer | 2011-05-09 08:12:59 +0000 | |
commit | b3ebb256717364d6d6ed631cd7830e46a8ab6863 (patch) | |
tree | b9948c4abfe44c39e8e192c3b23f7fe61aa5ec3a | |
parent | f8f2e9b68b8b97d0ae85b93bbb395f637cce105b (diff) |
Improved lia + experimental nlia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | plugins/micromega/MExtraction.v | 4 | ||||
-rw-r--r-- | plugins/micromega/Psatz.v | 9 | ||||
-rw-r--r-- | plugins/micromega/QMicromega.v | 12 | ||||
-rw-r--r-- | plugins/micromega/RMicromega.v | 12 | ||||
-rw-r--r-- | plugins/micromega/RingMicromega.v | 106 | ||||
-rw-r--r-- | plugins/micromega/Tauto.v | 213 | ||||
-rw-r--r-- | plugins/micromega/ZMicromega.v | 316 | ||||
-rw-r--r-- | plugins/micromega/certificate.ml | 1236 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 197 | ||||
-rw-r--r-- | plugins/micromega/csdpcert.ml | 2 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 5 | ||||
-rw-r--r-- | plugins/micromega/mfourier.ml | 179 | ||||
-rw-r--r-- | plugins/micromega/micromega.ml | 2064 | ||||
-rw-r--r-- | plugins/micromega/micromega.mli | 214 | ||||
-rw-r--r-- | plugins/micromega/micromega_plugin.mllib | 1 | ||||
-rw-r--r-- | plugins/micromega/mutils.ml | 36 | ||||
-rw-r--r-- | plugins/micromega/polynomial.ml | 735 |
17 files changed, 3461 insertions, 1880 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 5e03d5b24..9b55eea45 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -23,7 +23,7 @@ Require Import NArith. Require Import QArith. Extract Inductive prod => "( * )" [ "(,)" ]. -Extract Inductive List.list => list [ "[]" "(::)" ]. +Extract Inductive list => list [ "[]" "(::)" ]. Extract Inductive bool => bool [ true false ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive option => option [ Some None ]. @@ -41,7 +41,7 @@ Extract Inlined Constant andb => "(&&)". Extraction "micromega.ml" List.map simpl_cone (*map_cone indexes*) denorm Qpower - n_of_Z Nnat.N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + n_of_Z N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index c2c7de703..39c98bc5d 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -18,7 +18,7 @@ Require Import RMicromega. Require Import QArith. Require Export Ring_normalize. Require Import ZArith. -Require Import Raxioms. +Require Import Rdefinitions. Require Export RingMicromega. Require Import VarMap. Require Tauto. @@ -81,6 +81,13 @@ Ltac lia := change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. +Ltac nlia := + xnlia ; + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index e0056c5fa..f64504a54 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -173,8 +173,15 @@ Require Import Tauto. Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. +Definition qunsat := check_inconsistent 0 Qeq_bool Qle_bool. + +Definition qdeduce := nformula_plus_nformula 0 Qplus Qeq_bool. + + + Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := @tauto_checker (Formula Q) (NFormula Q) + qunsat qdeduce Qnormalise Qnegate QWitness QWeakChecker f w. @@ -186,6 +193,11 @@ Proof. unfold QTautoChecker. apply (tauto_checker_sound Qeval_formula Qeval_nformula). apply Qeval_nformula_dec. + intros until env. + unfold eval_nformula. unfold RingMicromega.eval_nformula. + destruct t. + apply (check_inconsistent_sound Qsor QSORaddon) ; auto. + unfold qdeduce. apply (nformula_plus_nformula_correct Qsor QSORaddon). intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_normalise_correct Qsor QSORaddon). intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now apply (cnf_negate_correct Qsor QSORaddon). intros t w0. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 3f29a4fcf..406b4ba25 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -158,8 +158,15 @@ Require Import Tauto. Definition Rnormalise := @cnf_normalise Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. Definition Rnegate := @cnf_negate Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. +Definition runsat := check_inconsistent 0%Z Zeq_bool Zle_bool. + +Definition rdeduce := nformula_plus_nformula 0%Z Zplus Zeq_bool. + + + Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness) : bool := @tauto_checker (Formula Z) (NFormula Z) + runsat rdeduce Rnormalise Rnegate RWitness RWeakChecker f w. @@ -169,6 +176,11 @@ Proof. unfold RTautoChecker. apply (tauto_checker_sound Reval_formula Reval_nformula). apply Reval_nformula_dec. + intros until env. + unfold eval_nformula. unfold RingMicromega.eval_nformula. + destruct t. + apply (check_inconsistent_sound Rsor RZSORaddon) ; auto. + unfold rdeduce. apply (nformula_plus_nformula_correct Rsor RZSORaddon). intros. rewrite Reval_formula_compat. unfold Reval_formula'. now apply (cnf_normalise_correct Rsor RZSORaddon). intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor RZSORaddon). diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 4dc65f9cc..e658ad237 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -355,6 +355,7 @@ Fixpoint eval_Psatz (l : list NFormula) (e : Psatz) {struct e} : option NFormula | PsatzZ => Some (Pc cO, Equal) (* Just to make life easier *) end. + Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFormula), eval_nformula env f -> pexpr_times_nformula e f = Some f' -> eval_nformula env f'. @@ -490,6 +491,99 @@ Fixpoint xhyps_of_psatz (base:nat) (acc : list nat) (prf : Psatz) : list nat := | PsatzIn n => if ge_bool n base then (n::acc) else acc end. +Fixpoint nhyps_of_psatz (prf : Psatz) : list nat := + match prf with + | PsatzC _ | PsatzZ | PsatzSquare _ => nil + | PsatzMulC _ prf => nhyps_of_psatz prf + | PsatzAdd e1 e2 | PsatzMulE e1 e2 => nhyps_of_psatz e1 ++ nhyps_of_psatz e2 + | PsatzIn n => n :: nil + end. + + +Fixpoint extract_hyps (l: list NFormula) (ln : list nat) : list NFormula := + match ln with + | nil => nil + | n::ln => nth n l (Pc cO, Equal) :: extract_hyps l ln + end. + +Lemma extract_hyps_app : forall l ln1 ln2, + extract_hyps l (ln1 ++ ln2) = (extract_hyps l ln1) ++ (extract_hyps l ln2). +Proof. + induction ln1. + reflexivity. + simpl. + intros. + rewrite IHln1. reflexivity. +Qed. + +Ltac inv H := inversion H ; try subst ; clear H. + +Lemma nhyps_of_psatz_correct : forall (env : PolEnv) (e:Psatz) (l : list NFormula) (f: NFormula), + eval_Psatz l e = Some f -> + ((forall f', In f' (extract_hyps l (nhyps_of_psatz e)) -> eval_nformula env f') -> eval_nformula env f). +Proof. + induction e ; intros. + (*PsatzIn*) + simpl in *. + apply H0. intuition congruence. + (* PsatzSquare *) + simpl in *. + inv H. + simpl. + unfold eval_pol. + rewrite (Psquare_ok sor.(SORsetoid) Rops_wd + (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)); + now apply (Rtimes_square_nonneg sor). + (* PsatzMulC *) + simpl in *. + case_eq (eval_Psatz l e). + intros. rewrite H1 in H. simpl in H. + apply pexpr_times_nformula_correct with (2:= H). + apply IHe with (1:= H1); auto. + intros. rewrite H1 in H. simpl in H ; discriminate. + (* PsatzMulE *) + simpl in *. + revert H. + case_eq (eval_Psatz l e1). + case_eq (eval_Psatz l e2) ; simpl ; intros. + apply nformula_times_nformula_correct with (3:= H2). + apply IHe1 with (1:= H1) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + apply IHe2 with (1:= H) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + discriminate. simpl. discriminate. + (* PsatzAdd *) + simpl in *. + revert H. + case_eq (eval_Psatz l e1). + case_eq (eval_Psatz l e2) ; simpl ; intros. + apply nformula_plus_nformula_correct with (3:= H2). + apply IHe1 with (1:= H1) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + apply IHe2 with (1:= H) ; auto. + intros. apply H0. rewrite extract_hyps_app. + apply in_or_app. tauto. + discriminate. simpl. discriminate. + (* PsatzC *) + simpl in H. + case_eq (cO [<] c). + intros. rewrite H1 in H. inv H. + unfold eval_nformula. simpl. + rewrite <- addon.(SORrm).(morph0). now apply cltb_sound. + intros. rewrite H1 in H. discriminate. + (* PsatzZ *) + simpl in *. inv H. + unfold eval_nformula. simpl. + apply addon.(SORrm).(morph0). +Qed. + + + + + (* roughly speaking, normalise_pexpr_correct is a proof of forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *) @@ -546,6 +640,7 @@ apply cleb_sound in H1. now apply -> (Rle_ngt sor). apply cltb_sound in H1. now apply -> (Rlt_nge sor). Qed. + Definition check_normalised_formulas : list NFormula -> Psatz -> bool := fun l cm => match eval_Psatz l cm with @@ -602,6 +697,7 @@ Definition eval_formula (env : PolEnv) (f : Formula) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs). + (* We normalize Formulas by moving terms to one side *) Definition norm := norm_aux cO cI cplus ctimes cminus copp ceqb. @@ -687,7 +783,7 @@ rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). Qed. -(** Another normalistion - this is used for cnf conversion **) +(** Another normalisation - this is used for cnf conversion **) Definition xnormalise (t:Formula) : list (NFormula) := let (lhs,o,rhs) := t in @@ -711,10 +807,10 @@ Definition cnf_normalise (t:Formula) : cnf (NFormula) := Add Ring SORRing : sor.(SORrt). -Lemma cnf_normalise_correct : forall env t, eval_cnf (eval_nformula env) (cnf_normalise t) -> eval_formula env t. +Lemma cnf_normalise_correct : forall env t, eval_cnf eval_nformula env (cnf_normalise t) -> eval_formula env t. Proof. unfold cnf_normalise, xnormalise ; simpl ; intros env t. - unfold eval_cnf. + unfold eval_cnf, eval_clause. destruct t as [lhs o rhs]; case_eq o ; simpl; repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; generalize (eval_pexpr env lhs); @@ -746,10 +842,10 @@ Definition xnegate (t:Formula) : list (NFormula) := Definition cnf_negate (t:Formula) : cnf (NFormula) := List.map (fun x => x::nil) (xnegate t). -Lemma cnf_negate_correct : forall env t, eval_cnf (eval_nformula env) (cnf_negate t) -> ~ eval_formula env t. +Lemma cnf_negate_correct : forall env t, eval_cnf eval_nformula env (cnf_negate t) -> ~ eval_formula env t. Proof. unfold cnf_negate, xnegate ; simpl ; intros env t. - unfold eval_cnf. + unfold eval_cnf, eval_clause. destruct t as [lhs o rhs]; case_eq o ; simpl; repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; generalize (eval_pexpr env lhs); diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index fcbf7f969..ed7a104e8 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-20011 *) (* *) (************************************************************************) @@ -64,6 +64,15 @@ Set Implicit Arguments. Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). + Variable unsat : Term' -> bool. + + Variable unsat_prop : forall t, unsat t = true -> + forall env, eval' env t -> False. + + Variable deduce : Term' -> Term' -> option Term'. + + Variable deduce_prop : forall env t t' u, + eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u. Definition clause := list Term'. Definition cnf := list clause. @@ -76,8 +85,48 @@ Set Implicit Arguments. Definition ff : cnf := cons (@nil Term') nil. + Fixpoint add_term (t: Term') (cl : clause) : option clause := + match cl with + | nil => + match deduce t t with + | None => Some (t ::nil) + | Some u => if unsat u then None else Some (t::nil) + end + | t'::cl => + match deduce t t' with + | None => + match add_term t cl with + | None => None + | Some cl' => Some (t' :: cl') + end + | Some u => + if unsat u then None else + match add_term t cl with + | None => None + | Some cl' => Some (t' :: cl') + end + end + end. + + Fixpoint or_clause (cl1 cl2 : clause) : option clause := + match cl1 with + | nil => Some cl2 + | t::cl => match add_term t cl2 with + | None => None + | Some cl' => or_clause cl cl' + end + end. + +(* Definition or_clause_cnf (t:clause) (f:cnf) : cnf := + List.map (fun x => (t++x)) f. *) + Definition or_clause_cnf (t:clause) (f:cnf) : cnf := - List.map (fun x => (t++x)) f. + List.fold_right (fun e acc => + match or_clause t e with + | None => acc + | Some cl => cl :: acc + end) nil f. + Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf := match f with @@ -102,46 +151,154 @@ Set Implicit Arguments. | I e1 e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2) end. - Definition eval_cnf (env : Term' -> Prop) (f:cnf) := make_conj (fun cl => ~ make_conj env cl) f. + Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval' env) cl. + + Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f. + + + Lemma eval_cnf_app : forall env x y, eval_cnf env (x++y) -> eval_cnf env x /\ eval_cnf env y. + Proof. + unfold eval_cnf. + intros. + rewrite make_conj_app in H ; auto. + Qed. - Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x++y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y. + Definition eval_opt_clause (env : Env) (cl: option clause) := + match cl with + | None => True + | Some cl => eval_clause env cl + end. + + + Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) -> eval_clause env (t::cl). + Proof. + induction cl. + (* BC *) + simpl. + case_eq (deduce t t) ; auto. + intros until 0. + case_eq (unsat t0) ; auto. + unfold eval_clause. + rewrite make_conj_cons. + intros. intro. + apply unsat_prop with (1:= H) (env := env). + apply deduce_prop with (3:= H0) ; tauto. + (* IC *) + simpl. + case_eq (deduce t a). + intro u. + case_eq (unsat u). + simpl. intros. + unfold eval_clause. + intro. + apply unsat_prop with (1:= H) (env:= env). + repeat rewrite make_conj_cons in H2. + apply deduce_prop with (3:= H0); tauto. + intro. + case_eq (add_term t cl) ; intros. + simpl in H2. + rewrite H0 in IHcl. + simpl in IHcl. + unfold eval_clause in *. + intros. + repeat rewrite make_conj_cons in *. + tauto. + rewrite H0 in IHcl ; simpl in *. + unfold eval_clause in *. + intros. + repeat rewrite make_conj_cons in *. + tauto. + case_eq (add_term t cl) ; intros. + simpl in H1. + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + rewrite H in IHcl. + simpl in IHcl. + tauto. + simpl in *. + rewrite H in IHcl. + simpl in IHcl. + unfold eval_clause in *. + repeat rewrite make_conj_cons in *. + tauto. + Qed. + + + Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') -> eval_clause env cl \/ eval_clause env cl'. Proof. - unfold eval_cnf. + induction cl. + simpl. tauto. + intros until 0. + simpl. + assert (HH := add_term_correct env a cl'). + case_eq (add_term a cl'). + simpl in *. + intros. + apply IHcl in H0. + rewrite H in HH. + simpl in HH. + unfold eval_clause in *. + destruct H0. + repeat rewrite make_conj_cons in *. + tauto. + apply HH in H0. + apply not_make_conj_cons in H0 ; auto. + repeat rewrite make_conj_cons in *. + tauto. + simpl. intros. - rewrite make_conj_app in H ; auto. + rewrite H in HH. + simpl in HH. + unfold eval_clause in *. + assert (HH' := HH Coq.Init.Logic.I). + apply not_make_conj_cons in HH'; auto. + repeat rewrite make_conj_cons in *. + tauto. Qed. + - - Lemma or_clause_correct : forall env t f, eval_cnf (eval' env) (or_clause_cnf t f) -> (~ make_conj (eval' env) t) \/ (eval_cnf (eval' env) f). + Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) -> (eval_clause env t) \/ (eval_cnf env f). Proof. unfold eval_cnf. unfold or_clause_cnf. + intros until t. + set (F := (fun (e : clause) (acc : list clause) => + match or_clause t e with + | Some cl => cl :: acc + | None => acc + end)). induction f. - simpl. - intros ; right;auto. + auto. (**) - rewrite map_simpl. + simpl. intros. - rewrite make_conj_cons in H. - destruct H as [HH1 HH2]. - generalize (IHf HH2) ; clear IHf ; intro. - destruct H. - left ; auto. - rewrite make_conj_cons. - destruct (not_make_conj_app _ _ _ (no_middle_eval' env) HH1). - tauto. + destruct f. + simpl in H. + simpl in IHf. + unfold F in H. + revert H. + intros. + apply or_clause_correct. + destruct (or_clause t a) ; simpl in * ; auto. + unfold F in H at 1. + revert H. + assert (HH := or_clause_correct t a env). + destruct (or_clause t a); simpl in HH ; + rewrite make_conj_cons in * ; intuition. + rewrite make_conj_cons in *. tauto. Qed. - Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval' env) a) -> eval_cnf (eval' env) f -> eval_cnf (eval' env) (a::f). + + Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval' env) a) -> eval_cnf env f -> eval_cnf env (a::f). Proof. intros. unfold eval_cnf in *. rewrite make_conj_cons ; eauto. Qed. - Lemma or_cnf_correct : forall env f f', eval_cnf (eval' env) (or_cnf f f') -> (eval_cnf (eval' env) f) \/ (eval_cnf (eval' env) f'). + Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') -> (eval_cnf env f) \/ (eval_cnf env f'). Proof. induction f. unfold eval_cnf. @@ -153,19 +310,19 @@ Set Implicit Arguments. destruct (eval_cnf_app _ _ _ H). clear H. destruct (IHf _ H0). - destruct (or_clause_correct _ _ _ H1). + destruct (or_clause_cnf_correct _ _ _ H1). left. apply eval_cnf_cons ; auto. right ; auto. right ; auto. Qed. - Variable normalise_correct : forall env t, eval_cnf (eval' env) (normalise t) -> eval env t. + Variable normalise_correct : forall env t, eval_cnf env (normalise t) -> eval env t. - Variable negate_correct : forall env t, eval_cnf (eval' env) (negate t) -> ~ eval env t. + Variable negate_correct : forall env t, eval_cnf env (negate t) -> ~ eval env t. - Lemma xcnf_correct : forall f pol env, eval_cnf (eval' env) (xcnf pol f) -> eval_f (eval env) (if pol then f else N f). + Lemma xcnf_correct : forall f pol env, eval_cnf env (xcnf pol f) -> eval_f (eval env) (if pol then f else N f). Proof. induction f. (* TT *) @@ -175,15 +332,19 @@ Set Implicit Arguments. (* FF *) unfold eval_cnf. destruct pol; simpl ; auto. + unfold eval_clause ; simpl. + tauto. (* P *) simpl. destruct pol ; intros ;simpl. unfold eval_cnf in H. (* Here I have to drop the proposition *) simpl in H. + unfold eval_clause in H ; simpl in H. tauto. (* Here, I could store P in the clause *) unfold eval_cnf in H;simpl in H. + unfold eval_clause in H ; simpl in H. tauto. (* A *) simpl. @@ -282,7 +443,7 @@ Set Implicit Arguments. end end. - Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf (eval' env) t. + Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf env t. Proof. unfold eval_cnf. induction t. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 2db4db676..6dad2ba60 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -200,12 +200,12 @@ Definition normalise (t:Formula Z) : cnf (NFormula Z) := List.map (fun x => x::nil) (xnormalise t). -Lemma normalise_correct : forall env t, eval_cnf (eval_nformula env) (normalise t) <-> Zeval_formula env t. +Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t. Proof. Opaque padd. unfold normalise, xnormalise ; simpl; intros env t. rewrite Zeval_formula_compat. - unfold eval_cnf. + unfold eval_cnf, eval_clause. destruct t as [lhs o rhs]; case_eq o; simpl; repeat rewrite eval_pol_sub; repeat rewrite eval_pol_add; @@ -235,14 +235,14 @@ Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := Definition negate (t:RingMicromega.Formula Z) : cnf (NFormula Z) := List.map (fun x => x::nil) (xnegate t). -Lemma negate_correct : forall env t, eval_cnf (eval_nformula env) (negate t) <-> ~ Zeval_formula env t. +Lemma negate_correct : forall env t, eval_cnf eval_nformula env (negate t) <-> ~ Zeval_formula env t. Proof. Proof. Opaque padd. intros env t. rewrite Zeval_formula_compat. unfold negate, xnegate ; simpl. - unfold eval_cnf. + unfold eval_cnf,eval_clause. destruct t as [lhs o rhs]; case_eq o; simpl; repeat rewrite eval_pol_sub; repeat rewrite eval_pol_add; @@ -256,10 +256,13 @@ Proof. Transparent padd. Qed. +Definition Zunsat := check_inconsistent 0 Zeq_bool Zle_bool. + +Definition Zdeduce := nformula_plus_nformula 0 Zplus Zeq_bool. Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := - @tauto_checker (Formula Z) (NFormula Z) normalise negate ZWitness ZWeakChecker f w. + @tauto_checker (Formula Z) (NFormula Z) Zunsat Zdeduce normalise negate ZWitness ZWeakChecker f w. (* To get a complete checker, the proof format has to be enriched *) @@ -273,6 +276,36 @@ Definition ceiling (a b:Z) : Z := | _ => q + 1 end. + +Require Import Znumtheory. + +Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Zdiv a b. +Proof. + unfold ceiling. + intros. + apply Zdivide_mod in H. + case_eq (Zdiv_eucl a b). + intros. + change z with (fst (z,z0)). + rewrite <- H0. + change (fst (Zdiv_eucl a b)) with (Zdiv a b). + change z0 with (snd (z,z0)). + rewrite <- H0. + change (snd (Zdiv_eucl a b)) with (Zmod a b). + rewrite H. + reflexivity. +Qed. + +Lemma Zdivide_Zdiv : forall a b c, b <> 0 -> (b | c) -> b * a = c -> a = c / b. +Proof. + intros. + inv H0. + rewrite H2. + rewrite Z_div_mult_full ; auto. + apply Zmult_reg_l with (p :=b) ; auto. + rewrite (Zmult_comm b q). auto. +Qed. + Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x >= b -> x >= ceiling b a. Proof. unfold ceiling. @@ -307,40 +340,13 @@ Inductive ZArithProof : Type := | DoneProof | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof -| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof. - -(* n/d <= x -> d*x - n >= 0 *) -(* -Definition makeLb (v:PExpr Z) (q:Q) : NFormula Z := - let (n,d) := q in (PEsub (PEmul (PEc (Zpos d)) v) (PEc n),NonStrict). - -(* x <= n/d -> d * x <= d *) -Definition makeUb (v:PExpr Z) (q:Q) : NFormula Z := - let (n,d) := q in - (PEsub (PEc n) (PEmul (PEc (Zpos d)) v), NonStrict). - -Definition qceiling (q:Q) : Z := - let (n,d) := q in ceiling n (Zpos d). +| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof +(*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof*). -Definition qfloor (q:Q) : Z := - let (n,d) := q in Zdiv n (Zpos d). -Definition makeLbCut (v:PExprC Z) (q:Q) : NFormula Z := - (PEsub v (PEc (qceiling q)), NonStrict). -Definition neg_nformula (f : NFormula Z) := - let (e,o) := f in - (PEopp (PEadd e (PEc 1%Z)), o). +(* n/d <= x -> d*x - n >= 0 *) -Lemma neg_nformula_sound : forall env f, snd f = NonStrict ->( ~ (Zeval_nformula env (neg_nformula f)) <-> Zeval_nformula env f). -Proof. - unfold neg_nformula. - destruct f. - simpl. - intros ; subst ; simpl in *. - split; auto with zarith. -Qed. -*) (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b. - b is the constant @@ -566,9 +572,11 @@ Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) := let (e,op) := f in match op with | Equal => let (g,c) := Zgcd_pol e in - if andb (Zgt_bool g Z0) (andb (Zgt_bool c Z0) (negb (Zeq_bool (Zgcd g c) g))) + if andb (Zgt_bool g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Zgcd g c) g))) then None (* inconsistent *) - else Some (e, Z0,op) (* It could still be inconsistent -- but not a cut *) + else (* Could be optimised Zgcd_pol is recomputed *) + let (p,c) := makeCuttingPlane e in + Some (p,c,Equal) | NonEqual => Some (e,Z0,op) | Strict => let (p,c) := makeCuttingPlane (PsubC Zminus e 1) in Some (p,c,NonStrict) @@ -596,16 +604,16 @@ Proof. Qed. - - - Definition eval_Psatz : list (NFormula Z) -> ZWitness -> option (NFormula Z) := eval_Psatz 0 1 Zplus Zmult Zeq_bool Zle_bool. -Definition check_inconsistent := check_inconsistent 0 Zeq_bool Zle_bool. - - +Definition valid_cut_sign (op:Op1) := + match op with + | Equal => true + | NonStrict => true + | _ => false + end. Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool := match pf with @@ -614,7 +622,7 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : match eval_Psatz l w with | None => false | Some f => - if check_inconsistent f then true + if Zunsat f then true else ZChecker (f::l) pf end | CutProof w pf => @@ -627,29 +635,24 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : end end | EnumProof w1 w2 pf => - match eval_Psatz l w1 , eval_Psatz l w2 with - | Some f1 , Some f2 => - match genCuttingPlane f1 , genCuttingPlane f2 with - |Some (e1,z1,op1) , Some (e2,z2,op2) => - match op1 , op2 with - | NonStrict , NonStrict => - if is_pol_Z0 (padd e1 e2) - then - (fix label (pfs:list ZArithProof) := - fun lb ub => - match pfs with - | nil => if Zgt_bool lb ub then true else false - | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) - end) - pf (Zopp z1) z2 - else false - | _ , _ => false - end - | _ , _ => false - end - | _ , _ => false - end - end. + match eval_Psatz l w1 , eval_Psatz l w2 with + | Some f1 , Some f2 => + match genCuttingPlane f1 , genCuttingPlane f2 with + |Some (e1,z1,op1) , Some (e2,z2,op2) => + if (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd e1 e2)) + then + (fix label (pfs:list ZArithProof) := + fun lb ub => + match pfs with + | nil => if Zgt_bool lb ub then true else false + | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) + end) pf (Zopp z1) z2 + else false + | _ , _ => true + end + | _ , _ => false + end +end. @@ -702,7 +705,7 @@ Proof. apply make_conj_in ; auto. Qed. -Lemma makeCuttingPlane_sound : forall env e e' c, +Lemma makeCuttingPlane_ns_sound : forall env e e' c, eval_nformula env (e, NonStrict) -> makeCuttingPlane e = (e',c) -> eval_nformula env (nformula_of_cutting_plane (e', c, NonStrict)). @@ -729,7 +732,6 @@ Proof. intros. inv H2. auto with zarith. Qed. - Lemma cutting_plane_sound : forall env f p, eval_nformula env f -> genCuttingPlane f = Some p -> @@ -741,13 +743,51 @@ Proof. (* Equal *) destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. - destruct (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))) ; [discriminate|]. - intros. inv H1. unfold nformula_of_cutting_plane. - unfold eval_nformula in *. - unfold RingMicromega.eval_nformula in *. - unfold eval_op1 in *. - rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). - simpl. rewrite H0. reflexivity. + case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))) ; [discriminate|]. + case_eq (makeCuttingPlane e). + intros. + inv H3. + unfold makeCuttingPlane in H. + rewrite H1 in H. + revert H. + change (eval_pol env e = 0) in H2. + case_eq (Zgt_bool g 0). + intros. + rewrite <- Zgt_is_gt_bool in H. + rewrite Zgcd_pol_correct_lt with (1:= H1) in H2; auto with zarith. + unfold nformula_of_cutting_plane. + change (eval_pol env (padd e' (Pc z)) = 0). + inv H3. + rewrite eval_pol_add. + set (x:=eval_pol env (Zdiv_pol (PsubC Zminus e c) g)) in *; clearbody x. + simpl. + rewrite andb_false_iff in H0. + destruct H0. + rewrite Zgt_is_gt_bool in H ; congruence. + rewrite andb_false_iff in H0. + destruct H0. + rewrite negb_false_iff in H0. + apply Zeq_bool_eq in H0. + subst. simpl. + rewrite Zplus_0_r in H2. + apply Zmult_integral in H2. + intuition auto with zarith. + rewrite negb_false_iff in H0. + apply Zeq_bool_eq in H0. + assert (HH := Zgcd_is_gcd g c). + rewrite H0 in HH. + inv HH. + apply Zdivide_opp_r in H4. + rewrite Zdivide_ceiling ; auto. + apply Zeq_minus. + apply Zdivide_Zdiv ; auto with zarith. + intros. + unfold nformula_of_cutting_plane. + inv H3. + change (eval_pol env (padd e' (Pc 0)) = 0). + rewrite eval_pol_add. + simpl. + auto with zarith. (* NonEqual *) intros. inv H0. @@ -762,7 +802,7 @@ Proof. case_eq (makeCuttingPlane (PsubC Zminus e 1)). intros. inv H1. - apply makeCuttingPlane_sound with (env:=env) (2:= H). + apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). auto with zarith. @@ -771,7 +811,7 @@ Proof. case_eq (makeCuttingPlane e). intros. inv H1. - apply makeCuttingPlane_sound with (env:=env) (2:= H). + apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). assumption. Qed. @@ -783,23 +823,24 @@ Proof. destruct f. destruct o. case_eq (Zgcd_pol p) ; intros g c. - case_eq (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))). + case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))). intros. flatten_bool. rewrite negb_true_iff in H5. apply Zeq_bool_neq in H5. - contradict H5. rewrite <- Zgt_is_gt_bool in H3. - rewrite <- Zgt_is_gt_bool in H. - apply Zis_gcd_gcd; auto with zarith. - constructor; auto with zarith. + rewrite negb_true_iff in H. + apply Zeq_bool_neq in H. change (eval_pol env p = 0) in H2. rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith. set (x:=eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) in *; clearbody x. + contradict H5. + apply Zis_gcd_gcd; auto with zarith. + constructor; auto with zarith. exists (-x). rewrite <- Zopp_mult_distr_l, Zmult_comm; auto with zarith. (**) - discriminate. + destruct (makeCuttingPlane p); discriminate. discriminate. destruct (makeCuttingPlane (PsubC Zminus p 1)) ; discriminate. destruct (makeCuttingPlane p) ; discriminate. @@ -816,11 +857,11 @@ Proof. simpl. intro l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. - case_eq (check_inconsistent f). + case_eq (Zunsat f). intros. apply (checker_nf_sound Zsor ZSORaddon l w). unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. - unfold check_inconsistent in H0. assumption. + unfold Zunsat in H0. assumption. intros. assert (make_impl (eval_nformula env) (f::l) False). apply H with (2:= H1). @@ -868,55 +909,54 @@ Proof. case_eq (eval_Psatz l w1) ; [ | discriminate]. case_eq (eval_Psatz l w2) ; [ | discriminate]. intros f1 Hf1 f2 Hf2. - case_eq (genCuttingPlane f2) ; [ | discriminate]. + case_eq (genCuttingPlane f2). destruct p as [ [p1 z1] op1]. - case_eq (genCuttingPlane f1) ; [ | discriminate]. + case_eq (genCuttingPlane f1). destruct p as [ [p2 z2] op2]. - case_eq op1 ; case_eq op2 ; try discriminate. - case_eq (is_pol_Z0 (padd p1 p2)) ; try discriminate. - intros. + case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). + intros Hcond. + flatten_bool. + rename H1 into HZ0. + rename H2 into Hop1. + rename H3 into Hop2. + intros HCutL HCutR Hfix env. (* get the bounds of the enum *) rewrite <- make_conj_impl. intro. assert (-z1 <= eval_pol env p1 <= z2). split. apply eval_Psatz_sound with (env:=env) in Hf2 ; auto. - apply cutting_plane_sound with (1:= Hf2) in H4. - unfold nformula_of_cutting_plane in H4. - unfold eval_nformula in H4. - unfold RingMicromega.eval_nformula in H4. - change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H4. - unfold eval_op1 in H4. - rewrite eval_pol_add in H4. simpl in H4. - auto with zarith. + apply cutting_plane_sound with (1:= Hf2) in HCutR. + unfold nformula_of_cutting_plane in HCutR. + unfold eval_nformula in HCutR. + unfold RingMicromega.eval_nformula in HCutR. + change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutR. + unfold eval_op1 in HCutR. + destruct op1 ; simpl in Hop1 ; try discriminate; + rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith. (**) - apply is_pol_Z0_eval_pol with (env := env) in H0. - rewrite eval_pol_add in H0. + apply is_pol_Z0_eval_pol with (env := env) in HZ0. + rewrite eval_pol_add in HZ0. replace (eval_pol env p1) with (- eval_pol env p2) by omega. apply eval_Psatz_sound with (env:=env) in Hf1 ; auto. - apply cutting_plane_sound with (1:= Hf1) in H3. - unfold nformula_of_cutting_plane in H3. - unfold eval_nformula in H3. - unfold RingMicromega.eval_nformula in H3. - change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H3. - unfold eval_op1 in H3. - rewrite eval_pol_add in H3. simpl in H3. - omega. - revert H5. - set (FF := (fix label (pfs : list ZArithProof) (lb ub : Z) {struct pfs} : bool := - match pfs with - | nil => if Z_gt_dec lb ub then true else false - | pf :: rsr => - (ZChecker ((PsubC Zminus p1 lb, Equal) :: l) pf && - label rsr (lb + 1)%Z ub)%bool - end)). + apply cutting_plane_sound with (1:= Hf1) in HCutL. + unfold nformula_of_cutting_plane in HCutL. + unfold eval_nformula in HCutL. + unfold RingMicromega.eval_nformula in HCutL. + change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutL. + unfold eval_op1 in HCutL. + rewrite eval_pol_add in HCutL. simpl in HCutL. + destruct op2 ; simpl in Hop2 ; try discriminate ; omega. + revert Hfix. + match goal with + | |- context[?F pf (-z1) z2 = true] => set (FF := F) + end. intros. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ ZChecker ((PsubC Zminus p1 x,Equal) :: l) pr = true)%Z). - clear H. - clear H0 H1 H2 H3 H4 H7. - revert H5. + clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1. + revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. induction pf;simpl ;intros. @@ -931,16 +971,22 @@ Proof. subst. exists a ; auto. assert (z1 + 1 <= x <= z2)%Z by omega. - destruct (IHpf _ _ H1 _ H3). + elim IHpf with (2:=H2) (3:= H4). destruct H4. - exists x0 ; split;auto. + intros. + exists x0 ; split;tauto. + intros until 1. + apply H ; auto. + unfold ltof in *. + simpl in *. + zify. omega. (*/asser *) - destruct (HH _ H7) as [pr [Hin Hcheker]]. + destruct (HH _ H1) as [pr [Hin Hcheker]]. assert (make_impl (eval_nformula env) ((PsubC Zminus p1 (eval_pol env p1),Equal) :: l) False). apply (H pr);auto. apply in_bdepth ; auto. - rewrite <- make_conj_impl in H8. - apply H8. + rewrite <- make_conj_impl in H2. + apply H2. rewrite make_conj_cons. split ;auto. unfold eval_nformula. @@ -948,10 +994,23 @@ Proof. simpl. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). unfold eval_pol. ring. + discriminate. + (* No cutting plane *) + intros. + rewrite <- make_conj_impl. + intros. + apply eval_Psatz_sound with (2:= Hf1) in H3. + apply genCuttingPlaneNone with (2:= H3) ; auto. + (* No Cutting plane (bis) *) + intros. + rewrite <- make_conj_impl. + intros. + apply eval_Psatz_sound with (2:= Hf2) in H2. + apply genCuttingPlaneNone with (2:= H2) ; auto. Qed. Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool := - @tauto_checker (Formula Z) (NFormula Z) normalise negate ZArithProof ZChecker f w. + @tauto_checker (Formula Z) (NFormula Z) Zunsat Zdeduce normalise negate ZArithProof ZChecker f w. Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (Zeval_formula env) f. Proof. @@ -959,6 +1018,11 @@ Proof. unfold ZTautoChecker. apply (tauto_checker_sound Zeval_formula eval_nformula). apply Zeval_nformula_dec. + intros until env. + unfold eval_nformula. unfold RingMicromega.eval_nformula. + destruct t. + apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. + unfold Zdeduce. apply (nformula_plus_nformula_correct Zsor ZSORaddon). intros env t. rewrite normalise_correct ; auto. intros env t. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2d5762679..6e8018b91 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -15,153 +15,18 @@ (* We take as input a list of polynomials [p1...pn] and return an unfeasibility certificate polynomial. *) -(*open Micromega.Polynomial*) +type var = int + + + open Big_int open Num -open Sos_lib +open Polynomial module Mc = Micromega module Ml2C = Mutils.CamlToCoq module C2Ml = Mutils.CoqToCaml -let (<+>) = add_num -let (<->) = minus_num -let (<*>) = mult_num - -type var = Mc.positive - -module Monomial : -sig - type t - val const : t - val var : var -> t - val find : var -> t -> int - val mult : var -> t -> t - val prod : t -> t -> t - val compare : t -> t -> int - val pp : out_channel -> t -> unit - val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a -end - = -struct - (* A monomial is represented by a multiset of variables *) - module Map = Map.Make(struct type t = var let compare = Pervasives.compare end) - open Map - - type t = int Map.t - - (* The monomial that corresponds to a constant *) - let const = Map.empty - - (* The monomial 'x' *) - let var x = Map.add x 1 Map.empty - - (* Get the degre of a variable in a monomial *) - let find x m = try find x m with Not_found -> 0 - - (* Multiply a monomial by a variable *) - let mult x m = add x ( (find x m) + 1) m - - (* Product of monomials *) - let prod m1 m2 = Map.fold (fun k d m -> add k ((find k m) + d) m) m1 m2 - - (* Total ordering of monomials *) - let compare m1 m2 = Map.compare Pervasives.compare m1 m2 - - let pp o m = Map.iter (fun k v -> - if v = 1 then Printf.fprintf o "x%i." (C2Ml.index k) - else Printf.fprintf o "x%i^%i." (C2Ml.index k) v) m - - let fold = fold - -end - - -module Poly : - (* A polynomial is a map of monomials *) - (* - This is probably a naive implementation - (expected to be fast enough - Coq is probably the bottleneck) - *The new ring contribution is using a sparse Horner representation. - *) -sig - type t - val get : Monomial.t -> t -> num - val variable : var -> t - val add : Monomial.t -> num -> t -> t - val constant : num -> t - val mult : Monomial.t -> num -> t -> t - val product : t -> t -> t - val addition : t -> t -> t - val uminus : t -> t - val fold : (Monomial.t -> num -> 'a -> 'a) -> t -> 'a -> 'a - val pp : out_channel -> t -> unit - val compare : t -> t -> int - val is_null : t -> bool -end = -struct - (*normalisation bug : 0*x ... *) - module P = Map.Make(Monomial) - open P - - type t = num P.t - - let pp o p = P.iter (fun k v -> - if compare_num v (Int 0) <> 0 - then - if Monomial.compare Monomial.const k = 0 - then Printf.fprintf o "%s " (string_of_num v) - else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p - - (* Get the coefficient of monomial mn *) - let get : Monomial.t -> t -> num = - fun mn p -> try find mn p with Not_found -> (Int 0) - - - (* The polynomial 1.x *) - let variable : var -> t = - fun x -> add (Monomial.var x) (Int 1) empty - - (*The constant polynomial *) - let constant : num -> t = - fun c -> add (Monomial.const) c empty - - (* The addition of a monomial *) - - let add : Monomial.t -> num -> t -> t = - fun mn v p -> - let vl = (get mn p) <+> v in - add mn vl p - - - (** Design choice: empty is not a polynomial - I do not remember why .... - **) - - (* The product by a monomial *) - let mult : Monomial.t -> num -> t -> t = - fun mn v p -> - fold (fun mn' v' res -> P.add (Monomial.prod mn mn') (v<*>v') res) p empty - - - let addition : t -> t -> t = - fun p1 p2 -> fold (fun mn v p -> add mn v p) p1 p2 - - - let product : t -> t -> t = - fun p1 p2 -> - fold (fun mn v res -> addition (mult mn v p2) res ) p1 empty - - - let uminus : t -> t = - fun p -> map (fun v -> minus_num v) p - - let fold = P.fold - - let is_null p = fold (fun mn vl b -> b & sign_num vl = 0) p true - - let compare = compare compare_num -end open Mutils type 'a number_spec = { @@ -181,7 +46,7 @@ let z_spec = { mult = Mc.zmult; eqb = Mc.zeq_bool } - + let q_spec = { bigint_to_number = (fun x -> {Mc.qnum = Ml2C.bigint x; Mc.qden = Mc.XH}); @@ -194,53 +59,59 @@ let q_spec = { let r_spec = z_spec + let dev_form n_spec p = - let rec dev_form p = + let rec dev_form p = match p with | Mc.PEc z -> Poly.constant (n_spec.number_to_num z) - | Mc.PEX v -> Poly.variable v - | Mc.PEmul(p1,p2) -> + | Mc.PEX v -> Poly.variable (C2Ml.positive v) + | Mc.PEmul(p1,p2) -> let p1 = dev_form p1 in let p2 = dev_form p2 in - Poly.product p1 p2 + Poly.product p1 p2 | Mc.PEadd(p1,p2) -> Poly.addition (dev_form p1) (dev_form p2) | Mc.PEopp p -> Poly.uminus (dev_form p) | Mc.PEsub(p1,p2) -> Poly.addition (dev_form p1) (Poly.uminus (dev_form p2)) - | Mc.PEpow(p,n) -> + | Mc.PEpow(p,n) -> let p = dev_form p in let n = C2Ml.n n in - let rec pow n = - if n = 0 + let rec pow n = + if n = 0 then Poly.constant (n_spec.number_to_num n_spec.unit) else Poly.product p (pow (n-1)) in pow n in dev_form p -let monomial_to_polynomial mn = - Monomial.fold - (fun v i acc -> - let mn = if i = 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in - if acc = Mc.PEc (Mc.Zpos Mc.XH) - then mn - else Mc.PEmul(mn,acc)) - mn - (Mc.PEc (Mc.Zpos Mc.XH)) - -let list_to_polynomial vars l = + +let monomial_to_polynomial mn = + Monomial.fold + (fun v i acc -> + let v = Ml2C.positive v in + let mn = if i = 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in + if acc = Mc.PEc (Mc.Zpos Mc.XH) + then mn + else Mc.PEmul(mn,acc)) + mn + (Mc.PEc (Mc.Zpos Mc.XH)) + + + +let list_to_polynomial vars l = assert (List.for_all (fun x -> ceiling_num x =/ x) l); let var x = monomial_to_polynomial (List.nth vars x) in + let rec xtopoly p i = function | [] -> p - | c::l -> if c =/ (Int 0) then xtopoly p (i+1) l + | c::l -> if c =/ (Int 0) then xtopoly p (i+1) l else let c = Mc.PEc (Ml2C.bigint (numerator c)) in - let mn = + let mn = if c = Mc.PEc (Mc.Zpos Mc.XH) then var i else Mc.PEmul (c,var i) in let p' = if p = Mc.PEc Mc.Z0 then mn else Mc.PEadd (mn, p) in xtopoly p' (i+1) l in - + xtopoly (Mc.PEc Mc.Z0) 0 l let rec fixpoint f x = @@ -248,51 +119,54 @@ let rec fixpoint f x = if y' = x then y' else fixpoint f y' -let rec_simpl_cone n_spec e = - let simpl_cone = +let rec_simpl_cone n_spec e = + let simpl_cone = Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in let rec rec_simpl_cone = function - | Mc.PsatzMulE(t1, t2) -> + | Mc.PsatzMulE(t1, t2) -> simpl_cone (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2)) - | Mc.PsatzAdd(t1,t2) -> + | Mc.PsatzAdd(t1,t2) -> simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2)) | x -> simpl_cone x in rec_simpl_cone e - + + let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c - -type cone_prod = - Const of cone - | Ideal of cone *cone - | Mult of cone * cone + +type cone_prod = + Const of cone + | Ideal of cone *cone + | Mult of cone * cone | Other of cone and cone = Mc.zWitness -let factorise_linear_cone c = - let rec cone_list c l = + +let factorise_linear_cone c = + + let rec cone_list c l = match c with | Mc.PsatzAdd (x,r) -> cone_list r (x::l) | _ -> c :: l in - + let factorise c1 c2 = match c1 , c2 with - | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> + | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None - | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> + | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None | _ -> None in - + let rec rebuild_cone l pending = match l with | [] -> (match pending with | None -> Mc.PsatzZ | Some p -> p ) - | e::l -> + | e::l -> (match pending with - | None -> rebuild_cone l (Some e) + | None -> rebuild_cone l (Some e) | Some p -> (match factorise p e with | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e)) | Some f -> rebuild_cone l (Some f) ) @@ -300,15 +174,17 @@ let factorise_linear_cone c = (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None) -(* The binding with Fourier might be a bit obsolete + + +(* The binding with Fourier might be a bit obsolete -- how does it handle equalities ? *) (* Certificates are elements of the cone such that P = 0 *) (* To begin with, we search for certificates of the form: - a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0 + a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0 where pi >= 0 qi > 0 - ai >= 0 + ai >= 0 bi >= 0 Sum bi + c >= 1 This is a linear problem: each monomial is considered as a variable. @@ -318,216 +194,209 @@ let factorise_linear_cone c = *) open Mfourier - (*module Fourier = Fourier(Vector.VList)(SysSet(Vector.VList))*) - (*module Fourier = Fourier(Vector.VSparse)(SysSetAlt(Vector.VSparse))*) -(*module Fourier = Mfourier.Fourier(Vector.VSparse)(*(SysSetAlt(Vector.VMap))*)*) - -(*module Vect = Fourier.Vect*) -(*open Fourier.Cstr*) (* fold_left followed by a rev ! *) -let constrain_monomial mn l = +let constrain_monomial mn l = let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in if mn = Monomial.const - then - { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; - op = Eq ; + then + { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; + op = Eq ; cst = Big_int zero_big_int } else - { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; - op = Eq ; + { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; + op = Eq ; cst = Big_int zero_big_int } - -let positivity l = - let rec xpositivity i l = + +let positivity l = + let rec xpositivity i l = match l with | [] -> [] | (_,Mc.Equal)::l -> xpositivity (i+1) l - | (_,_)::l -> - {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; - op = Ge ; + | (_,_)::l -> + {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; + op = Ge ; cst = Int 0 } :: (xpositivity (i+1) l) in xpositivity 0 l let string_of_op = function - | Mc.Strict -> "> 0" - | Mc.NonStrict -> ">= 0" + | Mc.Strict -> "> 0" + | Mc.NonStrict -> ">= 0" | Mc.Equal -> "= 0" | Mc.NonEqual -> "<> 0" -(* If the certificate includes at least one strict inequality, +(* If the certificate includes at least one strict inequality, the obtained polynomial can also be 0 *) let build_linear_system l = - (* Gather the monomials: HINT add up of the polynomials *) + (* Gather the monomials: HINT add up of the polynomials ==> This does not work anymore *) let l' = List.map fst l in - let monomials = - List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l' + + let module MonSet = Set.Make(Monomial) in + + let monomials = + List.fold_left (fun acc p -> + Poly.fold (fun m _ acc -> MonSet.add m acc) p acc) + (MonSet.singleton Monomial.const) l' in (* For each monomial, compute a constraint *) - let s0 = - Poly.fold (fun mn _ res -> (constrain_monomial mn l')::res) monomials [] in + let s0 = + MonSet.fold (fun mn res -> (constrain_monomial mn l')::res) monomials [] in (* I need at least something strictly positive *) let strict = { coeffs = Vect.from_list ((Big_int unit_big_int):: - (List.map (fun (x,y) -> - match y with Mc.Strict -> - Big_int unit_big_int + (List.map (fun (x,y) -> + match y with Mc.Strict -> + Big_int unit_big_int | _ -> Big_int zero_big_int) l)); op = Ge ; cst = Big_int unit_big_int } in (* Add the positivity constraint *) - {coeffs = Vect.from_list ([Big_int unit_big_int]) ; - op = Ge ; + {coeffs = Vect.from_list ([Big_int unit_big_int]) ; + op = Ge ; cst = Big_int zero_big_int}::(strict::(positivity l)@s0) let big_int_to_z = Ml2C.bigint - -(* For Q, this is a pity that the certificate has been scaled + +(* For Q, this is a pity that the certificate has been scaled -- at a lower layer, certificates are using nums... *) -let make_certificate n_spec (cert,li) = +let make_certificate n_spec (cert,li) = let bint_to_cst = n_spec.bigint_to_number in match cert with | [] -> failwith "empty_certificate" - | e::cert' -> - let cst = match compare_big_int e zero_big_int with + | e::cert' -> +(* let cst = match compare_big_int e zero_big_int with | 0 -> Mc.PsatzZ - | 1 -> Mc.PsatzC (bint_to_cst e) - | _ -> failwith "positivity error" - in + | 1 -> Mc.PsatzC (bint_to_cst e) + | _ -> failwith "positivity error" + in *) let rec scalar_product cert l = match cert with | [] -> Mc.PsatzZ - | c::cert -> match l with - | [] -> failwith "make_certificate(1)" - | i::l -> - let r = scalar_product cert l in - match compare_big_int c zero_big_int with - | -1 -> Mc.PsatzAdd ( - Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), - r) - | 0 -> r - | _ -> Mc.PsatzAdd ( - Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), - r) in - - ((factorise_linear_cone - (simplify_cone n_spec (Mc.PsatzAdd (cst, scalar_product cert' li))))) + | c::cert -> + match l with + | [] -> failwith "make_certificate(1)" + | i::l -> + let r = scalar_product cert l in + match compare_big_int c zero_big_int with + | -1 -> Mc.PsatzAdd ( + Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), + r) + | 0 -> r + | _ -> Mc.PsatzAdd ( + Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), + r) in + (factorise_linear_cone + (simplify_cone n_spec (scalar_product cert' li))) exception Found of Monomial.t exception Strict -let primal l = +let primal l = let vr = ref 0 in let module Mmn = Map.Make(Monomial) in let vect_of_poly map p = - Poly.fold (fun mn vl (map,vect) -> - if mn = Monomial.const + Poly.fold (fun mn vl (map,vect) -> + if mn = Monomial.const then (map,vect) - else + else let (mn,m) = try (Mmn.find mn map,map) with Not_found -> let res = (!vr, Mmn.add mn !vr map) in incr vr ; res in (m,if sign_num vl = 0 then vect else (mn,vl)::vect)) p (map,[]) in - + let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in let cmp x y = Pervasives.compare (fst x) (fst y) in snd (List.fold_right (fun (p,op) (map,l) -> - let (mp,vect) = vect_of_poly map p in + let (mp,vect) = vect_of_poly map p in let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in (mp,cstr::l)) l (Mmn.empty,[])) -let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = +let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = (* List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *) - - + let sys = build_linear_system l in - try + try match Fourier.find_point sys with | Inr _ -> None - | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) + | Inl cert -> Some (rats_to_ints (Vect.to_list cert)) (* should not use rats_to_ints *) - with x -> - if debug - then (Printf.printf "raw certificate %s" (Printexc.to_string x); + with x -> + if debug + then (Printf.printf "raw certificate %s" (Printexc.to_string x); flush stdout) ; None -let raw_certificate l = - try +let raw_certificate l = + try let p = primal l in match Fourier.find_point p with - | Inr prf -> - if debug then Printf.printf "AProof : %a\n" pp_proof prf ; - let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Mfourier.Proof.mk_proof p prf))) in - if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; + | Inr prf -> + if debug then Printf.printf "AProof : %a\n" pp_proof prf ; + let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in + if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; Some (rats_to_ints (Vect.to_list cert)) | Inl _ -> None - with Strict -> + with Strict -> (* Fourier elimination should handle > *) - dual_raw_certificate l + dual_raw_certificate l -let simple_linear_prover (*to_constant*) l = +let simple_linear_prover l = let (lc,li) = List.split l in match raw_certificate lc with | None -> None (* No certificate *) - | Some cert -> (* make_certificate to_constant*)Some (cert,li) + | Some cert -> Some (cert,li) + -let linear_prover n_spec l = - let li = List.combine l (interval 0 (List.length l -1)) in - let (l1,l') = List.partition - (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in - let l' = List.map - (fun ((x,y),i) -> match y with - Mc.NonEqual -> failwith "cannot happen" - | y -> ((dev_form n_spec x, y),i)) l' in - simple_linear_prover (*n_spec*) l' +let linear_prover n_spec l = + let build_system n_spec l = + let li = List.combine l (interval 0 (List.length l -1)) in + let (l1,l') = List.partition + (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in + List.map + (fun ((x,y),i) -> match y with + Mc.NonEqual -> failwith "cannot happen" + | y -> ((dev_form n_spec x, y),i)) l' in + let l' = build_system n_spec l in + simple_linear_prover (*n_spec*) l' let linear_prover n_spec l = try linear_prover n_spec l with x -> (print_string (Printexc.to_string x); None) -let linear_prover_with_cert spec l = +let linear_prover_with_cert spec l = match linear_prover spec l with | None -> None | Some cert -> Some (make_certificate spec cert) -(* zprover.... *) - -(* I need to gather the set of variables ---> - Then go for fold - Once I have an interval, I need a certificate : 2 other fourier elims. - (I could probably get the certificate directly - as it is done in the fourier contrib.) -*) let make_linear_system l = let l' = List.map fst l in - let monomials = List.fold_left (fun acc p -> Poly.addition p acc) + let monomials = List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l' in - let monomials = Poly.fold + let monomials = Poly.fold (fun mn _ l -> if mn = Monomial.const then l else mn::l) monomials [] in - (List.map (fun (c,op) -> - {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; - op = op ; + (List.map (fun (c,op) -> + {coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ; + op = op ; cst = minus_num ( (Poly.get Monomial.const c))}) l ,monomials) @@ -536,130 +405,66 @@ let pplus x y = Mc.PEadd(x,y) let pmult x y = Mc.PEmul(x,y) let pconst x = Mc.PEc x let popp x = Mc.PEopp x - + let debug = false - + (* keep track of enumerated vectors *) -let rec mem p x l = +let rec mem p x l = match l with [] -> false | e::l -> if p x e then true else mem p x l -let rec remove_assoc p x l = +let rec remove_assoc p x l = match l with [] -> [] | e::l -> if p x (fst e) then - remove_assoc p x l else e::(remove_assoc p x l) + remove_assoc p x l else e::(remove_assoc p x l) let eq x y = Vect.compare x y = 0 let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l -(* The prover is (probably) incomplete -- +(* The prover is (probably) incomplete -- only searching for naive cutting planes *) -let candidates sys = - let ll = List.fold_right ( - fun (e,k) r -> - match k with - | Mc.NonStrict -> (dev_form z_spec e , Ge)::r - | Mc.Equal -> (dev_form z_spec e , Eq)::r - (* we already know the bound -- don't compute it again *) - | _ -> failwith "Cannot happen candidates") sys [] in - - let (sys,var_mn) = make_linear_system ll in - let vars = mapi (fun _ i -> Vect.set i (Int 1) Vect.null) var_mn in - (List.fold_left (fun l cstr -> - let gcd = Big_int (Vect.gcd cstr.coeffs) in - if gcd =/ (Int 1) && cstr.op = Eq - then l - else (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars - - - - -let rec xzlinear_prover planes sys = - match linear_prover z_spec sys with - | Some prf -> Some (Mc.RatProof (make_certificate z_spec prf,Mc.DoneProof)) - | None -> (* find the candidate with the smallest range *) - (* Grrr - linear_prover is also calling 'make_linear_system' *) - let ll = List.fold_right (fun (e,k) r -> match k with - Mc.NonEqual -> r - | k -> (dev_form z_spec e , - match k with - Mc.NonStrict -> Ge - | Mc.Equal -> Eq - | Mc.Strict | Mc.NonEqual -> failwith "Cannot happen") :: r) sys [] in - let (ll,var) = make_linear_system ll in - let candidates = List.fold_left (fun acc vect -> - match Fourier.optimise vect ll with - | None -> acc - | Some i -> -(* Printf.printf "%s in %s\n" (Vect.string vect) (string_of_intrvl i) ; *) - flush stdout ; - (vect,i) ::acc) [] planes in - - let smallest_interval = - match List.fold_left (fun (x1,i1) (x2,i2) -> - if Itv.smaller_itv i1 i2 - then (x1,i1) else (x2,i2)) (Vect.null,(None,None)) candidates - with - | (x,(Some i, Some j)) -> Some(i,x,j) - | x -> None (* This might be a cutting plane *) - in - match smallest_interval with - | Some (lb,e,ub) -> - let (lbn,lbd) = - (Ml2C.bigint (sub_big_int (numerator lb) unit_big_int), - Ml2C.bigint (denominator lb)) in - let (ubn,ubd) = - (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , - Ml2C.bigint (denominator ub)) in - let expr = list_to_polynomial var (Vect.to_list e) in - (match - (*x <= ub -> x > ub *) - linear_prover z_spec - ((pplus (pmult (pconst ubd) expr) (popp (pconst ubn)), - Mc.NonStrict) :: sys), - (* lb <= x -> lb > x *) - linear_prover z_spec - ((pplus (popp (pmult (pconst lbd) expr)) (pconst lbn), - Mc.NonStrict)::sys) - with - | Some cub , Some clb -> - (match zlinear_enum (remove e planes) expr - (ceiling_num lb) (floor_num ub) sys - with - | None -> None - | Some prf -> - let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in - - Some (Mc.EnumProof((*Ml2C.q lb,expr,Ml2C.q ub,*) bound_proof clb, bound_proof cub,prf))) - | _ -> None - ) - | _ -> None -and zlinear_enum planes expr clb cub l = - if clb >/ cub - then Some [] - else - let pexpr = pplus (popp (pconst (Ml2C.bigint (numerator clb)))) expr in - let sys' = (pexpr, Mc.Equal)::l in - (*let enum = *) - match xzlinear_prover planes sys' with - | None -> if debug then print_string "zlp?"; None - | Some prf -> if debug then print_string "zlp!"; - match zlinear_enum planes expr (clb +/ (Int 1)) cub l with - | None -> None - | Some prfl -> Some (prf :: prfl) +let develop_constraint z_spec (e,k) = + match k with + | Mc.NonStrict -> (dev_form z_spec e , Ge) + | Mc.Equal -> (dev_form z_spec e , Eq) + | _ -> assert false + + +let op_of_op_compat = function + | Ge -> Mc.NonStrict + | Eq -> Mc.Equal + + +let integer_vector coeffs = + let vars , coeffs = List.split coeffs in + List.combine vars (List.map (fun x -> Big_int x) (rats_to_ints coeffs)) + +let integer_cstr {coeffs = coeffs ; op = op ; cst = cst } = + let vars , coeffs = List.split coeffs in + match rats_to_ints (cst::coeffs) with + | cst :: coeffs -> + { + coeffs = List.combine vars (List.map (fun x -> Big_int x) coeffs) ; + op = op ; cst = Big_int cst} + | _ -> assert false + + +let pexpr_of_cstr_compat var cstr = + let {coeffs = coeffs ; op = op ; cst = cst } = integer_cstr cstr in + try + let expr = list_to_polynomial var (Vect.to_list coeffs) in + let d = Ml2C.bigint (denominator cst) in + let n = Ml2C.bigint (numerator cst) in + (pplus (pmult (pconst d) expr) (popp (pconst n)), op_of_op_compat op) + with Failure _ -> failwith "pexpr_of_cstr_compat" + + -let zlinear_prover sys = - let candidates = candidates sys in - (* Printf.printf "candidates %d" (List.length candidates) ; *) - (*let t0 = Sys.time () in*) - let res = xzlinear_prover candidates sys in - (*Printf.printf "Time prover : %f" (Sys.time () -. t0) ;*) res open Sos_types -open Mutils -let rec scale_term t = +let rec scale_term t = match t with | Zero -> unit_big_int , Zero | Const n -> (denominator n) , Const (Big_int (numerator n)) @@ -692,7 +497,7 @@ let get_index_of_ith_match f i l = match l with | [] -> failwith "bad index" | e::l -> if f e - then + then (if j = i then res else get (j+1) (res+1) l ) else get j (res+1) l in get 0 0 l @@ -706,19 +511,19 @@ let rec scale_certificate pos = match pos with | Rational_eq n -> (denominator n) , Rational_eq (Big_int (numerator n)) | Rational_le n -> (denominator n) , Rational_le (Big_int (numerator n)) | Rational_lt n -> (denominator n) , Rational_lt (Big_int (numerator n)) - | Square t -> let s,t' = scale_term t in + | Square t -> let s,t' = scale_term t in mult_big_int s s , Square t' | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in mult_big_int s1 s2 , Eqmul (y1,y2) - | Sum (y, z) -> let s1,y1 = scale_certificate y + | Sum (y, z) -> let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in let g = gcd_big_int s1 s2 in let s1' = div_big_int s1 g in let s2' = div_big_int s2 g in - mult_big_int g (mult_big_int s1' s2'), + mult_big_int g (mult_big_int s1' s2'), Sum (Product(Rational_le (Big_int s2'), y1), Product (Rational_le (Big_int s1'), y2)) - | Product (y, z) -> + | Product (y, z) -> let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in mult_big_int s1 s2 , Product (y1,y2) @@ -727,7 +532,7 @@ open Micromega let rec term_to_q_expr = function | Const n -> PEc (Ml2C.q n) | Zero -> PEc ( Ml2C.q (Int 0)) - | Var s -> PEX (Ml2C.index + | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) | Mul(p1,p2) -> PEmul(term_to_q_expr p1, term_to_q_expr p2) | Add(p1,p2) -> PEadd(term_to_q_expr p1, term_to_q_expr p2) @@ -739,20 +544,20 @@ open Micromega let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e) - let rec product l = + let rec product l = match l with | [] -> Mc.PsatzZ | [i] -> Mc.PsatzIn (Ml2C.nat i) | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l) -let q_cert_of_pos pos = +let q_cert_of_pos pos = let rec _cert_of_pos = function Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l - | Rational_eq n | Rational_le n | Rational_lt n -> + | Rational_eq n | Rational_le n | Rational_lt n -> if compare_num n (Int 0) = 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.q n) | Square t -> Mc.PsatzSquare (term_to_q_pol t) @@ -765,7 +570,7 @@ let q_cert_of_pos pos = let rec term_to_z_expr = function | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) | Zero -> PEc ( Z0) - | Var s -> PEX (Ml2C.index + | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) | Mul(p1,p2) -> PEmul(term_to_z_expr p1, term_to_z_expr p2) | Add(p1,p2) -> PEadd(term_to_z_expr p1, term_to_z_expr p2) @@ -776,22 +581,645 @@ let q_cert_of_pos pos = let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e) -let z_cert_of_pos pos = +let z_cert_of_pos pos = let s,pos = (scale_certificate pos) in let rec _cert_of_pos = function Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_le i -> Mc.PsatzIn (Ml2C.nat i) | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l - | Rational_eq n | Rational_le n | Rational_lt n -> + | Rational_eq n | Rational_le n | Rational_lt n -> if compare_num n (Int 0) = 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.bigint (big_int_of_num n)) | Square t -> Mc.PsatzSquare (term_to_z_pol t) - | Eqmul (t, y) -> Mc.PsatzMulC(term_to_z_pol t, _cert_of_pos y) + | Eqmul (t, y) -> + let is_unit = + match t with + | Const n -> n =/ Int 1 + | _ -> false in + if is_unit + then _cert_of_pos y + else Mc.PsatzMulC(term_to_z_pol t, _cert_of_pos y) | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z) | Product (y, z) -> Mc.PsatzMulE (_cert_of_pos y, _cert_of_pos z) in simplify_cone z_spec (_cert_of_pos pos) +(** All constraints (initial or derived) have an index and have a justification i.e., proof. + Given a constraint, all the coefficients are always integers. +*) +open Mutils +open Mfourier +open Num +open Big_int +open Polynomial + +(*module Mc = Micromega*) +(*module Ml2C = Mutils.CamlToCoq +module C2Ml = Mutils.CoqToCaml +*) +let debug = false + + + +module Env = +struct + + type t = int list + + let id_of_hyp hyp l = + let rec xid_of_hyp i l = + match l with + | [] -> failwith "id_of_hyp" + | hyp'::l -> if hyp = hyp' then i else xid_of_hyp (i+1) l in + xid_of_hyp 0 l + +end + + +let coq_poly_of_linpol (p,c) = + + let pol_of_mon m = + Monomial.fold (fun x v p -> Mc.PEmul(Mc.PEpow(Mc.PEX(Ml2C.positive x),Ml2C.n v),p)) m (Mc.PEc (Mc.Zpos Mc.XH)) in + + List.fold_left (fun acc (x,v) -> + let mn = LinPoly.MonT.retrieve x in + Mc.PEadd(Mc.PEmul(Mc.PEc (Ml2C.bigint (numerator v)), pol_of_mon mn),acc)) (Mc.PEc (Ml2C.bigint (numerator c))) p + + + + +let rec cmpl_prf_rule env = function + | Hyp i | Def i -> Mc.PsatzIn (Ml2C.nat (Env.id_of_hyp i env)) + | Cst i -> Mc.PsatzC (Ml2C.bigint i) + | Zero -> Mc.PsatzZ + | MulPrf(p1,p2) -> Mc.PsatzMulE(cmpl_prf_rule env p1, cmpl_prf_rule env p2) + | AddPrf(p1,p2) -> Mc.PsatzAdd(cmpl_prf_rule env p1 , cmpl_prf_rule env p2) + | MulC(lp,p) -> let lp = Mc.norm0 (coq_poly_of_linpol lp) in + Mc.PsatzMulC(lp,cmpl_prf_rule env p) + | Square lp -> Mc.PsatzSquare (Mc.norm0 (coq_poly_of_linpol lp)) + | _ -> failwith "Cuts should already be compiled" + + +let rec cmpl_proof env = function + | Done -> Mc.DoneProof + | Step(i,p,prf) -> + begin + match p with + | CutPrf p' -> + Mc.CutProof(cmpl_prf_rule env p', cmpl_proof (i::env) prf) + | _ -> Mc.RatProof(cmpl_prf_rule env p,cmpl_proof (i::env) prf) + end + | Enum(i,p1,_,p2,l) -> + Mc.EnumProof(cmpl_prf_rule env p1,cmpl_prf_rule env p2,List.map (cmpl_proof (i::env)) l) + + +let compile_proof env prf = + let id = 1 + proof_max_id prf in + let _,prf = normalise_proof id prf in + if debug then Printf.fprintf stdout "compiled proof %a\n" output_proof prf; + cmpl_proof env prf + +type prf_sys = (cstr_compat * prf_rule) list + + +let xlinear_prover sys = + match Fourier.find_point sys with + | Inr prf -> + if debug then Printf.printf "AProof : %a\n" pp_proof prf ; + let cert = (*List.map (fun (x,n) -> x+1,n)*) (fst (List.hd (Proof.mk_proof sys prf))) in + if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; + Some (rats_to_ints (Vect.to_list cert)) + | Inl _ -> None + + +let output_num o n = output_string o (string_of_num n) +let output_bigint o n = output_string o (string_of_big_int n) + +let proof_of_farkas prf cert = +(* Printf.printf "\nproof_of_farkas %a , %a \n" (pp_list output_prf_rule) prf (pp_list output_bigint) cert ; *) + let rec mk_farkas acc prf cert = + match prf, cert with + | _ , [] -> acc + | [] , _ -> failwith "proof_of_farkas : not enough hyps" + | p::prf,c::cert -> + mk_farkas (add_proof (mul_proof c p) acc) prf cert in + let res = mk_farkas Zero prf cert in + (*Printf.printf "==> %a" output_prf_rule res ; *) + res + + +let linear_prover sys = + let (sysi,prfi) = List.split sys in + match xlinear_prover sysi with + | None -> None + | Some cert -> Some (proof_of_farkas prfi cert) + +let linear_prover = + if debug + then + fun sys -> + Printf.printf "<linear_prover"; flush stdout ; + let res = linear_prover sys in + Printf.printf ">"; flush stdout ; + res + else linear_prover + + + + +(** A single constraint can be unsat for the following reasons: + - 0 >= c for c a negative constant + - 0 = c for c a non-zero constant + - e = c when the coeffs of e are all integers and c is rational +*) + +type checksat = + | Tauto (* Tautology *) + | Unsat of prf_rule (* Unsatisfiable *) + | Cut of cstr_compat * prf_rule (* Cutting plane *) + | Normalise of cstr_compat * prf_rule (* coefficients are relatively prime *) + + +(** [check_sat] + - detects constraints that are not satisfiable; + - normalises constraints and generate cuts. +*) + +let check_sat (cstr,prf) = + let {coeffs=coeffs ; op=op ; cst=cst} = cstr in + match coeffs with + | [] -> + if eval_op op (Int 0) cst then Tauto else Unsat prf + | _ -> + let gcdi = (gcd_list (List.map snd coeffs)) in + let gcd = Big_int gcdi in + if eq_num gcd (Int 1) + then Normalise(cstr,prf) + else + if sign_num (mod_num cst gcd) = 0 + then (* We can really normalise *) + begin + assert (sign_num gcd >=1 ) ; + let cstr = { + coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; + op = op ; cst = cst // gcd + } in + Normalise(cstr,Gcd(gcdi,prf)) + (* Normalise(cstr,CutPrf prf)*) + end + else + match op with + | Eq -> Unsat (CutPrf prf) + | Ge -> + let cstr = { + coeffs = List.map (fun (x,v) -> (x, v // gcd)) coeffs; + op = op ; cst = ceiling_num (cst // gcd) + } in Cut(cstr,CutPrf prf) + + +(** Proof generating pivoting over variable v *) +let pivot v (c1,p1) (c2,p2) = + let {coeffs = v1 ; op = op1 ; cst = n1} = c1 + and {coeffs = v2 ; op = op2 ; cst = n2} = c2 in + + + + (* Could factorise gcd... *) + let xpivot cv1 cv2 = + ( + {coeffs = Vect.add (Vect.mul cv1 v1) (Vect.mul cv2 v2) ; + op = Proof.add_op op1 op2 ; + cst = n1 */ cv1 +/ n2 */ cv2 }, + + AddPrf(mul_proof (numerator cv1) p1,mul_proof (numerator cv2) p2)) in + + match Vect.get v v1 , Vect.get v v2 with + | None , _ | _ , None -> None + | Some a , Some b -> + if (sign_num a) * (sign_num b) = -1 + then + let cv1 = abs_num b + and cv2 = abs_num a in + Some (xpivot cv1 cv2) + else + if op1 = Eq + then + let cv1 = minus_num (b */ (Int (sign_num a))) + and cv2 = abs_num a in + Some (xpivot cv1 cv2) + else if op2 = Eq + then + let cv1 = abs_num b + and cv2 = minus_num (a */ (Int (sign_num b))) in + Some (xpivot cv1 cv2) + else None (* op2 could be Eq ... this might happen *) + +exception FoundProof of prf_rule + +let rec simpl_sys sys = + List.fold_left (fun acc (c,p) -> + match check_sat (c,p) with + | Tauto -> acc + | Unsat prf -> raise (FoundProof prf) + | Cut(c,p) -> (c,p)::acc + | Normalise (c,p) -> (c,p)::acc) [] sys + + +(** [ext_gcd a b] is the extended Euclid algorithm. + [ext_gcd a b = (x,y,g)] iff [ax+by=g] + Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm +*) +let rec ext_gcd a b = + if sign_big_int b = 0 + then (unit_big_int,zero_big_int) + else + let (q,r) = quomod_big_int a b in + let (s,t) = ext_gcd b r in + (t, sub_big_int s (mult_big_int q t)) + + +let pp_ext_gcd a b = + let a' = big_int_of_int a in + let b' = big_int_of_int b in + + let (x,y) = ext_gcd a' b' in + Printf.fprintf stdout "%s * %s + %s * %s = %s\n" + (string_of_big_int x) (string_of_big_int a') + (string_of_big_int y) (string_of_big_int b') + (string_of_big_int (add_big_int (mult_big_int x a') (mult_big_int y b'))) + +exception Result of (int * (proof * cstr_compat)) + +let split_equations psys = + List.partition (fun (c,p) -> c.op = Eq) + + +let extract_coprime (c1,p1) (c2,p2) = + let rec exist2 vect1 vect2 = + match vect1 , vect2 with + | _ , [] | [], _ -> None + | (v1,n1)::vect1' , (v2, n2) :: vect2' -> + if v1 = v2 + then + if compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int = 0 + then Some (v1,n1,n2) + else + exist2 vect1' vect2' + else + if v1 < v2 + then exist2 vect1' vect2 + else exist2 vect1 vect2' in + + if c1.op = Eq && c2.op = Eq + then exist2 c1.coeffs c2.coeffs + else None + +let extract2 pred l = + let rec xextract2 rl l = + match l with + | [] -> (None,rl) (* Did not find *) + | e::l -> + match extract (pred e) l with + | None,_ -> xextract2 (e::rl) l + | Some (r,e'),l' -> Some (r,e,e'), List.rev_append rl l' in + + xextract2 [] l + + +let extract_coprime_equation psys = + extract2 extract_coprime psys + + +let apply_and_normalise f psys = + List.fold_left (fun acc pc' -> + match f pc' with + | None -> pc'::acc + | Some pc' -> + match check_sat pc' with + | Tauto -> acc + | Unsat prf -> raise (FoundProof prf) + | Cut(c,p) -> (c,p)::acc + | Normalise (c,p) -> (c,p)::acc + ) [] psys + + + + +let pivot_sys v pc psys = apply_and_normalise (pivot v pc) psys + + +let reduce_coprime psys = + let oeq,sys = extract_coprime_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some((v,n1,n2),(c1,p1),(c2,p2) ) -> + let (l1,l2) = ext_gcd (numerator n1) (numerator n2) in + let l1' = Big_int l1 and l2' = Big_int l2 in + let cstr = + {coeffs = Vect.add (Vect.mul l1' c1.coeffs) (Vect.mul l2' c2.coeffs); + op = Eq ; + cst = (l1' */ c1.cst) +/ (l2' */ c2.cst) + } in + let prf = add_proof (mul_proof (numerator l1') p1) (mul_proof (numerator l2') p2) in + + Some (pivot_sys v (cstr,prf) ((c1,p1)::sys)) + +(** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *) +let reduce_unary psys = + let is_unary_equation (cstr,prf) = + if cstr.op = Eq + then + try + Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs)) + with Not_found -> None + else None in + + let (oeq,sys) = extract is_unary_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + Some(pivot_sys v pc sys) + +let reduce_non_lin_unary psys = + + let is_unary_equation (cstr,prf) = + if cstr.op = Eq + then + try + let x = fst (List.find (fun (x,n) -> (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in + let x' = LinPoly.MonT.retrieve x in + if List.for_all (fun (y,_) -> y = x || snd (Monomial.div (LinPoly.MonT.retrieve y) x') = 0) cstr.coeffs + then Some x + else None + with Not_found -> None + else None in + + + let (oeq,sys) = extract is_unary_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + Some(apply_and_normalise (LinPoly.pivot_eq v pc) sys) + +let reduce_var_change psys = + + let rec rel_prime vect = + match vect with + | [] -> None + | (x,v)::vect -> + let v = numerator v in + try + let (x',v') = List.find (fun (_,v') -> + let v' = numerator v' in + eq_big_int (gcd_big_int v v') unit_big_int) vect in + Some ((x,v),(x',numerator v')) + with Not_found -> rel_prime vect in + + let rel_prime (cstr,prf) = if cstr.op = Eq then rel_prime cstr.coeffs else None in + + let (oeq,sys) = extract rel_prime psys in + + match oeq with + | None -> None + | Some(((x,v),(x',v')),(c,p)) -> + let (l1,l2) = ext_gcd v v' in + let l1,l2 = Big_int l1 , Big_int l2 in + + let get v vect = + match Vect.get v vect with + | None -> Int 0 + | Some n -> n in + + let pivot_eq (c',p') = + let {coeffs = coeffs ; op = op ; cst = cst} = c' in + let vx = get x coeffs in + let vx' = get x' coeffs in + let m = minus_num (vx */ l1 +/ vx' */ l2) in + Some ({coeffs = + Vect.add (Vect.mul m c.coeffs) coeffs ; op = op ; cst = m */ c.cst +/ cst} , + AddPrf(MulC(([], m),p),p')) in + + Some (apply_and_normalise pivot_eq sys) + + + + + let reduce_pivot psys = + let is_equation (cstr,prf) = + if cstr.op = Eq + then + try + Some (fst (List.hd cstr.coeffs)) + with Not_found -> None + else None in + let (oeq,sys) = extract is_equation psys in + match oeq with + | None -> None (* Nothing to do *) + | Some(v,pc) -> + if debug then + Printf.printf "Bad news : loss of completeness %a=%s" Vect.pp_vect (fst pc).coeffs (string_of_num (fst pc).cst); + Some(pivot_sys v pc sys) + + + + + + let iterate_until_stable f x = + let rec iter x = + match f x with + | None -> x + | Some x' -> iter x' in + iter x + + let rec app_funs l x = + match l with + | [] -> None + | f::fl -> + match f x with + | None -> app_funs fl x + | Some x' -> Some x' + + let reduction_equations psys = + iterate_until_stable (app_funs + [reduce_unary ; reduce_coprime ; + reduce_var_change (*; reduce_pivot*)]) psys + + let reduction_non_lin_equations psys = + iterate_until_stable (app_funs + [reduce_non_lin_unary (*; reduce_coprime ; + reduce_var_change ; reduce_pivot *)]) psys + + + + + (** [get_bound sys] returns upon success an interval (lb,e,ub) with proofs *) + let get_bound sys = + let is_small (v,i) = + match Itv.range i with + | None -> false + | Some i -> i <=/ (Int 1) in + + let select_best (x1,i1) (x2,i2) = + if Itv.smaller_itv i1 i2 + then (x1,i1) else (x2,i2) in + + (* For lia, there are no equations => these precautions are not needed *) + (* For nlia, there are equations => do not enumerate over equations! *) + let all_planes sys = + let (eq,ineq) = List.partition (fun c -> c.op = Eq) sys in + match eq with + | [] -> List.rev_map (fun c -> c.coeffs) ineq + | _ -> + List.fold_left (fun acc c -> + if List.exists (fun c' -> Vect.equal c.coeffs c'.coeffs) eq + then acc else c.coeffs ::acc) [] ineq in + + let smallest_interval = + List.fold_left + (fun acc vect -> + if is_small acc + then acc + else + match Fourier.optimise vect sys with + | None -> acc + | Some i -> + if debug then Printf.printf "Found a new bound %a" Vect.pp_vect vect ; + select_best (vect,i) acc) (Vect.null, (None,None)) (all_planes sys) in + let smallest_interval = + match smallest_interval + with + | (x,(Some i, Some j)) -> Some(i,x,j) + | x -> None (* This should not be possible *) + in + match smallest_interval with + | Some (lb,e,ub) -> + let (lbn,lbd) = (sub_big_int (numerator lb) unit_big_int, denominator lb) in + let (ubn,ubd) = (add_big_int unit_big_int (numerator ub) , denominator ub) in + (match + (* x <= ub -> x > ub *) + xlinear_prover ({coeffs = Vect.mul (Big_int ubd) e ; op = Ge ; cst = Big_int ubn} :: sys), + (* lb <= x -> lb > x *) + xlinear_prover + ({coeffs = Vect.mul (minus_num (Big_int lbd)) e ; op = Ge ; cst = minus_num (Big_int lbn)} :: sys) + with + | Some cub , Some clb -> Some(List.tl clb,(lb,e,ub), List.tl cub) + | _ -> failwith "Interval without proof" + ) + | None -> None + + + let check_sys sys = + List.for_all (fun (c,p) -> List.for_all (fun (_,n) -> sign_num n <> 0) c.coeffs) sys + + + let xlia reduction_equations sys = + + let rec enum_proof (id:int) (sys:prf_sys) : proof option = + if debug then (Printf.printf "enum_proof\n" ; flush stdout) ; + assert (check_sys sys) ; + + let nsys,prf = List.split sys in + match get_bound nsys with + | None -> None (* Is the systeme really unbounded ? *) + | Some(prf1,(lb,e,ub),prf2) -> + if debug then Printf.printf "Found interval: %a in [%s;%s] -> " Vect.pp_vect e (string_of_num lb) (string_of_num ub) ; + (match start_enum id e (ceiling_num lb) (floor_num ub) sys + with + | Some prfl -> + Some(Enum(id,proof_of_farkas prf prf1,e, proof_of_farkas prf prf2,prfl)) + | None -> None + ) + + and start_enum id e clb cub sys = + if clb >/ cub + then Some [] + else + let eq = {coeffs = e ; op = Eq ; cst = clb} in + match aux_lia (id+1) ((eq, Def id) :: sys) with + | None -> None + | Some prf -> + match start_enum id e (clb +/ (Int 1)) cub sys with + | None -> None + | Some l -> Some (prf::l) + + and aux_lia (id:int) (sys:prf_sys) : proof option = + assert (check_sys sys) ; + if debug then Printf.printf "xlia: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; + try + let sys = reduction_equations sys in + if debug then + Printf.printf "after reduction: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; + match linear_prover sys with + | Some prf -> Some (Step(id,prf,Done)) + | None -> enum_proof id sys + with FoundProof prf -> + (* [reduction_equations] can find a proof *) + Some(Step(id,prf,Done)) in + + (* let sys' = List.map (fun (p,o) -> Mc.norm0 p , o) sys in*) + let id = List.length sys in + let orpf = + try + let sys = simpl_sys sys in + aux_lia id sys + with FoundProof pr -> Some(Step(id,pr,Done)) in + match orpf with + | None -> None + | Some prf -> + (*Printf.printf "direct proof %a\n" output_proof prf ; *) + let env = mapi (fun _ i -> i) sys in + let prf = compile_proof env prf in + (*try + if Mc.zChecker sys' prf then Some prf else + raise Certificate.BadCertificate + with Failure s -> (Printf.printf "%s" s ; Some prf) + *) Some prf + + + let cstr_compat_of_poly (p,o) = + let (v,c) = LinPoly.linpol_of_pol p in + {coeffs = v ; op = o ; cst = minus_num c } + + + let lia sys = + let sys = List.map (develop_constraint z_spec) sys in + let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in + let sys = mapi (fun c i -> (c,Hyp i)) sys in + xlia reduction_equations sys + + + let nlia sys = + let sys = List.map (develop_constraint z_spec) sys in + let sys = mapi (fun c i -> (c,Hyp i)) sys in + + let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in + + let module MonMap = Map.Make(Monomial) in + + let collect_square = + List.fold_left (fun acc ((p,_),_) -> Poly.fold + (fun m _ acc -> + match Monomial.sqrt m with + | None -> acc + | Some s -> MonMap.add s m acc) p acc) MonMap.empty sys in + let sys = MonMap.fold (fun s m acc -> + let s = LinPoly.linpol_of_pol (Poly.add s (Int 1) (Poly.constant (Int 0))) in + let m = Poly.add m (Int 1) (Poly.constant (Int 0)) in + ((m, Ge), (Square s))::acc) collect_square sys in + +(* List.iter (fun ((p,_),_) -> Printf.printf "square %a\n" Poly.pp p) gen_square*) + + let sys = + if is_linear then sys + else sys @ (all_sym_pairs (fun ((c,o),p) ((c',o'),p') -> + ((Poly.product c c',opMult o o'), MulPrf(p,p'))) sys) in + + let sys = List.map (fun (c,p) -> cstr_compat_of_poly c,p) sys in + assert (check_sys sys) ; + xlia (if is_linear then reduction_equations else reduction_non_lin_equations) sys + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 877d468fd..687d24ac7 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -12,7 +12,7 @@ (* *) (* - Modules ISet, M, Mc, Env, Cache, CacheZ *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2009 *) +(* Frédéric Besson (Irisa/Inria) 2006-20011 *) (* *) (************************************************************************) @@ -125,7 +125,9 @@ let ff : 'cst cnf = [ [] ] * and the freeform formulas ('cst formula) that is retrieved from Coq. *) -type 'cst mc_cnf = ('cst Micromega.nFormula) list list +module Mc = Micromega + +type 'cst mc_cnf = ('cst Mc.nFormula) list list (** * From a freeform formula, build a cnf. @@ -134,7 +136,12 @@ type 'cst mc_cnf = ('cst Micromega.nFormula) list list * and RingMicromega.v). *) -let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) (f:'cst formula) = +type 'a tagged_option = T of tag list | S of 'a + +let cnf + (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) + (unsat : 'cst Mc.nFormula -> bool) (deduce : 'cst Mc.nFormula -> 'cst Mc.nFormula -> 'cst Mc.nFormula option) (f:'cst formula) = + let negate a t = List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in @@ -143,26 +150,79 @@ let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) let and_cnf x y = x @ y in - let or_clause_cnf t f = List.map (fun x -> t@x) f in +let rec add_term t0 = function + | [] -> + (match deduce (fst t0) (fst t0) with + | Some u -> if unsat u then T [snd t0] else S (t0::[]) + | None -> S (t0::[])) + | t'::cl0 -> + (match deduce (fst t0) (fst t') with + | Some u -> + if unsat u + then T [snd t0 ; snd t'] + else (match add_term t0 cl0 with + | S cl' -> S (t'::cl') + | T l -> T l) + | None -> + (match add_term t0 cl0 with + | S cl' -> S (t'::cl') + | T l -> T l)) in + + + let rec or_clause cl1 cl2 = + match cl1 with + | [] -> S cl2 + | t0::cl -> + (match add_term t0 cl2 with + | S cl' -> or_clause cl cl' + | T l -> T l) in + + + + let or_clause_cnf t f = + List.fold_right (fun e (acc,tg) -> + match or_clause t e with + | S cl -> (cl :: acc,tg) + | T l -> (acc,tg@l)) f ([],[]) in + let rec or_cnf f f' = match f with - | [] -> tt - | e :: rst -> (or_cnf rst f') @ (or_clause_cnf e f') in + | [] -> tt,[] + | e :: rst -> + let (rst_f',t) = or_cnf rst f' in + let (e_f', t') = or_clause_cnf e f' in + (rst_f' @ e_f', t @ t') in + let rec xcnf (polarity : bool) f = match f with - | TT -> if polarity then tt else ff - | FF -> if polarity then ff else tt - | X p -> if polarity then ff else ff - | A(x,t,_) -> if polarity then normalise x t else negate x t + | TT -> if polarity then (tt,[]) else (ff,[]) + | FF -> if polarity then (ff,[]) else (tt,[]) + | X p -> if polarity then (ff,[]) else (ff,[]) + | A(x,t,_) -> ((if polarity then normalise x t else negate x t),[]) | N(e) -> xcnf (not polarity) e - | C(e1,e2) -> - (if polarity then and_cnf else or_cnf) (xcnf polarity e1) (xcnf polarity e2) + | C(e1,e2) -> + let e1,t1 = xcnf polarity e1 in + let e2,t2 = xcnf polarity e2 in + if polarity + then and_cnf e1 e2, t1 @ t2 + else let f',t' = or_cnf e1 e2 in + (f', t1 @ t2 @ t') | D(e1,e2) -> - (if polarity then or_cnf else and_cnf) (xcnf polarity e1) (xcnf polarity e2) + let e1,t1 = xcnf polarity e1 in + let e2,t2 = xcnf polarity e2 in + if polarity + then let f',t' = or_cnf e1 e2 in + (f', t1 @ t2 @ t') + else and_cnf e1 e2, t1 @ t2 | I(e1,_,e2) -> - (if polarity then or_cnf else and_cnf) (xcnf (not polarity) e1) (xcnf polarity e2) in + let e1 , t1 = (xcnf (not polarity) e1) in + let e2 , t2 = (xcnf polarity e2) in + if polarity + then let f',t' = or_cnf e1 e2 in + (f', t1 @ t2 @ t') + else and_cnf e1 e2, t1 @ t2 in xcnf true f @@ -447,8 +507,6 @@ struct (* Access the Micromega module *) - module Mc = Micromega - (* parse/dump/print from numbers up to expressions and formulas *) let rec parse_nat term = @@ -513,7 +571,7 @@ struct | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|]) | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) - let pp_z o x = Printf.fprintf o "%i" (CoqToCaml.z x) + let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) let dump_num bd1 = Term.mkApp(Lazy.force coq_Qmake, @@ -1022,9 +1080,9 @@ let tags_of_clause tgs wit clause = | _ -> tgs in xtags tgs wit -let tags_of_cnf wits cnf = +(*let tags_of_cnf wits cnf = List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl) - Names.Idset.empty wits cnf + Names.Idset.empty wits cnf *) let find_witness prover polys1 = try_any prover polys1 @@ -1101,6 +1159,27 @@ let rec dump_proof_term = function [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) + +let rec size_of_psatz = function + | Micromega.PsatzIn _ -> 1 + | Micromega.PsatzSquare _ -> 1 + | Micromega.PsatzMulC(_,p) -> 1 + (size_of_psatz p) + | Micromega.PsatzMulE(p1,p2) | Micromega.PsatzAdd(p1,p2) -> size_of_psatz p1 + size_of_psatz p2 + | Micromega.PsatzC _ -> 1 + | Micromega.PsatzZ -> 1 + +let rec size_of_pf = function + | Micromega.DoneProof -> 1 + | Micromega.RatProof(p,a) -> (size_of_pf a) + (size_of_psatz p) + | Micromega.CutProof(p,a) -> (size_of_pf a) + (size_of_psatz p) + | Micromega.EnumProof(p1,p2,l) -> (size_of_psatz p1) + (size_of_psatz p2) + (List.fold_left (fun acc p -> size_of_pf p + acc) 0 l) + +let dump_proof_term t = + if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t) ; + dump_proof_term t + + + let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden @@ -1258,14 +1337,14 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let remap i = let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in List.assoc formula new_cl in - if debug then +(* if debug then begin Printf.printf "\ncompact_proof : %a %a %a" (pp_ml_list prover.pp_f) (List.map fst old_cl) prover.pp_prf prf (pp_ml_list prover.pp_f) (List.map fst new_cl) ; flush stdout - end ; + end ; *) let res = try prover.compact prf remap with x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) @@ -1337,7 +1416,7 @@ exception CsdpNotFound * prune unused fomulas, and finally modify the proof state. *) -let micromega_tauto negate normalise spec prover env polys1 polys2 gl = +let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = let spec = Lazy.force spec in (* Express the goal as one big implication *) @@ -1350,7 +1429,7 @@ let micromega_tauto negate normalise spec prover env polys1 polys2 gl = polys1 (polys2,[]) in (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *) - let cnf_ff = cnf negate normalise ff in + let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in if debug then begin @@ -1369,13 +1448,13 @@ let micromega_tauto negate normalise spec prover env polys1 polys2 gl = let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ; (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in - TagSet.union s tags) TagSet.empty (List.combine cnf_ff res) in + TagSet.union s tags) (List.fold_left (fun s i -> TagSet.add i s) TagSet.empty cnf_ff_tags) (List.combine cnf_ff res) in if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout; Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ; let ff' = abstract_formula hyps ff in - let cnf_ff' = cnf negate normalise ff' in + let cnf_ff',_ = cnf negate normalise unsat deduce ff' in if debug then begin @@ -1416,16 +1495,17 @@ let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) + unsat deduce spec prover gl = let concl = Tacmach.pf_concl gl in let hyps = Tacmach.pf_hyps_types gl in try let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in let env = Env.elements env in - micromega_tauto negate normalise spec prover env hyps concl gl + micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with - | Failure x -> flush stdout ; Pp.pp_flush () ; - Tacticals.tclFAIL 0 (Pp.str x) gl +(* | Failure x -> flush stdout ; Pp.pp_flush () ; + Tacticals.tclFAIL 0 (Pp.str x) gl *) | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; Tacticals.tclFAIL 0 (Pp.str @@ -1647,7 +1727,13 @@ module CacheZ = PHashtable(struct let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover) +let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia) +let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia) + +(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*) +(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*) + + let linear_Z = { name = "lia"; @@ -1658,50 +1744,79 @@ let linear_Z = { pp_f = fun o x -> pp_pol pp_z o (fst x) } +let nlinear_Z = { + name = "nlia"; + prover = memo_nlia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) +} + + + +let tauto_lia ff = + let prover = linear_Z in + let cnf_ff,_ = cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce ff in + match witness_list_tags [prover] cnf_ff with + | None -> None + | Some l -> Some (List.map fst l) + + (** * Functions instantiating micromega_gen with the appropriate theories and * solvers *) let psatzl_Z gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_prover_Z ] gl let psatzl_Q gl = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ linear_prover_Q ] gl let psatz_Q i gl = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl let psatzl_R gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec + micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec [ linear_prover_R ] gl let psatz_R i gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec + micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl let psatz_Z i gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec + [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl let sos_Z gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ non_linear_prover_Z "pure_sos" None ] gl let sos_Q gl = - micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "pure_sos" None ] gl let sos_R gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec + micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec [ non_linear_prover_R "pure_sos" None ] gl let xlia gl = - micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [ linear_Z ] gl + try + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec + [ linear_Z ] gl + with z -> Printexc.print_backtrace stdout ; raise z + +let xnlia gl = + try + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec + [ nlinear_Z ] gl + with z -> Printexc.print_backtrace stdout ; raise z + + (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index f5314df5c..1604b0eb1 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -28,7 +28,7 @@ type csdp_certificate = S of Sos_types.positivstellensatz option | F of string type provername = string * int option -let debug = true +let debug = false let flags = [Open_append;Open_binary;Open_creat] let chan = open_out_gen flags 0o666 "trace" diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 20fcd9720..3b6b69879 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -35,6 +35,11 @@ TACTIC EXTEND ZOmicron [ "xlia" ] -> [ Coq_micromega.xlia] END +TACTIC EXTEND Nlia +[ "xnlia" ] -> [ Coq_micromega.xnlia] +END + + TACTIC EXTEND Sos_Z | [ "sos_Z" ] -> [ Coq_micromega.sos_Z] diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 6250e324a..d9201722d 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -1,5 +1,8 @@ open Num module Utils = Mutils +open Polynomial +open Vect + let map_option = Utils.map_option let from_option = Utils.from_option @@ -7,132 +10,6 @@ let from_option = Utils.from_option let debug = false type ('a,'b) lr = Inl of 'a | Inr of 'b - -module Vect = - struct - (** [t] is the type of vectors. - A vector [(x1,v1) ; ... ; (xn,vn)] is such that: - - variables indexes are ordered (x1 < ... < xn - - values are all non-zero - *) - type var = int - type t = (var * num) list - -(** [equal v1 v2 = true] if the vectors are syntactically equal. - ([num] is not handled by [Pervasives.equal] *) - - let rec equal v1 v2 = - match v1 , v2 with - | [] , [] -> true - | [] , _ -> false - | _::_ , [] -> false - | (i1,n1)::v1 , (i2,n2)::v2 -> - (i1 = i2) && n1 =/ n2 && equal v1 v2 - - let hash v = - let rec hash i = function - | [] -> i - | (vr,vl)::l -> hash (i + (Hashtbl.hash (vr, float_of_num vl))) l in - Hashtbl.hash (hash 0 v ) - - - let null = [] - - let pp_vect o vect = - List.iter (fun (v,n) -> Printf.printf "%sx%i + " (string_of_num n) v) vect - - let from_list (l: num list) = - let rec xfrom_list i l = - match l with - | [] -> [] - | e::l -> - if e <>/ Int 0 - then (i,e)::(xfrom_list (i+1) l) - else xfrom_list (i+1) l in - - xfrom_list 0 l - - let zero_num = Int 0 - let unit_num = Int 1 - - - let to_list m = - let rec xto_list i l = - match l with - | [] -> [] - | (x,v)::l' -> - if i = x then v::(xto_list (i+1) l') else zero_num ::(xto_list (i+1) l) in - xto_list 0 m - - - let cons i v rst = if v =/ Int 0 then rst else (i,v)::rst - - let rec update i f t = - match t with - | [] -> cons i (f zero_num) [] - | (k,v)::l -> - match Pervasives.compare i k with - | 0 -> cons k (f v) l - | -1 -> cons i (f zero_num) t - | 1 -> (k,v) ::(update i f l) - | _ -> failwith "compare_num" - - let rec set i n t = - match t with - | [] -> cons i n [] - | (k,v)::l -> - match Pervasives.compare i k with - | 0 -> cons k n l - | -1 -> cons i n t - | 1 -> (k,v) :: (set i n l) - | _ -> failwith "compare_num" - - let gcd m = - let res = List.fold_left (fun x (i,e) -> Big_int.gcd_big_int x (Utils.numerator e)) Big_int.zero_big_int m in - if Big_int.compare_big_int res Big_int.zero_big_int = 0 - then Big_int.unit_big_int else res - - let rec mul z t = - match z with - | Int 0 -> [] - | Int 1 -> t - | _ -> List.map (fun (i,n) -> (i, mult_num z n)) t - - let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical - [ - (fun () -> Pervasives.compare (fst x) (fst y)); - (fun () -> compare_num (snd x) (snd y))]) - - (** [tail v vect] returns - - [None] if [v] is not a variable of the vector [vect] - - [Some(vl,rst)] where [vl] is the value of [v] in vector [vect] - and [rst] is the remaining of the vector - We exploit that vectors are ordered lists - *) - let rec tail (v:var) (vect:t) = - match vect with - | [] -> None - | (v',vl)::vect' -> - match Pervasives.compare v' v with - | 0 -> Some (vl,vect) (* Ok, found *) - | -1 -> tail v vect' (* Might be in the tail *) - | _ -> None (* Hopeless *) - - let get v vect = - match tail v vect with - | None -> None - | Some(vl,_) -> Some vl - - - let rec fresh v = - match v with - | [] -> 1 - | [v,_] -> v + 1 - | _::v -> fresh v - - end -open Vect - (** Implementation of intervals *) module Itv = struct @@ -203,11 +80,11 @@ let in_bound bnd v = | Some a , None -> a <=/ v | Some a , Some b -> a <=/ v && v <=/ b + end open Itv type vector = Vect.t -type cstr = { coeffs : vector ; bound : interval } (** 'cstr' is the type of constraints. {coeffs = v ; bound = (l,r) } models the constraints l <= v <= r **) @@ -275,10 +152,6 @@ let pp_bound o = function let pp_itv o (l,r) = Printf.fprintf o "(%a,%a)" pp_bound l pp_bound r -let rec pp_list f o l = - match l with - | [] -> () - | e::l -> f o e ; output_string o ";" ; pp_list f o l let pp_iset o s = output_string o "{" ; @@ -366,12 +239,7 @@ let normalise_cstr vect cinfo = then{cinfo with bound = (map_option divn l , map_option divn r) } else {cinfo with pos = cinfo.neg ; neg = cinfo.pos ; bound = (map_option divn r , map_option divn l)}) -(** For compatibility, there an external representation of constraints *) - -type cstr_compat = {coeffs : vector ; op : op ; cst : num} -and op = |Eq | Ge - -let string_of_op = function Eq -> "=" | Ge -> ">=" +(** For compatibility, there is an external representation of constraints *) let eval_op = function @@ -653,7 +521,7 @@ let solve_sys black_v choose_eq choose_variable sys sys_l = let vars = choose_variable sys in try let (v,est) = (List.find (fun (v,_) -> v <> black_v) vars) in - if debug then (Printf.printf "\nV : %i esimate %f\n" v est ; flush stdout) ; + if debug then (Printf.printf "\nV : %i estimate %f\n" v est ; flush stdout) ; let sys' = project v sys in solve_sys sys' ((v,sys)::sys_l) with Not_found -> (* we are done *) Inl (sys,sys_l) in @@ -666,7 +534,7 @@ let solve black_v choose_eq choose_variable cstrs = try let sys = load_system cstrs in -(* Printf.printf "solve :\n %a" pp_system sys.sys ; *) + if debug then Printf.printf "solve :\n %a" pp_system sys.sys ; solve_sys black_v choose_eq choose_variable sys [] with SystemContradiction prf -> Inr prf @@ -752,20 +620,33 @@ struct else if i < v then unroll_until v rl else (false,l) + let rec choose_simple_equation eqs = + match eqs with + | [] -> None + | (vect,a,prf,ln)::eqs -> + match vect with + | [i,_] -> Some (i,vect,a,prf,ln) + | _ -> choose_simple_equation eqs + + + let choose_primal_equation eqs sys_l = + (* Counts the number of equations refering to variable [v] -- + It looks like nb_cst is dead... + *) let is_primal_equation_var v = - List.fold_left (fun (nb_eq,nb_cst) (vect,info) -> + List.fold_left (fun nb_eq (vect,info) -> if fst (unroll_until v vect) - then if itv_point info.bound then (nb_eq + 1,nb_cst) else (nb_eq,nb_cst) - else (nb_eq,nb_cst)) (0,0) sys_l in + then if itv_point info.bound then nb_eq + 1 else nb_eq + else nb_eq) 0 sys_l in let rec find_var vect = match vect with | [] -> None | (i,_)::vect -> - let (nb_eq,nb_cst) = is_primal_equation_var i in - if nb_eq = 2 && nb_cst = 0 + let nb_eq = is_primal_equation_var i in + if nb_eq = 2 then Some i else find_var vect in let rec find_eq_var eqs = @@ -776,10 +657,9 @@ struct | None -> find_eq_var l | Some r -> Some (r,vect,a,prf,ln) in - - - find_eq_var eqs - + match choose_simple_equation eqs with + | None -> find_eq_var eqs + | Some res -> Some res @@ -913,7 +793,8 @@ struct | None , _ | _ , None -> None | Some a , Some b -> if (sign_num a) * (sign_num b) = -1 - then Some (add (p1,abs_num a) (p2,abs_num b) , + then + Some (add (p1,abs_num a) (p2,abs_num b) , {coeffs = add (v1,abs_num a) (v2,abs_num b) ; op = add_op op1 op2 ; cst = n1 // (abs_num a) +/ n2 // (abs_num b) }) diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index c350ed0f6..39b6cd2a3 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1,308 +1,323 @@ (** val negb : bool -> bool **) let negb = function - | true -> false - | false -> true +| true -> false +| false -> true type nat = - | O - | S of nat +| O +| S of nat type comparison = - | Eq - | Lt - | Gt +| Eq +| Lt +| Gt (** val compOpp : comparison -> comparison **) let compOpp = function - | Eq -> Eq - | Lt -> Gt - | Gt -> Lt - -(** val plus : nat -> nat -> nat **) - -let rec plus n0 m = - match n0 with - | O -> m - | S p -> S (plus p m) +| Eq -> Eq +| Lt -> Gt +| Gt -> Lt (** val app : 'a1 list -> 'a1 list -> 'a1 list **) let rec app l m = match l with - | [] -> m - | a :: l1 -> a :: (app l1 m) + | [] -> m + | a::l1 -> a::(app l1 m) -(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **) +(** val plus : nat -> nat -> nat **) -let rec nth n0 l default = +let rec plus n0 m = match n0 with - | O -> (match l with - | [] -> default - | x :: l' -> x) - | S m -> (match l with - | [] -> default - | x :: t0 -> nth m t0 default) - -(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) - -let rec map f = function - | [] -> [] - | a :: t0 -> (f a) :: (map f t0) + | O -> m + | S p -> S (plus p m) type positive = - | XI of positive - | XO of positive - | XH +| XI of positive +| XO of positive +| XH (** val psucc : positive -> positive **) let rec psucc = function - | XI p -> XO (psucc p) - | XO p -> XI p - | XH -> XO XH +| XI p -> XO (psucc p) +| XO p -> XI p +| XH -> XO XH (** val pplus : positive -> positive -> positive **) let rec pplus x y = match x with - | XI p -> - (match y with - | XI q0 -> XO (pplus_carry p q0) - | XO q0 -> XI (pplus p q0) - | XH -> XO (psucc p)) - | XO p -> - (match y with - | XI q0 -> XI (pplus p q0) - | XO q0 -> XO (pplus p q0) - | XH -> XI p) - | XH -> - (match y with - | XI q0 -> XO (psucc q0) - | XO q0 -> XI q0 - | XH -> XO XH) + | XI p -> + (match y with + | XI q0 -> XO (pplus_carry p q0) + | XO q0 -> XI (pplus p q0) + | XH -> XO (psucc p)) + | XO p -> + (match y with + | XI q0 -> XI (pplus p q0) + | XO q0 -> XO (pplus p q0) + | XH -> XI p) + | XH -> + (match y with + | XI q0 -> XO (psucc q0) + | XO q0 -> XI q0 + | XH -> XO XH) (** val pplus_carry : positive -> positive -> positive **) and pplus_carry x y = match x with - | XI p -> - (match y with - | XI q0 -> XI (pplus_carry p q0) - | XO q0 -> XO (pplus_carry p q0) - | XH -> XI (psucc p)) - | XO p -> - (match y with - | XI q0 -> XO (pplus_carry p q0) - | XO q0 -> XI (pplus p q0) - | XH -> XO (psucc p)) - | XH -> - (match y with - | XI q0 -> XI (psucc q0) - | XO q0 -> XO (psucc q0) - | XH -> XI XH) + | XI p -> + (match y with + | XI q0 -> XI (pplus_carry p q0) + | XO q0 -> XO (pplus_carry p q0) + | XH -> XI (psucc p)) + | XO p -> + (match y with + | XI q0 -> XO (pplus_carry p q0) + | XO q0 -> XI (pplus p q0) + | XH -> XO (psucc p)) + | XH -> + (match y with + | XI q0 -> XI (psucc q0) + | XO q0 -> XO (psucc q0) + | XH -> XI XH) (** val p_of_succ_nat : nat -> positive **) let rec p_of_succ_nat = function - | O -> XH - | S x -> psucc (p_of_succ_nat x) +| O -> XH +| S x -> psucc (p_of_succ_nat x) (** val pdouble_minus_one : positive -> positive **) let rec pdouble_minus_one = function - | XI p -> XI (XO p) - | XO p -> XI (pdouble_minus_one p) - | XH -> XH +| XI p -> XI (XO p) +| XO p -> XI (pdouble_minus_one p) +| XH -> XH type positive_mask = - | IsNul - | IsPos of positive - | IsNeg +| IsNul +| IsPos of positive +| IsNeg (** val pdouble_plus_one_mask : positive_mask -> positive_mask **) let pdouble_plus_one_mask = function - | IsNul -> IsPos XH - | IsPos p -> IsPos (XI p) - | IsNeg -> IsNeg +| IsNul -> IsPos XH +| IsPos p -> IsPos (XI p) +| IsNeg -> IsNeg (** val pdouble_mask : positive_mask -> positive_mask **) let pdouble_mask = function - | IsNul -> IsNul - | IsPos p -> IsPos (XO p) - | IsNeg -> IsNeg +| IsPos p -> IsPos (XO p) +| x0 -> x0 (** val pdouble_minus_two : positive -> positive_mask **) let pdouble_minus_two = function - | XI p -> IsPos (XO (XO p)) - | XO p -> IsPos (XO (pdouble_minus_one p)) - | XH -> IsNul +| XI p -> IsPos (XO (XO p)) +| XO p -> IsPos (XO (pdouble_minus_one p)) +| XH -> IsNul (** val pminus_mask : positive -> positive -> positive_mask **) let rec pminus_mask x y = match x with - | XI p -> - (match y with - | XI q0 -> pdouble_mask (pminus_mask p q0) - | XO q0 -> pdouble_plus_one_mask (pminus_mask p q0) - | XH -> IsPos (XO p)) - | XO p -> - (match y with - | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_mask (pminus_mask p q0) - | XH -> IsPos (pdouble_minus_one p)) - | XH -> (match y with - | XH -> IsNul - | _ -> IsNeg) + | XI p -> + (match y with + | XI q0 -> pdouble_mask (pminus_mask p q0) + | XO q0 -> pdouble_plus_one_mask (pminus_mask p q0) + | XH -> IsPos (XO p)) + | XO p -> + (match y with + | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) + | XO q0 -> pdouble_mask (pminus_mask p q0) + | XH -> IsPos (pdouble_minus_one p)) + | XH -> + (match y with + | XH -> IsNul + | _ -> IsNeg) (** val pminus_mask_carry : positive -> positive -> positive_mask **) and pminus_mask_carry x y = match x with - | XI p -> - (match y with - | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_mask (pminus_mask p q0) - | XH -> IsPos (pdouble_minus_one p)) - | XO p -> - (match y with - | XI q0 -> pdouble_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XH -> pdouble_minus_two p) - | XH -> IsNeg + | XI p -> + (match y with + | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) + | XO q0 -> pdouble_mask (pminus_mask p q0) + | XH -> IsPos (pdouble_minus_one p)) + | XO p -> + (match y with + | XI q0 -> pdouble_mask (pminus_mask_carry p q0) + | XO q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) + | XH -> pdouble_minus_two p) + | XH -> IsNeg (** val pminus : positive -> positive -> positive **) let pminus x y = match pminus_mask x y with - | IsPos z0 -> z0 - | _ -> XH + | IsPos z0 -> z0 + | _ -> XH (** val pmult : positive -> positive -> positive **) let rec pmult x y = match x with - | XI p -> pplus y (XO (pmult p y)) - | XO p -> XO (pmult p y) - | XH -> y + | XI p -> pplus y (XO (pmult p y)) + | XO p -> XO (pmult p y) + | XH -> y + +(** val psize : positive -> nat **) + +let rec psize = function +| XI p2 -> S (psize p2) +| XO p2 -> S (psize p2) +| XH -> S O (** val pcompare : positive -> positive -> comparison -> comparison **) let rec pcompare x y r = match x with - | XI p -> - (match y with - | XI q0 -> pcompare p q0 r - | XO q0 -> pcompare p q0 Gt - | XH -> Gt) - | XO p -> - (match y with - | XI q0 -> pcompare p q0 Lt - | XO q0 -> pcompare p q0 r - | XH -> Gt) - | XH -> (match y with - | XH -> r - | _ -> Lt) + | XI p -> + (match y with + | XI q0 -> pcompare p q0 r + | XO q0 -> pcompare p q0 Gt + | XH -> Gt) + | XO p -> + (match y with + | XI q0 -> pcompare p q0 Lt + | XO q0 -> pcompare p q0 r + | XH -> Gt) + | XH -> + (match y with + | XH -> r + | _ -> Lt) -(** val psize : positive -> nat **) +type n = +| N0 +| Npos of positive -let rec psize = function - | XI p2 -> S (psize p2) - | XO p2 -> S (psize p2) - | XH -> S O +(** val n_of_nat : nat -> n **) -type n = - | N0 - | Npos of positive +let n_of_nat = function +| O -> N0 +| S n' -> Npos (p_of_succ_nat n') (** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) let rec pow_pos rmul x = function - | XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p) - | XO i0 -> let p = pow_pos rmul x i0 in rmul p p - | XH -> x +| XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p) +| XO i0 -> let p = pow_pos rmul x i0 in rmul p p +| XH -> x + +(** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **) + +let rec nth n0 l default = + match n0 with + | O -> + (match l with + | [] -> default + | x::l' -> x) + | S m -> + (match l with + | [] -> default + | x::t0 -> nth m t0 default) + +(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) + +let rec map f = function +| [] -> [] +| a::t0 -> (f a)::(map f t0) + +(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) + +let rec fold_right f a0 = function +| [] -> a0 +| b::t0 -> f b (fold_right f a0 t0) type z = - | Z0 - | Zpos of positive - | Zneg of positive +| Z0 +| Zpos of positive +| Zneg of positive (** val zdouble_plus_one : z -> z **) let zdouble_plus_one = function - | Z0 -> Zpos XH - | Zpos p -> Zpos (XI p) - | Zneg p -> Zneg (pdouble_minus_one p) +| Z0 -> Zpos XH +| Zpos p -> Zpos (XI p) +| Zneg p -> Zneg (pdouble_minus_one p) (** val zdouble_minus_one : z -> z **) let zdouble_minus_one = function - | Z0 -> Zneg XH - | Zpos p -> Zpos (pdouble_minus_one p) - | Zneg p -> Zneg (XI p) +| Z0 -> Zneg XH +| Zpos p -> Zpos (pdouble_minus_one p) +| Zneg p -> Zneg (XI p) (** val zdouble : z -> z **) let zdouble = function - | Z0 -> Z0 - | Zpos p -> Zpos (XO p) - | Zneg p -> Zneg (XO p) +| Z0 -> Z0 +| Zpos p -> Zpos (XO p) +| Zneg p -> Zneg (XO p) (** val zPminus : positive -> positive -> z **) let rec zPminus x y = match x with - | XI p -> - (match y with - | XI q0 -> zdouble (zPminus p q0) - | XO q0 -> zdouble_plus_one (zPminus p q0) - | XH -> Zpos (XO p)) - | XO p -> - (match y with - | XI q0 -> zdouble_minus_one (zPminus p q0) - | XO q0 -> zdouble (zPminus p q0) - | XH -> Zpos (pdouble_minus_one p)) - | XH -> - (match y with - | XI q0 -> Zneg (XO q0) - | XO q0 -> Zneg (pdouble_minus_one q0) - | XH -> Z0) + | XI p -> + (match y with + | XI q0 -> zdouble (zPminus p q0) + | XO q0 -> zdouble_plus_one (zPminus p q0) + | XH -> Zpos (XO p)) + | XO p -> + (match y with + | XI q0 -> zdouble_minus_one (zPminus p q0) + | XO q0 -> zdouble (zPminus p q0) + | XH -> Zpos (pdouble_minus_one p)) + | XH -> + (match y with + | XI q0 -> Zneg (XO q0) + | XO q0 -> Zneg (pdouble_minus_one q0) + | XH -> Z0) (** val zplus : z -> z -> z **) let zplus x y = match x with - | Z0 -> y - | Zpos x' -> - (match y with - | Z0 -> Zpos x' - | Zpos y' -> Zpos (pplus x' y') - | Zneg y' -> - (match pcompare x' y' Eq with - | Eq -> Z0 - | Lt -> Zneg (pminus y' x') - | Gt -> Zpos (pminus x' y'))) - | Zneg x' -> - (match y with - | Z0 -> Zneg x' - | Zpos y' -> - (match pcompare x' y' Eq with - | Eq -> Z0 - | Lt -> Zpos (pminus y' x') - | Gt -> Zneg (pminus x' y')) - | Zneg y' -> Zneg (pplus x' y')) + | Z0 -> y + | Zpos x' -> + (match y with + | Z0 -> Zpos x' + | Zpos y' -> Zpos (pplus x' y') + | Zneg y' -> + (match pcompare x' y' Eq with + | Eq -> Z0 + | Lt -> Zneg (pminus y' x') + | Gt -> Zpos (pminus x' y'))) + | Zneg x' -> + (match y with + | Z0 -> Zneg x' + | Zpos y' -> + (match pcompare x' y' Eq with + | Eq -> Z0 + | Lt -> Zpos (pminus y' x') + | Gt -> Zneg (pminus x' y')) + | Zneg y' -> Zneg (pplus x' y')) (** val zopp : z -> z **) let zopp = function - | Z0 -> Z0 - | Zpos x0 -> Zneg x0 - | Zneg x0 -> Zpos x0 +| Z0 -> Z0 +| Zpos x0 -> Zneg x0 +| Zneg x0 -> Zpos x0 (** val zminus : z -> z -> z **) @@ -313,135 +328,172 @@ let zminus m n0 = let zmult x y = match x with - | Z0 -> Z0 - | Zpos x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zpos (pmult x' y') - | Zneg y' -> Zneg (pmult x' y')) - | Zneg x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zneg (pmult x' y') - | Zneg y' -> Zpos (pmult x' y')) + | Z0 -> Z0 + | Zpos x' -> + (match y with + | Z0 -> Z0 + | Zpos y' -> Zpos (pmult x' y') + | Zneg y' -> Zneg (pmult x' y')) + | Zneg x' -> + (match y with + | Z0 -> Z0 + | Zpos y' -> Zneg (pmult x' y') + | Zneg y' -> Zpos (pmult x' y')) (** val zcompare : z -> z -> comparison **) let zcompare x y = match x with - | Z0 -> (match y with - | Z0 -> Eq - | Zpos y' -> Lt - | Zneg y' -> Gt) - | Zpos x' -> (match y with - | Zpos y' -> pcompare x' y' Eq - | _ -> Gt) - | Zneg x' -> - (match y with - | Zneg y' -> compOpp (pcompare x' y' Eq) - | _ -> Lt) + | Z0 -> + (match y with + | Z0 -> Eq + | Zpos y' -> Lt + | Zneg y' -> Gt) + | Zpos x' -> + (match y with + | Zpos y' -> pcompare x' y' Eq + | _ -> Gt) + | Zneg x' -> + (match y with + | Zneg y' -> compOpp (pcompare x' y' Eq) + | _ -> Lt) -(** val zabs : z -> z **) +(** val zmax : z -> z -> z **) -let zabs = function - | Z0 -> Z0 - | Zpos p -> Zpos p - | Zneg p -> Zpos p +let zmax n0 m = + match zcompare n0 m with + | Lt -> m + | _ -> n0 -(** val zmax : z -> z -> z **) +(** val zabs : z -> z **) -let zmax m n0 = - match zcompare m n0 with - | Lt -> n0 - | _ -> m +let zabs = function +| Zneg p -> Zpos p +| x -> x (** val zle_bool : z -> z -> bool **) let zle_bool x y = match zcompare x y with - | Gt -> false - | _ -> true + | Gt -> false + | _ -> true (** val zge_bool : z -> z -> bool **) let zge_bool x y = match zcompare x y with - | Lt -> false - | _ -> true + | Lt -> false + | _ -> true (** val zgt_bool : z -> z -> bool **) let zgt_bool x y = match zcompare x y with - | Gt -> true - | _ -> false + | Gt -> true + | _ -> false (** val zeq_bool : z -> z -> bool **) let zeq_bool x y = match zcompare x y with - | Eq -> true - | _ -> false + | Eq -> true + | _ -> false -(** val n_of_nat : nat -> n **) +(** val pgcdn : nat -> positive -> positive -> positive **) -let n_of_nat = function - | O -> N0 - | S n' -> Npos (p_of_succ_nat n') +let rec pgcdn n0 a b = + match n0 with + | O -> XH + | S n1 -> + (match a with + | XI a' -> + (match b with + | XI b' -> + (match pcompare a' b' Eq with + | Eq -> a + | Lt -> pgcdn n1 (pminus b' a') a + | Gt -> pgcdn n1 (pminus a' b') b) + | XO b0 -> pgcdn n1 a b0 + | XH -> XH) + | XO a0 -> + (match b with + | XI p -> pgcdn n1 a0 b + | XO b0 -> XO (pgcdn n1 a0 b0) + | XH -> XH) + | XH -> XH) -(** val zdiv_eucl_POS : positive -> z -> z * z **) +(** val pgcd : positive -> positive -> positive **) + +let pgcd a b = + pgcdn (plus (psize a) (psize b)) a b + +(** val zgcd : z -> z -> z **) + +let zgcd a b = + match a with + | Z0 -> zabs b + | Zpos a0 -> + (match b with + | Z0 -> zabs a + | Zpos b0 -> Zpos (pgcd a0 b0) + | Zneg b0 -> Zpos (pgcd a0 b0)) + | Zneg a0 -> + (match b with + | Z0 -> zabs a + | Zpos b0 -> Zpos (pgcd a0 b0) + | Zneg b0 -> Zpos (pgcd a0 b0)) + +(** val zdiv_eucl_POS : positive -> z -> z * z **) let rec zdiv_eucl_POS a b = match a with - | XI a' -> - let q0 , r = zdiv_eucl_POS a' b in - let r' = zplus (zmult (Zpos (XO XH)) r) (Zpos XH) in - if zgt_bool b r' - then (zmult (Zpos (XO XH)) q0) , r' - else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)) , (zminus r' b) - | XO a' -> - let q0 , r = zdiv_eucl_POS a' b in - let r' = zmult (Zpos (XO XH)) r in - if zgt_bool b r' - then (zmult (Zpos (XO XH)) q0) , r' - else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)) , (zminus r' b) - | XH -> - if zge_bool b (Zpos (XO XH)) then Z0 , (Zpos XH) else (Zpos XH) , Z0 - -(** val zdiv_eucl : z -> z -> z * z **) + | XI a' -> + let q0,r = zdiv_eucl_POS a' b in + let r' = zplus (zmult (Zpos (XO XH)) r) (Zpos XH) in + if zgt_bool b r' + then (zmult (Zpos (XO XH)) q0),r' + else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),(zminus r' b) + | XO a' -> + let q0,r = zdiv_eucl_POS a' b in + let r' = zmult (Zpos (XO XH)) r in + if zgt_bool b r' + then (zmult (Zpos (XO XH)) q0),r' + else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),(zminus r' b) + | XH -> if zge_bool b (Zpos (XO XH)) then Z0,(Zpos XH) else (Zpos XH),Z0 + +(** val zdiv_eucl : z -> z -> z * z **) let zdiv_eucl a b = match a with - | Z0 -> Z0 , Z0 - | Zpos a' -> - (match b with - | Z0 -> Z0 , Z0 - | Zpos p -> zdiv_eucl_POS a' b - | Zneg b' -> - let q0 , r = zdiv_eucl_POS a' (Zpos b') in - (match r with - | Z0 -> (zopp q0) , Z0 - | _ -> (zopp (zplus q0 (Zpos XH))) , (zplus b r))) - | Zneg a' -> - (match b with - | Z0 -> Z0 , Z0 - | Zpos p -> - let q0 , r = zdiv_eucl_POS a' b in - (match r with - | Z0 -> (zopp q0) , Z0 - | _ -> (zopp (zplus q0 (Zpos XH))) , (zminus b r)) - | Zneg b' -> - let q0 , r = zdiv_eucl_POS a' (Zpos b') in q0 , (zopp r)) + | Z0 -> Z0,Z0 + | Zpos a' -> + (match b with + | Z0 -> Z0,Z0 + | Zpos p -> zdiv_eucl_POS a' b + | Zneg b' -> + let q0,r = zdiv_eucl_POS a' (Zpos b') in + (match r with + | Z0 -> (zopp q0),Z0 + | _ -> (zopp (zplus q0 (Zpos XH))),(zplus b r))) + | Zneg a' -> + (match b with + | Z0 -> Z0,Z0 + | Zpos p -> + let q0,r = zdiv_eucl_POS a' b in + (match r with + | Z0 -> (zopp q0),Z0 + | _ -> (zopp (zplus q0 (Zpos XH))),(zminus b r)) + | Zneg b' -> let q0,r = zdiv_eucl_POS a' (Zpos b') in q0,(zopp r)) (** val zdiv : z -> z -> z **) let zdiv a b = - let q0 , x = zdiv_eucl a b in q0 + let q0,x = zdiv_eucl a b in q0 type 'c pol = - | Pc of 'c - | Pinj of positive * 'c pol - | PX of 'c pol * positive * 'c pol +| Pc of 'c +| Pinj of positive * 'c pol +| PX of 'c pol * positive * 'c pol (** val p0 : 'a1 -> 'a1 pol **) @@ -457,49 +509,49 @@ let p1 cI = let rec peq ceqb p p' = match p with - | Pc c -> (match p' with - | Pc c' -> ceqb c c' - | _ -> false) - | Pinj (j, q0) -> - (match p' with - | Pinj (j', q') -> - (match pcompare j j' Eq with - | Eq -> peq ceqb q0 q' - | _ -> false) - | _ -> false) - | PX (p2, i, q0) -> - (match p' with - | PX (p'0, i', q') -> - (match pcompare i i' Eq with - | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false - | _ -> false) - | _ -> false) + | Pc c -> + (match p' with + | Pc c' -> ceqb c c' + | _ -> false) + | Pinj (j, q0) -> + (match p' with + | Pinj (j', q') -> + (match pcompare j j' Eq with + | Eq -> peq ceqb q0 q' + | _ -> false) + | _ -> false) + | PX (p2, i, q0) -> + (match p' with + | PX (p'0, i', q') -> + (match pcompare i i' Eq with + | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false + | _ -> false) + | _ -> false) + +(** val mkPinj : positive -> 'a1 pol -> 'a1 pol **) + +let mkPinj j p = match p with +| Pc c -> p +| Pinj (j', q0) -> Pinj ((pplus j j'), q0) +| PX (p2, p3, p4) -> Pinj (j, p) (** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) let mkPinj_pred j p = match j with - | XI j0 -> Pinj ((XO j0), p) - | XO j0 -> Pinj ((pdouble_minus_one j0), p) - | XH -> p + | XI j0 -> Pinj ((XO j0), p) + | XO j0 -> Pinj ((pdouble_minus_one j0), p) + | XH -> p (** val mkPX : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let mkPX cO ceqb p i q0 = match p with - | Pc c -> - if ceqb c cO - then (match q0 with - | Pc c0 -> q0 - | Pinj (j', q1) -> Pinj ((pplus XH j'), q1) - | PX (p2, p3, p4) -> Pinj (XH, q0)) - else PX (p, i, q0) - | Pinj (p2, p3) -> PX (p, i, q0) - | PX (p', i', q') -> - if peq ceqb q' (p0 cO) - then PX (p', (pplus i' i), q0) - else PX (p, i, q0) + | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) + | Pinj (p2, p3) -> PX (p, i, q0) + | PX (p', i', q') -> + if peq ceqb q' (p0 cO) then PX (p', (pplus i' i), q0) else PX (p, i, q0) (** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **) @@ -514,202 +566,154 @@ let mkX cO cI = (** val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **) let rec popp copp = function - | Pc c -> Pc (copp c) - | Pinj (j, q0) -> Pinj (j, (popp copp q0)) - | PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0)) +| Pc c -> Pc (copp c) +| Pinj (j, q0) -> Pinj (j, (popp copp q0)) +| PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0)) (** val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) let rec paddC cadd p c = match p with - | Pc c1 -> Pc (cadd c1 c) - | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c)) + | Pc c1 -> Pc (cadd c1 c) + | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c)) + | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c)) (** val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) let rec psubC csub p c = match p with - | Pc c1 -> Pc (csub c1 c) - | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c)) + | Pc c1 -> Pc (csub c1 c) + | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c)) + | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c)) (** val paddI : ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec paddI cadd pop q0 j = function - | Pc c -> - let p2 = paddC cadd q0 c in - (match p2 with - | Pc c0 -> p2 - | Pinj (j', q1) -> Pinj ((pplus j j'), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Pinj (j', q') -> - (match zPminus j' j with - | Z0 -> - let p2 = pop q' q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zpos k -> - let p2 = pop (Pinj (k, q')) q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zneg k -> - let p2 = paddI cadd pop q0 k q' in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j' j'0), q1) - | PX (p3, p4, p5) -> Pinj (j', p2))) - | PX (p2, i, q') -> - (match j with - | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (paddI cadd pop q0 (pdouble_minus_one j0) q')) - | XH -> PX (p2, i, (pop q' q0))) +| Pc c -> mkPinj j (paddC cadd q0 c) +| Pinj (j', q') -> + (match zPminus j' j with + | Z0 -> mkPinj j (pop q' q0) + | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (paddI cadd pop q0 k q')) +| PX (p2, i, q') -> + (match j with + | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) + | XO j0 -> PX (p2, i, (paddI cadd pop q0 (pdouble_minus_one j0) q')) + | XH -> PX (p2, i, (pop q' q0))) (** val psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubI cadd copp pop q0 j = function - | Pc c -> - let p2 = paddC cadd (popp copp q0) c in - (match p2 with - | Pc c0 -> p2 - | Pinj (j', q1) -> Pinj ((pplus j j'), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Pinj (j', q') -> - (match zPminus j' j with - | Z0 -> - let p2 = pop q' q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zpos k -> - let p2 = pop (Pinj (k, q')) q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zneg k -> - let p2 = psubI cadd copp pop q0 k q' in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j' j'0), q1) - | PX (p3, p4, p5) -> Pinj (j', p2))) - | PX (p2, i, q') -> - (match j with - | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, - (psubI cadd copp pop q0 (pdouble_minus_one j0) q')) - | XH -> PX (p2, i, (pop q' q0))) +| Pc c -> mkPinj j (paddC cadd (popp copp q0) c) +| Pinj (j', q') -> + (match zPminus j' j with + | Z0 -> mkPinj j (pop q' q0) + | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q')) +| PX (p2, i, q') -> + (match j with + | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) + | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (pdouble_minus_one j0) q')) + | XH -> PX (p2, i, (pop q' q0))) (** val paddX : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec paddX cO ceqb pop p' i' p = match p with - | Pc c -> PX (p', i', p) - | Pinj (j, q') -> - (match j with - | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) - | XO j0 -> PX (p', i', (Pinj ((pdouble_minus_one j0), q'))) - | XH -> PX (p', i', q')) - | PX (p2, i, q') -> - (match zPminus i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') +| Pc c -> PX (p', i', p) +| Pinj (j, q') -> + (match j with + | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) + | XO j0 -> PX (p', i', (Pinj ((pdouble_minus_one j0), q'))) + | XH -> PX (p', i', q')) +| PX (p2, i, q') -> + (match zPminus i i' with + | Z0 -> mkPX cO ceqb (pop p2 p') i q' + | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' + | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') (** val psubX : 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec psubX cO copp ceqb pop p' i' p = match p with - | Pc c -> PX ((popp copp p'), i', p) - | Pinj (j, q') -> - (match j with - | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) - | XO j0 -> PX ((popp copp p'), i', (Pinj ( - (pdouble_minus_one j0), q'))) - | XH -> PX ((popp copp p'), i', q')) - | PX (p2, i, q') -> - (match zPminus i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') +| Pc c -> PX ((popp copp p'), i', p) +| Pinj (j, q') -> + (match j with + | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) + | XO j0 -> PX ((popp copp p'), i', (Pinj ((pdouble_minus_one j0), q'))) + | XH -> PX ((popp copp p'), i', q')) +| PX (p2, i, q') -> + (match zPminus i i' with + | Z0 -> mkPX cO ceqb (pop p2 p') i q' + | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' + | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') (** val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec padd cO cadd ceqb p = function - | Pc c' -> paddC cadd p c' - | Pinj (j', q') -> paddI cadd (fun x x0 -> padd cO cadd ceqb x x0) q' j' p - | PX (p'0, i', q') -> - (match p with - | Pc c -> PX (p'0, i', (paddC cadd q' c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> PX (p'0, i', - (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) - | XO j0 -> PX (p'0, i', - (padd cO cadd ceqb (Pinj ((pdouble_minus_one j0), q0)) - q')) - | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) - | PX (p2, i, q0) -> - (match zPminus i i' with - | Z0 -> - mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i - (padd cO cadd ceqb q0 q') - | Zpos k -> - mkPX cO ceqb - (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' - (padd cO cadd ceqb q0 q') - | Zneg k -> - mkPX cO ceqb - (paddX cO ceqb (fun x x0 -> padd cO cadd ceqb x x0) p'0 - k p2) i (padd cO cadd ceqb q0 q'))) +| Pc c' -> paddC cadd p c' +| Pinj (j', q') -> paddI cadd (padd cO cadd ceqb) q' j' p +| PX (p'0, i', q') -> + (match p with + | Pc c -> PX (p'0, i', (paddC cadd q' c)) + | Pinj (j, q0) -> + (match j with + | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) + | XO j0 -> + PX (p'0, i', + (padd cO cadd ceqb (Pinj ((pdouble_minus_one j0), q0)) q')) + | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) + | PX (p2, i, q0) -> + (match zPminus i i' with + | Z0 -> + mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') + | Zpos k -> + mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' + (padd cO cadd ceqb q0 q') + | Zneg k -> + mkPX cO ceqb (paddX cO ceqb (padd cO cadd ceqb) p'0 k p2) i + (padd cO cadd ceqb q0 q'))) (** val psub : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec psub cO cadd csub copp ceqb p = function - | Pc c' -> psubC csub p c' - | Pinj (j', q') -> - psubI cadd copp (fun x x0 -> psub cO cadd csub copp ceqb x x0) q' j' p - | PX (p'0, i', q') -> - (match p with - | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) - | XO j0 -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj - ((pdouble_minus_one j0), q0)) q')) - | XH -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb q0 q'))) - | PX (p2, i, q0) -> - (match zPminus i i' with - | Z0 -> - mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i - (psub cO cadd csub copp ceqb q0 q') - | Zpos k -> - mkPX cO ceqb - (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) - i' (psub cO cadd csub copp ceqb q0 q') - | Zneg k -> - mkPX cO ceqb - (psubX cO copp ceqb (fun x x0 -> - psub cO cadd csub copp ceqb x x0) p'0 k p2) i - (psub cO cadd csub copp ceqb q0 q'))) +| Pc c' -> psubC csub p c' +| Pinj (j', q') -> psubI cadd copp (psub cO cadd csub copp ceqb) q' j' p +| PX (p'0, i', q') -> + (match p with + | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c)) + | Pinj (j, q0) -> + (match j with + | XI j0 -> + PX ((popp copp p'0), i', + (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) + | XO j0 -> + PX ((popp copp p'0), i', + (psub cO cadd csub copp ceqb (Pinj ((pdouble_minus_one j0), q0)) + q')) + | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) + | PX (p2, i, q0) -> + (match zPminus i i' with + | Z0 -> + mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i + (psub cO cadd csub copp ceqb q0 q') + | Zpos k -> + mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) + i' (psub cO cadd csub copp ceqb q0 q') + | Zneg k -> + mkPX cO ceqb + (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i + (psub cO cadd csub copp ceqb q0 q'))) (** val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> @@ -717,16 +721,11 @@ let rec psub cO cadd csub copp ceqb p = function let rec pmulC_aux cO cmul ceqb p c = match p with - | Pc c' -> Pc (cmul c' c) - | Pinj (j, q0) -> - let p2 = pmulC_aux cO cmul ceqb q0 c in - (match p2 with - | Pc c0 -> p2 - | Pinj (j', q1) -> Pinj ((pplus j j'), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | PX (p2, i, q0) -> - mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i - (pmulC_aux cO cmul ceqb q0 c) + | Pc c' -> Pc (cmul c' c) + | Pinj (j, q0) -> mkPinj j (pmulC_aux cO cmul ceqb q0 c) + | PX (p2, i, q0) -> + mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i + (pmulC_aux cO cmul ceqb q0 c) (** val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> @@ -742,108 +741,75 @@ let pmulC cO cI cmul ceqb p c = 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) let rec pmulI cO cI cmul ceqb pmul0 q0 j = function - | Pc c -> - let p2 = pmulC cO cI cmul ceqb q0 c in - (match p2 with - | Pc c0 -> p2 - | Pinj (j', q1) -> Pinj ((pplus j j'), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Pinj (j', q') -> - (match zPminus j' j with - | Z0 -> - let p2 = pmul0 q' q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zpos k -> - let p2 = pmul0 (Pinj (k, q')) q0 in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j j'0), q1) - | PX (p3, p4, p5) -> Pinj (j, p2)) - | Zneg k -> - let p2 = pmulI cO cI cmul ceqb pmul0 q0 k q' in - (match p2 with - | Pc c -> p2 - | Pinj (j'0, q1) -> Pinj ((pplus j' j'0), q1) - | PX (p3, p4, p5) -> Pinj (j', p2))) - | PX (p', i', q') -> - (match j with - | XI j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') - | XO j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (pdouble_minus_one j') q') - | XH -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' - (pmul0 q' q0)) +| Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) +| Pinj (j', q') -> + (match zPminus j' j with + | Z0 -> mkPinj j (pmul0 q' q0) + | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q')) +| PX (p', i', q') -> + (match j with + | XI j' -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' + (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') + | XO j' -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' + (pmulI cO cI cmul ceqb pmul0 q0 (pdouble_minus_one j') q') + | XH -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) (** val pmul : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with - | Pc c -> pmulC cO cI cmul ceqb p c - | Pinj (j', q') -> - pmulI cO cI cmul ceqb (fun x x0 -> pmul cO cI cadd cmul ceqb x x0) q' - j' p - | PX (p', i', q') -> - (match p with - | Pc c -> pmulC cO cI cmul ceqb p'' c - | Pinj (j, q0) -> - mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' - (match j with - | XI j0 -> - pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' - | XO j0 -> - pmul cO cI cadd cmul ceqb (Pinj - ((pdouble_minus_one j0), q0)) q' - | XH -> pmul cO cI cadd cmul ceqb q0 q') - | PX (p2, i, q0) -> - padd cO cadd ceqb - (mkPX cO ceqb - (padd cO cadd ceqb - (mkPX cO ceqb (pmul cO cI cadd cmul ceqb p2 p') i (p0 cO)) - (pmul cO cI cadd cmul ceqb - (match q0 with - | Pc c -> q0 - | Pinj (j', q1) -> Pinj ((pplus XH j'), q1) - | PX (p3, p4, p5) -> Pinj (XH, q0)) p')) i' - (p0 cO)) - (mkPX cO ceqb - (pmulI cO cI cmul ceqb (fun x x0 -> - pmul cO cI cadd cmul ceqb x x0) q' XH p2) i - (pmul cO cI cadd cmul ceqb q0 q'))) +| Pc c -> pmulC cO cI cmul ceqb p c +| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p +| PX (p', i', q') -> + (match p with + | Pc c -> pmulC cO cI cmul ceqb p'' c + | Pinj (j, q0) -> + let qQ' = + match j with + | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' + | XO j0 -> + pmul cO cI cadd cmul ceqb (Pinj ((pdouble_minus_one j0), q0)) q' + | XH -> pmul cO cI cadd cmul ceqb q0 q' + in + mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' + | PX (p2, i, q0) -> + let qQ' = pmul cO cI cadd cmul ceqb q0 q' in + let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in + let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in + let pP' = pmul cO cI cadd cmul ceqb p2 p' in + padd cO cadd ceqb + (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i' + (p0 cO)) (mkPX cO ceqb pQ' i qQ')) (** val psquare : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol **) let rec psquare cO cI cadd cmul ceqb = function - | Pc c -> Pc (cmul c c) - | Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0)) - | PX (p2, i, q0) -> - mkPX cO ceqb - (padd cO cadd ceqb - (mkPX cO ceqb (psquare cO cI cadd cmul ceqb p2) i (p0 cO)) - (pmul cO cI cadd cmul ceqb p2 - (let p3 = pmulC cO cI cmul ceqb q0 (cadd cI cI) in - match p3 with - | Pc c -> p3 - | Pinj (j', q1) -> Pinj ((pplus XH j'), q1) - | PX (p4, p5, p6) -> Pinj (XH, p3)))) i - (psquare cO cI cadd cmul ceqb q0) +| Pc c -> Pc (cmul c c) +| Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0)) +| PX (p2, i, q0) -> + let twoPQ = + pmul cO cI cadd cmul ceqb p2 + (mkPinj XH (pmulC cO cI cmul ceqb q0 (cadd cI cI))) + in + let q2 = psquare cO cI cadd cmul ceqb q0 in + let p3 = psquare cO cI cadd cmul ceqb p2 in + mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 type 'c pExpr = - | PEc of 'c - | PEX of positive - | PEadd of 'c pExpr * 'c pExpr - | PEsub of 'c pExpr * 'c pExpr - | PEmul of 'c pExpr * 'c pExpr - | PEopp of 'c pExpr - | PEpow of 'c pExpr * n +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) @@ -856,68 +822,66 @@ let mk_X cO cI j = pol **) let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function - | XI p3 -> - subst_l - (pmul cO cI cadd cmul ceqb - (ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) p) - | XO p3 -> - ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3 - | XH -> subst_l (pmul cO cI cadd cmul ceqb res p) +| XI p3 -> + subst_l + (pmul cO cI cadd cmul ceqb + (ppow_pos cO cI cadd cmul ceqb subst_l + (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) p) +| XO p3 -> + ppow_pos cO cI cadd cmul ceqb subst_l + (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3 +| XH -> subst_l (pmul cO cI cadd cmul ceqb res p) (** val ppow_N : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) let ppow_N cO cI cadd cmul ceqb subst_l p = function - | N0 -> p1 cI - | Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 +| N0 -> p1 cI +| Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 (** val norm_aux : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) let rec norm_aux cO cI cadd cmul csub copp ceqb = function - | PEc c -> Pc c - | PEX j -> mk_X cO cI j - | PEadd (pe1, pe2) -> - (match pe1 with - | PEopp pe3 -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe2) - (norm_aux cO cI cadd cmul csub copp ceqb pe3) - | _ -> - (match pe2 with - | PEopp pe3 -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe3) - | _ -> - padd cO cadd ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2))) - | PEsub (pe1, pe2) -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2) - | PEmul (pe1, pe2) -> - pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2) - | PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1) - | PEpow (pe1, n0) -> - ppow_N cO cI cadd cmul ceqb (fun p -> p) - (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 +| PEc c -> Pc c +| PEX j -> mk_X cO cI j +| PEadd (pe1, pe2) -> + (match pe1 with + | PEopp pe3 -> + psub cO cadd csub copp ceqb + (norm_aux cO cI cadd cmul csub copp ceqb pe2) + (norm_aux cO cI cadd cmul csub copp ceqb pe3) + | _ -> + (match pe2 with + | PEopp pe3 -> + psub cO cadd csub copp ceqb + (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe3) + | _ -> + padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2))) +| PEsub (pe1, pe2) -> + psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2) +| PEmul (pe1, pe2) -> + pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2) +| PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1) +| PEpow (pe1, n0) -> + ppow_N cO cI cadd cmul ceqb (fun p -> p) + (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 type 'a bFormula = - | TT - | FF - | X - | A of 'a - | Cj of 'a bFormula * 'a bFormula - | D of 'a bFormula * 'a bFormula - | N of 'a bFormula - | I of 'a bFormula * 'a bFormula +| TT +| FF +| X +| A of 'a +| Cj of 'a bFormula * 'a bFormula +| D of 'a bFormula * 'a bFormula +| N of 'a bFormula +| I of 'a bFormula * 'a bFormula type 'term' clause = 'term' list @@ -931,19 +895,61 @@ let tt = (** val ff : 'a1 cnf **) let ff = - [] :: [] + []::[] + +(** val add_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 + clause option **) + +let rec add_term unsat deduce t0 = function +| [] -> + (match deduce t0 t0 with + | Some u -> if unsat u then None else Some (t0::[]) + | None -> Some (t0::[])) +| t'::cl0 -> + (match deduce t0 t' with + | Some u -> + if unsat u + then None + else (match add_term unsat deduce t0 cl0 with + | Some cl' -> Some (t'::cl') + | None -> None) + | None -> + (match add_term unsat deduce t0 cl0 with + | Some cl' -> Some (t'::cl') + | None -> None)) + +(** val or_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause + -> 'a1 clause option **) + +let rec or_clause unsat deduce cl1 cl2 = + match cl1 with + | [] -> Some cl2 + | t0::cl -> + (match add_term unsat deduce t0 cl2 with + | Some cl' -> or_clause unsat deduce cl cl' + | None -> None) -(** val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf **) +(** val or_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> + 'a1 cnf **) -let or_clause_cnf t0 f = - map (fun x -> app t0 x) f +let or_clause_cnf unsat deduce t0 f = + fold_right (fun e acc -> + match or_clause unsat deduce t0 e with + | Some cl -> cl::acc + | None -> acc) [] f -(** val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) +(** val or_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 + cnf **) -let rec or_cnf f f' = +let rec or_cnf unsat deduce f f' = match f with - | [] -> tt - | e :: rst -> app (or_cnf rst f') (or_clause_cnf e f') + | [] -> tt + | e::rst -> + app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) @@ -951,133 +957,168 @@ let and_cnf f1 f2 = app f1 f2 (** val xcnf : - ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **) - -let rec xcnf normalise0 negate0 pol0 = function - | TT -> if pol0 then tt else ff - | FF -> if pol0 then ff else tt - | X -> ff - | A x -> if pol0 then normalise0 x else negate0 x - | Cj (e1, e2) -> - if pol0 - then and_cnf (xcnf normalise0 negate0 pol0 e1) - (xcnf normalise0 negate0 pol0 e2) - else or_cnf (xcnf normalise0 negate0 pol0 e1) - (xcnf normalise0 negate0 pol0 e2) - | D (e1, e2) -> - if pol0 - then or_cnf (xcnf normalise0 negate0 pol0 e1) - (xcnf normalise0 negate0 pol0 e2) - else and_cnf (xcnf normalise0 negate0 pol0 e1) - (xcnf normalise0 negate0 pol0 e2) - | N e -> xcnf normalise0 negate0 (negb pol0) e - | I (e1, e2) -> - if pol0 - then or_cnf (xcnf normalise0 negate0 (negb pol0) e1) - (xcnf normalise0 negate0 pol0 e2) - else and_cnf (xcnf normalise0 negate0 (negb pol0) e1) - (xcnf normalise0 negate0 pol0 e2) + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 + -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf **) + +let rec xcnf unsat deduce normalise0 negate0 pol0 = function +| TT -> if pol0 then tt else ff +| FF -> if pol0 then ff else tt +| X -> ff +| A x -> if pol0 then normalise0 x else negate0 x +| Cj (e1, e2) -> + if pol0 + then and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) + else or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) +| D (e1, e2) -> + if pol0 + then or_cnf unsat deduce (xcnf unsat deduce normalise0 negate0 pol0 e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) + else and_cnf (xcnf unsat deduce normalise0 negate0 pol0 e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) +| N e -> xcnf unsat deduce normalise0 negate0 (negb pol0) e +| I (e1, e2) -> + if pol0 + then or_cnf unsat deduce + (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) + else and_cnf (xcnf unsat deduce normalise0 negate0 (negb pol0) e1) + (xcnf unsat deduce normalise0 negate0 pol0 e2) (** val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool **) let rec cnf_checker checker f l = match f with - | [] -> true - | e :: f0 -> - (match l with - | [] -> false - | c :: l0 -> - if checker e c then cnf_checker checker f0 l0 else false) + | [] -> true + | e::f0 -> + (match l with + | [] -> false + | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) (** val tauto_checker : - ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 - bFormula -> 'a3 list -> bool **) + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 + -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> + bool **) + +let tauto_checker unsat deduce normalise0 negate0 checker f w = + cnf_checker checker (xcnf unsat deduce normalise0 negate0 true f) w + +(** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) + +let cneqb ceqb x y = + negb (ceqb x y) -let tauto_checker normalise0 negate0 checker f w = - cnf_checker checker (xcnf normalise0 negate0 true f) w +(** val cltb : + ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) + +let cltb ceqb cleb x y = + (&&) (cleb x y) (cneqb ceqb x y) type 'c polC = 'c pol type op1 = - | Equal - | NonEqual - | Strict - | NonStrict +| Equal +| NonEqual +| Strict +| NonStrict + +type 'c nFormula = 'c polC * op1 -type 'c nFormula = 'c polC * op1 +(** val opMult : op1 -> op1 -> op1 option **) + +let opMult o o' = + match o with + | Equal -> Some Equal + | NonEqual -> + (match o' with + | Strict -> None + | NonStrict -> None + | x -> Some x) + | Strict -> + (match o' with + | NonEqual -> None + | _ -> Some o') + | NonStrict -> + (match o' with + | NonEqual -> None + | Strict -> Some NonStrict + | x -> Some x) (** val opAdd : op1 -> op1 -> op1 option **) let opAdd o o' = match o with - | Equal -> Some o' - | NonEqual -> (match o' with - | Equal -> Some NonEqual - | _ -> None) - | Strict -> (match o' with - | NonEqual -> None - | _ -> Some Strict) - | NonStrict -> - (match o' with - | NonEqual -> None - | Strict -> Some Strict - | _ -> Some NonStrict) + | Equal -> Some o' + | NonEqual -> + (match o' with + | Equal -> Some NonEqual + | _ -> None) + | Strict -> + (match o' with + | NonEqual -> None + | _ -> Some Strict) + | NonStrict -> + (match o' with + | Equal -> Some NonStrict + | NonEqual -> None + | x -> Some x) type 'c psatz = - | PsatzIn of nat - | PsatzSquare of 'c polC - | PsatzMulC of 'c polC * 'c psatz - | PsatzMulE of 'c psatz * 'c psatz - | PsatzAdd of 'c psatz * 'c psatz - | PsatzC of 'c - | PsatzZ +| PsatzIn of nat +| PsatzSquare of 'c polC +| PsatzMulC of 'c polC * 'c psatz +| PsatzMulE of 'c psatz * 'c psatz +| PsatzAdd of 'c psatz * 'c psatz +| PsatzC of 'c +| PsatzZ + +(** val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option **) + +let map_option f = function +| Some x -> f x +| None -> None + +(** val map_option2 : + ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option **) + +let map_option2 f o o' = + match o with + | Some x -> + (match o' with + | Some x' -> f x x' + | None -> None) + | None -> None (** val pexpr_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option **) let pexpr_times_nformula cO cI cplus ctimes ceqb e = function - | ef , o -> - (match o with - | Equal -> Some ((pmul cO cI cplus ctimes ceqb e ef) , Equal) - | _ -> None) +| ef,o -> + (match o with + | Equal -> Some ((pmul cO cI cplus ctimes ceqb e ef),Equal) + | _ -> None) (** val nformula_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) let nformula_times_nformula cO cI cplus ctimes ceqb f1 f2 = - let e1 , o1 = f1 in - let e2 , o2 = f2 in - (match o1 with - | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal) - | NonEqual -> - (match o2 with - | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal) - | NonEqual -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , - NonEqual) - | _ -> None) - | Strict -> - (match o2 with - | NonEqual -> None - | _ -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , o2)) - | NonStrict -> - (match o2 with - | Equal -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , Equal) - | NonEqual -> None - | _ -> Some ((pmul cO cI cplus ctimes ceqb e1 e2) , NonStrict))) + let e1,o1 = f1 in + let e2,o2 = f2 in + map_option (fun x -> Some ((pmul cO cI cplus ctimes ceqb e1 e2),x)) + (opMult o1 o2) (** val nformula_plus_nformula : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option **) let nformula_plus_nformula cO cplus ceqb f1 f2 = - let e1 , o1 = f1 in - let e2 , o2 = f2 in - (match opAdd o1 o2 with - | Some x -> Some ((padd cO cplus ceqb e1 e2) , x) - | None -> None) + let e1,o1 = f1 in + let e2,o2 = f2 in + map_option (fun x -> Some ((padd cO cplus ceqb e1 e2),x)) (opAdd o1 o2) (** val eval_Psatz : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1085,47 +1126,36 @@ let nformula_plus_nformula cO cplus ceqb f1 f2 = nFormula option **) let rec eval_Psatz cO cI cplus ctimes ceqb cleb l = function - | PsatzIn n0 -> Some (nth n0 l ((Pc cO) , Equal)) - | PsatzSquare e0 -> Some ((psquare cO cI cplus ctimes ceqb e0) , NonStrict) - | PsatzMulC (re, e0) -> - (match eval_Psatz cO cI cplus ctimes ceqb cleb l e0 with - | Some x -> pexpr_times_nformula cO cI cplus ctimes ceqb re x - | None -> None) - | PsatzMulE (f1, f2) -> - (match eval_Psatz cO cI cplus ctimes ceqb cleb l f1 with - | Some x -> - (match eval_Psatz cO cI cplus ctimes ceqb cleb l f2 with - | Some x' -> - nformula_times_nformula cO cI cplus ctimes ceqb x x' - | None -> None) - | None -> None) - | PsatzAdd (f1, f2) -> - (match eval_Psatz cO cI cplus ctimes ceqb cleb l f1 with - | Some x -> - (match eval_Psatz cO cI cplus ctimes ceqb cleb l f2 with - | Some x' -> nformula_plus_nformula cO cplus ceqb x x' - | None -> None) - | None -> None) - | PsatzC c -> - if (&&) (cleb cO c) (negb (ceqb cO c)) - then Some ((Pc c) , Strict) - else None - | PsatzZ -> Some ((Pc cO) , Equal) +| PsatzIn n0 -> Some (nth n0 l ((Pc cO),Equal)) +| PsatzSquare e0 -> Some ((psquare cO cI cplus ctimes ceqb e0),NonStrict) +| PsatzMulC (re, e0) -> + map_option (pexpr_times_nformula cO cI cplus ctimes ceqb re) + (eval_Psatz cO cI cplus ctimes ceqb cleb l e0) +| PsatzMulE (f1, f2) -> + map_option2 (nformula_times_nformula cO cI cplus ctimes ceqb) + (eval_Psatz cO cI cplus ctimes ceqb cleb l f1) + (eval_Psatz cO cI cplus ctimes ceqb cleb l f2) +| PsatzAdd (f1, f2) -> + map_option2 (nformula_plus_nformula cO cplus ceqb) + (eval_Psatz cO cI cplus ctimes ceqb cleb l f1) + (eval_Psatz cO cI cplus ctimes ceqb cleb l f2) +| PsatzC c -> if cltb ceqb cleb cO c then Some ((Pc c),Strict) else None +| PsatzZ -> Some ((Pc cO),Equal) (** val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool **) let check_inconsistent cO ceqb cleb = function - | e , op -> - (match e with - | Pc c -> - (match op with - | Equal -> negb (ceqb c cO) - | NonEqual -> ceqb c cO - | Strict -> cleb c cO - | NonStrict -> (&&) (cleb c cO) (negb (ceqb c cO))) - | _ -> false) +| e,op -> + (match e with + | Pc c -> + (match op with + | Equal -> cneqb ceqb c cO + | NonEqual -> ceqb c cO + | Strict -> cleb c cO + | NonStrict -> cltb ceqb cleb c cO) + | _ -> false) (** val check_normalised_formulas : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1134,16 +1164,16 @@ let check_inconsistent cO ceqb cleb = function let check_normalised_formulas cO cI cplus ctimes ceqb cleb l cm = match eval_Psatz cO cI cplus ctimes ceqb cleb l cm with - | Some f -> check_inconsistent cO ceqb cleb f - | None -> false + | Some f -> check_inconsistent cO ceqb cleb f + | None -> false type op2 = - | OpEq - | OpNEq - | OpLe - | OpGe - | OpLt - | OpGt +| OpEq +| OpNEq +| OpLe +| OpGe +| OpLt +| OpGt type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr } @@ -1163,22 +1193,22 @@ let frhs x = x.frhs 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb pe = - norm_aux cO cI cplus ctimes cminus copp ceqb pe +let norm cO cI cplus ctimes cminus copp ceqb = + norm_aux cO cI cplus ctimes cminus copp ceqb (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb p p' = - psub cO cplus cminus copp ceqb p p' +let psub0 cO cplus cminus copp ceqb = + psub cO cplus cminus copp ceqb (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb p p' = - padd cO cplus ceqb p p' +let padd0 cO cplus ceqb = + padd cO cplus ceqb (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1190,15 +1220,16 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in (match o with - | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: - (((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: []) - | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Equal) :: [] - | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: [] - | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: [] - | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , NonStrict) :: - [] - | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , NonStrict) :: - []) + | OpEq -> + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus + cminus copp + ceqb rhs0 + lhs0),Strict)::[]) + | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] + | OpLe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[] + | OpGe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] + | OpLt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] + | OpGt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[]) (** val cnf_normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1206,7 +1237,7 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = nFormula cnf **) let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x :: []) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) + map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) (** val xnegate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1218,15 +1249,16 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t0 = let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in (match o with - | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Equal) :: [] - | OpNEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: - (((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: []) - | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , NonStrict) :: - [] - | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , NonStrict) :: - [] - | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0) , Strict) :: [] - | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0) , Strict) :: []) + | OpEq -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Equal)::[] + | OpNEq -> + ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::(((psub0 cO cplus + cminus copp + ceqb rhs0 + lhs0),Strict)::[]) + | OpLe -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),NonStrict)::[] + | OpGe -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),NonStrict)::[] + | OpLt -> ((psub0 cO cplus cminus copp ceqb rhs0 lhs0),Strict)::[] + | OpGt -> ((psub0 cO cplus cminus copp ceqb lhs0 rhs0),Strict)::[]) (** val cnf_negate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 @@ -1234,15 +1266,16 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t0 = nFormula cnf **) let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x :: []) (xnegate cO cI cplus ctimes cminus copp ceqb t0) + map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) (** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **) let rec xdenorm jmp = function - | Pc c -> PEc c - | Pinj (j, p2) -> xdenorm (pplus j jmp) p2 - | PX (p2, j, q0) -> PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp), - (Npos j))))), (xdenorm (psucc jmp) q0)) +| Pc c -> PEc c +| Pinj (j, p2) -> xdenorm (pplus j jmp) p2 +| PX (p2, j, q0) -> + PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp), (Npos j))))), + (xdenorm (psucc jmp) q0)) (** val denorm : 'a1 pol -> 'a1 pExpr **) @@ -1254,66 +1287,59 @@ let denorm p = 'a1 psatz **) let simpl_cone cO cI ctimes ceqb e = match e with - | PsatzSquare t0 -> - (match t0 with - | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c) - | _ -> PsatzSquare t0) - | PsatzMulE (t1, t2) -> - (match t1 with - | PsatzMulE (x, x0) -> - (match x with - | PsatzC p2 -> - (match t2 with - | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x0) - | PsatzZ -> PsatzZ - | _ -> e) - | _ -> - (match x0 with - | PsatzC p2 -> - (match t2 with - | PsatzC c -> PsatzMulE ((PsatzC - (ctimes c p2)), x) - | PsatzZ -> PsatzZ - | _ -> e) - | _ -> - (match t2 with - | PsatzC c -> - if ceqb cI c - then t1 - else PsatzMulE (t1, t2) - | PsatzZ -> PsatzZ - | _ -> e))) - | PsatzC c -> - (match t2 with - | PsatzMulE (x, x0) -> - (match x with - | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x0) - | _ -> - (match x0 with - | PsatzC p2 -> PsatzMulE ((PsatzC - (ctimes c p2)), x) - | _ -> - if ceqb cI c - then t2 - else PsatzMulE (t1, t2))) - | PsatzAdd (y, z0) -> PsatzAdd ((PsatzMulE ((PsatzC c), y)), - (PsatzMulE ((PsatzC c), z0))) - | PsatzC c0 -> PsatzC (ctimes c c0) - | PsatzZ -> PsatzZ - | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)) +| PsatzSquare t0 -> + (match t0 with + | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c) + | _ -> PsatzSquare t0) +| PsatzMulE (t1, t2) -> + (match t1 with + | PsatzMulE (x, x0) -> + (match x with + | PsatzC p2 -> + (match t2 with + | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x0) | PsatzZ -> PsatzZ + | _ -> e) + | _ -> + (match x0 with + | PsatzC p2 -> + (match t2 with + | PsatzC c -> PsatzMulE ((PsatzC (ctimes c p2)), x) + | PsatzZ -> PsatzZ + | _ -> e) + | _ -> + (match t2 with + | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2) + | PsatzZ -> PsatzZ + | _ -> e))) + | PsatzC c -> + (match t2 with + | PsatzMulE (x, x0) -> + (match x with + | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x0) | _ -> - (match t2 with - | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2) - | PsatzZ -> PsatzZ - | _ -> e)) - | PsatzAdd (t1, t2) -> - (match t1 with - | PsatzZ -> t2 - | _ -> (match t2 with - | PsatzZ -> t1 - | _ -> PsatzAdd (t1, t2))) - | _ -> e + (match x0 with + | PsatzC p2 -> PsatzMulE ((PsatzC (ctimes c p2)), x) + | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2))) + | PsatzAdd (y, z0) -> + PsatzAdd ((PsatzMulE ((PsatzC c), y)), (PsatzMulE ((PsatzC c), z0))) + | PsatzC c0 -> PsatzC (ctimes c c0) + | PsatzZ -> PsatzZ + | _ -> if ceqb cI c then t2 else PsatzMulE (t1, t2)) + | PsatzZ -> PsatzZ + | _ -> + (match t2 with + | PsatzC c -> if ceqb cI c then t1 else PsatzMulE (t1, t2) + | PsatzZ -> PsatzZ + | _ -> e)) +| PsatzAdd (t1, t2) -> + (match t1 with + | PsatzZ -> t2 + | _ -> + (match t2 with + | PsatzZ -> t1 + | _ -> PsatzAdd (t1, t2))) +| _ -> e type q = { qnum : z; qden : positive } @@ -1360,9 +1386,9 @@ let qminus x y = let qinv x = match x.qnum with - | Z0 -> { qnum = Z0; qden = XH } - | Zpos p -> { qnum = (Zpos x.qden); qden = p } - | Zneg p -> { qnum = (Zneg x.qden); qden = p } + | Z0 -> { qnum = Z0; qden = XH } + | Zpos p -> { qnum = (Zpos x.qden); qden = p } + | Zneg p -> { qnum = (Zneg x.qden); qden = p } (** val qpower_positive : q -> positive -> q **) @@ -1372,92 +1398,48 @@ let qpower_positive q0 p = (** val qpower : q -> z -> q **) let qpower q0 = function - | Z0 -> { qnum = (Zpos XH); qden = XH } - | Zpos p -> qpower_positive q0 p - | Zneg p -> qinv (qpower_positive q0 p) - -(** val pgcdn : nat -> positive -> positive -> positive **) - -let rec pgcdn n0 a b = - match n0 with - | O -> XH - | S n1 -> - (match a with - | XI a' -> - (match b with - | XI b' -> - (match pcompare a' b' Eq with - | Eq -> a - | Lt -> pgcdn n1 (pminus b' a') a - | Gt -> pgcdn n1 (pminus a' b') b) - | XO b0 -> pgcdn n1 a b0 - | XH -> XH) - | XO a0 -> - (match b with - | XI p -> pgcdn n1 a0 b - | XO b0 -> XO (pgcdn n1 a0 b0) - | XH -> XH) - | XH -> XH) - -(** val pgcd : positive -> positive -> positive **) - -let pgcd a b = - pgcdn (plus (psize a) (psize b)) a b - -(** val zgcd : z -> z -> z **) - -let zgcd a b = - match a with - | Z0 -> zabs b - | Zpos a0 -> - (match b with - | Z0 -> zabs a - | Zpos b0 -> Zpos (pgcd a0 b0) - | Zneg b0 -> Zpos (pgcd a0 b0)) - | Zneg a0 -> - (match b with - | Z0 -> zabs a - | Zpos b0 -> Zpos (pgcd a0 b0) - | Zneg b0 -> Zpos (pgcd a0 b0)) +| Z0 -> { qnum = (Zpos XH); qden = XH } +| Zpos p -> qpower_positive q0 p +| Zneg p -> qinv (qpower_positive q0 p) type 'a t = - | Empty - | Leaf of 'a - | Node of 'a t * 'a * 'a t +| Empty +| Leaf of 'a +| Node of 'a t * 'a * 'a t (** val find : 'a1 -> 'a1 t -> positive -> 'a1 **) let rec find default vm p = match vm with - | Empty -> default - | Leaf i -> i - | Node (l, e, r) -> - (match p with - | XI p2 -> find default r p2 - | XO p2 -> find default l p2 - | XH -> e) + | Empty -> default + | Leaf i -> i + | Node (l, e, r) -> + (match p with + | XI p2 -> find default r p2 + | XO p2 -> find default l p2 + | XH -> e) type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) -let zWeakChecker x x0 = - check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0 +let zWeakChecker = + check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool (** val psub1 : z pol -> z pol -> z pol **) -let psub1 p p' = - psub0 Z0 zplus zminus zopp zeq_bool p p' +let psub1 = + psub0 Z0 zplus zminus zopp zeq_bool (** val padd1 : z pol -> z pol -> z pol **) -let padd1 p p' = - padd0 Z0 zplus zeq_bool p p' +let padd1 = + padd0 Z0 zplus zeq_bool (** val norm0 : z pExpr -> z pol **) -let norm0 pe = - norm Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool pe +let norm0 = + norm Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool (** val xnormalise0 : z formula -> z nFormula list **) @@ -1466,18 +1448,21 @@ let xnormalise0 t0 = let lhs0 = norm0 lhs in let rhs0 = norm0 rhs in (match o with - | OpEq -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: - (((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: []) - | OpNEq -> ((psub1 lhs0 rhs0) , Equal) :: [] - | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: [] - | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: [] - | OpLt -> ((psub1 lhs0 rhs0) , NonStrict) :: [] - | OpGt -> ((psub1 rhs0 lhs0) , NonStrict) :: []) + | OpEq -> + ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 + (padd1 lhs0 + (Pc (Zpos + XH)))),NonStrict)::[]) + | OpNEq -> ((psub1 lhs0 rhs0),Equal)::[] + | OpLe -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[] + | OpGe -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] + | OpLt -> ((psub1 lhs0 rhs0),NonStrict)::[] + | OpGt -> ((psub1 rhs0 lhs0),NonStrict)::[]) (** val normalise : z formula -> z nFormula cnf **) let normalise t0 = - map (fun x -> x :: []) (xnormalise0 t0) + map (fun x -> x::[]) (xnormalise0 t0) (** val xnegate0 : z formula -> z nFormula list **) @@ -1486,218 +1471,235 @@ let xnegate0 t0 = let lhs0 = norm0 lhs in let rhs0 = norm0 rhs in (match o with - | OpEq -> ((psub1 lhs0 rhs0) , Equal) :: [] - | OpNEq -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: - (((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: []) - | OpLe -> ((psub1 rhs0 lhs0) , NonStrict) :: [] - | OpGe -> ((psub1 lhs0 rhs0) , NonStrict) :: [] - | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))) , NonStrict) :: [] - | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))) , NonStrict) :: []) + | OpEq -> ((psub1 lhs0 rhs0),Equal)::[] + | OpNEq -> + ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::(((psub1 rhs0 + (padd1 lhs0 + (Pc (Zpos + XH)))),NonStrict)::[]) + | OpLe -> ((psub1 rhs0 lhs0),NonStrict)::[] + | OpGe -> ((psub1 lhs0 rhs0),NonStrict)::[] + | OpLt -> ((psub1 rhs0 (padd1 lhs0 (Pc (Zpos XH)))),NonStrict)::[] + | OpGt -> ((psub1 lhs0 (padd1 rhs0 (Pc (Zpos XH)))),NonStrict)::[]) (** val negate : z formula -> z nFormula cnf **) let negate t0 = - map (fun x -> x :: []) (xnegate0 t0) + map (fun x -> x::[]) (xnegate0 t0) + +(** val zunsat : z nFormula -> bool **) + +let zunsat = + check_inconsistent Z0 zeq_bool zle_bool + +(** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) + +let zdeduce = + nformula_plus_nformula Z0 zplus zeq_bool (** val ceiling : z -> z -> z **) let ceiling a b = - let q0 , r = zdiv_eucl a b in + let q0,r = zdiv_eucl a b in (match r with - | Z0 -> q0 - | _ -> zplus q0 (Zpos XH)) + | Z0 -> q0 + | _ -> zplus q0 (Zpos XH)) type zArithProof = - | DoneProof - | RatProof of zWitness * zArithProof - | CutProof of zWitness * zArithProof - | EnumProof of zWitness * zWitness * zArithProof list +| DoneProof +| RatProof of zWitness * zArithProof +| CutProof of zWitness * zArithProof +| EnumProof of zWitness * zWitness * zArithProof list (** val zgcdM : z -> z -> z **) let zgcdM x y = zmax (zgcd x y) (Zpos XH) -(** val zgcd_pol : z polC -> z * z **) +(** val zgcd_pol : z polC -> z * z **) let rec zgcd_pol = function - | Pc c -> Z0 , c - | Pinj (p2, p3) -> zgcd_pol p3 - | PX (p2, p3, q0) -> - let g1 , c1 = zgcd_pol p2 in - let g2 , c2 = zgcd_pol q0 in (zgcdM (zgcdM g1 c1) g2) , c2 +| Pc c -> Z0,c +| Pinj (p2, p3) -> zgcd_pol p3 +| PX (p2, p3, q0) -> + let g1,c1 = zgcd_pol p2 in + let g2,c2 = zgcd_pol q0 in (zgcdM (zgcdM g1 c1) g2),c2 (** val zdiv_pol : z polC -> z -> z polC **) let rec zdiv_pol p x = match p with - | Pc c -> Pc (zdiv c x) - | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x)) - | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x)) + | Pc c -> Pc (zdiv c x) + | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x)) + | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x)) -(** val makeCuttingPlane : z polC -> z polC * z **) +(** val makeCuttingPlane : z polC -> z polC * z **) let makeCuttingPlane p = - let g , c = zgcd_pol p in + let g,c = zgcd_pol p in if zgt_bool g Z0 - then (zdiv_pol (psubC zminus p c) g) , (zopp (ceiling (zopp c) g)) - else p , Z0 + then (zdiv_pol (psubC zminus p c) g),(zopp (ceiling (zopp c) g)) + else p,Z0 -(** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **) +(** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **) let genCuttingPlane = function - | e , op -> - (match op with - | Equal -> - let g , c = zgcd_pol e in - if (&&) (zgt_bool g Z0) - ((&&) (zgt_bool c Z0) (negb (zeq_bool (zgcd g c) g))) - then None - else Some ((e , Z0) , op) - | NonEqual -> Some ((e , Z0) , op) - | Strict -> - let p , c = makeCuttingPlane (psubC zminus e (Zpos XH)) in - Some ((p , c) , NonStrict) - | NonStrict -> - let p , c = makeCuttingPlane e in Some ((p , c) , NonStrict)) - -(** val nformula_of_cutting_plane : - ((z polC * z) * op1) -> z nFormula **) +| e,op -> + (match op with + | Equal -> + let g,c = zgcd_pol e in + if (&&) (zgt_bool g Z0) + ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (zgcd g c) g))) + then None + else Some ((makeCuttingPlane e),Equal) + | NonEqual -> Some ((e,Z0),op) + | Strict -> Some ((makeCuttingPlane (psubC zminus e (Zpos XH))),NonStrict) + | NonStrict -> Some ((makeCuttingPlane e),NonStrict)) + +(** val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula **) let nformula_of_cutting_plane = function - | e_z , o -> let e , z0 = e_z in (padd1 e (Pc z0)) , o +| e_z,o -> let e,z0 = e_z in (padd1 e (Pc z0)),o (** val is_pol_Z0 : z polC -> bool **) let is_pol_Z0 = function - | Pc z0 -> (match z0 with - | Z0 -> true - | _ -> false) - | _ -> false +| Pc z0 -> + (match z0 with + | Z0 -> true + | _ -> false) +| _ -> false (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) -let eval_Psatz0 x x0 = - eval_Psatz Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0 +let eval_Psatz0 = + eval_Psatz Z0 (Zpos XH) zplus zmult zeq_bool zle_bool -(** val check_inconsistent0 : z nFormula -> bool **) +(** val valid_cut_sign : op1 -> bool **) -let check_inconsistent0 f = - check_inconsistent Z0 zeq_bool zle_bool f +let valid_cut_sign = function +| Equal -> true +| NonStrict -> true +| _ -> false (** val zChecker : z nFormula list -> zArithProof -> bool **) let rec zChecker l = function - | DoneProof -> false - | RatProof (w, pf0) -> - (match eval_Psatz0 l w with - | Some f -> - if check_inconsistent0 f then true else zChecker (f :: l) pf0 - | None -> false) - | CutProof (w, pf0) -> - (match eval_Psatz0 l w with - | Some f -> - (match genCuttingPlane f with - | Some cp -> - zChecker ((nformula_of_cutting_plane cp) :: l) pf0 - | None -> true) - | None -> false) - | EnumProof (w1, w2, pf0) -> - (match eval_Psatz0 l w1 with - | Some f1 -> - (match eval_Psatz0 l w2 with - | Some f2 -> - (match genCuttingPlane f1 with - | Some p -> - let p2 , op3 = p in - let e1 , z1 = p2 in - (match genCuttingPlane f2 with - | Some p3 -> - let p4 , op4 = p3 in - let e2 , z2 = p4 in - (match op3 with - | NonStrict -> - (match op4 with - | NonStrict -> - if is_pol_Z0 (padd1 e1 e2) - then - let rec label pfs lb ub = - - match pfs with - | - [] -> zgt_bool lb ub - | - pf1 :: rsr -> - (&&) - (zChecker - (((psub1 e1 (Pc lb)) , - Equal) :: l) pf1) - (label rsr - (zplus lb (Zpos XH)) ub) - in label pf0 (zopp z1) z2 - else false - | _ -> false) - | _ -> false) - | None -> false) - | None -> false) - | None -> false) - | None -> false) +| DoneProof -> false +| RatProof (w, pf0) -> + (match eval_Psatz0 l w with + | Some f -> if zunsat f then true else zChecker (f::l) pf0 + | None -> false) +| CutProof (w, pf0) -> + (match eval_Psatz0 l w with + | Some f -> + (match genCuttingPlane f with + | Some cp -> zChecker ((nformula_of_cutting_plane cp)::l) pf0 + | None -> true) + | None -> false) +| EnumProof (w1, w2, pf0) -> + (match eval_Psatz0 l w1 with + | Some f1 -> + (match eval_Psatz0 l w2 with + | Some f2 -> + (match genCuttingPlane f1 with + | Some p -> + let p2,op3 = p in + let e1,z1 = p2 in + (match genCuttingPlane f2 with + | Some p3 -> + let p4,op4 = p3 in + let e2,z2 = p4 in + if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4)) + (is_pol_Z0 (padd1 e1 e2)) + then let rec label pfs lb ub = + match pfs with + | [] -> zgt_bool lb ub + | pf1::rsr -> + (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1) + (label rsr (zplus lb (Zpos XH)) ub) + in label pf0 (zopp z1) z2 + else false + | None -> true) + | None -> true) + | None -> false) + | None -> false) (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) let zTautoChecker f w = - tauto_checker normalise negate zChecker f w + tauto_checker zunsat zdeduce normalise negate zChecker f w (** val n_of_Z : z -> n **) let n_of_Z = function - | Zpos p -> Npos p - | _ -> N0 +| Zpos p -> Npos p +| _ -> N0 type qWitness = q psatz (** val qWeakChecker : q nFormula list -> q psatz -> bool **) -let qWeakChecker x x0 = +let qWeakChecker = check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); - qden = XH } qplus qmult qeq_bool qle_bool x x0 + qden = XH } qplus qmult qeq_bool qle_bool (** val qnormalise : q formula -> q nFormula cnf **) -let qnormalise t0 = +let qnormalise = cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } - qplus qmult qminus qopp qeq_bool t0 + qplus qmult qminus qopp qeq_bool (** val qnegate : q formula -> q nFormula cnf **) -let qnegate t0 = +let qnegate = cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus - qmult qminus qopp qeq_bool t0 + qmult qminus qopp qeq_bool + +(** val qunsat : q nFormula -> bool **) + +let qunsat = + check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool + +(** val qdeduce : q nFormula -> q nFormula -> q nFormula option **) + +let qdeduce = + nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool (** val qTautoChecker : q formula bFormula -> qWitness list -> bool **) let qTautoChecker f w = - tauto_checker qnormalise qnegate qWeakChecker f w + tauto_checker qunsat qdeduce qnormalise qnegate qWeakChecker f w type rWitness = z psatz (** val rWeakChecker : z nFormula list -> z psatz -> bool **) -let rWeakChecker x x0 = - check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool x x0 +let rWeakChecker = + check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool (** val rnormalise : z formula -> z nFormula cnf **) -let rnormalise t0 = - cnf_normalise Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool t0 +let rnormalise = + cnf_normalise Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool (** val rnegate : z formula -> z nFormula cnf **) -let rnegate t0 = - cnf_negate Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool t0 +let rnegate = + cnf_negate Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool + +(** val runsat : z nFormula -> bool **) + +let runsat = + check_inconsistent Z0 zeq_bool zle_bool + +(** val rdeduce : z nFormula -> z nFormula -> z nFormula option **) + +let rdeduce = + nformula_plus_nformula Z0 zplus zeq_bool (** val rTautoChecker : z formula bFormula -> rWitness list -> bool **) let rTautoChecker f w = - tauto_checker rnormalise rnegate rWeakChecker f w + tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker f w diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 3e3ae2c31..675a5a0cc 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -1,28 +1,24 @@ val negb : bool -> bool type nat = - | O - | S of nat +| O +| S of nat type comparison = - | Eq - | Lt - | Gt +| Eq +| Lt +| Gt val compOpp : comparison -> comparison -val plus : nat -> nat -> nat - val app : 'a1 list -> 'a1 list -> 'a1 list -val nth : nat -> 'a1 list -> 'a1 -> 'a1 - -val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list +val plus : nat -> nat -> nat type positive = - | XI of positive - | XO of positive - | XH +| XI of positive +| XO of positive +| XH val psucc : positive -> positive @@ -35,9 +31,9 @@ val p_of_succ_nat : nat -> positive val pdouble_minus_one : positive -> positive type positive_mask = - | IsNul - | IsPos of positive - | IsNeg +| IsNul +| IsPos of positive +| IsNeg val pdouble_plus_one_mask : positive_mask -> positive_mask @@ -53,20 +49,28 @@ val pminus : positive -> positive -> positive val pmult : positive -> positive -> positive -val pcompare : positive -> positive -> comparison -> comparison - val psize : positive -> nat +val pcompare : positive -> positive -> comparison -> comparison + type n = - | N0 - | Npos of positive +| N0 +| Npos of positive + +val n_of_nat : nat -> n val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 +val nth : nat -> 'a1 list -> 'a1 -> 'a1 + +val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list + +val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 + type z = - | Z0 - | Zpos of positive - | Zneg of positive +| Z0 +| Zpos of positive +| Zneg of positive val zdouble_plus_one : z -> z @@ -86,10 +90,10 @@ val zmult : z -> z -> z val zcompare : z -> z -> comparison -val zabs : z -> z - val zmax : z -> z -> z +val zabs : z -> z + val zle_bool : z -> z -> bool val zge_bool : z -> z -> bool @@ -98,18 +102,22 @@ val zgt_bool : z -> z -> bool val zeq_bool : z -> z -> bool -val n_of_nat : nat -> n +val pgcdn : nat -> positive -> positive -> positive -val zdiv_eucl_POS : positive -> z -> z * z +val pgcd : positive -> positive -> positive -val zdiv_eucl : z -> z -> z * z +val zgcd : z -> z -> z + +val zdiv_eucl_POS : positive -> z -> z * z + +val zdiv_eucl : z -> z -> z * z val zdiv : z -> z -> z type 'c pol = - | Pc of 'c - | Pinj of positive * 'c pol - | PX of 'c pol * positive * 'c pol +| Pc of 'c +| Pinj of positive * 'c pol +| PX of 'c pol * positive * 'c pol val p0 : 'a1 -> 'a1 pol @@ -117,6 +125,8 @@ val p1 : 'a1 -> 'a1 pol val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool +val mkPinj : positive -> 'a1 pol -> 'a1 pol + val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol val mkPX : @@ -177,13 +187,13 @@ val psquare : bool) -> 'a1 pol -> 'a1 pol type 'c pExpr = - | PEc of 'c - | PEX of positive - | PEadd of 'c pExpr * 'c pExpr - | PEsub of 'c pExpr * 'c pExpr - | PEmul of 'c pExpr * 'c pExpr - | PEopp of 'c pExpr - | PEpow of 'c pExpr * n +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol @@ -200,14 +210,14 @@ val norm_aux : 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol type 'a bFormula = - | TT - | FF - | X - | A of 'a - | Cj of 'a bFormula * 'a bFormula - | D of 'a bFormula * 'a bFormula - | N of 'a bFormula - | I of 'a bFormula * 'a bFormula +| TT +| FF +| X +| A of 'a +| Cj of 'a bFormula * 'a bFormula +| D of 'a bFormula * 'a bFormula +| N of 'a bFormula +| I of 'a bFormula * 'a bFormula type 'term' clause = 'term' list @@ -217,41 +227,65 @@ val tt : 'a1 cnf val ff : 'a1 cnf -val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf +val add_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 + clause option + +val or_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 clause -> + 'a1 clause option + +val or_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> 'a1 + cnf -val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf +val or_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 cnf -> 'a1 cnf -> 'a1 + cnf val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf val xcnf : - ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 -> + 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool val tauto_checker : - ('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 - bFormula -> 'a3 list -> bool + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 -> + 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1 bFormula -> 'a3 list -> bool + +val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool + +val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool type 'c polC = 'c pol type op1 = - | Equal - | NonEqual - | Strict - | NonStrict +| Equal +| NonEqual +| Strict +| NonStrict -type 'c nFormula = 'c polC * op1 +type 'c nFormula = 'c polC * op1 + +val opMult : op1 -> op1 -> op1 option val opAdd : op1 -> op1 -> op1 option type 'c psatz = - | PsatzIn of nat - | PsatzSquare of 'c polC - | PsatzMulC of 'c polC * 'c psatz - | PsatzMulE of 'c psatz * 'c psatz - | PsatzAdd of 'c psatz * 'c psatz - | PsatzC of 'c - | PsatzZ +| PsatzIn of nat +| PsatzSquare of 'c polC +| PsatzMulC of 'c polC * 'c psatz +| PsatzMulE of 'c psatz * 'c psatz +| PsatzAdd of 'c psatz * 'c psatz +| PsatzC of 'c +| PsatzZ + +val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option + +val map_option2 : + ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option val pexpr_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> @@ -278,12 +312,12 @@ val check_normalised_formulas : bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool type op2 = - | OpEq - | OpNEq - | OpLe - | OpGe - | OpLt - | OpGt +| OpEq +| OpNEq +| OpLe +| OpGe +| OpLt +| OpGt type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr } @@ -357,16 +391,10 @@ val qpower_positive : q -> positive -> q val qpower : q -> z -> q -val pgcdn : nat -> positive -> positive -> positive - -val pgcd : positive -> positive -> positive - -val zgcd : z -> z -> z - type 'a t = - | Empty - | Leaf of 'a - | Node of 'a t * 'a * 'a t +| Empty +| Leaf of 'a +| Node of 'a t * 'a * 'a t val find : 'a1 -> 'a1 t -> positive -> 'a1 @@ -388,31 +416,35 @@ val xnegate0 : z formula -> z nFormula list val negate : z formula -> z nFormula cnf +val zunsat : z nFormula -> bool + +val zdeduce : z nFormula -> z nFormula -> z nFormula option + val ceiling : z -> z -> z type zArithProof = - | DoneProof - | RatProof of zWitness * zArithProof - | CutProof of zWitness * zArithProof - | EnumProof of zWitness * zWitness * zArithProof list +| DoneProof +| RatProof of zWitness * zArithProof +| CutProof of zWitness * zArithProof +| EnumProof of zWitness * zWitness * zArithProof list val zgcdM : z -> z -> z -val zgcd_pol : z polC -> z * z +val zgcd_pol : z polC -> z * z val zdiv_pol : z polC -> z -> z polC -val makeCuttingPlane : z polC -> z polC * z +val makeCuttingPlane : z polC -> z polC * z -val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option +val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option -val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula +val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula val is_pol_Z0 : z polC -> bool val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option -val check_inconsistent0 : z nFormula -> bool +val valid_cut_sign : op1 -> bool val zChecker : z nFormula list -> zArithProof -> bool @@ -428,6 +460,10 @@ val qnormalise : q formula -> q nFormula cnf val qnegate : q formula -> q nFormula cnf +val qunsat : q nFormula -> bool + +val qdeduce : q nFormula -> q nFormula -> q nFormula option + val qTautoChecker : q formula bFormula -> qWitness list -> bool type rWitness = z psatz @@ -438,5 +474,9 @@ val rnormalise : z formula -> z nFormula cnf val rnegate : z formula -> z nFormula cnf +val runsat : z nFormula -> bool + +val rdeduce : z nFormula -> z nFormula -> z nFormula option + val rTautoChecker : z formula bFormula -> rWitness list -> bool diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib index debc296e3..f53a9e379 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mllib @@ -1,6 +1,7 @@ Sos_types Mutils Micromega +Polynomial Mfourier Certificate Persistent_cache diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 80d66760d..c4dbf6af8 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -19,6 +19,12 @@ let debug = false +let rec pp_list f o l = + match l with + | [] -> () + | e::l -> f o e ; output_string o ";" ; pp_list f o l + + let finally f rst = try let res = f () in @@ -51,12 +57,16 @@ let iteri f l = | e::l -> f i e ; xiter (i+1) l in xiter 0 l -let mapi f l = - let rec xmap i l = - match l with - | [] -> [] - | e::l -> (f i e)::xmap (i+1) l in - xmap 0 l +let all_sym_pairs f l = + let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in + + let rec xpairs acc l = + match l with + | [] -> acc + | e::l -> xpairs (pair_with acc e l) l in + xpairs [] l + + let rec map3 f l1 l2 l3 = match l1 , l2 ,l3 with @@ -92,6 +102,18 @@ let interval n m = in interval_n ([],m) +let extract pred l = + List.fold_left (fun (fd,sys) e -> + match fd with + | None -> + begin + match pred e with + | None -> fd, e::sys + | Some v -> Some(v,e) , sys + end + | _ -> (fd, e::sys) + ) (None,[]) l + open Num open Big_int @@ -251,7 +273,7 @@ struct else if n land 1 = 1 then XI (positive (n lsr 1)) else XO (positive (n lsr 1)) - let n nt = + let n nt = if nt < 0 then assert false else if nt = 0 then N0 diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml new file mode 100644 index 000000000..d203f0e87 --- /dev/null +++ b/plugins/micromega/polynomial.ml @@ -0,0 +1,735 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-20011 *) +(* *) +(************************************************************************) + +open Num +module Utils = Mutils +open Utils + +type var = int + + +let (<+>) = add_num +let (<->) = minus_num +let (<*>) = mult_num + + +module Monomial : +sig + type t + val const : t + val is_const : t -> bool + val var : var -> t + val is_var : t -> bool + val find : var -> t -> int + val mult : var -> t -> t + val prod : t -> t -> t + val exp : t -> int -> t + val div : t -> t -> t * int + val compare : t -> t -> int + val pp : out_channel -> t -> unit + val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a + val sqrt : t -> t option +end + = +struct + (* A monomial is represented by a multiset of variables *) + module Map = Map.Make(struct type t = var let compare = Pervasives.compare end) + open Map + + type t = int Map.t + + let pp o m = Map.iter + (fun k v -> + if v = 1 then Printf.fprintf o "x%i." k + else Printf.fprintf o "x%i^%i." k v) m + + + (* The monomial that corresponds to a constant *) + let const = Map.empty + + let sum_degree m = Map.fold (fun _ n s -> s + n) m 0 + + (* Total ordering of monomials *) + let compare: t -> t -> int = + fun m1 m2 -> + let s1 = sum_degree m1 + and s2 = sum_degree m2 in + if s1 = s2 then Map.compare Pervasives.compare m1 m2 + else Pervasives.compare s1 s2 + + let is_const m = (m = Map.empty) + + (* The monomial 'x' *) + let var x = Map.add x 1 Map.empty + + let is_var m = + try + not (Map.fold (fun _ i fk -> + if fk = true (* first key *) + then + if i = 1 then false + else raise Not_found + else raise Not_found) m true) + with Not_found -> false + + let sqrt m = + if is_const m then None + else + try + Some (Map.fold (fun v i acc -> + let i' = i / 2 in + if i mod 2 = 0 + then add v i' m + else raise Not_found) m const) + with Not_found -> None + + (* Get the degre of a variable in a monomial *) + let find x m = try find x m with Not_found -> 0 + + (* Multiply a monomial by a variable *) + let mult x m = add x ( (find x m) + 1) m + + (* Product of monomials *) + let prod m1 m2 = Map.fold (fun k d m -> add k ((find k m) + d) m) m1 m2 + + + let exp m n = + let rec exp acc n = + if n = 0 then acc + else exp (prod acc m) (n - 1) in + + exp const n + + + (* [div m1 m2 = mr,n] such that mr * (m2)^n = m1 *) + let div m1 m2 = + let n = fold (fun x i n -> let i' = find x m1 in + let nx = i' / i in + min n nx) m2 max_int in + + let mr = fold (fun x i' m -> + let i = find x m2 in + let ir = i' - i * n in + if ir = 0 then m + else add x ir m) m1 empty in + (mr,n) + + + let fold = fold + +end + +module Poly : + (* A polynomial is a map of monomials *) + (* + This is probably a naive implementation + (expected to be fast enough - Coq is probably the bottleneck) + *The new ring contribution is using a sparse Horner representation. + *) +sig + type t + val get : Monomial.t -> t -> num + val variable : var -> t + val add : Monomial.t -> num -> t -> t + val constant : num -> t + val mult : Monomial.t -> num -> t -> t + val product : t -> t -> t + val addition : t -> t -> t + val uminus : t -> t + val fold : (Monomial.t -> num -> 'a -> 'a) -> t -> 'a -> 'a + val pp : out_channel -> t -> unit + val compare : t -> t -> int + val is_null : t -> bool + val is_linear : t -> bool +end = +struct + (*normalisation bug : 0*x ... *) + module P = Map.Make(Monomial) + open P + + type t = num P.t + + let pp o p = P.iter + (fun k v -> + if Monomial.compare Monomial.const k = 0 + then Printf.fprintf o "%s " (string_of_num v) + else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p + + (* Get the coefficient of monomial mn *) + let get : Monomial.t -> t -> num = + fun mn p -> try find mn p with Not_found -> (Int 0) + + + (* The polynomial 1.x *) + let variable : var -> t = + fun x -> add (Monomial.var x) (Int 1) empty + + (*The constant polynomial *) + let constant : num -> t = + fun c -> add (Monomial.const) c empty + + (* The addition of a monomial *) + + let add : Monomial.t -> num -> t -> t = + fun mn v p -> + if sign_num v = 0 then p + else + let vl = (get mn p) <+> v in + if sign_num vl = 0 then + remove mn p + else add mn vl p + + + (** Design choice: empty is not a polynomial + I do not remember why .... + **) + + (* The product by a monomial *) + let mult : Monomial.t -> num -> t -> t = + fun mn v p -> + if sign_num v = 0 + then constant (Int 0) + else + fold (fun mn' v' res -> P.add (Monomial.prod mn mn') (v<*>v') res) p empty + + + let addition : t -> t -> t = + fun p1 p2 -> fold (fun mn v p -> add mn v p) p1 p2 + + + let product : t -> t -> t = + fun p1 p2 -> + fold (fun mn v res -> addition (mult mn v p2) res ) p1 empty + + + let uminus : t -> t = + fun p -> map (fun v -> minus_num v) p + + let fold = P.fold + + let is_null p = fold (fun mn vl b -> b & sign_num vl = 0) p true + + let compare = compare compare_num + + let is_linear p = P.fold (fun m _ acc -> acc && (Monomial.is_const m || Monomial.is_var m)) p true + +(* let is_linear p = + let res = is_linear p in + Printf.printf "is_linear %a = %b\n" pp p res ; res +*) +end + + +module Vect = + struct + (** [t] is the type of vectors. + A vector [(x1,v1) ; ... ; (xn,vn)] is such that: + - variables indexes are ordered (x1 <c ... < xn + - values are all non-zero + *) + type var = int + type t = (var * num) list + +(** [equal v1 v2 = true] if the vectors are syntactically equal. + ([num] is not handled by [Pervasives.equal] *) + + let rec equal v1 v2 = + match v1 , v2 with + | [] , [] -> true + | [] , _ -> false + | _::_ , [] -> false + | (i1,n1)::v1 , (i2,n2)::v2 -> + (i1 = i2) && n1 =/ n2 && equal v1 v2 + + let hash v = + let rec hash i = function + | [] -> i + | (vr,vl)::l -> hash (i + (Hashtbl.hash (vr, float_of_num vl))) l in + Hashtbl.hash (hash 0 v ) + + + let null = [] + + let pp_vect o vect = + List.iter (fun (v,n) -> Printf.printf "%sx%i + " (string_of_num n) v) vect + + let from_list (l: num list) = + let rec xfrom_list i l = + match l with + | [] -> [] + | e::l -> + if e <>/ Int 0 + then (i,e)::(xfrom_list (i+1) l) + else xfrom_list (i+1) l in + + xfrom_list 0 l + + let zero_num = Int 0 + let unit_num = Int 1 + + + let to_list m = + let rec xto_list i l = + match l with + | [] -> [] + | (x,v)::l' -> + if i = x then v::(xto_list (i+1) l') else zero_num ::(xto_list (i+1) l) in + xto_list 0 m + + + let cons i v rst = if v =/ Int 0 then rst else (i,v)::rst + + let rec update i f t = + match t with + | [] -> cons i (f zero_num) [] + | (k,v)::l -> + match Pervasives.compare i k with + | 0 -> cons k (f v) l + | -1 -> cons i (f zero_num) t + | 1 -> (k,v) ::(update i f l) + | _ -> failwith "compare_num" + + let rec set i n t = + match t with + | [] -> cons i n [] + | (k,v)::l -> + match Pervasives.compare i k with + | 0 -> cons k n l + | -1 -> cons i n t + | 1 -> (k,v) :: (set i n l) + | _ -> failwith "compare_num" + + let gcd m = + let res = List.fold_left (fun x (i,e) -> Big_int.gcd_big_int x (Utils.numerator e)) Big_int.zero_big_int m in + if Big_int.compare_big_int res Big_int.zero_big_int = 0 + then Big_int.unit_big_int else res + + let rec mul z t = + match z with + | Int 0 -> [] + | Int 1 -> t + | _ -> List.map (fun (i,n) -> (i, mult_num z n)) t + + + let rec add v1 v2 = + match v1 , v2 with + | (x1,n1)::v1' , (x2,n2)::v2' -> + if x1 = x2 + then + let n' = n1 +/ n2 in + if n' =/ Int 0 then add v1' v2' + else + let res = add v1' v2' in + (x1,n') ::res + else if x1 < x2 + then let res = add v1' v2 in + (x1, n1)::res + else let res = add v1 v2' in + (x2, n2)::res + | [] , [] -> [] + | [] , _ -> v2 + | _ , [] -> v1 + + + + + let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical + [ + (fun () -> Pervasives.compare (fst x) (fst y)); + (fun () -> compare_num (snd x) (snd y))]) + + (** [tail v vect] returns + - [None] if [v] is not a variable of the vector [vect] + - [Some(vl,rst)] where [vl] is the value of [v] in vector [vect] + and [rst] is the remaining of the vector + We exploit that vectors are ordered lists + *) + let rec tail (v:var) (vect:t) = + match vect with + | [] -> None + | (v',vl)::vect' -> + match Pervasives.compare v' v with + | 0 -> Some (vl,vect) (* Ok, found *) + | -1 -> tail v vect' (* Might be in the tail *) + | _ -> None (* Hopeless *) + + let get v vect = + match tail v vect with + | None -> None + | Some(vl,_) -> Some vl + + + let rec fresh v = + match v with + | [] -> 1 + | [v,_] -> v + 1 + | _::v -> fresh v + + end + +type vector = Vect.t + +type cstr_compat = {coeffs : vector ; op : op ; cst : num} +and op = |Eq | Ge + +let string_of_op = function Eq -> "=" | Ge -> ">=" + +let output_cstr o {coeffs = coeffs ; op = op ; cst = cst} = + Printf.fprintf o "%a %s %s" Vect.pp_vect coeffs (string_of_op op) (string_of_num cst) + +let opMult o1 o2 = + match o1, o2 with + | Eq , Eq -> Eq + | Eq , Ge | Ge , Eq -> Ge + | Ge , Ge -> Ge + +let opAdd o1 o2 = + match o1 , o2 with + | Eq , _ | _ , Eq -> Eq + | Ge , Ge -> Ge + + + + +open Big_int + +type index = int + +type prf_rule = + | Hyp of int + | Def of int + | Cst of big_int + | Zero + | Square of (Vect.t * num) + | MulC of (Vect.t * num) * prf_rule + | Gcd of big_int * prf_rule + | MulPrf of prf_rule * prf_rule + | AddPrf of prf_rule * prf_rule + | CutPrf of prf_rule + +type proof = + | Done + | Step of int * prf_rule * proof + | Enum of int * prf_rule * Vect.t * prf_rule * proof list + + +let rec output_prf_rule o = function + | Hyp i -> Printf.fprintf o "Hyp %i" i + | Def i -> Printf.fprintf o "Def %i" i + | Cst c -> Printf.fprintf o "Cst %s" (string_of_big_int c) + | Zero -> Printf.fprintf o "Zero" + | Square _ -> Printf.fprintf o "( )^2" + | MulC(p,pr) -> Printf.fprintf o "P * %a" output_prf_rule pr + | MulPrf(p1,p2) -> Printf.fprintf o "%a * %a" output_prf_rule p1 output_prf_rule p2 + | AddPrf(p1,p2) -> Printf.fprintf o "%a + %a" output_prf_rule p1 output_prf_rule p2 + | CutPrf(p) -> Printf.fprintf o "[%a]" output_prf_rule p + | Gcd(c,p) -> Printf.fprintf o "(%a)/%s" output_prf_rule p (string_of_big_int c) + +let rec output_proof o = function + | Done -> Printf.fprintf o "." + | Step(i,p,pf) -> Printf.fprintf o "%i:= %a ; %a" i output_prf_rule p output_proof pf + | Enum(i,p1,v,p2,pl) -> Printf.fprintf o "%i{%a<=%a<=%a}%a" i + output_prf_rule p1 Vect.pp_vect v output_prf_rule p2 + (pp_list output_proof) pl + +let rec pr_rule_max_id = function + | Hyp i | Def i -> i + | Cst _ | Zero | Square _ -> -1 + | MulC(_,p) | CutPrf p | Gcd(_,p) -> pr_rule_max_id p + | MulPrf(p1,p2)| AddPrf(p1,p2) -> max (pr_rule_max_id p1) (pr_rule_max_id p2) + +let rec proof_max_id = function + | Done -> -1 + | Step(i,pr,prf) -> max i (max (pr_rule_max_id pr) (proof_max_id prf)) + | Enum(i,p1,_,p2,l) -> + let m = max (pr_rule_max_id p1) (pr_rule_max_id p2) in + List.fold_left (fun i prf -> max i (proof_max_id prf)) (max i m) l + +let rec pr_rule_def_cut id = function + | MulC(p,prf) -> + let (bds,id',prf') = pr_rule_def_cut id prf in + (bds, id', MulC(p,prf')) + | MulPrf(p1,p2) -> + let (bds1,id,p1) = pr_rule_def_cut id p1 in + let (bds2,id,p2) = pr_rule_def_cut id p2 in + (bds2@bds1,id,MulPrf(p1,p2)) + | AddPrf(p1,p2) -> + let (bds1,id,p1) = pr_rule_def_cut id p1 in + let (bds2,id,p2) = pr_rule_def_cut id p2 in + (bds2@bds1,id,AddPrf(p1,p2)) + | CutPrf p -> + let (bds,id,p) = pr_rule_def_cut id p in + ((id,p)::bds,id+1,Def id) + | Gcd(c,p) -> + let (bds,id,p) = pr_rule_def_cut id p in + ((id,p)::bds,id+1,Def id) + | Square _|Cst _|Def _|Hyp _|Zero as x -> ([],id,x) + + +(* Do not define top-level cuts *) +let pr_rule_def_cut id = function + | CutPrf p -> + let (bds,ids,p') = pr_rule_def_cut id p in + bds,ids, CutPrf p' + | p -> pr_rule_def_cut id p + + +let rec implicit_cut p = + match p with + | CutPrf p -> implicit_cut p + | _ -> p + + +let rec normalise_proof id prf = + match prf with + | Done -> (id,Done) + | Step(i,Gcd(c,p),Done) -> normalise_proof id (Step(i,p,Done)) + | Step(i,p,prf) -> + let bds,id,p' = pr_rule_def_cut id p in + let (id,prf) = normalise_proof id prf in + let prf = List.fold_left (fun acc (i,p) -> Step(i, CutPrf p,acc)) + (Step(i,p',prf)) bds in + + (id,prf) + | Enum(i,p1,v,p2,pl) -> + (* Why do I have top-level cuts ? *) +(* let p1 = implicit_cut p1 in + let p2 = implicit_cut p2 in + let (ids,prfs) = List.split (List.map (normalise_proof id) pl) in + (List.fold_left max 0 ids , + Enum(i,p1,v,p2,prfs)) +*) + + let bds1,id,p1' = pr_rule_def_cut id (implicit_cut p1) in + let bds2,id,p2' = pr_rule_def_cut id (implicit_cut p2) in + let (ids,prfs) = List.split (List.map (normalise_proof id) pl) in + (List.fold_left max 0 ids , + List.fold_left (fun acc (i,p) -> Step(i, CutPrf p,acc)) + (Enum(i,p1',v,p2',prfs)) (bds2@bds1)) + + +let normalise_proof id prf = + let res = normalise_proof id prf in + if debug then Printf.printf "normalise_proof %a -> %a" output_proof prf output_proof (snd res) ; + res + + + +let add_proof x y = + match x, y with + | Zero , p | p , Zero -> p + | _ -> AddPrf(x,y) + + +let mul_proof c p = + match sign_big_int c with + | 0 -> Zero (* This is likely to be a bug *) + | -1 -> MulC(([],Big_int c),p) (* [p] should represent an equality *) + | 1 -> + if eq_big_int c unit_big_int + then p + else MulPrf(Cst c,p) + | _ -> assert false + + +let mul_proof_ext (p,c) prf = + match p with + | [] -> mul_proof (numerator c) prf + | _ -> MulC((p,c),prf) + + + +(* + let rec scale_prf_rule = function + | Hyp i -> (unit_big_int, Hyp i) + | Def i -> (unit_big_int, Def i) + | Cst c -> (unit_big_int, Cst i) + | Zero -> (unit_big_int, Zero) + | Square p -> (unit_big_int,Square p) + | Div(c,pr) -> + let (bi,pr') = scale_prf_rule pr in + (mult_big_int c bi , pr') + | MulC(p,pr) -> + let bi,pr' = scale_prf_rule pr in + (bi,MulC p,pr') + | MulPrf(p1,p2) -> + let b1,p1 = scale_prf_rule p1 in + let b2,p2 = scale_prf_rule p2 in + + + | AddPrf(p1,p2) -> + let b1,p1 = scale_prf_rule p1 in + let b2,p2 = scale_prf_rule p2 in + let g = gcd_big_int +*) + + + + + +module LinPoly = +struct + type t = Vect.t * num + + module MonT = + struct + module MonoMap = Map.Make(Monomial) + module IntMap = Map.Make(struct type t = int let compare = Pervasives.compare end) + + (** A hash table might be preferable but requires a hash function. *) + let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) + let (monomial_of_index : Monomial.t IntMap.t ref) = ref (IntMap.empty) + + + let fresh = ref 0 + + let register m = + try + MonoMap.find m !index_of_monomial + with Not_found -> + begin + let res = !fresh in + index_of_monomial := MonoMap.add m res !index_of_monomial ; + monomial_of_index := IntMap.add res m !monomial_of_index ; + incr fresh ; res + end + + let retrieve i = IntMap.find i !monomial_of_index + + + end + + let normalise (v,c) = + (List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) v , c) + + + let output_mon o (x,v) = + Printf.fprintf o "%s.%a +" (string_of_num v) Monomial.pp (MonT.retrieve x) + + + + let output_cstr o {coeffs = coeffs ; op = op ; cst = cst} = + Printf.fprintf o "%a %s %s" (pp_list output_mon) coeffs (string_of_op op) (string_of_num cst) + + + + let linpol_of_pol p = + let (v,c) = + Poly.fold + (fun mon num (vct,cst) -> + if Monomial.is_const mon then (vct,num) + else + let vr = MonT.register mon in + ((vr,num)::vct,cst)) p ([], Int 0) in + normalise (v,c) + + let mult v m (vect,c) = + if Monomial.is_const m + then + (Vect.mul v vect, v <*> c) + else + if sign_num v <> 0 + then + let hd = + if sign_num c <> 0 + then [MonT.register m,v <*> c] + else [] in + + let vect = hd @ (List.map (fun (x,n) -> + let x = MonT.retrieve x in + let x_m = MonT.register (Monomial.prod m x) in + (x_m, v <*> n)) vect ) in + normalise (vect , Int 0) + else ([],Int 0) + + let mult v m (vect,c) = + let (vect',c') = mult v m (vect,c) in + if debug then + Printf.printf "mult %s %a (%a,%s) -> (%a,%s)\n" (string_of_num v) Monomial.pp m + (pp_list output_mon) vect (string_of_num c) + (pp_list output_mon) vect' (string_of_num c') ; + (vect',c') + + + + let make_lin_pol v mon = + if Monomial.is_const mon + then [] , v + else [MonT.register mon, v],Int 0 + + + + + + + let xpivot_eq (c,prf) x v (c',prf') = + if debug then Printf.printf "xpivot_eq {%a} %a %s {%a}\n" + output_cstr c + Monomial.pp (MonT.retrieve x) + (string_of_num v) output_cstr c' ; + + + let {coeffs = coeffs ; op = op ; cst = cst} = c' in + let m = MonT.retrieve x in + + let apply_pivot (vqn,q,n) (c',prf') = + (* Morally, we have (Vect.get (q*x^n) c'.coeffs) = vmn with n >=0 *) + + let cc' = abs_num v in + let cc_num = Int (- (sign_num v)) <*> vqn in + let cc_mon = Monomial.prod q (Monomial.exp m (n-1)) in + + let (c_coeff,c_cst) = mult cc_num cc_mon (c.coeffs, minus_num c.cst) in + + let c' = {coeffs = Vect.add (Vect.mul cc' c'.coeffs) c_coeff ; op = op ; cst = (minus_num c_cst) <+> (cc' <*> c'.cst)} in + let prf' = add_proof + (mul_proof_ext (make_lin_pol cc_num cc_mon) prf) + (mul_proof (numerator cc') prf') in + + if debug then Printf.printf "apply_pivot -> {%a}\n" output_cstr c' ; + (c',prf') in + + + let cmp (q,n) (q',n') = + if n < n' then -1 + else if n = n' then Monomial.compare q q' + else 1 in + + + let find_pivot (c',prf') = + let (v,q,n) = List.fold_left + (fun (v,q,n) (x,v') -> + let x = MonT.retrieve x in + let (q',n') = Monomial.div x m in + if cmp (q,n) (q',n') = -1 then (v',q',n') else (v,q,n)) (Int 0, Monomial.const,0) c'.coeffs in + if n > 0 then Some (v,q,n) else None in + + let rec pivot (q,n) (c',prf') = + match find_pivot (c',prf') with + | None -> (c',prf') + | Some(v,q',n') -> + if cmp (q',n') (q,n) = -1 + then pivot (q',n') (apply_pivot (v,q',n') (c',prf')) + else (c',prf') in + + pivot (Monomial.const,max_int) (c',prf') + + + let pivot_eq x (c,prf) = + match Vect.get x c.coeffs with + | None -> (fun x -> None) + | Some v -> fun cp' -> Some (xpivot_eq (c,prf) x v cp') + + +end |