Commit f4f2c2dc authored by David Hauzar's avatar David Hauzar

Merge branch 'counter-examples' of...

Merge branch 'counter-examples' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into counter-examples
parents d0f00735 54e975a3
......@@ -16,7 +16,7 @@ open Ident
open Printer
(*
***************************************************************
***************************************************************
** Counter-example model values
****************************************************************
*)
......@@ -41,8 +41,8 @@ let array_create_constant ~value =
}
let array_add_element ~array ~index ~value =
(*
Adds the element value to the array on specified index.
(*
Adds the element value to the array on specified index.
*)
let int_index = match index with
| Integer s -> int_of_string s
......@@ -64,7 +64,7 @@ let rec print_indices sanit_print fmt indices =
print_model_value_sanit sanit_print fmt index.arr_index_value;
print_indices sanit_print fmt tail
and
print_array sanit_print fmt arr =
print_array sanit_print fmt arr =
fprintf fmt "{others -> ";
print_model_value_sanit sanit_print fmt arr.arr_others;
print_indices sanit_print fmt arr.arr_indices;
......@@ -82,11 +82,11 @@ let print_model_value fmt value =
(*
***************************************************************
***************************************************************
** Model elements
***************************************************************
*)
type model_element = {
type model_element = {
me_name : string;
me_value : model_value;
me_location : Loc.position option;
......@@ -109,10 +109,10 @@ let print_location fmt m_element =
*)
(*
***************************************************************
***************************************************************
** Model definitions
***************************************************************
*)
*)
module IntMap = Map.Make(struct type t = int let compare = compare end)
module StringMap = Map.Make(String)
......@@ -127,29 +127,24 @@ type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser = string -> model_element list
(*
***************************************************************
***************************************************************
** Quering the model
***************************************************************
*)
let print_model_element fmt m_element =
fprintf fmt "%s = %a"
fprintf fmt "%s = %a"
m_element.me_name print_model_value m_element.me_value
let print_model_elements ?(delimiter = "\n") fmt m_elements =
List.iter
(fun m_element ->
print_model_element fmt m_element;
fprintf fmt "%s" delimiter
)
m_elements
let print_model_elements ?(sep = "\n") fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) print_model_element fmt m_elements
let print_model_file fmt filename model_file =
fprintf fmt "File %s:\n" filename;
IntMap.iter
IntMap.iter
(fun line m_elements ->
fprintf fmt "Line %d:\n" line;
print_model_elements fmt m_elements)
print_model_elements fmt m_elements)
model_file
let print_model fmt model =
......@@ -172,7 +167,7 @@ let get_elements model_file line_number =
[]
let get_padding line =
try
try
let r = Str.regexp " *" in
ignore (Str.search_forward r line 0);
Str.matched_string line
......@@ -181,24 +176,23 @@ let get_padding line =
let interleave_line start_comment end_comment model_file (source_code, line_number) line =
try
let model_elements = IntMap.find line_number model_file in
print_model_elements str_formatter model_elements ~delimiter:"; ";
let cntexmp_line =
print_model_elements str_formatter model_elements ~sep:"; ";
let cntexmp_line =
(get_padding line) ^
start_comment ^
(flush_str_formatter ()) ^
start_comment ^
(flush_str_formatter ()) ^
end_comment in
(source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1)
with Not_found ->
(source_code ^ line, line_number + 1)
let interleave_with_source
?(start_comment="(* ")
?(end_comment=" *)")
model
filename
let interleave_with_source
?(start_comment="(* ")
?(end_comment=" *)")
model
filename
source_code =
try
let model_file = StringMap.find filename model in
......@@ -219,41 +213,41 @@ let print_model_value_json fmt me_value =
fprintf fmt "%a" (print_model_value_sanit Json.string) me_value
let model_elements_to_map_bindings model_elements =
List.fold_left
List.fold_left
(fun map_bindings me ->
(me.me_name, me.me_value)::map_bindings
)
[]
[]
model_elements
let print_model_elements_json fmt model_elements =
Json.map_bindings
Json.map_bindings
(fun i -> i)
print_model_value_json
fmt
(model_elements_to_map_bindings model_elements)
let print_model_elements_on_lines_json fmt model_file =
Json.map_bindings
(fun i -> string_of_int i)
print_model_elements_json
fmt
(IntMap.bindings model_file)
let print_model_json fmt model =
Json.map_bindings
(fun s -> s)
Json.map_bindings
(fun s -> s)
print_model_elements_on_lines_json
fmt
fmt
(StringMap.bindings model)
let model_to_string_json model =
print_model_json str_formatter model;
flush_str_formatter ()
(*
***************************************************************
***************************************************************
** Building the model from raw model
***************************************************************
*)
......@@ -275,14 +269,14 @@ let rec extract_element_name labels raw_string regexp =
| [] -> raw_string
| label::labels_tail ->
let l_string = label.lab_string in
begin
try
begin
try
ignore(Str.search_forward regexp l_string 0);
let end_pos = Str.match_end () in
String.sub l_string end_pos ((String.length l_string) - end_pos)
with Not_found -> extract_element_name labels_tail raw_string regexp
end
let get_element_name term raw_string =
let labels = Slab.elements term.t_label in
let regexp = Str.regexp "model_trace:" in
......@@ -293,32 +287,32 @@ let rec build_model_rec raw_model terms model =
match raw_model with
| [] -> model
| model_element::raw_strings_tail ->
let (element_name, element_location, element_term, terms_tail) =
let (element_name, element_location, element_term, terms_tail) =
match terms with
| [] -> (model_element.me_name, None, None, [])
| term::t_tail ->
((get_element_name term model_element.me_name),
term.t_loc,
| term::t_tail ->
((get_element_name term model_element.me_name),
term.t_loc,
Some term, t_tail) in
let new_model_element = create_model_element
~name:element_name
~value:model_element.me_value
?location:element_location
?term:element_term
~name:element_name
~value:model_element.me_value
?location:element_location
?term:element_term
() in
let model = add_to_model model new_model_element in
build_model_rec
raw_strings_tail
terms_tail
build_model_rec
raw_strings_tail
terms_tail
model
let build_model raw_model printer_mapping =
build_model_rec raw_model printer_mapping.queried_terms empty_model
(*
***************************************************************
***************************************************************
** Registering model parser
***************************************************************
*)
......
......@@ -80,17 +80,29 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let check_related_loc = ref None
let check_funct_name = ref None
module TermCmp = struct
type t = term
let compare a b =
if (a.t_loc = b.t_loc) && (a.t_label = b.t_label)
then 0 else 1
end
module S = Set.Make(TermCmp)
type info = {
info_syn : syntax_map;
info_converters : converter_map;
mutable info_model : term list;
mutable info_model : S.t;
}
let debug_print_term message t =
let form = Debug.get_debug_formatter () in
begin
Debug.dprintf debug message;
if Debug.test_flag debug then
if Debug.test_flag debug then
Pretty.print_term form t;
Debug.dprintf debug "@.";
end
......@@ -128,21 +140,71 @@ let print_var_list info fmt vsl =
print_list space (print_typed_var info) fmt vsl
let model_label = Ident.create_label "model"
let model_vc_label = Ident.create_label "model_vc"
let collect_model_ls info ls =
if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
let t = t_app ls [] ls.ls_value in
info.info_model <-
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) :: info.info_model
S.add
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model
let model_trace_regexp = Str.regexp "model_trace:"
let label_starts_with regexp l =
try
ignore(Str.search_forward regexp l.lab_string 0);
true
with Not_found -> false
let get_label labels regexp =
Slab.choose (Slab.filter (label_starts_with regexp) labels)
let labels_at_vc_pos ~labels =
try
let trace_label = get_label labels model_trace_regexp in
try
ignore(Str.search_forward (Str.regexp "@") trace_label.lab_string 0);
labels
with Not_found ->
let other_labels = Slab.remove trace_label labels in
let new_label = Ident.create_label (trace_label.lab_string^"@"^"old") in
Slab.add new_label other_labels
with Not_found ->
Slab.add
(Ident.create_label
("model_trace:" ^ (Opt.get_def "" !check_funct_name) ^ "@result"))
labels
let add_check_related t =
if Slab.mem model_vc_label t.t_label then begin
check_related_loc := t.t_loc;
try
let fun_label = get_label t.t_label (Str.regexp "model_func:") in
let str_lab = fun_label.lab_string in
let func_name_start = 11 in
let func_name_len = (String.length str_lab) - 11 in
check_funct_name := Some (String.sub str_lab func_name_start func_name_len);
with Not_found -> ()
end
let remove_check_related t =
if Slab.mem model_vc_label t.t_label then begin
check_related_loc := None;
check_funct_name := None;
end
(** expr *)
let rec print_term info fmt t =
debug_print_term "Printing term: " t;
let rec print_term info fmt t =
debug_print_term "Printing term: " t;
if Slab.mem model_label t.t_label then
info.info_model <- (t) :: info.info_model;
info.info_model <- S.add t info.info_model;
add_check_related t;
match t.t_node with
let () = match t.t_node with
| Tconst c ->
let number_format = {
Number.long_int_support = true;
......@@ -176,9 +238,19 @@ let rec print_term info fmt t =
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ -> fprintf fmt "@[(%a@ %a)@]"
print_ident ls.ls_name (print_list space (print_term info)) tl
| [] ->
let () = match !check_related_loc with
| None -> ()
| Some loc ->
let labels = labels_at_vc_pos ~labels:ls.ls_name.id_label in
let t_check_pos = t_label ~loc labels t in
info.info_model <- S.add t_check_pos info.info_model;
() in
();
fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ ->
fprintf fmt "@[(%a@ %a)@]"
print_ident ls.ls_name (print_list space (print_term info)) tl
end end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
......@@ -199,13 +271,20 @@ let rec print_term info fmt t =
| Teps _ -> unsupportedTerm t
"smtv2: you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
in
and print_fmla info fmt f =
debug_print_term "Printing formula: " f;
remove_check_related t;
and print_fmla info fmt f =
debug_print_term "Printing formula: " f;
if Slab.mem model_label f.t_label then
info.info_model <- (f) :: info.info_model;
match f.t_node with
info.info_model <- S.add f info.info_model;
add_check_related f;
let () = 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
......@@ -264,7 +343,9 @@ and print_fmla info fmt f =
print_var subject (print_term info) t
(print_branches info subject print_fmla) bl;
forget_var subject
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
remove_check_related f
and print_branches info subject pr fmt bl = match bl with
| [] -> assert false
......@@ -330,20 +411,20 @@ let print_logic_decl info fmt (ls,def) =
List.iter forget_var vsl
end
let print_info_model cntexample fmt info =
let print_info_model cntexample fmt model_list info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if info_model != [] && cntexample then
if model_list != [] && cntexample then
begin
(*
fprintf fmt "@[(get-value (%a))@]@\n"
(Pp.print_list Pp.space (print_fmla info_copy)) model_list;*)
fprintf fmt "@[(get-value (";
List.iter (fun f ->
List.iter (fun f ->
fprintf str_formatter "%a" (print_fmla info) f;
let s = flush_str_formatter () in
fprintf fmt "%s " s;
) info_model;
) model_list;
fprintf fmt "))@]@\n";
(* Printing model has modification of info.info_model as undesirable
......@@ -364,12 +445,13 @@ let print_prop_decl cntexample args info fmt k pr f = match k with
| Some loc -> fprintf fmt " @[;; %a@]@\n"
Loc.gen_report_position loc);
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
let model_list = S.elements info.info_model in
fprintf fmt "@[(check-sat)@]@\n";
print_info_model cntexample fmt info;
print_info_model cntexample fmt model_list info;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
queried_terms = info.info_model; }
queried_terms = model_list; }
| Plemma| Pskip -> assert false
......@@ -423,12 +505,12 @@ let print_decls cntexample args =
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm, []),[])))
Trans.fold print_decl ((sm, cm, S.empty),[])))
let set_produce_models fmt cntexample =
let set_produce_models fmt cntexample =
if cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
......
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