Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 08e25d93 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch '303-support-for-alt-ergo-2-3-0-and-cvc4-1-7' into 'master' 

Resolve "Support for Alt-Ergo 2.3.0 and CVC4 1.7"

Closes #303

See merge request why3/why3!127
parents 31356e2b 21c9b227
No related branches found
No related tags found
1 merge request!127Resolve "Support for Alt-Ergo 2.3.0 and CVC4 1.7"
Hide whitespace changes
Inline Side-by-side
CHANGES.md
+ 4
− 0
View file @ 08e25d93
...@@ -39,6 +39,10 @@ Realizations ...@@ -39,6 +39,10 @@ Realizations
* Added experimental realizations for new Set theories in both Isabelle and * Added experimental realizations for new Set theories in both Isabelle and
Coq Coq
Provers
* support for CVC4 1.7 (released April 9, 2019)
* support for Alt-Ergo 2.3.0 (released February 11, 2019)
Version 1.2.0, February 11, 2019 Version 1.2.0, February 11, 2019
-------------------------------- --------------------------------
......
examples/logic/genealogy/why3session.xml
+ 38
− 22
View file @ 08e25d93
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="0" memlimit="1000"/>
...@@ -37,6 +37,8 @@ ...@@ -37,6 +37,8 @@
<prover id="32" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="32" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="34" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="4000"/> <prover id="34" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="35" name="CVC4" version="1.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="36" name="Alt-Ergo" version="2.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
<path name=".."/> <path name=".."/>
<path name="genealogy.why"/> <path name="genealogy.why"/>
...@@ -53,26 +55,28 @@ ...@@ -53,26 +55,28 @@
<proof prover="9"><result status="valid" time="0.01"/></proof> <proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof> <proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02" steps="1631"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof> <proof prover="15"><result status="valid" time="0.02"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02"/></proof> <proof prover="17"><result status="valid" time="0.02" steps="1654"/></proof>
<proof prover="18" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"><result status="valid" time="0.24"/></proof> <proof prover="18" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"><result status="valid" time="0.24"/></proof>
<proof prover="19" timelimit="60" memlimit="1000"><result status="valid" time="0.00"/></proof> <proof prover="19" timelimit="60" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="20"><result status="valid" time="0.00"/></proof> <proof prover="20"><result status="valid" time="0.00"/></proof>
<proof prover="22"><result status="valid" time="0.00"/></proof> <proof prover="22"><result status="valid" time="0.00"/></proof>
<proof prover="23"><result status="valid" time="0.02"/></proof> <proof prover="23"><result status="valid" time="0.02" steps="1654"/></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> <proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.01"/></proof> <proof prover="29"><result status="valid" time="0.01" steps="1654"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="6.10"/></proof> <proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="6.10"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof> <proof prover="33"><result status="valid" time="0.02" steps="1631"/></proof>
<proof prover="34" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.31"/></proof> <proof prover="34" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="1.20"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="9"/></proof>
</goal> </goal>
<goal name="Sibling_sym" proved="true"> <goal name="Sibling_sym" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
...@@ -87,7 +91,7 @@ ...@@ -87,7 +91,7 @@
<proof prover="10"><result status="valid" time="0.02"/></proof> <proof prover="10"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof> <proof prover="12"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02" steps="1983"/></proof>
<proof prover="15"><result status="valid" time="0.12"/></proof> <proof prover="15"><result status="valid" time="0.12"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
...@@ -102,7 +106,9 @@ ...@@ -102,7 +106,9 @@
<proof prover="30" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="6.00"/></proof> <proof prover="30" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="6.00"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="4"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof> <proof prover="33"><result status="valid" time="0.02" steps="1983"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="4"/></proof>
</goal> </goal>
<goal name="Sibling_is_brother_or_sister" proved="true"> <goal name="Sibling_is_brother_or_sister" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
...@@ -116,7 +122,7 @@ ...@@ -116,7 +122,7 @@
<proof prover="9"><result status="valid" time="0.01"/></proof> <proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof> <proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02" steps="2763"/></proof>
<proof prover="15"><result status="valid" time="0.04"/></proof> <proof prover="15"><result status="valid" time="0.04"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
...@@ -130,7 +136,9 @@ ...@@ -130,7 +136,9 @@
<proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="6.36"/></proof> <proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="6.36"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof> <proof prover="33"><result status="valid" time="0.02" steps="2763"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="9"/></proof>
</goal> </goal>
<goal name="Grandparent_is_grandfather_or_grandmother" proved="true"> <goal name="Grandparent_is_grandfather_or_grandmother" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="28"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="28"/></proof>
...@@ -144,7 +152,7 @@ ...@@ -144,7 +152,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof> <proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.04"/></proof> <proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02" steps="4234"/></proof>
<proof prover="15"><result status="valid" time="0.07"/></proof> <proof prover="15"><result status="valid" time="0.07"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
...@@ -159,7 +167,9 @@ ...@@ -159,7 +167,9 @@
<proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="6.24"/></proof> <proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="6.24"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="20"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="20"/></proof>
<proof prover="33"><result status="valid" time="0.01"/></proof> <proof prover="33"><result status="valid" time="0.01" steps="4234"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="21"/></proof>
</goal> </goal>
<goal name="Grandfather_male" proved="true"> <goal name="Grandfather_male" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
...@@ -174,7 +184,7 @@ ...@@ -174,7 +184,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof> <proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof> <proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02" steps="3608"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof> <proof prover="15"><result status="valid" time="0.03"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
...@@ -188,7 +198,9 @@ ...@@ -188,7 +198,9 @@
<proof prover="28"><result status="valid" time="0.00"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="11"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof> <proof prover="33"><result status="valid" time="0.02" steps="3608"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="11"/></proof>
</goal> </goal>
<goal name="Grandmother_female" proved="true"> <goal name="Grandmother_female" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
...@@ -203,7 +215,7 @@ ...@@ -203,7 +215,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof> <proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof> <proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.03"/></proof> <proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof> <proof prover="14"><result status="valid" time="0.01" steps="3614"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof> <proof prover="15"><result status="valid" time="0.03"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
...@@ -217,7 +229,9 @@ ...@@ -217,7 +229,9 @@
<proof prover="28"><result status="valid" time="0.00"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="11"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="33"><result status="valid" time="0.01"/></proof> <proof prover="33"><result status="valid" time="0.01" steps="3614"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="11"/></proof>
</goal> </goal>
<goal name="Only_two_grandfathers" proved="true"> <goal name="Only_two_grandfathers" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
...@@ -232,24 +246,26 @@ ...@@ -232,24 +246,26 @@
<proof prover="10"><result status="valid" time="0.03"/></proof> <proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof> <proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof> <proof prover="12"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof> <proof prover="14"><result status="valid" time="0.01" steps="3863"/></proof>
<proof prover="15"><result status="valid" time="0.05"/></proof> <proof prover="15"><result status="valid" time="0.05"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof> <proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01"/></proof> <proof prover="17"><result status="valid" time="0.01" steps="3915"/></proof>
<proof prover="19"><result status="valid" time="0.00"/></proof> <proof prover="19"><result status="valid" time="0.00"/></proof>
<proof prover="20"><result status="valid" time="0.00"/></proof> <proof prover="20"><result status="valid" time="0.00"/></proof>
<proof prover="21"><result status="valid" time="0.00"/></proof> <proof prover="21"><result status="valid" time="0.00"/></proof>
<proof prover="22"><result status="valid" time="0.01"/></proof> <proof prover="22"><result status="valid" time="0.01"/></proof>
<proof prover="23"><result status="valid" time="0.02"/></proof> <proof prover="23"><result status="valid" time="0.02" steps="3915"/></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="18"/></proof> <proof prover="25"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof> <proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27"><result status="valid" time="0.01"/></proof> <proof prover="27"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.01"/></proof> <proof prover="29"><result status="valid" time="0.01" steps="3915"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof> <proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32"><result status="valid" time="0.00" steps="18"/></proof> <proof prover="32"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof> <proof prover="33"><result status="valid" time="0.02" steps="3863"/></proof>
<proof prover="35"><result status="valid" time="0.02"/></proof>
<proof prover="36"><result status="valid" time="0.00" steps="18"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
share/provers-detection-data.conf
+ 6
− 0
View file @ 08e25d93
[ATP alt-ergo] [ATP alt-ergo]
name = "Alt-Ergo" name = "Alt-Ergo"
exec = "alt-ergo" exec = "alt-ergo"
exec = "alt-ergo-2.3.0"
exec = "alt-ergo-2.2.0" exec = "alt-ergo-2.2.0"
exec = "alt-ergo-2.1.0" exec = "alt-ergo-2.1.0"
exec = "alt-ergo-2.0.0" exec = "alt-ergo-2.0.0"
version_switch = "-version" version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$" version_regexp = "^\\([0-9.]+\\)$"
version_ok = "2.3.0"
version_ok = "2.2.0" version_ok = "2.2.0"
version_ok = "2.1.0" version_ok = "2.1.0"
version_ok = "2.0.0" version_ok = "2.0.0"
...@@ -25,9 +27,11 @@ name = "CVC4" ...@@ -25,9 +27,11 @@ name = "CVC4"
alternative = "counterexamples" alternative = "counterexamples"
exec = "cvc4" exec = "cvc4"
exec = "cvc4-1.6" exec = "cvc4-1.6"
exec = "cvc4-1.7"
version_switch = "--version" version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.6" version_ok = "1.6"
version_ok = "1.7"
driver = "cvc4_16_counterexample" driver = "cvc4_16_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call # to try: --inst-when=full-last-call
...@@ -39,9 +43,11 @@ command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" ...@@ -39,9 +43,11 @@ command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
name = "CVC4" name = "CVC4"
exec = "cvc4" exec = "cvc4"
exec = "cvc4-1.6" exec = "cvc4-1.6"
exec = "cvc4-1.7"
version_switch = "--version" version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.6" version_ok = "1.6"
version_ok = "1.7"
driver = "cvc4_16" driver = "cvc4_16"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call # to try: --inst-when=full-last-call
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment