Commit db10ea94 authored by MARCHE Claude's avatar MARCHE Claude

prover alternative for CVC4 and Z3: noBV

parent 484e6603
......@@ -2,100 +2,109 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="25" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="25" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="25" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="25" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="0fc617e41642d752fa5c59917fa533b2" expanded="true">
<goal name="WP_parameter min_elt" expl="VC for min_elt">
<transf name="split_goal_wp">
<theory name="Rmbt" sum="8b7e47a05b0ba582f9171c5d62077316" expanded="true">
<goal name="WP_parameter min_elt" expl="VC for min_elt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter min_elt.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.21"/></proof>
<proof prover="0"><result status="valid" time="2.18" steps="182"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter min_elt.2" expl="2. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.64"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="1.44" steps="355"/></proof>
<proof prover="1"><result status="valid" time="0.55"/></proof>
<proof prover="0"><result status="valid" time="1.14" steps="296"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter min_elt.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><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>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><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>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.7" expl="7. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter min_elt.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter min_elt.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick">
<transf name="split_goal_wp">
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter rightmost_bit_trick.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="69"/></proof>
<proof prover="2"><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>
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.2" expl="2. assertion">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.20" steps="140"/></proof>
<proof prover="1"><result status="valid" time="0.11"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="142"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="0"><result status="valid" time="0.16" steps="146"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="80"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.89"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.15" steps="177"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="200"/></proof>
<proof prover="4"><result status="timeout" time="5.05"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......
......@@ -30,7 +30,7 @@ editor = "altgr-ergo"
# CVC4 version 1.5-prerelease
[ATP cvc4]
name = "CVC4 (BV)"
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
exec = "cvc4-1.5"
......@@ -46,7 +46,7 @@ command_steps = "%l/why3-cpulimit %U %m -s %e --stats --rlimit=%S --lang=smt2 %f
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
name = "CVC4 (BV)"
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
......@@ -61,9 +61,10 @@ command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
# CVC4 version 1.4
# CVC4 version 1.4, not using SMTLIB bitvectors
[ATP cvc4]
name = "CVC4"
alternative = "noBV"
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
......@@ -317,9 +318,9 @@ command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
driver = "drivers/verit.drv"
version_old = "201310"
# Z3 with BV support
# Z3 >= 4.4.0, with BV support
[ATP z3]
name = "Z3 (BV)"
name = "Z3"
exec = "z3"
exec = "z3-4.4.0"
version_switch = "-version"
......@@ -329,12 +330,24 @@ 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"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 >= 4.4.0, without BV support
[ATP z3]
name = "Z3"
alternative = "noBV"
exec = "z3"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
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"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
# Z3 4.3.2 supports Datatypes
[ATP z3]
name = "Z3"
exec = "z3-4.4.0"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
......
......@@ -28,7 +28,7 @@ A block with more than one exec fields is now the same thing than if you
split the block into blocks containing one fields.
New message field that allows to print a message when a prover is
detected. If a message is not present, we print ", Ok." if the version
detected. If a message is not present, we print ", OK." if the version
is good (version_good) and not old, and " (it is an old version)." if
the version is old (version_old).
......@@ -401,8 +401,14 @@ let detect_exec env main data acc exec_name =
if good || old then begin
eprintf "Found prover %s version %s%s@."
data.prover_name ver
(Opt.get_def (if old then
" (old version, please consider upgrading)." else ", Ok.")
(Opt.get_def
(if old then
" (old version, please consider upgrading)."
else
if data.prover_altern <> "" then
" (alternative: " ^ data.prover_altern ^ ")"
else
", OK.")
data.message);
known_version env exec_name;
add_prover_shortcuts env prover;
......
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