Commit 588b5df8 authored by Andrei Paskevich's avatar Andrei Paskevich

upgrade Alt-Ergo proofs to 0.95.1

in three cases, we use a proof by an earlier version of Alt-Ergo
as a sample for bisection and then reprove it with other provers.

Also, moved all sessions in theories/ and modules/ to
tests/theory-sessions/. These sessions are not replayed
by nightly-builds and should not be distributed.
Please, do not run why3ide on the standard library files,
make separate files in examples/ using those theories, or
just realize them in Coq. Don't clobber the loadpath.
parent 20a82b81
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="Z3"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
......@@ -4,37 +4,29 @@
<prover
id="0"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.94"/>
<prover
id="2"
name="Alt-Ergo"
version="0.95.1"/>
<prover
id="3"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="4"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="5"
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="6"
id="4"
name="Z3"
version="2.19"/>
<prover
id="7"
id="5"
name="Z3"
version="3.2"/>
<prover
id="8"
id="6"
name="Z3"
version="4.3.1"/>
<file
......@@ -56,7 +48,7 @@
expanded="false"
shape="ainfix &lt;=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F">
<proof
prover="5"
prover="3"
timelimit="10"
memlimit="1000"
edited="alphaBeta_TwoPlayerGame_Test_1.v"
......@@ -65,7 +57,7 @@
<result status="valid" time="0.51"/>
</proof>
<proof
prover="6"
prover="4"
timelimit="10"
memlimit="1000"
obsolete="false"
......@@ -73,7 +65,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="10"
memlimit="1000"
obsolete="false"
......@@ -90,7 +82,7 @@
expanded="false"
shape="ainfix &lt;aminmaxV0V1ainfinityAainfix &lt;aprefix -ainfinityaminmaxV0V1Iainfix &gt;=V1c0F">
<proof
prover="5"
prover="3"
timelimit="3"
memlimit="1000"
edited="alphaBeta_TwoPlayerGame_minmax_bound_1.v"
......@@ -113,7 +105,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -121,7 +113,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -129,14 +121,6 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
......@@ -145,18 +129,10 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -164,7 +140,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -219,7 +195,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......@@ -229,32 +205,16 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -262,7 +222,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -376,7 +336,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -399,7 +359,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -407,7 +367,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -427,7 +387,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -435,7 +395,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -455,7 +415,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -463,7 +423,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -500,7 +460,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -508,7 +468,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -516,7 +476,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -536,7 +496,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -544,7 +504,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -552,7 +512,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -572,7 +532,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -580,7 +540,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -588,7 +548,7 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -610,7 +570,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -618,7 +578,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -626,7 +586,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -658,7 +618,7 @@
<label
name="expl:VC for negabeta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -666,7 +626,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -674,7 +634,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -723,7 +683,7 @@
<label
name="expl:VC for negabeta_rec"/>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -743,7 +703,7 @@
<label
name="expl:VC for negabeta_rec"/>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -775,7 +735,7 @@
<label
name="expl:VC for negabeta_rec"/>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -809,7 +769,7 @@
<label
name="expl:VC for alpha_beta"/>
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -817,7 +777,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -825,7 +785,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
prover="6"
timelimit="3"
memlimit="1000"
obsolete="false"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="Z3"
......@@ -62,7 +62,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="CVC3"
......
This diff is collapsed.
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.95.1"/>
<prover
id="1"
name="Z3"
......
......@@ -149,13 +149,20 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
(x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = 1%Z).
Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\
(x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\
(x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x
(pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z ->
((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)).
Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\
(x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x
y) = (-2%Z)%Z).
Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z ->
((((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z)).
Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
......@@ -282,7 +289,7 @@ Axiom to_nat_of_one : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\
i) = ((pow2 ((j - i)%Z + 1%Z)%Z) - 1%Z)%Z)).
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.94" timelimit 5.
Ltac ae := why3 "alt-ergo" timelimit 5.
Open Scope Z_scope.
(* Why3 goal *)
......@@ -306,7 +313,7 @@ destruct h.
rewrite to_nat_sub_zero; auto with zarith.
ae.
rewrite to_nat_sub_one; auto with zarith.
ae.
why3 "alt-ergo" timelimit 15.
Qed.
......@@ -4,29 +4,25 @@
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.1"/>
<prover
id="2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="3"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="4"
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="5"
id="4"
name="Z3"
version="2.19"/>
<prover
id="6"
id="5"
name="Z3"
version="3.2"/>
<file
......@@ -60,14 +56,6 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.57"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.33"/>
</proof>
</goal>
......@@ -85,14 +73,6 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.75"/>