Skip to content

why3
why3
Commit b0fff343 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

improve eval_match

parent d6c0afc8
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 10362 additions and 8048 deletions
examples/bts/13853/why3session.xml
View file @ b0fff343
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13853/why3session.xml">
name="bts/13853/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -9,19 +9,19 @@
<file
name="../13853.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP T"
locfile="13853/../13853.mlw"
locfile="bts/13853/../13853.mlw"
loclnum="10" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter f"
locfile="13853/../13853.mlw"
locfile="bts/13853/../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
sum="ae08fd30941b510f8d344e85ce6d2985"
sum="e1beec1ee049a06190316b698fd46877"
proved="true"
expanded="false"
shape="t">
......@@ -33,15 +33,15 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter g"
locfile="13853/../13853.mlw"
locfile="bts/13853/../13853.mlw"
loclnum="18" loccnumb="7" loccnume="8"
expl="exceptional postcondition"
sum="4a3609e7c6245ef3b76fa886e82409e2"
sum="5e073fd874cb745c16e29e63a5caab88"
proved="true"
expanded="false"
shape="t">
......
examples/check-builtin/bool/why3session.xml
View file @ b0fff343
......@@ -3,160 +3,140 @@
<why3session
name="check-builtin/bool/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="2"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<file
name="../bool.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Test"
locfile="check-builtin/bool/../bool.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="G1"
sum="969c403f9c22509f17918ed3d3b37bd2"
locfile="check-builtin/bool/../bool.why"
loclnum="4" loccnumb="11" loccnume="13"
sum="1f30b23be48217e149fb64c21f9f9378"
proved="true"
expanded="true"
shape="ainfix =aTrueaFalseN">
<proof
prover="cvc3-2.2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
sum="78a2bf185ba7da8e25d94706bbd9c161"
locfile="check-builtin/bool/../bool.why"
loclnum="5" loccnumb="11" loccnume="13"
sum="a7ef2d89ff85180057fa7183acf6c6d2"
proved="true"
expanded="true"
shape="ainfix =V0aFalseOainfix =V0aTrueF">
<proof
prover="cvc3-2.2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G3"
sum="a0bc68bb0d3f237c6ad0611e98d62612"
locfile="check-builtin/bool/../bool.why"
loclnum="6" loccnumb="11" loccnume="13"
sum="dd23e4302e39a1d20bc5a55f4bb3c2ff"
proved="true"
expanded="true"
shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof
prover="cvc3-2.2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/hoare_logic/formula/why3session.xml
View file @ b0fff343
......@@ -3,88 +3,62 @@
<why3session
name="hoare_logic/formula/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
id="2"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
name="Z3"
version="2.19"/>
<file
name="../formula.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Formula"
locfile="hoare_logic/formula/../formula.why"
loclnum="1" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
</theory>
<theory
name="PropositionalCalculus"
locfile="hoare_logic/formula/../formula.why"
loclnum="21" loccnumb="7" loccnume="28"
verified="true"
expanded="true">
<goal
name="Test1"
sum="e329e8a4a6efb1ac7341b8e1c61a6554"
locfile="hoare_logic/formula/../formula.why"
loclnum="47" loccnumb="7" loccnume="12"
sum="165e2a83a67ae016033765c90250ca52"
proved="true"
expanded="true"
shape="Lamk_identc0LasetaconstaFalseV0aTrueainfix =aevalaForaFnotaFatomV0aFfalseV1aFalse">
<proof
prover="cvc3-2.2"
prover="1"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="vampire"
prover="2"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.19"/>
obsolete="false"
archived="false">
<result status="valid" time="0.18"/>
</proof>
</goal>
</theory>
......
examples/programs/assigning_meanings_to_programs/why3session.xml
View file @ b0fff343
......@@ -3,97 +3,67 @@
<why3session
name="programs/assigning_meanings_to_programs/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../assigning_meanings_to_programs.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP Sum"
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="4" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="parameter sum"
sum="ac7ea50a728198affd2e552d9ccb013c"
sum="ab6ece0ccf048de22ee253bbefd81b26"
proved="true"
expanded="true"
shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF">
<label
name="expl:parameter sum">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="WP Division"
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="28" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<goal
name="WP_parameter division"
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="39" loccnumb="6" loccnume="14"
expl="parameter division"
sum="90864aa1fddf212df2ea743e1dd1aaa4"
sum="4ae56abf35642f92abc882dea8823761"
proved="true"
expanded="true"
shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF">
<label
name="expl:parameter division">
</label>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
......
examples/programs/binary_search/why3session.xml
View file @ b0fff343
......@@ -3,125 +3,102 @@
<why3session
name="programs/binary_search/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="1"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../binary_search.mlw"
verified="true"
expanded="true">
expanded="false">
<theory
name="WP BinarySearch"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="5" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
<goal
name="WP_parameter binary_search"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="17" loccnumb="6" loccnume="19"
expl="parameter binary_search"
sum="e8d9926c0894b230b716a68f7c7ef320"
sum="01f4f15024cb46b8dde333e7be87903b"
proved="true"
expanded="true"
shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<label
name="expl:parameter binary_search">
</label>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
<theory
name="WP BinarySearchAnyMidPoint"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="48" loccnumb="7" loccnume="30"
verified="true"
expanded="true">
<goal
name="WP_parameter binary_search"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="59" loccnumb="6" loccnume="19"
expl="parameter binary_search"
sum="696fef5b78c82e8bb343f48b112ea18c"
sum="4d2d8b250c84dcb1cca8870c974bbcd1"
proved="true"
expanded="true"
shape="iainfix <=V4V3iainfix <agetV2V5V1ainfix <ainfix -V3V6ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V7V3Aainfix <=V6V7Iainfix =agetV2V7V1Iainfix <V7V0Aainfix <=c0V7FAainfix <V3V0Aainfix <=c0V6Iainfix =V6ainfix +V5c1Fiainfix >agetV2V5V1ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Iainfix <=V5V3Aainfix <=V4V5FAainfix <=V4V3ainfix =agetV2V10V1NIainfix <V10V0Aainfix <=c0V10FIainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FFFF">
<label
name="expl:parameter binary_search">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="WP BinarySearchInt32"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="88" loccnumb="7" loccnume="24"
verified="true"
expanded="true">
<goal
name="WP_parameter binary_search"
locfile="programs/binary_search/../binary_search.mlw"
loclnum="99" loccnumb="6" loccnume="19"
expl="parameter binary_search"
sum="3c3b1b1cf794ec6c371eb738a4e84015"
sum="c426f5bceb7394f61477135985a213e4"
proved="true"
expanded="true"
shape="iainfix <=V4V3Lainfix -V3V4Lainfix +V4adivV5c2iainfix <agetV2V6V1ainfix <ainfix -V3V7ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V3Aainfix <=V7V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V7Iainfix =V7ainfix +V6c1FAainfix <=ainfix +V6c1amax_intAainfix <=amin_intainfix +V6c1iainfix >agetV2V6V1ainfix <ainfix -V9V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V9Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V9V0Aainfix <=c0V4Iainfix =V9ainfix -V6c1FAainfix <=ainfix -V6c1amax_intAainfix <=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Aainfix <=ainfix +V4adivV5c2amax_intAainfix <=amin_intainfix +V4adivV5c2Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix <V11V0Aainfix <=c0V11FIainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FFF">
<label
name="expl:parameter binary_search">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.15"/>
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
</theory>
......
examples/programs/bresenham/why3session.xml
View file @ b0fff343
This diff is collapsed.
examples/programs/counting_sort/why3session.xml
View file @ b0fff343
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/programs/decrease1/why3session.xml
View file @ b0fff343
This diff is collapsed.
examples/programs/ewd673/why3session.xml
View file @ b0fff343
......@@ -3,78 +3,37 @@
<why3session
name="programs/ewd673/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"