Commit 86ebcd21 authored by Sylvain Dailler's avatar Sylvain Dailler

Why3 counterex: Changing the way counterex value are get from prover.

This commit solve a problem raised by Mohamed Iguernlala. If provers give
more values than asked, the results of counterex becomes inconsistent.

We changed the way corresponding terms are associated to counterex value.
Now we have a map containing the term corresponding to a counterex asked to
a prover.

* src/core/model_parser.ml
(construct_name): Takes a string and create a model_name.
(build_model_rec): Changed to use term_map which allow a name of asked
counterex to correspond to the term asked.

* src/core/printer.ml
(printer_mapping): Changed type of queried_terms to store correspondance
between names and terms.
(printer_args): Changed initial value of queried_terms accordingly.

* src/core/smtv2.ml
(print_info_model): This function now returns the map of names to terms.
(print_prop_decl): Changed variable model_list accordingly.
parent 3c9accc9
......@@ -142,6 +142,14 @@ let create_model_element ~name ~value ?location ?term () =
me_term = term;
}
let construct_name (name: string): model_element_name =
let (name, type_s) = split_model_trace_name name in
let me_kind = match type_s with
| "result" -> Result
| "old" -> Old
| _ -> Other in
{men_name = name; men_kind = me_kind}
(*
let print_location fmt m_element =
match m_element.me_location with
......@@ -403,32 +411,24 @@ let add_to_model model model_element =
let model_file = IntMap.add line_number elements model_file in
StringMap.add filename model_file model
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) =
match terms with
| [] -> (model_element.me_name.men_name, None, None, [])
| term::t_tail ->
let get_element_name term raw_string =
let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) =
List.fold_left (fun model raw_element ->
let raw_element_name = raw_element.me_name.men_name in
try
get_model_trace_string ~labels:term.t_label
with Not_found -> raw_string in
((get_element_name term model_element.me_name.men_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
() in
let model = add_to_model model new_model_element in
build_model_rec
raw_strings_tail
terms_tail
(
let t = Mstr.find raw_element_name term_map in
let real_model_trace = construct_name (get_model_trace_string ~labels:t.t_label) in
let model_element = {
me_name = real_model_trace;
me_value = raw_element.me_value;
me_location = t.t_loc;
me_term = Some t;
} in
add_to_model model model_element
)
with Not_found -> model)
model
raw_model
let handle_contradictory_vc model_files vc_term_loc =
(* The VC is contradictory if the location of the term that triggers VC
......
......@@ -31,7 +31,7 @@ type 'a pp = Pp.formatter -> 'a -> unit
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
queried_terms : Term.term list;
queried_terms : Term.term Stdlib.Mstr.t;
}
type printer_args = {
......@@ -54,7 +54,7 @@ exception UnknownPrinter of string
let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_term_loc = None;
queried_terms = [];
queried_terms = Stdlib.Mstr.empty;
}
let register_printer ~desc s p =
......
......@@ -30,7 +30,7 @@ type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
(* The position of the term that triggers the VC *)
queried_terms : Term.term list;
queried_terms : Term.term Stdlib.Mstr.t;
(* The list of terms that were queried for the counter-example
by the printer *)
}
......
......@@ -547,26 +547,33 @@ let print_logic_decl info fmt (ls,def) =
List.iter (forget_var info) vsl
end
let print_info_model cntexample fmt model_list info =
let print_info_model cntexample fmt info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if model_list != [] && cntexample then
if not (S.is_empty info_model) && 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 ->
let model_map =
S.fold (fun f acc ->
fprintf str_formatter "%a" (print_fmla info) f;
let s = flush_str_formatter () in
fprintf fmt "%s " s;
) model_list;
Stdlib.Mstr.add s f acc)
info_model
Stdlib.Mstr.empty in
fprintf fmt "))@]@\n";
(* Printing model has modification of info.info_model as undesirable
side-effect. Revert it back. *)
info.info_model <- info_model
info.info_model <- info_model;
model_map
end
else
Stdlib.Mstr.empty
let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
| Paxiom ->
......@@ -583,9 +590,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
info.info_in_goal <- true;
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
info.info_in_goal <- false;
let model_list = S.elements info.info_model in
fprintf fmt "@[(check-sat)@]@\n";
print_info_model cntexample fmt model_list info;
let model_list = print_info_model cntexample fmt info in
if cntexample then begin
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
......
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