Commit e3ddf3b3 authored by David Hauzar's avatar David Hauzar Committed by MARCHE Claude
Browse files

Different command for running prover when steps are given

parent 2605aec2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<!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.95.1"/>
<file
name="../alt-ergo-models.mlw"
verified="false"
expanded="true">
<theory
name="M1"
locfile="../alt-ergo-models.mlw"
loclnum="12" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="WP_parameter f"
locfile="../alt-ergo-models.mlw"
loclnum="16" loccnumb="6" loccnume="7"
expl="VC for f"
sum="8cc242702e67821a4b9cf0e7042df2d3"
proved="false"
expanded="true"
shape="ainfix &lt;=ic0ainfix +V0c3ainfix &gt;=V0c42c50F">
<label
name="expl:VC for f"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f_no_lab"
locfile="../alt-ergo-models.mlw"
loclnum="20" loccnumb="6" loccnume="14"
expl="VC for f_no_lab"
sum="8cc242702e67821a4b9cf0e7042df2d3"
proved="false"
expanded="true"
shape="ainfix &lt;=ic0ainfix +V0c3ainfix &gt;=V0c42c50F">
<label
name="expl:VC for f_no_lab"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter g"
locfile="../alt-ergo-models.mlw"
loclnum="26" loccnumb="6" loccnume="7"
expl="VC for g"
sum="618aa543d0727345b8225c89dc0690b9"
proved="false"
expanded="true"
shape="iainfix &lt;=c0c50ainfix &lt;=ainfix +V1c3c50ainfix &gt;=V1c42Iainfix =V1ainfix +V0c1FF">
<label
name="expl:VC for g"/>
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
</file>
<file
name="../alt-ergo-models.why"
verified="false"
expanded="true">
<theory
name="T"
locfile="../alt-ergo-models.why"
loclnum="2" loccnumb="7" loccnume="8"
verified="false"
expanded="true">
<goal
name="g_no_lab"
locfile="../alt-ergo-models.why"
loclnum="6" loccnumb="7" loccnume="15"
sum="627c96c9b461fb071df86eada7d65f95"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="g_lab0"
locfile="../alt-ergo-models.why"
loclnum="8" loccnumb="7" loccnume="13"
sum="627c96c9b461fb071df86eada7d65f95"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="g_lab1"
locfile="../alt-ergo-models.why"
loclnum="11" loccnumb="7" loccnume="13"
sum="627c96c9b461fb071df86eada7d65f95"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="g2_lab"
locfile="../alt-ergo-models.why"
loclnum="16" loccnumb="7" loccnume="13"
sum="232991503d841172f01395ebf7ae7117"
proved="false"
expanded="true"
shape="ainfix &gt;=agV0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ModelInt"
locfile="../alt-ergo-models.why"
loclnum="21" loccnumb="7" loccnume="15"
verified="false"
expanded="true">
<goal
name="test0"
locfile="../alt-ergo-models.why"
loclnum="25" loccnumb="5" loccnume="10"
sum="a0bc7a7a97032889157cbb3c5797ec15"
proved="true"
expanded="true"
shape="Nainfix &lt;V0c1Aainfix &lt;c0V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="test1"
locfile="../alt-ergo-models.why"
loclnum="27" loccnumb="5" loccnume="10"
sum="a80724b74e6d3f07259cf28151c0a91b"
proved="false"
expanded="true"
shape="Nainfix &lt;=V0c1Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test2"
locfile="../alt-ergo-models.why"
loclnum="31" loccnumb="5" loccnume="10"
sum="3b50e45f9cf257ff1a45c145f2bf2aa9"
proved="false"
expanded="true"
shape="ainfix =adivV0V0c1F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow"
locfile="../alt-ergo-models.why"
loclnum="33" loccnumb="5" loccnume="18"
sum="c97b4d6b7974770fe61439bd443172a6"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=c0ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=c0V1Aainfix &lt;=V0c65535Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
</goal>
<goal
name="test_overflow2"
locfile="../alt-ergo-models.why"
loclnum="37" loccnumb="5" loccnume="19"
sum="51c498882d0a7f6d2f5db208f42d22a2"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c2ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c2V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c2V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int16"
locfile="../alt-ergo-models.why"
loclnum="43" loccnumb="5" loccnume="24"
sum="3071369d6a6c845db3ebe9bf95d22604"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iais_int16V1Aais_int16V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int16_alt"
locfile="../alt-ergo-models.why"
loclnum="47" loccnumb="5" loccnume="28"
sum="a7aeee5b74f229ebacddc2f4cf497d76"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c65536ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c65536V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c65536V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int16_bis"
locfile="../alt-ergo-models.why"
loclnum="51" loccnumb="5" loccnume="28"
sum="07d551c70d0c2447a5b7a8eb744c10dc"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int16V1Aais_int16V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int32"
locfile="../alt-ergo-models.why"
loclnum="58" loccnumb="5" loccnume="24"
sum="a3a6500fc3bbee788ba786d16e740f4b"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iais_int32V1Aais_int32V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int32_bis"
locfile="../alt-ergo-models.why"
loclnum="62" loccnumb="5" loccnume="28"
sum="8f1827a14a5174920a0be997984c68ba"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int32V1Aais_int32V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int32_bis_inline"
locfile="../alt-ergo-models.why"
loclnum="66" loccnumb="5" loccnume="35"
sum="970bf31058dc0fdfaec0a26009cca599"
proved="false"
expanded="false"
shape="ainfix &lt;=ainfix +V0V1c2147483647Aainfix &lt;=aprefix -c2147483648ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aainfix &lt;=V1c2147483647Aainfix &lt;=aprefix -c2147483648V1Aainfix &lt;=V0c2147483647Aainfix &lt;=aprefix -c2147483648V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ModelReal"
locfile="../alt-ergo-models.why"
loclnum="72" loccnumb="7" loccnume="16"
verified="false"
expanded="true">
<goal
name="test1"
locfile="../alt-ergo-models.why"
loclnum="76" loccnumb="5" loccnume="10"
sum="96ad11941d867fa01a7875d715fd26ff"
proved="false"
expanded="true"
shape="Nainfix &lt;V0c1.0Aainfix &lt;c0.0V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test2"
locfile="../alt-ergo-models.why"
loclnum="78" loccnumb="5" loccnume="10"
sum="f869600230aa70233d2529e22105a0cc"
proved="false"
expanded="true"
shape="ainfix =ainfix /V0V0c1.0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ModelArray"
locfile="../alt-ergo-models.why"
loclnum="82" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
<goal
name="t1"
locfile="../alt-ergo-models.why"
loclnum="86" loccnumb="5" loccnume="7"
sum="876b42a2b842e2269139141ed72f4d4e"
proved="false"
expanded="true"
shape="ainfix =agetasetV0c0c42V1agetV0V1F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
</file>
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="3" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5-prerelease" alternative="alt" timelimit="5" memlimit="1000"/>
<file name="../alt-ergo-models.mlw" expanded="true">
<theory name="M1" sum="45cd4826531ba4318cd9f922ff2db845" expanded="true">
<goal name="WP_parameter f" expl="VC for f" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter f_no_lab" expl="VC for f_no_lab" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter g" expl="VC for g" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
</file>
<file name="../alt-ergo-models.why" expanded="true">
<theory name="T" sum="71e1048a3f0d6884624a12172edc2c6d" expanded="true">
<goal name="g_no_lab" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="g_lab0" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="g_lab1" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="g2_lab" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="ModelInt" sum="86d7bbce2fd83bdd0688d6bfc3ab82f4" expanded="true">
<goal name="test0" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="251"/></proof>
</goal>
<goal name="test1" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="test2" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
</goal>
<goal name="test_overflow2" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow_int16" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="test_overflow_int16_alt" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow_int16_bis" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow_int32" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow_int32_bis" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="test_overflow_int32_bis_inline">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="ModelReal" sum="d4f5e4342f18bd51a4eeb52ac528edca" expanded="true">
<goal name="test1" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="test2" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="ModelArray" sum="383dfd1f27dfc597caf304c8ef52e35e" expanded="true">
<goal name="t1" expanded="true">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -7,7 +7,8 @@ version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\|~beta.prv\\)?\\)"
version_ok = "0.99.1"
version_ok = "0.95.2"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t -steps-bound %S %f"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t %f"
command_steps = "%l/why3-cpulimit %t %m -s %e -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
......@@ -97,7 +98,8 @@ version_ok = "1.5-prerelease"
driver = "drivers/cvc4.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --rlimit=%S --lang=smt2 %f"
command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%l/why3-cpulimit %T %m -s %e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version 1.4
[ATP cvc4]
......
......@@ -66,6 +66,7 @@ type prover_autodetection_data =
versions_bad : Str.regexp list;
(** If none it's a fake prover (very bad version) *)
prover_command : string option;
prover_command_steps : string option;
prover_driver : string;
prover_editor : string;
prover_in_place : bool;
......@@ -96,6 +97,7 @@ let load_prover kind (id,section) =
versions_old = reg_map (get_stringl section ~default:[] "version_old");
versions_bad = reg_map (get_stringl section ~default:[] "version_bad");
prover_command = get_stringo section "command";
prover_command_steps = get_stringo section "commad_steps";
prover_driver = get_string section ~default:"" "driver";
prover_editor = get_string section ~default:"" "editor";
prover_in_place = get_bool section ~default:false "in_place";
......@@ -377,12 +379,17 @@ let detect_exec env main data acc exec_name =
| Some prover_command ->
(** create the prover config *)
let c = make_command exec_name prover_command in
let c_steps = (match data.prover_command_steps with
| None -> None
| Some prover_command_steps ->
Some (make_command exec_name prover_command_steps)) in
let prover = {Wc.prover_name = data.prover_name;
prover_version = ver;
prover_altern = data.prover_altern} in
let prover_config =
{prover = prover;
command = c;
command_steps = c_steps;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor;
in_place = data.prover_in_place;
......
......@@ -114,6 +114,7 @@ type prover_upgrade_policy =
type config_prover = {
prover : prover;
command : string;
command_steps : string option;
driver : string;
in_place: bool;
editor : string;
......@@ -202,9 +203,17 @@ let loadpath m =
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let get_complete_command pc =
String.concat " " (pc.command :: pc.extra_options)
exception StepsCommandNotSpecified of string
let get_complete_command pc stepslimit =
let comm = if stepslimit < 0 then pc.command
else
match pc.command_steps with
| None -> raise (StepsCommandNotSpecified "The solver is used with step limit and the command for running the solver with steplimit is not specified.")
| Some command_steps -> command_steps in
String.concat " " (comm :: pc.extra_options)
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
......@@ -388,6 +397,7 @@ let load_prover dirname (provers,shortcuts) section =
let provers = Mprover.add prover
{ prover = prover;
command = get_string section "command";
command_steps = get_stringo section "command_steps";
driver = absolute_filename dirname (get_string section "driver");
in_place = get_bool ~default:false section "in_place";
editor = get_string ~default:"" section "editor";
......
......@@ -107,17 +107,18 @@ module Hprover : Exthtbl.S with type key = prover
(** {3 Prover configuration} *)
type config_prover = {
prover : prover; (* unique name for session *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
in_place: bool; (* verification should be performed in-place *)
editor : string; (* Dedicated editor *)
interactive : bool; (* Interactive theorem prover *)
extra_options : string list;
extra_drivers : string list;
prover : prover; (* unique name for session *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
command_steps: string option; (* The command when the number of steps is limited "exec why-limit %t %m -steps-bound %S alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
in_place : bool; (* verification should be performed in-place *)
editor : string; (* Dedicated editor *)
interactive : bool; (* Interactive theorem prover *)
extra_options: string list;