Commit a9b1712c authored by MARCHE Claude's avatar MARCHE Claude

Cleaned implementation of counter-example generation

parent d4484d2e
import "alt_ergo_bare.drv"
theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "printer_option" "show_labels"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
import "alt_ergo.drv"
theory BuiltIn
meta "printer_option" "show_labels"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
......@@ -3,7 +3,7 @@ theory T1
use import int.Int
goal G : forall x "0":int. ("cond" (x >= 42)) -> x + 3 <= 50
goal G : forall x "0":int. ("cond" x >= 42) -> x + 3 <= 50
end
......
......@@ -35,31 +35,6 @@
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<transf
name="split_goal"
proved="false"
expanded="true">
<goal
name="WP_parameter f.0"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="6" loccnumb="6" loccnume="7"
expl="normal postcondition"
sum="a0d81048eafffca9c2034507529acd5c"
proved="false"
expanded="true"
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
<label
name="expl:parameter f"/>
<proof
prover="0"
timelimit="5"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
[ATP alt-ergo-0.95]
[ATP alt-ergo-model]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95-dev"
......@@ -16,7 +16,7 @@ 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_0.95.drv"
driver = "drivers/alt_ergo_model.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
......
......@@ -30,7 +30,8 @@ open Task
open Printer
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
let meta_printer_option = Theory.register_meta "printer_option" [Theory.MTstring]
let meta_printer_option =
Theory.register_meta "printer_option" [Theory.MTstring]
type info = {
info_syn : syntax_map;
......@@ -134,7 +135,7 @@ and print_tapp info fmt = function
| [] -> ()
| tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
let rec print_fmla info fmt f =
let rec print_fmla info fmt f =
if info.info_show_labels then
match Slab.elements f.t_label with
| [] -> print_fmla_node info fmt f
......@@ -312,12 +313,8 @@ let check_showlabels acc l =
match l with
| [Theory.MAstr s] ->
begin match s with
| "show_labels" ->
eprintf "printer_option show_labels set@.";
true
| _ ->
eprintf "printer_option %s ignored@." s;
acc
| "show_labels" -> true
| _ -> acc
end
| _ -> assert false
......
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