Skip to content

GitLab

why3
why3
Commit d1526cc9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Merge branch 'master' into claude

parents ad4f0165 8d30888a
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 577 additions and 565 deletions
Makefile.in
View file @ d1526cc9
......@@ -1618,7 +1618,7 @@ STDLIBS = algebra \
sum
# function ? tptp ?
STDMODS = array hashtbl impset pqueue queue random ref stack string
STDMODS = array matrix hashtbl impset pqueue queue random ref stack string
STDMACS = array int
......
bench/bench
View file @ d1526cc9
......@@ -105,37 +105,45 @@ extract_and_run () {
shift
echo -n "$dir... "
rm -f $dir/$prg
echo -n "extract... "
if BENCH=yes make -C $dir extract > /dev/null 2>&1; then
echo -n "compile... "
if BENCH=yes make -C $dir > /dev/null 2>&1; then
echo -n "execute... "
if $dir/main.opt "$@" > /dev/null 2>&1; then
echo -n "doc... "
if BENCH=yes make -C $dir doc > /dev/null 2>&1; then
echo "ok"
else
echo "documentation failed!"
echo BENCH=yes make -C $dir doc
BENCH=yes make -C $dir doc
exit 1
fi
else
echo "execution failed!"
echo $dir/main.opt "$@"
$dir/main.opt "$@"
exit 1
fi
echo -n "clean... "
if BENCH=yes make -C $dir clean > /dev/null 2>&1; then
echo -n "extract... "
if BENCH=yes make -C $dir extract > /dev/null 2>&1; then
echo -n "compile... "
if BENCH=yes make -C $dir > /dev/null 2>&1; then
echo -n "execute... "
if $dir/main.opt "$@" > /dev/null 2>&1; then
echo -n "doc... "
if BENCH=yes make -C $dir doc > /dev/null 2>&1; then
echo "ok"
else
echo "documentation failed!"
echo BENCH=yes make -C $dir doc
BENCH=yes make -C $dir doc
exit 1
fi
else
echo "execution failed!"
echo $dir/main.opt "$@"
$dir/main.opt "$@"
exit 1
fi
else
echo "compilation failed!"
echo BENCH=yes make -C $dir
BENCH=yes make -C $dir
exit 1
fi
else
echo "compilation failed!"
echo BENCH=yes make -C $dir
BENCH=yes make -C $dir
echo "extract failed!"
echo BENCH=yes make -C $dir extract
BENCH=yes make -C $dir extract
exit 1
fi
else
echo "extract failed!"
echo BENCH=yes make -C $dir extract
BENCH=yes make -C $dir extract
echo "clean failed!"
echo BENCH=yes make -C $dir clean
BENCH=yes make -C $dir clean
exit 1
fi
}
......
examples/check-builtin/int/why3session.xml
View file @ d1526cc9
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Eprover" version="1.6" timelimit="5" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Eprover" version="1.6" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="4" name="Spass" version="3.7" timelimit="10" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" memlimit="0"/>
......@@ -12,25 +12,25 @@
<file name="../int.why" expanded="true">
<theory name="Test" sum="fc4f5a5b6868cb7535da7ff9ae921fff" expanded="true">
<goal name="G1" expanded="true">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.99"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.06"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="timeout" time="4.98"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.98"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.04"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="10.09"/></proof>
<proof prover="6"><result status="timeout" time="10.09"/></proof>
</goal>
<goal name="CompatOrderAdd" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -39,25 +39,25 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="CompatOrderMult" expanded="true">
<proof prover="0"><result status="valid" time="1.28"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="1.28"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="InvMult" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.86"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="InvSquare" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -66,7 +66,7 @@
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="ZeroMult" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -75,25 +75,25 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="SquareNonNeg1" expanded="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.04"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="10.10"/></proof>
<proof prover="6"><result status="timeout" time="10.10"/></proof>
</goal>
<goal name="SquareNonNeg" expanded="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.74"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="unknown" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
</goal>
<goal name="ZeroLessOne" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -104,13 +104,13 @@
</theory>
<theory name="MinMax" sum="5a65a1cfb37258d4746169718f12d1d3" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="timeout" time="4.96"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="0"><result status="timeout" time="10.06"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="unknown" time="10.03"/></proof>
<proof prover="6"><result status="timeout" time="10.03"/></proof>
</goal>
</theory>
</file>
......
examples/gcd/why3session.xml
View file @ d1526cc9
......@@ -29,7 +29,7 @@
<proof prover="5" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. postcondition">
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="0.92"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
......@@ -75,7 +75,7 @@
<proof prover="5" memlimit="1000"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="gcd_even_odd">
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="1.78"/></proof>
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="gcd_even_odd2">
<proof prover="5" memlimit="1000"><result status="valid" time="0.17" steps="28"/></proof>
......@@ -160,7 +160,7 @@
<proof prover="6"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.20" expl="20. precondition">
<proof prover="4"><result status="valid" time="6.49"/></proof>
<proof prover="4"><result status="valid" time="3.49"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.03" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -171,29 +171,29 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31" sum="d566d8cda9a9bac5bbc9bd41ecf5cfb3" expanded="true">
<theory name="EuclideanAlgorithm31" sum="7e6c4a6c940f11f7bb2278b052b9d3e7" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. division by zero">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. integer overflow">
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="46"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="51"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease">
<proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="114"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="169"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. precondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="21"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition">
<proof prover="5" timelimit="5"><result status="valid" time="0.97" steps="42"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="45"/></proof>
</goal>
</transf>
</goal>
......
examples/logic/bitvectors/why3session.xml
View file @ d1526cc9
......@@ -53,19 +53,19 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="g7b" expanded="true">
<proof prover="1"><result status="timeout" time="2.96"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="g8a" expanded="true">
<proof prover="1"><result status="timeout" time="2.93"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="g8b" expanded="true">
<proof prover="1"><result status="timeout" time="3.01"/></proof>
<proof prover="1"><result status="timeout" time="4.00"/></proof>
</goal>
<goal name="Nth_bw_and">
<proof prover="1"><result status="valid" time="0.16"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_bw_or">
<proof prover="1"><result status="valid" time="0.16"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_bw_xor">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -82,7 +82,7 @@
<goal name="Lsr_nth_low" expanded="true">
</goal>
<goal name="Lsr_nth_high" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Asr_nth_low" expanded="true">
</goal>
......
examples/logic/einstein/why3session.xml
View file @ d1526cc9
......@@ -5,19 +5,18 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="30" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.6" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="14" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="5" name="Spass" version="3.7" timelimit="30" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="7" name="Spass" version="3.7" timelimit="30" memlimit="1000"/>
<prover id="8" name="Yices" version="1.0.38" timelimit="7" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="7" memlimit="0"/>
<prover id="8" name="Metis" version="2.3" timelimit="5" memlimit="4000"/>
<prover id="9" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="10" name="Metis" version="2.3" timelimit="5" memlimit="4000"/>
<prover id="11" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="12" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="13" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="14" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="15" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
<theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -27,55 +26,52 @@
<goal name="G1" expanded="true">
<proof prover="0"><result status="valid" time="13.44" steps="1560"/></proof>
<proof prover="2"><result status="unknown" time="0.17"/></proof>
<proof prover="3" timelimit="17"><result status="valid" time="21.79"/></proof>
<proof prover="4"><result status="valid" time="1.20"/></proof>
<proof prover="5" timelimit="5"><result status="unknown" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="4.51"/></proof>
<proof prover="7"><result status="valid" time="5.72"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="3" timelimit="5"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.88"/></proof>
<proof prover="5"><result status="valid" time="4.35"/></proof>
<proof prover="6"><result status="valid" time="3.56"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8" memlimit="1000"><result status="timeout" time="9.99"/></proof>
<proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10" memlimit="1000"><result status="unknown" time="9.99"/></proof>
<proof prover="11"><result status="valid" time="4.13"/></proof>
<proof prover="10"><result status="valid" time="2.88"/></proof>
<proof prover="11"><result status="valid" time="12.38" steps="969"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="12.38" steps="969"/></proof>
<proof prover="14"><result status="unknown" time="0.06"/></proof>
<proof prover="15"><result status="valid" time="2.72"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="Wrong" expanded="true">
<proof prover="0"><result status="unknown" time="15.98"/></proof>
<proof prover="1" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3" timelimit="5"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4" timelimit="5"><result status="timeout" time="4.95"/></proof>
<proof prover="5"><result status="unknown" time="0.04"/></proof>
<proof prover="5" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="6" timelimit="5"><result status="timeout" time="4.97"/></proof>
<proof prover="7" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="8" timelimit="5"><result status="unknown" time="0.00"/></proof>
<proof prover="7" timelimit="5"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="timeout" time="10.02"/></proof>
<proof prover="9" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="10"><result status="unknown" time="10.02"/></proof>
<proof prover="11"><result status="timeout" time="5.00"/></proof>
<proof prover="10"><result status="timeout" time="5.00"/></proof>
<proof prover="11"><result status="unknown" time="9.98"/></proof>
<proof prover="12"><result status="timeout" time="4.97"/></proof>
<proof prover="13"><result status="unknown" time="9.98"/></proof>
<proof prover="14"><result status="unknown" time="0.06"/></proof>
<proof prover="15" timelimit="5"><result status="unknown" time="10.08"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14" timelimit="5"><result status="timeout" time="10.08"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="12.12" steps="1747"/></proof>
<proof prover="1"><result status="valid" time="33.44"/></proof>
<proof prover="1"><result status="valid" time="17.81"/></proof>
<proof prover="2" timelimit="30"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="13.26"/></proof>
<proof prover="4"><result status="valid" time="2.70"/></proof>
<proof prover="5"><result status="unknown" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="4.45"/></proof>
<proof prover="7"><result status="valid" time="5.40"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.83"/></proof>
<proof prover="10"><result status="valid" time="7.04"/></proof>
<proof prover="11"><result status="valid" time="1.71"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="1.99"/></proof>
<proof prover="5"><result status="valid" time="4.18"/></proof>
<proof prover="6"><result status="valid" time="3.46"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="3.74"/></proof>
<proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="valid" time="7.55" steps="1007"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="7.55" steps="1007"/></proof>
<proof prover="14" timelimit="3"><result status="unknown" time="0.06"/></proof>
<proof prover="15"><result status="valid" time="2.66"/></proof>
<proof prover="13" timelimit="3"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof>
</goal>
</theory>
</file>
......
examples/tests-provers/div/why3session.xml
View file @ d1526cc9
This diff is collapsed.
lib/coq/map/Occ.v
View file @ d1526cc9
......@@ -5,76 +5,76 @@ Require BuiltIn.
Require int.Int.
Require map.Map.
Require Recdef.
Function occ_ (a:Type) (a_WT:WhyType a) (v:a) (m: map.Map.map Z a)
(l: Z) (delta: Z) {measure Zabs_nat delta } : Z :=
if Z_le_gt_dec delta 0%Z then 0%Z else
((if why_decidable_eq (map.Map.get m (l + delta - 1)%Z) v then 1 else 0) +
occ_ a a_WT v m l (delta-1))%Z.
intros a a_WT _ _ _ delta h.
destruct (Z_le_gt_dec delta 0); intros.
now omega.
now apply Zabs_nat_lt; omega.
Defined.
(* Why3 goal *)
Definition occ: forall {a:Type} {a_WT:WhyType a}, a -> (map.Map.map Z a) ->
Z -> Z -> Z.
Proof.
intros a a_WT v m l u.
exact (occ_ a a_WT v m l (u-l)%Z).
induction (Z.to_nat (u-l)) as [|delta occ_].
exact Z0.
exact ((if why_decidable_eq (map.Map.get m (l + Z_of_nat delta)%Z) v then 1 else 0) + occ_)%Z.
Defined.
Lemma occ_equation :
forall {a:Type} {a_WT:WhyType a} v m l u,
(l < u)%Z ->
occ v m l u =
((if why_decidable_eq (map.Map.get m (u - 1)%Z) v then 1 else 0) + occ v m l (u - 1))%Z.
Proof.
intros a a_WT v m l u Hlu.
assert (0 < u - l)%Z as h1' by omega.
unfold occ.
replace (u - 1 - l)%Z with (u - l - 1)%Z by ring.
replace (u - 1)%Z with (l + (u - l - 1))%Z by ring.
rewrite <- (Z2Nat.id (u - l - 1)) by omega.
rewrite (Z2Nat.inj_sub _ 1) by easy.
destruct (u - l)%Z ; try easy.
simpl.
assert (exists n, Pos.to_nat p = S n) as [n ->].
exists (Z.to_nat (Zpred (Zpos p))).
rewrite Z2Nat.inj_pred.
apply (S_pred _ O).
apply Pos2Nat.is_pos.
simpl.
now rewrite <- minus_n_O, Nat2Z.id.
Qed.
(* Why3 goal *)
Lemma occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (u <= l)%Z -> ((occ v m l u) = 0%Z).
Proof.
intros a a_WT v m l u h1.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
now trivial.
omega.
assert (u - l <= 0)%Z as h1' by omega.
unfold occ.
destruct (u - l)%Z ; try easy.
now elim h1'.
Qed.
(* Why3 goal *)
Lemma occ_right_no_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((map.Map.get m
(u - 1%Z)%Z) = v)) -> ((occ v m l u) = (occ v m l (u - 1%Z)%Z))).
Proof.
intros a a_WT v m l u h1 h2.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
rewrite occ__equation.
destruct (Z_le_gt_dec (u - 1 - l) 0)%Z; intros.
now trivial.
omega.
destruct (why_decidable_eq (Map.get m (l + (u - l) - 1)%Z) v).
replace (l + (u - l) - 1)%Z with (u-1)%Z in e by omega.
intuition.
replace (u - 1 - l)%Z with (u - l - 1)%Z by omega.
ring.
rewrite occ_equation with (1 := h1).
now destruct why_decidable_eq as [H|H].
Qed.
(* Why3 goal *)
Lemma occ_right_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (l < u)%Z -> (((map.Map.get m
(u - 1%Z)%Z) = v) -> ((occ v m l u) = (1%Z + (occ v m l (u - 1%Z)%Z))%Z)).
Proof.
intros a a_WT v m l u h1 h2.
unfold occ. rewrite occ__equation.
destruct (Z_le_gt_dec (u - l) 0)%Z; intros.
rewrite occ__equation.
destruct (Z_le_gt_dec (u - 1 - l) 0)%Z; intros.
omega.
omega.
destruct (why_decidable_eq (Map.get m (l + (u - l) - 1)%Z) v).
replace (u - 1 - l)%Z with (u - l - 1)%Z by omega.
ring.
replace (l + (u - l) - 1)%Z with (u-1)%Z in n by omega.
intuition.
rewrite occ_equation with (1 := h1).
now destruct why_decidable_eq as [H|H].
Qed.
(* Why3 goal *)
Lemma occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (l <= u)%Z -> ((0%Z <= (occ v m l
u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z).
Proof.
intros a a_WT v m l u h1.
cut (0 <= u - l)%Z. 2: omega.
replace (occ v m l u) with (occ v m l (l + (u - l)))%Z.
......@@ -107,6 +107,7 @@ Qed.
Lemma occ_append : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (mid:Z) (u:Z), ((l <= mid)%Z /\
(mid <= u)%Z) -> ((occ v m l u) = ((occ v m l mid) + (occ v m mid u))%Z).
Proof.
intros a a_WT v m l mid u (h1,h2).
cut (0 <= u - mid)%Z. 2: omega.
replace (occ v m l u) with (occ v m l (mid + (u - mid)))%Z.
......@@ -150,6 +151,7 @@ Qed.
Lemma occ_neq : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> ~ ((map.Map.get m i) = v)) -> ((occ v m l u) = 0%Z).
Proof.
intros a a_WT v m l u.
assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.
rewrite occ_empty. trivial. omega.
......@@ -176,6 +178,7 @@ Qed.
Lemma occ_exists : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m:(map.Map.map Z a)) (l:Z) (u:Z), (0%Z < (occ v m l u))%Z -> exists i:Z,
((l <= i)%Z /\ (i < u)%Z) /\ ((map.Map.get m i) = v).
Proof.
intros a a_WT v m l u h1.
assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.
rewrite occ_empty in h1. elimtype False; omega. omega.
......@@ -200,6 +203,7 @@ Qed.
Lemma occ_pos : forall {a:Type} {a_WT:WhyType a}, forall (m:(map.Map.map Z
a)) (l:Z) (u:Z) (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
(0%Z < (occ (map.Map.get m i) m l u))%Z.
Proof.
intros a a_WT m l u i (h1,h2).
pose (v := (Map.get m i)). fold v.
assert (occ v m l u = occ v m l i + occ v m i u)%Z.
......@@ -221,6 +225,7 @@ Lemma occ_eq : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
(m1:(map.Map.map Z a)) (m2:(map.Map.map Z a)) (l:Z) (u:Z), (forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get m1 i) = (map.Map.get m2 i))) ->
((occ v m1 l u) = (occ v m2 l u)).
Proof.
intros a a_WT v m1 m2 l u h1.
assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.