Commit 3ea32678 authored by Sylvain Dailler's avatar Sylvain Dailler

Change the way counterexamples are parsed

The way records are recognized during model parsing is changed:
we previously recognized records during parsing by looking at the name of
the variable returned by the prover (mk_r mk__rep etc).
Now, we collect the names of constructor of records (recognized using
their id_string beginning with "mk ") during the printing of the smt2
files. So, after parsing of the model, we can match the name of an
application with a previously collected constructor: we can recreate
the record.

The same can be done for all algebraic datatype.

This change also solve the problem of parsing in ce-bench.
parent 67fb9627
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "-1" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } } },
{"others" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "-1" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } } },
{"others" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 47:
old rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test3 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 51:
......@@ -9,6 +41,10 @@ re_rec_map.f_map = {"type" : "Array" ,
re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 53:
rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "false" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 54:
......@@ -17,14 +53,54 @@ old re_rec_map.f_map = {"type" : "Array" ,
"val" : "0" } }] }
old re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
old rec_map.f_map = {"type" : "Array" ,
"val" : [{"indice" : "false" , "value" : {"type" : "Integer" ,
"val" : "-1" } }, {"others" : {"type" : "Integer" ,
"val" : "1" } }] }
old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "-1" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } } },
{"others" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "-1" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } } },
{"others" : {"type" : "Record" , "val" : {"Field" : [{"field" : ".field_f" ,
"value" : {"type" : "Integer" , "val" : "0" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 47:
old rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "true" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test3 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 51:
re_rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "false" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 53:
......@@ -34,6 +110,10 @@ rec_map.f_map = {"type" : "Array" ,
rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 54:
old re_rec_map.f_map = {"type" : "Array" , "val" : [{"indice" : "false" ,
"value" : {"type" : "Integer" , "val" : "-1" } },
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
old re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
old rec_map.f_map = {"type" : "Array" ,
......
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
......@@ -37,6 +49,18 @@ old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
......
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
......@@ -37,6 +49,18 @@ old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
ce/record_map.mlw M WP_parameter map_record_proj_test1 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 41:
map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
Line 42:
old map_rec = {"type" : "Array" , "val" : [{"others" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".field_f" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 46:
......
......@@ -44,6 +44,7 @@ type model_value =
| Array of model_array
| Record of model_record
| Bitvector of string
| Apply of string * model_value list
| Unparsed of string
and arr_index = {
arr_index_key : string; (* Even array indices can exceed MAX_INT with Z3 *)
......@@ -53,10 +54,8 @@ and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_record = {
discrs : model_value list;
fields : model_value list;
}
and model_record = (field_name * model_value) list
and field_name = string
let array_create_constant ~value =
{
......@@ -136,6 +135,16 @@ let rec convert_model_value value : Json_base.json =
let m = Mstr.add "type" (Json_base.String "Array") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.List l) m in
Json_base.Record m
| Apply (s, lt) ->
let lt = List.map convert_model_value lt in
let slt =
let m = Mstr.add "list" (Json_base.List lt) Stdlib.Mstr.empty in
let m = Mstr.add "apply" (Json_base.String s) m in
Json_base.Record m
in
let m = Mstr.add "type" (Json_base.String "Apply") Stdlib.Mstr.empty in
let m = Mstr.add "val" slt m in
Json_base.Record m
| Record r ->
convert_record r
......@@ -154,18 +163,19 @@ and convert_indices indices =
and convert_record r =
let m = Mstr.add "type" (Json_base.String "Record") Stdlib.Mstr.empty in
let fields = convert_fields r.fields in
let discrs = convert_discrs r.discrs in
let m_field_discr = Mstr.add "Field" fields Stdlib.Mstr.empty in
let m_field_discr = Mstr.add "Discr" discrs m_field_discr in
let m = Mstr.add "val" (Json_base.Record m_field_discr) m in
let fields = convert_fields r in
let m_field = Mstr.add "Field" fields Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.Record m_field) m in
Json_base.Record m
and convert_fields fields =
Json_base.List (List.map convert_model_value fields)
and convert_discrs discrs =
Json_base.List (List.map convert_model_value discrs)
Json_base.List
(List.map
(fun (f, v) ->
let m = Mstr.add "field" (Json_base.String f) Stdlib.Mstr.empty in
let m = Mstr.add "value" (convert_model_value v) m in
Json_base.Record m)
fields)
let print_model_value_sanit fmt v =
let v = convert_model_value v in
......@@ -199,11 +209,10 @@ let rec print_array_human fmt (arr: model_array) =
arr.arr_indices;
fprintf fmt "others => %a)" print_model_value_human arr.arr_others
(* TODO there should be no record printed that way currently in Why3 *)
and print_record_human fmt r =
fprintf fmt "Record(";
List.iter (fun x -> fprintf fmt "%a" print_model_value_human x) r.fields;
fprintf fmt ")"
fprintf fmt "%a"
(Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi
(fun fmt (f, v) -> fprintf fmt "%s = %a" f print_model_value_human v)) r
and print_model_value_human fmt (v: model_value) =
match v with
......@@ -212,6 +221,8 @@ and print_model_value_human fmt (v: model_value) =
| Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
| Float f -> print_float_human fmt f
| Boolean b -> fprintf fmt "%b" b
| Apply (s, lt) ->
fprintf fmt "[%s %a]" s (Pp.print_list Pp.space print_model_value_human) lt
| Array arr -> print_array_human fmt arr
| Record r -> print_record_human fmt r
| Bitvector s -> fprintf fmt "%s" s
......@@ -307,7 +318,9 @@ let default_model = {
type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser = Stdlib.Sstr.t -> string -> model_element list
type raw_model_parser =
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t ->
string -> model_element list
(*
***************************************************************
......@@ -713,7 +726,8 @@ 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 raw_model = raw_mp list_proj input in
let list_records = printer_mapping.list_records in
let raw_model = raw_mp list_proj list_records input in
build_model raw_model printer_mapping
let register_model_parser ~desc s p =
......@@ -732,4 +746,4 @@ let list_model_parsers () =
let () = register_model_parser
~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
(fun _ _ -> [])
(fun _ _ _ -> [])
......@@ -32,6 +32,7 @@ type model_value =
| Array of model_array
| Record of model_record
| Bitvector of string
| Apply of string * model_value list
| Unparsed of string
and arr_index = {
arr_index_key : string;
......@@ -41,10 +42,8 @@ and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_record ={
discrs : model_value list;
fields : model_value list;
}
and model_record = (field_name * model_value) list
and field_name = string
val array_create_constant :
value : model_value ->
......@@ -313,9 +312,13 @@ type model_parser = string -> Printer.printer_mapping -> model
and builds model data structure.
*)
type raw_model_parser = Stdlib.Sstr.t -> string -> model_element list
type raw_model_parser =
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t ->
string -> model_element list
(** Parses the input string into model elements. It contains the list of
projections that are collected in the task.
projections and a map associating the name of printed projections to the
fields (couple of printed field and model_trace name) that are collected in
the task.
*)
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
......
......@@ -33,6 +33,7 @@ type printer_mapping = {
vc_term_loc : Loc.position option;
queried_terms : Term.term Stdlib.Mstr.t;
list_projections: Stdlib.Sstr.t;
list_records: ((string * string) list) Stdlib.Mstr.t;
}
type printer_args = {
......@@ -57,6 +58,7 @@ let get_default_printer_mapping = {
vc_term_loc = None;
queried_terms = Stdlib.Mstr.empty;
list_projections = Stdlib.Sstr.empty;
list_records = Stdlib.Mstr.empty;
}
let register_printer ~desc s p =
......
......@@ -35,6 +35,7 @@ type printer_mapping = {
by the printer *)
list_projections: Stdlib.Sstr.t;
(* List of projections as printed in the model *)
list_records: ((string * string) list) Stdlib.Mstr.t;
}
type printer_args = {
......
......@@ -41,11 +41,12 @@ let rec get_variables_term (table: correspondence_table) t =
else
Mstr.add cvc (false, Noelement) table
| Record (_, l) ->
List.fold_left (fun table t -> get_variables_term table t) table l
| Discr (_, l) ->
List.fold_left (fun table t -> get_variables_term table t) table l
List.fold_left (fun table (_f, t) -> get_variables_term table t) table l
| To_array t ->
get_variables_term table t
| Apply (_s, lt) ->
List.fold_left (fun table t -> get_variables_term table t) table lt
and get_variables_array table a =
match a with
......@@ -195,11 +196,11 @@ and refine_function table term =
| Array a ->
Array (refine_array table a)
| Record (n, l) ->
Record (n, List.map (fun x -> refine_function table x) l)
| Discr (n, l) ->
Discr (n, List.map (fun x -> refine_function table x) l)
Record (n, List.map (fun (f, v) -> f, refine_function table v) l)
| To_array t ->
To_array (refine_function table t)
| Apply (s, lt) ->
Apply (s, List.map (refine_function table) lt)
and refine_variable_value (table: correspondence_table) key v =
......@@ -225,6 +226,7 @@ let convert_to_indice t =
match t with
| Integer i -> i
| Bitvector bv -> bv
| Boolean b -> string_of_bool b
| _ -> raise Not_value
let rec convert_array_value (a: array) : Model_parser.model_array =
......@@ -257,7 +259,8 @@ and convert_to_model_value (t: term): Model_parser.model_value =
| Cvc4_Variable _v -> raise Not_value (*Model_parser.Unparsed "!"*)
(* TODO change the value returned for non populated Cvc4 variable '!' -> '?' ? *)
| To_array t -> convert_to_model_value (Array (convert_z3_array t))
| Function_Local_Variable _ | Variable _ | Ite _ | Discr _ -> raise Not_value
| Apply (s, lt) -> Model_parser.Apply (s, List.map convert_to_model_value lt)
| Function_Local_Variable _ | Variable _ | Ite _ -> raise Not_value
and convert_z3_array (t: term) : array =
......@@ -281,21 +284,7 @@ and convert_z3_array (t: term) : array =
convert_array t
and convert_record l =
let acc = ref [] in
let rec convert_aux l =
match l with
| Discr (_n, l) :: tl ->
acc := List.map convert_to_model_value l;
convert_aux tl
| a :: tl ->
convert_to_model_value a :: convert_aux tl
| [] -> []
in
let record_field = convert_aux l in
{
Model_parser.discrs = !acc;
Model_parser.fields = record_field
}
List.map (fun (f, v) -> f, convert_to_model_value v) l
let convert_to_model_element name t =
match t with
......@@ -304,7 +293,70 @@ let convert_to_model_element name t =
let value = convert_to_model_value t in
Model_parser.create_model_element ~name ~value ()
let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table) =
let apply_to_record (list_records: (string list) Mstr.t) (t: term) =
let rec array_apply_to_record (a: array) =
match a with
| Const x ->
let x = apply_to_record x in
Const x
| Store (a, t1, t2) ->
let a = array_apply_to_record a in
let t1 = apply_to_record t1 in
let t2 = apply_to_record t2 in
Store (a, t1, t2)
and apply_to_record (v: term) =
match v with
| Integer _ | Decimal _ | Fraction _ | Float _ | Boolean _ | Bitvector _
| Cvc4_Variable _ | Function_Local_Variable _ | Variable _ | Other _ -> v
| Array a ->
Array (array_apply_to_record a)
| Record (s, l) ->
let l = List.map (fun (f,v) -> f, apply_to_record v) l in
Record (s, l)
| Apply (s, l) ->
let l = List.map apply_to_record l in
if Mstr.mem s list_records then
Record (s, List.combine (Mstr.find s list_records) l)
else
Apply (s, l)
| Ite (t1, t2, t3, t4) ->
let t1 = apply_to_record t1 in
let t2 = apply_to_record t2 in
let t3 = apply_to_record t3 in
let t4 = apply_to_record t4 in
Ite (t1, t2, t3, t4)
| To_array t1 ->
let t1 = apply_to_record t1 in
To_array t1
in
apply_to_record t
let definition_apply_to_record list_records d =
match d with
| Function (lt, t) ->
Function (lt, apply_to_record list_records t)
| Term t -> Term (apply_to_record list_records t)
| Noelement -> Noelement
let create_list (projections_list: Sstr.t) (list_records: ((string * string) list) Mstr.t)
(table: correspondence_table) =
(* 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
in
(* Convert Apply that were actually recorded as record to Record. *)
let table =
Mstr.fold (fun key (b, value) acc ->
let value = definition_apply_to_record list_records value in
Mstr.add key (b, value) acc) table Mstr.empty
in
(* First populate the table with all references to a cvc variable *)
let table = get_all_var table in
......@@ -312,7 +364,7 @@ let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table)
(* First recover values stored in projections that were registered *)
let table =
Mstr.fold (fun key value acc ->
if Stdlib.Sstr.mem key projections_list then
if Sstr.mem key projections_list then
add_vars_to_table acc value
else
acc)
......@@ -332,6 +384,7 @@ let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table)
Some t
| _ -> None in
try (convert_to_model_element key t :: list_acc)
with Not_value -> list_acc)
with Not_value when not (Debug.test_flag Debug.stack_trace) -> list_acc
| e -> raise e)
table
[]
......@@ -15,5 +15,5 @@ val print_table:
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Stdlib.Sstr.t -> Smt2_model_defs.correspondence_table ->
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t -> Smt2_model_defs.correspondence_table ->
Model_parser.model_element list
......@@ -50,16 +50,16 @@ let do_parsing model =
Stdlib.Mstr.empty
end
let do_parsing list_proj model =
let do_parsing list_proj list_records model =
let m = do_parsing model in
Collect_data_model.create_list list_proj m
Collect_data_model.create_list list_proj list_records 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 input ->
let parse : raw_model_parser = fun list_proj list_records input ->
try
let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Str.search_forward r input 0);
......@@ -67,7 +67,7 @@ let parse : raw_model_parser = fun list_proj input ->
let nr = Str.regexp "^)" in
let res = Str.search_backward nr input (String.length input) in
let model_string = String.sub input match_end (res + 1 - match_end) in
do_parsing list_proj model_string
do_parsing list_proj list_records model_string
with
| Not_found -> []
......
......@@ -59,23 +59,6 @@ rule token = parse
| "false" { FALSE }
| "LAMBDA" { LAMBDA }
| "ARRAY_LAMBDA" { ARRAY_LAMBDA }
| "mk___split_fields"(opt_num as n) dummy {
match n with
| "" -> MK_SPLIT_FIELD ("mk___split_fields",0)
| n -> MK_SPLIT_FIELD ("mk___split_fields"^n, int_of_string n) }
| "mk___rep"(opt_num as n) dummy {
match n with
| "" -> MK_REP ("mk___rep", 0)
| n -> MK_REP ("mk___rep"^n, int_of_string n) }
| "mk___t"(opt_num as n) dummy {
match n with
| "" -> MK_T ("mk___t", 0)
| n -> MK_T ("mk___t"^n, int_of_string n) }
| "mk___split_discrs"(opt_num as n) dummy {
match n with
| "" -> MK_SPLIT_DISCRS ("mk___split_discrs",0)
| n -> MK_SPLIT_DISCRS ("mk___split_discrs"^n, int_of_string n) }
| "mk" name dummy { MK_ANYTHING } (* encapsulate mk_int_ref etc (other refs) *)
| "(_" space+ "bv"(num as bv_value) space+ num")" { BITVECTOR_VALUE bv_value }
| "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
......
......@@ -42,11 +42,6 @@
%token <string * string> DEC_STR
%token <string * string> MINUS_DEC_STR
%token LPAREN RPAREN
%token MK_ANYTHING
%token <string * int> MK_REP
%token <string * int> MK_SPLIT_FIELD
%token <string * int> MK_T
%token <string * int> MK_SPLIT_DISCRS
%token EOF
%%
......@@ -67,27 +62,16 @@ list_decls:
))"
*)
decl:
| DEFINE_FUN tname LPAREN args_lists RPAREN
| DEFINE_FUN name LPAREN args_lists RPAREN
ireturn_type smt_term
{ let t = Smt2_model_defs.make_local $4 $7 in
Some ($2, (Smt2_model_defs.Function ($4, t))) }
| DECLARE_SORT isort_def { None }
| DECLARE_DATATYPES idata_def { None }
(* z3 declare function *)
| DECLARE_FUN tname LPAREN args_lists RPAREN ireturn_type { None }
| DECLARE_FUN name LPAREN args_lists RPAREN ireturn_type { None }
| FORALL LPAREN args_lists RPAREN smt_term { None } (* z3 cardinality *)
(* Names. For atoms that are used to recognize different types of values,
we return the string the lexer detected (as expected). These names
are not used. *)
tname:
| name { $1 }
| MK_REP { fst $1 }
| MK_SPLIT_FIELD { fst $1 }
| MK_T { fst $1 }
| MK_SPLIT_DISCRS { fst $1 }
| MK_ANYTHING { "" } (* ignore text on this keyword for the moment *)
smt_term:
| name { Smt2_model_defs.Variable $1 }
| integer { Smt2_model_defs.Integer $1 }
......@@ -105,33 +89,22 @@ smt_term:
| None -> Smt2_model_defs.Other ""
| Some (t1, t2) -> Smt2_model_defs.Ite (t1, t2, $4, $5) }
(* No parsable value are applications. *)
| application { Smt2_model_defs.Other "" }
(* This is SPARK-specific stuff. It is used to parse records, discriminants
and stuff generated by SPARK with specific "keywords" :
mk___rep(num), mk___split_field(num) etc *)
| LPAREN MK_REP list_smt_term RPAREN
{ Smt2_model_defs.build_record_discr (List.rev $3) }
(* Specifically for mk___t, we are only interested in the first value *)
| LPAREN MK_T list_smt_term RPAREN { List.hd (List.rev $3) }
| LPAREN MK_SPLIT_FIELD list_smt_term RPAREN
{ Smt2_model_defs.Record (snd $2, List.rev $3) }
| LPAREN MK_SPLIT_DISCRS list_smt_term RPAREN
{ Smt2_model_defs.Discr (snd $2, List.rev $3) }
| LPAREN MK_ANYTHING smt_term RPAREN { $3 } (* ad hoc for refs *)
| application { $1 }
(* Particular case for functions that are defined as an equality:
define-fun f ((a int) (b int)) (= a b) *)
| LPAREN EQUAL list_smt_term RPAREN { Smt2_model_defs.Other "" }
| LPAREN LET LPAREN list_let RPAREN smt_term RPAREN
{ Smt2_model_defs.substitute $4 $6 }
(* z3 specific constructor *)
| LPAREN UNDERSCORE AS_ARRAY tname RPAREN
| LPAREN UNDERSCORE AS_ARRAY name RPAREN
{ Smt2_model_defs.To_array (Smt2_model_defs.Variable $4) }
(* value of let are not used *)
list_let:
| { [] }
| LPAREN tname smt_term RPAREN list_let { ($2, $3) :: $5 }
| LPAREN name smt_term RPAREN list_let { ($2, $3) :: $5 }
(* TODO not efficient *)
(* Condition of an if-then-else. We are only interested in equality case *)
......@@ -152,7 +125,7 @@ list_smt_term:
| list_smt_term smt_term { $2 :: $1}
application: