Commit 2411344a authored by MARCHE Claude's avatar MARCHE Claude

Support for Z3 4.4.1, Alt-Ergo 1.20.prv

parent 56702947
......@@ -31,12 +31,16 @@ Encodings
Provers
* discarded support for Alt-Ergo versions older than 0.95.2
o support for Alt-Ergo 1.01 (released Feb 16, 2016) and
non-free versions 1.10 and 1.20
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Coq 8.5 (released Jan 21, 2016)
o support for Gappa 1.2.0 (released May 19, 2015)
* discarded support for Isabelle 2014
o support for Isabelle 2015 (released May 25, 2015) and Isabelle
2016 (released ?, 2016)
o support for Z3 4.4.0 (released Apr 29, 2015)
o support for Isabelle 2015 (released May 25, 2015) and
Isabelle 2016 (released Feb 17, 2016)
o support for Z3 4.4.0 (released Apr 29, 2015) and
4.4.1 (released Oct 5, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
......
......@@ -15,7 +15,7 @@ generated parts or adding empty lines inside them.
will be lost when the file is regenerated by \why. This part ends
at the first empty line.
\item Abstract logic symbols are assumed with the vernacular directive
\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
\verb+Parameter+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
......
......@@ -16,6 +16,7 @@
<prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="4000"/>
<prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="1" memlimit="1000"/>
......@@ -29,9 +30,10 @@
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" memlimit="4000"/>
<file name="../genealogy.why" 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.xml"><result status="valid" time="6.55"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -43,6 +45,7 @@
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01" steps="12"/></proof>
......@@ -55,8 +58,9 @@
<proof prover="25"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Sibling_sym">
<goal name="Sibling_sym" expanded="true">
<proof prover="0" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="6.09"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -69,6 +73,7 @@
<proof prover="10"><result status="valid" time="0.02"/></proof>
<proof prover="11"><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.00" steps="2"/></proof>
<proof prover="15"><result status="valid" time="0.12"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="5"/></proof>
......@@ -80,8 +85,9 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister">
<goal name="Sibling_is_brother_or_sister" expanded="true">
<proof prover="0" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="6.19"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -93,6 +99,7 @@
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="15"><result status="valid" time="0.04"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="9"/></proof>
......@@ -103,8 +110,9 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother">
<goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
<proof prover="0" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="6.50"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -116,6 +124,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="14"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="15"><result status="valid" time="0.07"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="32"/></proof>
......@@ -127,8 +136,9 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Grandfather_male">
<goal name="Grandfather_male" expanded="true">
<proof prover="1"><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>
......@@ -140,6 +150,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="14"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01" steps="6"/></proof>
......@@ -151,8 +162,9 @@
<proof prover="24"><result status="valid" time="0.00"/></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="28"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Grandmother_female">
<goal name="Grandmother_female" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
......@@ -164,6 +176,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="14"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="15"><result status="valid" time="0.03"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01" steps="5"/></proof>
......@@ -175,8 +188,9 @@
<proof prover="24"><result status="valid" time="0.00"/></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="28"><result status="valid" time="0.00"/></proof>
</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="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
......@@ -188,6 +202,7 @@
<proof prover="10"><result status="valid" time="0.03"/></proof>
<proof prover="11"><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.00" steps="8"/></proof>
<proof prover="15"><result status="valid" time="0.05"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01" steps="10"/></proof>
......@@ -199,6 +214,7 @@
<proof prover="24"><result status="valid" time="0.00"/></proof>
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.00.prv"
exec = "alt-ergo-1.01"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.01"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok = "1.20.prv"
version_ok = "1.10.prv"
version_ok = "1.01"
version_ok = "1.00.prv"
......@@ -324,9 +326,11 @@ version_old = "201310"
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.4.1"
version_ok = "4.4.0"
driver = "drivers/z3_440.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
......@@ -337,9 +341,11 @@ command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.ran
name = "Z3"
alternative = "noBV"
exec = "z3"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.4.1"
version_ok = "4.4.0"
driver = "drivers/z3_432.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
......
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