Skip to content

why3
why3
Commit 0a02cfc9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

add %T modifier in commands of config file 

Hopefully this solves the problem of unreliable answers from some
provers like Vampire: there is no such answer "unknown" just 0.01
seconds before the time limit anymore
parent a335cdf4
Hide whitespace changes
Inline Side-by-side
Showing with 303 additions and 359 deletions
drivers/vampire.drv
View file @ 0a02cfc9
......@@ -6,7 +6,7 @@ filename "%f-%t-%g.p"
valid "Refutation found"
timeout "Aborted by signal SIGXCPU on"
timeout "Time limit reached"
unknown "Refutation not found" "Unknown"
unknown "Refutation not found" "Unknown"
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
......
examples/einstein/why3session.xml
View file @ 0a02cfc9
......@@ -71,156 +71,170 @@
expanded="true">
<goal
name="G1"
sum="4e666b5243bdb1064743ec6e271cb8ec"
sum="b29963ab2946f6e953e24adc18bc2422"
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
<proof
prover="cvc3"
timelimit="5"
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="2.44"/>
<result status="timeout" time="2.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
<result status="valid" time="2.70"/>
</proof>
<proof
prover="z3"
timelimit="2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="yices"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.11"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="3.98"/>
</proof>
<proof
prover="spass"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.00"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
name="Wrong"
sum="1a0ed387ff3cda5c8323f4eb21fd248c"
sum="b6ada39e4ed1ac554d7bdbccbfadcff3"
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
<proof
prover="simplify"
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="timeout" time="2.31"/>
<result status="timeout" time="2.02"/>
</proof>
<proof
prover="cvc3"
timelimit="2"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.98"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="z3"
timelimit="2"
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
<result status="timeout" time="2.98"/>
</proof>
<proof
prover="yices"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.08"/>
<result status="timeout" time="3.98"/>
</proof>
<proof
prover="spass"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.04"/>
<result status="timeout" time="3.06"/>
</proof>
</goal>
<goal
name="G2"
sum="44df905be1d95d899616a903f2a08529"
sum="ad118f1b69459bb42f50fa8c2063d069"
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
<proof
prover="cvc3"
timelimit="5"
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="1.88"/>
<result status="timeout" time="2.02"/>
</proof>
<proof
prover="eprover"
timelimit="5"
prover="cvc3"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.99"/>
<result status="valid" time="2.04"/>
</proof>
<proof
prover="z3"
timelimit="2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="eprover"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="yices"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.08"/>
<result status="timeout" time="3.98"/>
</proof>
<proof
prover="spass"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="4.99"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
</theory>
......
examples/hoare_logic/imp_n/why3session.xml
View file @ 0a02cfc9
......@@ -9,7 +9,7 @@
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
......@@ -48,11 +48,11 @@
version="2.19"/>
<file
name="../imp_n.why"
verified="false"
verified="true"
expanded="true">
<theory
name="Imp"
verified="false"
verified="true"
expanded="true">
<goal
name="ident_eq_dec"
......@@ -163,56 +163,35 @@
timelimit="3"
edited="imp_n_Imp_progress_1.v"
obsolete="false">
<result status="valid" time="0.54"/>
</proof>
<proof
prover="eprover"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.01"/>
</proof>
<proof
prover="vampire"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="6.55"/>
</proof>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="9.51"/>
<result status="valid" time="0.63"/>
</proof>
</goal>
<goal
name="steps_non_neg"
sum="7fe79f6298fbe9fbaa31741ffa430e03"
proved="false"
proved="true"
expanded="true"
shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_steps_non_neg_1.v"
obsolete="true">
<result status="valid" time="0.46"/>
obsolete="false">
<result status="valid" time="0.60"/>
</proof>
</goal>
<goal
name="many_steps_seq"
sum="c4867410343f6c684f9ca00c1536720a"
proved="false"
proved="true"
expanded="true"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_many_steps_seq_1.v"
obsolete="true">
<result status="valid" time="0.54"/>
obsolete="false">
<result status="valid" time="0.72"/>
</proof>
</goal>
<goal
......@@ -226,7 +205,7 @@
timelimit="3"
edited="imp_n_Imp_eval_subst_expr_1.v"
obsolete="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.63"/>
</proof>
</goal>
<goal
......@@ -240,7 +219,7 @@
timelimit="3"
edited="imp_n_Imp_eval_subst_1.v"
obsolete="false">
<result status="valid" time="0.48"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
......@@ -260,57 +239,57 @@
<goal
name="assign_rule"
sum="2ce35dd2e431c206c4ef4d4353dd9c47"
proved="false"
proved="true"
expanded="true"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_assign_rule_1.v"
obsolete="true">
<result status="valid" time="0.72"/>
obsolete="false">
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="seq_rule"
sum="3da8614c2f6127af09be97a426dc327e"
proved="false"
proved="true"
expanded="true"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_seq_rule_1.v"
obsolete="true">
<result status="valid" time="0.52"/>
obsolete="false">
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
name="if_rule"
sum="5e738541b92efb7be1706db09a761442"
proved="false"
proved="true"
expanded="true"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_if_rule_1.v"
obsolete="true">
<result status="valid" time="0.68"/>
obsolete="false">
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="while_rule"
sum="17f0b6240f5cfd179c6cea9bfc294a9d"
proved="false"
proved="true"
expanded="true"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="coq"
timelimit="3"
edited="imp_n_Imp_while_rule_1.v"
obsolete="true">
<result status="valid" time="0.57"/>
obsolete="false">
<result status="valid" time="0.60"/>
</proof>
</goal>
<goal
......
examples/programs/vacid_0_binary_heaps/proofs/why3session.xml
View file @ 0a02cfc9
This source diff could not be displayed because it is too large. You can view the blob instead.
share/provers-detection-data.conf.in
View file @ 0a02cfc9
......@@ -38,7 +38,7 @@ version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t %f"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -timeout %T %f"
driver = "drivers/cvc3.drv"
[ATP yices]
......@@ -62,7 +62,9 @@ exec = "eprover"
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
version_ok = "1.4 Namring"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
# we pass %T ie time+1 to e-prover,
# to avoid replacing answer "timeout" by "unknown"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -s -R -xAuto -tAuto --cpu-limit=%T --tstp-in %f"
driver = "drivers/tptp.drv"
[ATP gappa]
......@@ -102,7 +104,9 @@ exec = "SPASS"
version_switch = "-TPTP || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
version_ok = "3.7"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
# we pass %T ie time+1 to spass,
# to avoid replacing answer "timeout" by "unknown"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%T %f"
driver = "drivers/tptp.drv"
[ATP vampire]
......@@ -110,7 +114,9 @@ name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -t %t"
# we pass %T ie time+1 to vampire,
# to avoid replacing answer "timeout" by "unknown"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -t %T"
driver = "drivers/vampire.drv"
version_ok = "0.6"
......
src/driver/call_provers.ml
View file @ 0a02cfc9
......@@ -128,6 +128,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
| "%" -> "%"
| "f" -> file
| "t" -> on_timelimit := true; string_of_int timelimit
| "T" -> on_timelimit := true; string_of_int (timelimit+1)
| "m" -> string_of_int memlimit
| "b" -> string_of_int (memlimit * 1024)
| _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
......
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