Commit 51d2defa authored by MARCHE Claude's avatar MARCHE Claude

Support for Alt-Ergo 1.00.prv

parent 74eaa93b
......@@ -21,9 +21,11 @@ provers
o support for Z3 4.3.2 (released Oct 25, 2014)
o support for MetiTarski 2.4 (released Oct 21, 2014)
o support for Alt-Ergo 0.99.1 (released Dec 30, 2014)
o support for Alt-Ergo 1.00.prv (released Jan 29, 2015)
o support for veriT 201410 (released Nov 2014)
o support for Psyche (experimental,
http://www.lix.polytechnique.fr/~lengrand/Psyche/)
o preliminary support for upcoming CVC4 1.5 (steps feature)
bug fixes:
o bug in interpreter in presence of nested mutable fields
......
......@@ -12,6 +12,8 @@ import "discrimination.gen"
(* specific message from veriT 201310 *)
unknown "non-linear reasoning desactivated" ""
(* specific message from veriT 201410 *)
unknown "error : Non linear expression with non-linear reasoning disabled" ""
transformation "inline_trivial"
......
......@@ -17,6 +17,7 @@
<prover id="12" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
<theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -38,6 +39,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof>
<proof prover="15"><result status="valid" time="2.86" steps="642"/></proof>
</goal>
<goal name="Wrong" expanded="true">
<proof prover="0"><result status="unknown" time="15.98"/></proof>
......@@ -55,6 +57,7 @@
<proof prover="12"><result status="timeout" time="4.97"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14" timelimit="5"><result status="timeout" time="10.08"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="0"><result status="valid" time="12.12" steps="1747"/></proof>
......@@ -72,6 +75,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="13" timelimit="3"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof>
<proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
</goal>
</theory>
</file>
......
......@@ -27,6 +27,7 @@
<prover id="22" name="Vampire" version="0.6" timelimit="3" 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="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter" expanded="true">
......@@ -55,6 +56,7 @@
<proof prover="22"><result status="valid" time="0.00"/></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="25"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="Sibling_sym" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -80,6 +82,7 @@
<proof prover="22"><result status="valid" time="0.00"/></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="25"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister" expanded="true">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
......@@ -105,6 +108,7 @@
<proof prover="22"><result status="valid" time="0.00"/></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="25"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -129,6 +133,7 @@
<proof prover="22"><result status="valid" time="0.01"/></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="25"><result status="valid" time="0.00" steps="38"/></proof>
</goal>
<goal name="Grandfather_male" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -153,6 +158,7 @@
<proof prover="22"><result status="valid" time="0.03"/></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="25"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Grandmother_female" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -177,6 +183,7 @@
<proof prover="22"><result status="valid" time="0.01"/></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="25"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Only_two_grandfathers" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -201,6 +208,7 @@
<proof prover="22"><result status="valid" time="0.01"/></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="25"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.00.prv"
exec = "alt-ergo-0.99.1"
exec = "alt-ergo-0.95.2"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\|~beta.prv\\)?\\)"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok = "1.00.prv"
version_ok = "0.99.1"
version_ok = "0.95.2"
# %T means timelimit+1
......
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