Commit 53339f1d authored by Benedikt Becker's avatar Benedikt Becker

Simplify raw_model_parser by using printing_mapping

parent e04e93cd
......@@ -619,9 +619,7 @@ let get_kind vc_attrs elt =
type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser =
Ident.ident Mstr.t -> Ident.ident Mstr.t -> ((string * string) list) Mstr.t ->
string list -> Ident.Sattr.t Mstr.t -> string -> model_element list
type raw_model_parser = printer_mapping -> string -> model_element list
(*
***************************************************************
......@@ -1233,16 +1231,6 @@ type reg_model_parser = Pp.formatted * raw_model_parser
let model_parsers : reg_model_parser Hstr.t = Hstr.create 17
let make_mp_from_raw (raw_mp:raw_model_parser) =
fun input printer_mapping ->
let list_proj = printer_mapping.list_projections in
let list_fields = printer_mapping.list_fields in
let list_records = printer_mapping.list_records in
let noarg_cons = printer_mapping.noarg_constructors in
let set_str = printer_mapping.set_str in
let raw_model = raw_mp list_proj list_fields list_records noarg_cons set_str input in
build_model raw_model printer_mapping
let register_model_parser ~desc s p =
if Hstr.mem model_parsers s then raise (KnownModelParser s);
Hstr.replace model_parsers s (desc, p)
......@@ -1252,11 +1240,14 @@ let lookup_raw_model_parser s : raw_model_parser =
with Not_found -> raise (UnknownModelParser s)
let lookup_model_parser s : model_parser =
make_mp_from_raw (lookup_raw_model_parser s)
let raw_mp = lookup_raw_model_parser s in
fun input printer_mapping ->
let raw_model = raw_mp printer_mapping input in
build_model raw_model printer_mapping
let list_model_parsers () =
Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) model_parsers []
let () = register_model_parser
~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
(fun _ _ _ _ _ _ -> [])
(fun _ _ -> [])
......@@ -282,20 +282,7 @@ type model_parser = string -> Printer.printer_mapping -> model
and builds model data structure.
*)
type raw_model_parser =
Ident.ident Wstdlib.Mstr.t -> Ident.ident Wstdlib.Mstr.t -> ((string * string) list) Wstdlib.Mstr.t ->
string list -> Ident.Sattr.t Wstdlib.Mstr.t -> string -> model_element list
(** Parses the input string into model elements.
[raw_model_parser: proj->record_map->noarg_cons->s->mel]
[proj]: is the list of projections
[list_field]: is the list of field function definition
[record_map]: is a map associating the name of printed projections to the
fields (couple of printed field and model_trace name).
[noarg_cons]: List of constructors with no arguments (collected to avoid
confusion between variable and constructors)
[s]: model
[mel]: collected model
*)
type raw_model_parser = Printer.printer_mapping -> string -> model_element list
val register_remove_field:
(Ident.Sattr.t * model_value -> Ident.Sattr.t * model_value) -> unit
......
......@@ -704,17 +704,13 @@ and convert_tarray_to_array a =
| TConst t -> Const (convert_tterm_to_term t)
| TStore (a, t1, t2) -> Store (convert_tarray_to_array a, convert_tterm_to_term t1, convert_tterm_to_term t2)
let create_list (projections_list: Ident.ident Mstr.t)
(field_list: Ident.ident Mstr.t)
(list_records: ((string * string) list) Mstr.t)
(noarg_constructors: string list) (set_str: Ident.Sattr.t Mstr.t)
(table: definition Mstr.t) =
let create_list pm (table: definition Mstr.t) =
(* Convert list_records to take replace fields with model_trace when
necessary. *)
let list_records =
Mstr.fold (fun key l acc ->
Mstr.add key (List.map (fun (a, b) -> if b = "" then a else b) l) acc) list_records Mstr.empty
Mstr.add key (List.map (fun (a, b) -> if b = "" then a else b) l) acc) pm.Printer.list_records Mstr.empty
in
(* Convert Apply that were actually recorded as record to Record. Also replace
......@@ -722,7 +718,7 @@ let create_list (projections_list: Ident.ident Mstr.t)
let table =
Mstr.fold (fun key value acc ->
let value =
definition_apply_to_record list_records noarg_constructors value
definition_apply_to_record list_records pm.Printer.noarg_constructors value
in
Mstr.add key value acc) table Mstr.empty
in
......@@ -752,7 +748,7 @@ let create_list (projections_list: Ident.ident Mstr.t)
(* First recover values stored in projections that were registered *)
let table =
Mstr.fold (fun key value acc ->
if Mstr.mem key projections_list || Mstr.mem key field_list then
if Mstr.mem key pm.Printer.list_projections || Mstr.mem key pm.Printer.list_fields then
add_vars_to_table acc key value
else
acc)
......@@ -779,7 +775,7 @@ let create_list (projections_list: Ident.ident Mstr.t)
(* Then converts all variables to raw_model_element *)
Mstr.fold
(fun key value list_acc ->
try (convert_to_model_element ~set_str field_list key value :: list_acc)
try (convert_to_model_element ~set_str:pm.Printer.set_str pm.Printer.list_fields key value :: list_acc)
with Not_value when not (Debug.test_flag debug_cntex &&
Debug.test_flag Debug.stack_trace) ->
Debug.dprintf debug_cntex "Element creation failed: %s@." key;
......
......@@ -24,8 +24,6 @@ val register_apply_to_records:
unit
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Ident.ident Mstr.t ->
Ident.ident Mstr.t -> ((string * string) list) Mstr.t -> string list ->
Ident.Sattr.t Mstr.t ->
Smt2_model_defs.definition Mstr.t -> Model_parser.model_element list
val create_list: Printer.printer_mapping ->
Smt2_model_defs.definition Mstr.t ->
Model_parser.model_element list
......@@ -57,28 +57,23 @@ let do_parsing model =
l;
Wstdlib.Mstr.empty
let do_parsing list_proj list_fields list_records noarg_constructors set_str model =
let m = do_parsing model in
Collect_data_model.create_list list_proj list_fields list_records noarg_constructors set_str m
(* Parses the model returned by CVC4, Z3 or Alt-ergo.
Returns the list of pairs term - value *)
(* For Alt-ergo the output is not the same and we
match on "I don't know". But we also need to begin
parsing on a fresh new line ".*" ensures it *)
let parse : raw_model_parser =
fun list_proj list_fields list_records noarg_constructors set_str input ->
try
(* let r = Re.Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Re.Str.search_forward r input 0);
let match_end = Re.Str.match_end () in*)
let nr = Re.Str.regexp "^)+" in
let res = Re.Str.search_backward nr input (String.length input) in
let model_string = String.sub input 0 (res + String.length (Re.Str.matched_string input)) in
do_parsing list_proj list_fields list_records noarg_constructors set_str model_string
with
| Not_found -> []
fun printer_mapping input ->
try
(* let r = Re.Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Re.Str.search_forward r input 0);
let match_end = Re.Str.match_end () in*)
let nr = Re.Str.regexp "^)+" in
let res = Re.Str.search_backward nr input (String.length input) in
let model_string = String.sub input 0 (res + String.length (Re.Str.matched_string input)) in
let model = do_parsing model_string in
Collect_data_model.create_list printer_mapping model
with Not_found -> []
let () = register_model_parser "smtv2" parse
~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
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