Commit 5b3a6b20 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Support for Zenon 0.8.0 and Zenon Modulo 0.4.1

parent 4d229969
...@@ -10,6 +10,8 @@ Encodings ...@@ -10,6 +10,8 @@ Encodings
format is direct format is direct
provers provers
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Isabelle 2015 (released May 25, 2015) o support for Isabelle 2015 (released May 25, 2015)
o support for Coq 8.4pl6 (released April 9, 2015) o support for Coq 8.4pl6 (released April 9, 2015)
o discarded support for Alt-Ergo versions older than 0.95.2 o discarded support for Alt-Ergo versions older than 0.95.2
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="4000"/> <prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" memlimit="1000"/> <prover id="1" name="CVC4" version="1.2" timelimit="60" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/> <prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="4" name="Eprover" version="1.6" timelimit="5" memlimit="0"/> <prover id="4" name="Eprover" version="1.6" timelimit="5" memlimit="0"/>
<prover id="5" name="Z3" version="2.19" timelimit="5" memlimit="0"/> <prover id="5" name="Z3" version="2.19" timelimit="5" memlimit="0"/>
...@@ -27,11 +28,13 @@ ...@@ -27,11 +28,13 @@
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/> <prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" memlimit="1000"/> <prover id="24" name="veriT" version="201410" timelimit="5" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/> <prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" memlimit="1000"/>
<file name="../genealogy.why" expanded="true"> <file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true"> <theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter"> <goal name="Child_is_son_or_daughter" expanded="true">
<proof prover="0" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof> <proof prover="0" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="1"><result status="unknown" time="0.00"/></proof> <proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -55,9 +58,11 @@ ...@@ -55,9 +58,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="Sibling_sym"> <goal name="Sibling_sym" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof> <proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="5.41"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -80,9 +85,11 @@ ...@@ -80,9 +85,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="2"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="2"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="Sibling_is_brother_or_sister"> <goal name="Sibling_is_brother_or_sister" expanded="true">
<proof prover="1"><result status="unknown" time="0.01"/></proof> <proof prover="1"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -105,9 +112,11 @@ ...@@ -105,9 +112,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="Grandparent_is_grandfather_or_grandmother"> <goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.34"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof> <proof prover="5"><result status="valid" time="0.00"/></proof>
...@@ -129,9 +138,11 @@ ...@@ -129,9 +138,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="32"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="38"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="Grandfather_male"> <goal name="Grandfather_male" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof> <proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="5.19"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -153,9 +164,11 @@ ...@@ -153,9 +164,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="Grandmother_female"> <goal name="Grandmother_female" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.17"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof> <proof prover="5"><result status="valid" time="0.00"/></proof>
...@@ -177,9 +190,11 @@ ...@@ -177,9 +190,11 @@
<proof prover="23"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="Only_two_grandfathers"> <goal name="Only_two_grandfathers" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.07"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof> <proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof> <proof prover="5"><result status="valid" time="0.01"/></proof>
...@@ -201,6 +216,7 @@ ...@@ -201,6 +216,7 @@
<proof prover="23"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="24"><result status="valid" time="0.00"/></proof> <proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
...@@ -376,9 +376,11 @@ driver = "drivers/z3_smtv1.drv" ...@@ -376,9 +376,11 @@ driver = "drivers/z3_smtv1.drv"
[ATP zenon] [ATP zenon]
name = "Zenon" name = "Zenon"
exec = "zenon" exec = "zenon"
exec = "zenon-0.8.0"
exec = "zenon-0.7.1" exec = "zenon-0.7.1"
version_switch = "-v" version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)" version_regexp = "zenon version \\([^ \n\t]+\\)"
version_ok = "0.8.0"
version_ok = "0.7.1" version_ok = "0.7.1"
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f" command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon.drv" driver = "drivers/zenon.drv"
...@@ -388,7 +390,7 @@ name = "Zenon Modulo" ...@@ -388,7 +390,7 @@ name = "Zenon Modulo"
exec = "zenon_modulo" exec = "zenon_modulo"
version_switch = "-v" version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)" version_regexp = "zenon_modulo version \\([0-9.]+\\)"
version_ok = "0.4.0" version_ok = "0.4.1"
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f" command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon_modulo.drv" driver = "drivers/zenon_modulo.drv"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment