Commit d9349898 authored by Sylvain Dailler's avatar Sylvain Dailler

Removed ad hoc support of projections in ce (to_rep/of_rep)

Formerly, projections were queried based on their name after parsing of
the model. The printed projections are now collected during printing of
the smtv task. They are given in printer_mapping together with queried
terms to the parser for models.
parent f7e92811
......@@ -307,7 +307,7 @@ let default_model = {
type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser = string -> model_element list
type raw_model_parser = Stdlib.Sstr.t -> string -> model_element list
(*
***************************************************************
......@@ -673,18 +673,19 @@ 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 raw_model = raw_mp input in
let list_proj = printer_mapping.list_projections in
let raw_model = raw_mp list_proj 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)
let lookup_raw_model_parser s =
let lookup_raw_model_parser s : raw_model_parser =
try snd (Hstr.find model_parsers s)
with Not_found -> raise (UnknownModelParser s)
let lookup_model_parser s =
let lookup_model_parser s : model_parser =
make_mp_from_raw (lookup_raw_model_parser s)
let list_model_parsers () =
......@@ -692,4 +693,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 _ _ -> [])
......@@ -309,8 +309,10 @@ type model_parser = string -> Printer.printer_mapping -> model
and builds model data structure.
*)
type raw_model_parser = string -> model_element list
(** Parses the input string into model elements. *)
type raw_model_parser = Stdlib.Sstr.t -> string -> model_element list
(** Parses the input string into model elements. It contains the list of
projections that are collected in the task.
*)
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
......
......@@ -32,6 +32,7 @@ type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
queried_terms : Term.term Stdlib.Mstr.t;
list_projections: Stdlib.Sstr.t;
}
type printer_args = {
......@@ -55,6 +56,7 @@ let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_term_loc = None;
queried_terms = Stdlib.Mstr.empty;
list_projections = Stdlib.Sstr.empty;
}
let register_printer ~desc s p =
......
......@@ -33,6 +33,8 @@ type printer_mapping = {
queried_terms : Term.term Stdlib.Mstr.t;
(* The list of terms that were queried for the counter-example
by the printer *)
list_projections: Stdlib.Sstr.t;
(* List of projections as printed in the model *)
}
type printer_args = {
......
......@@ -309,81 +309,91 @@ let print_table t =
(* Given a to_rep and its corresponding of_rep in the model gives a guessed
value to unknown variables using constant of_rep/to_rep and "else" case of
the ITE.*)
let corres_else_element table to_rep of_rep =
let corres_else_element table to_rep =
let (_key1, (_b1, to_rep)) = to_rep in
let (_key2, (_b2, of_rep)) = of_rep in
(*let (_key2, (_b2, of_rep)) = of_rep in*)
let to_rep = match to_rep with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Not_value in
(*
let of_rep = match of_rep with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Not_value in
let rec corres_else_element table to_rep of_rep =
match (to_rep, of_rep) with
| Ite (_, _, _, to_rep), _ -> corres_else_element table to_rep of_rep
| _, Ite (_, _, _, of_rep) -> corres_else_element table to_rep of_rep
| t, Cvc4_Variable cvc ->
*)
let cvc = ref None in
let rec corres_else_element table to_rep =
match to_rep with
| Ite (Function_Local_Variable _v, Cvc4_Variable v, _, to_rep) ->
cvc := Some v;
corres_else_element table to_rep
| t ->
(* Make all variables not already guessed equal to the else case *)
let s = remove_end_num cvc in
add_all_cvc s table (false, Term t)
| _ -> table
in
(* Case where to_rep, of_rep are constant values *)
let table =
match (to_rep, of_rep) with
| t, Cvc4_Variable cvc ->
Mstr.add cvc (false, Term t) table
| _ -> table
begin
match !cvc with
| None -> table
| Some cvc ->
(* Last element of the if is added for all unassigned variables of
same name. *)
let s = remove_end_num cvc in
add_all_cvc s table (false, Term t)
end
in
corres_else_element table to_rep of_rep
corres_else_element table to_rep
let to_rep_of_rep (table: correspondence_table) =
let to_reps =
let to_rep_of_rep (table: correspondence_table) (projections_list: Stdlib.Sstr.t) =
let projections_lists =
Mstr.fold (fun key value acc ->
if Stdlib.Sstr.mem key projections_list then
(key, value) :: acc else acc) table [] in
(*
List.sort (fun x y -> String.compare (fst x) (fst y))
(Mstr.fold (fun key value acc ->
if has_prefix "to_rep" key then
(key,value) :: acc else acc) table []) in
*)
(*
let of_reps =
List.sort (fun x y -> String.compare (fst x) (fst y))
(Mstr.fold (fun key value acc -> if has_prefix "of_rep" key then
(key,value) :: acc else acc) table []) in
*)
List.fold_left (fun table to_rep ->
corres_else_element table to_rep)
table projections_lists
(*
let to_rep_of_rep table to_reps =
List.fold_left (fun table to_rep ->
corres_else_element table to_rep)
table projections_lists
(*
match to_reps with
| to_rep :: tl1 ->
let table = corres_else_element table to_rep in
to_rep_of_rep table tl1
| [] -> table*)
in
let rec to_rep_of_rep table to_reps of_reps =
match to_reps, of_reps with
| to_rep :: tl1, of_rep :: tl2 ->
let table = corres_else_element table to_rep of_rep in
to_rep_of_rep table tl1 tl2
| [], [] -> table
| _ -> table (* Error case *) in
to_rep_of_rep table to_reps of_reps
to_rep_of_rep table projections_list
*)
let create_list (table: correspondence_table) =
let create_list (projections_list: Stdlib.Sstr.t) (table: correspondence_table) =
(* First populate the table with all references to a cvc variable *)
let table = get_all_var table in
(* First recover the values of variables that can be recovered in to/of_rep *)
(* First recover values stored in projections that were registered *)
let table =
Mstr.fold (fun key value acc ->
if has_prefix "of_rep" key && not (String.contains key '!') then
add_vars_to_table acc value else acc) table table in
(* of_rep is done before to_rep because we complete from value with the
else branch of the function *)
let table =
Mstr.fold (fun key value acc ->
if has_prefix "to_rep" key && not (String.contains key '!') then
add_vars_to_table acc value else acc) table table in
if Stdlib.Sstr.mem key projections_list then
add_vars_to_table acc value
else
acc)
table table in
(* Recover values from the combination of to_rep and of_rep *)
let table = to_rep_of_rep table in
let table = to_rep_of_rep table projections_list in
(* Then substitute all variables with their values *)
let table =
......
......@@ -15,4 +15,5 @@ val print_table:
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Smt2_model_defs.correspondence_table -> Model_parser.model_element list
Stdlib.Sstr.t -> Smt2_model_defs.correspondence_table ->
Model_parser.model_element list
......@@ -48,16 +48,16 @@ let do_parsing model =
Stdlib.Mstr.empty
end
let do_parsing model =
let do_parsing list_proj model =
let m = do_parsing model in
Collect_data_model.create_list m
Collect_data_model.create_list list_proj 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 = function input ->
let parse : raw_model_parser = fun list_proj input ->
try
let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Str.search_forward r input 0);
......@@ -65,7 +65,7 @@ let parse : raw_model_parser = function 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 model_string
do_parsing list_proj model_string
with
| Not_found -> []
......
......@@ -44,6 +44,7 @@ type info = {
mutable info_model: S.t;
info_vc_term: vc_term_info;
mutable info_in_goal: bool;
mutable list_projections: Stdlib.Sstr.t;
}
let ident_printer () =
......@@ -86,6 +87,8 @@ let print_ident_label info fmt id =
let forget_var info v = forget_id info.info_printer v.vs_name
let collect_model_ls info ls =
if Slab.mem model_projection ls.ls_name.id_label then
info.list_projections <- Stdlib.Sstr.add (sprintf "%a" (print_ident info) ls.ls_name) info.list_projections;
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 <-
......@@ -409,7 +412,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f =
let model_list = print_info_model cntexample info in
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
queried_terms = model_list; };
queried_terms = model_list;
list_projections = info.list_projections;};
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
(print_ident info) pr.pr_name (print_fmla info) f
| Plemma| Pskip -> assert false
......@@ -467,7 +471,9 @@ let print_task args ?old:_ fmt task =
info_printer = ident_printer ();
info_model = S.empty;
info_vc_term = vc_info;
info_in_goal = false;} in
info_in_goal = false;
list_projections = Stdlib.Sstr.empty;
} in
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print_decls = function
......
......@@ -75,6 +75,8 @@ let model_label = Ident.create_label "model"
(* This label identifies terms that should be in counter-example. *)
let model_vc_term_label = Ident.create_label "model_vc"
(* This label identifies the term that triggers the VC. *)
let model_projection = Ident.create_label "model_projection"
let add_model_element (el: term) info_model =
(** Add element el (term) to info_model.
......
......@@ -42,6 +42,8 @@ val print_label: Format.formatter -> Ident.label -> unit
val model_label: Ident.label
val model_projection: Ident.label
val model_vc_term_label: Ident.label
val add_model_element: Term.term -> S.t -> S.t
......
......@@ -121,6 +121,7 @@ type info = {
mutable info_in_goal : bool;
info_vc_term : vc_term_info;
info_printer : ident_printer;
mutable list_projections : Stdlib.Sstr.t;
}
let debug_print_term message t =
......@@ -170,6 +171,8 @@ let print_var_list info fmt vsl =
let model_projected_label = Ident.create_label "model_projected"
let collect_model_ls info ls =
if Slab.mem model_projection ls.ls_name.id_label then
info.list_projections <- Stdlib.Sstr.add (sprintf "%a" (print_ident info) ls.ls_name) info.list_projections;
if ls.ls_args = [] && (Slab.mem model_label ls.ls_name.id_label ||
Slab.mem model_projected_label ls.ls_name.id_label) then
let t = t_app ls [] ls.ls_value in
......@@ -509,7 +512,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
queried_terms = model_list; }
queried_terms = model_list;
list_projections = info.list_projections;}
| Plemma| Pskip -> assert false
......@@ -569,7 +573,9 @@ let print_task args ?old:_ fmt task =
info_model = S.empty;
info_in_goal = false;
info_vc_term = vc_info;
info_printer = ident_printer () } in
info_printer = ident_printer ();
list_projections = Stdlib.Sstr.empty;
} in
print_prelude fmt args.prelude;
set_produce_models fmt cntexample;
print_th_prelude task fmt args.th_prelude;
......
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