diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml index dc3a488a2f9f5bf7410a52a3726fd6e24db34793..3a76229d92f575f9f8b718bcd2827818fb513bb3 100644 --- a/src/core/model_parser.ml +++ b/src/core/model_parser.ml @@ -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 = - 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 - model +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 + ( + 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 diff --git a/src/core/printer.ml b/src/core/printer.ml index 56252d49dbbb1aa2b2e045976b2d0714e5b327df..9335f58a9106afd2ef8c5a9e96918925a6f3ef27 100644 --- a/src/core/printer.ml +++ b/src/core/printer.ml @@ -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 = diff --git a/src/core/printer.mli b/src/core/printer.mli index 95effcb7420684bbd3ecb0321bf5fc5398678c9c..bf924c8009aff92f6316df91d5aa1ebbfb0ae567 100644 --- a/src/core/printer.mli +++ b/src/core/printer.mli @@ -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 *) } diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml index cf65b66daac22c2add5c8481ed8315af45c9366c..8c2fcdac5cc2d5edbcd920247a3a45c52d29055d 100644 --- a/src/printer/smtv2.ml +++ b/src/printer/smtv2.ml @@ -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 -> - fprintf str_formatter "%a" (print_fmla info) f; - let s = flush_str_formatter () in - fprintf fmt "%s " s; - ) model_list; + + 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; + 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";