Commit 5442cbc9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Support for Metitarski 2.4

parent 4293c6e5
......@@ -8,7 +8,7 @@ library
provers
o support for Z3 4.3.2 (released Oct 25, 2014)
o support for MetiTarski 2.4 (released Oct 21, 2014)
version 0.85, September 17, 2014
================================
......
......@@ -7,46 +7,57 @@
<prover id="2" name="CVC3" version="2.4.1" timelimit="3" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="MetiTarski" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<prover id="6" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../lagrange_inequality.why" expanded="true">
<theory name="LagrangeInequality" sum="5e115a67d12d3b9e0cb091836baf8f27" expanded="true">
<goal name="norm2_pos" expanded="true">
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lagrange" expanded="true">
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="CauchySchwarzInequality" sum="6fcd96c715b7475a71d99c0f82d79af4" expanded="true">
<goal name="CauchySchwarz_aux" expanded="true">
<proof prover="1"><result status="valid" time="0.80"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="norm_pos" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="sqr_le_sqrt" expanded="true">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="1.49"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="CauchySchwarz" expanded="true">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.50"/></proof>
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" sum="c1ce71fbadfa600580a354699d029b51" expanded="true">
<goal name="triangle_aux" expanded="true">
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sqr_sqrt_le" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="triangle" expanded="true">
<proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="1.23"/></proof>
......
......@@ -5,15 +5,17 @@
<prover id="0" name="Coq" version="8.4pl4" timelimit="8" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="3" memlimit="0"/>
<prover id="2" name="MetiTarski" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="3" name="Gappa" version="1.1.1" timelimit="2" memlimit="0"/>
<prover id="3" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Gappa" version="1.1.1" timelimit="2" memlimit="0"/>
<file name="../my_cosine.why" expanded="true">
<theory name="CosineSingle" sum="755ee8878730ca0c5dd106b03f1b8590" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="3.65"/></proof>
<proof prover="2"><result status="valid" time="0.24"/></proof>
<proof prover="3"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="TotalErrorFullyExpanded" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="TotalErrorExpanded" expanded="true">
<proof prover="1"><result status="valid" time="2.34"/></proof>
......
......@@ -4,11 +4,13 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="MetiTarski" version="2.2" timelimit="5" memlimit="4000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<file name="../real.why" expanded="true">
<theory name="CosineSingle" sum="46cd6f72186946bb0faaa2aacb6342be" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="3.42"/></proof>
<proof prover="1"><result status="valid" time="0.15"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</theory>
</file>
......
......@@ -227,9 +227,12 @@ driver = "drivers/metis.drv"
[ATP metitarski]
name = "MetiTarski"
exec = "metit"
exec = "metit-2.4"
exec = "metit-2.2"
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
version_ok = "2.2"
version_ok = "2.4"
version_old = "2.2"
command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
driver = "drivers/metitarski.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