Commit 6baa20c7 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

preliminary support for counter-example generated by Alt-Ergo 0.95

parent d2ce8b08
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="programs/isqrt/why3session.xml">
name="isqrt/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95-dev"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="4"
name="Gappa"
version="0.16.0"/>
<prover
id="4"
id="5"
name="Z3"
version="2.19"/>
<prover
id="5"
id="6"
name="Z3"
version="3.2"/>
<file
name="../isqrt.mlw"
verified="false"
expanded="false">
expanded="true">
<theory
name="WP Simple"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="4" loccnumb="7" loccnume="13"
verified="true"
expanded="false">
<goal
name="WP_parameter isqrt"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="11" loccnumb="6" loccnume="11"
expl="parameter isqrt"
sum="ab231719695ec5b5452b6d8e3d44dac6"
......@@ -48,7 +52,7 @@
<label
name="expl:parameter isqrt"/>
<proof
prover="4"
prover="5"
timelimit="2"
memlimit="0"
obsolete="false"
......@@ -56,7 +60,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="2"
memlimit="0"
obsolete="false"
......@@ -66,7 +70,7 @@
</goal>
<goal
name="WP_parameter main"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="24" loccnumb="6" loccnume="10"
expl="parameter main"
sum="e9e630cabc49ebb5db70b68b7f798666"
......@@ -76,7 +80,7 @@
<label
name="expl:parameter main"/>
<proof
prover="4"
prover="5"
timelimit="2"
memlimit="0"
obsolete="false"
......@@ -87,13 +91,13 @@
</theory>
<theory
name="WP NewtonMethod"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="33" loccnumb="7" loccnume="19"
verified="false"
expanded="true">
<goal
name="WP_parameter sqrt"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="55b0132ccacf4693b33706fd8bf81f12"
......@@ -108,7 +112,7 @@
expanded="true">
<goal
name="WP_parameter sqrt.1"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="normal postcondition"
sum="2bac94036af94ed73785a28b4972c6cb"
......@@ -118,7 +122,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -126,7 +130,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -144,7 +148,7 @@
</goal>
<goal
name="WP_parameter sqrt.2"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="normal postcondition"
sum="ca658fe76283f01b26a13750e677281b"
......@@ -154,7 +158,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -162,7 +166,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -180,7 +184,7 @@
</goal>
<goal
name="WP_parameter sqrt.3"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="loop invariant init"
sum="e7e659592bb2ae13c62bbfee0fe4bb70"
......@@ -195,7 +199,7 @@
expanded="true">
<goal
name="WP_parameter sqrt.3.1"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="d26df8a56b47f425f7bfb0e2963d6939"
......@@ -205,7 +209,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -213,7 +217,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -231,7 +235,7 @@
</goal>
<goal
name="WP_parameter sqrt.3.2"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="def44d60edc1e1af127d3c82dae90bfb"
......@@ -241,7 +245,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -249,7 +253,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -267,7 +271,7 @@
</goal>
<goal
name="WP_parameter sqrt.3.3"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="1d13568646f5fbee5ce1b7f6cfa1d63f"
......@@ -277,7 +281,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -287,7 +291,7 @@
</goal>
<goal
name="WP_parameter sqrt.3.4"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="50fd09183279b23cbd0dab584359ca77"
......@@ -297,7 +301,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -305,7 +309,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -323,7 +327,7 @@
</goal>
<goal
name="WP_parameter sqrt.3.5"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="a4e8886e3a5da1022b8d9e270ecebe40"
......@@ -333,7 +337,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -341,7 +345,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -361,7 +365,7 @@
</goal>
<goal
name="WP_parameter sqrt.4"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="loop invariant preservation"
sum="d8d251db3857f55d55241256ed23f02d"
......@@ -376,7 +380,7 @@
expanded="true">
<goal
name="WP_parameter sqrt.4.1"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="f133ffeefd37638d2e57430aa42245da"
......@@ -386,7 +390,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -394,7 +398,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -412,7 +416,7 @@
</goal>
<goal
name="WP_parameter sqrt.4.2"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="bb375c976411945efedd34eede5d439f"
......@@ -422,7 +426,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -430,7 +434,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -448,7 +452,7 @@
</goal>
<goal
name="WP_parameter sqrt.4.3"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="aec9c69fd73b518b6806ca0d58cb70b9"
......@@ -458,7 +462,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -466,7 +470,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -484,7 +488,7 @@
</goal>
<goal
name="WP_parameter sqrt.4.4"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="d751ded627674f1ec4f4fd3fee89f1c1"
......@@ -494,7 +498,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -512,7 +516,7 @@
</goal>
<goal
name="WP_parameter sqrt.4.5"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="parameter sqrt"
sum="70bffbc1492354c8ea902c720e48d052"
......@@ -522,7 +526,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -530,7 +534,7 @@
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -546,7 +550,7 @@
<result status="unknown" time="1.73"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -554,7 +558,7 @@
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="5"
memlimit="0"
obsolete="false"
......@@ -562,19 +566,27 @@
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="1.49"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter sqrt.5"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="loop variant decreases"
sum="40783ad7a646cbd07bb5115cc1daa453"
......@@ -584,7 +596,7 @@
<label
name="expl:parameter sqrt"/>
<proof
prover="4"
prover="5"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -592,7 +604,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -610,7 +622,7 @@
</goal>
<goal
name="WP_parameter sqrt.6"
locfile="programs/isqrt/../isqrt.mlw"
locfile="isqrt/../isqrt.mlw"
loclnum="39" loccnumb="6" loccnume="10"
expl="normal postcondition"
sum="34e20bd488b899d4be56841a300e6468"
......
theory T1
use import int.Int
goal G : forall x "0":int. ("cond" (x >= 42)) -> x + 3 <= 50
end
theory T2
use import int.Int
constant x : int
goal g : forall y:int. x >= y
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="alt-ergo-models/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.95-dev"/>
<file
name="../alt-ergo-models.why"
verified="false"
expanded="true">
<theory
name="T"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="2" loccnumb="7" loccnume="8"
verified="false"
expanded="true">
<goal
name="G"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="6" loccnumb="7" loccnume="8"
sum="0a4bc6d339e5bafbbd8680953a519128"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="5"
memlimit="0"
edited="altmnergomnmodels-T-G_4.why"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
</file>
</why3session>
[ATP alt-ergo-0.95]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
version_regexp = "\\([0-9.]+-dev\\)"
version_ok = "0.95-dev"
version_bad = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -model %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
......@@ -16,6 +37,7 @@ version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
......@@ -291,3 +313,6 @@ command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
[editor proofgeneral-coq]
command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
[editor altgr-ergo]
command = "altgr-ergo %f"
......@@ -46,6 +46,19 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
let version_0_95 = false (* TODO *)
let print_ident_label fmt id =
if version_0_95 then
fprintf fmt "%s %a"
(id_unique ident_printer id)
(print_list space print_label) (Slab.elements id.id_label)
else
print_ident fmt id
let forget_var v = forget_id ident_printer v.vs_name
let tv_printer =
......@@ -121,7 +134,18 @@ and print_tapp info fmt = function
| [] -> ()
| tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
let rec print_fmla info fmt f = match f.t_node with
let rec print_fmla info fmt f =
if version_0_95 then
match Slab.elements f.t_label with
| [] -> print_fmla_node info fmt f
| l ->
fprintf fmt "(%a : %a)"
(print_list colon print_label) l
(print_fmla_node info) f
else
print_fmla_node info fmt f
and print_fmla_node info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
print_ident fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
......@@ -136,7 +160,7 @@ let rec print_fmla info fmt f = match f.t_node with
| Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
in
let forall fmt v =
fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type info) v.vs_ty
fprintf fmt "%s %a:%a" q print_ident_label v.vs_name (print_type info) v.vs_ty
in
fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
(print_triggers info) tl (print_fmla info) f;
......
......@@ -84,6 +84,7 @@ let star fmt () = fprintf fmt "*@ "
let simple_comma fmt () = fprintf fmt ", "
let underscore fmt () = fprintf fmt "_"
let semi fmt () = fprintf fmt ";@ "
let colon fmt () = fprintf fmt ":@ "
let space fmt () = fprintf fmt "@ "
let alt fmt () = fprintf fmt "|@ "
let alt2 fmt () = fprintf fmt "@ | "
......
......@@ -89,6 +89,7 @@ val comma : formatter -> unit -> unit
val star : formatter -> unit -> unit
val simple_comma : formatter -> unit -> unit
val semi : formatter -> unit -> unit