Skip to content

why3
why3
Commit bc0b6ca9 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

P419-017 counterex- Missing one liner with multidim array 

The one liner is missing because we did not project value of array
elements in intro_projections_counterexmp. I changed the whole algorithm
of projections to allow projecting values of multidim array. Also,
moved local functions outside the main function. Added some trivial
helping functions.

* intro_projections_counterexmp
 (detect_map_types): Takes a type and return the list of successive types
  in the map and the return type. On map int (map int int) returns
  ([int; int], int).
 (last_type): Takes a list of proj_functions and returns the return type
  of the last projections_function that will be applied.
 (recreate_types): Recreates the type of the map with projected return
  type.
 (create_index_list): Returns a list of new well typed symbol for
  application in the axiom.
 (recreate_term_applications): Apply array to indices.
 (list_projection_until_base_type): Returns the list of all possible
  list of proj_functions applied to it.
 (projections_for_term): Changed the map part almost completely. We do
  not call this function recursively but we used other functions to get
  the recursive behavior.
parent 10b87b23
Hide whitespace changes
Inline Side-by-side
Showing with 173 additions and 132 deletions
src/transform/intro_projections_counterexmp.ml
View file @ bc0b6ca9
......@@ -64,6 +64,178 @@ let intro_const_equal_to_term
(* Return the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
let introduce_constant ls t_rhs proj_name =
(* introduce new constant c and axiom stating c = t_rhs *)
let const_label = Slab.add model_label ls.ls_name.id_label in
let const_label = append_to_model_element_name ~labels:const_label ~to_append:proj_name in
let const_loc = Opt.get ls.ls_name.id_loc in
let const_name = ls.ls_name.id_string^"_proj_constant_"^proj_name in
let axiom_name = ls.ls_name.id_string^"_proj_axiom_"^proj_name in
let id_new = Ident.id_user ~label:const_label const_name const_loc in
intro_const_equal_to_term ~term:t_rhs ~id_new:id_new ~axiom_name
let get_record_field_suffix projection =
try
get_model_element_name ~labels:projection.ls_name.id_label
with Not_found -> ""
(* Takes a type of map and returns the list of successive type in the map
together with the return type. *)
let detect_map_types ty =
let rec detect_map_types t_froms ty =
match ty.ty_node with
| Tyapp (ts, [t_from; t_to]) when ts.ts_name.id_string = "map" ->
detect_map_types ((ts, t_from) :: t_froms) t_to
| _ -> (List.rev t_froms, ty)
in
detect_map_types [] ty
(* Returns the return type of the last functions of list proj_functions *)
let rec last_type proj_functions =
match proj_functions with
| [] -> failwith "Should not happen. Please report."
| [pf] -> (Opt.get pf.ls_value)
| _pf1 :: pf2 :: tl -> last_type (pf2 :: tl)
(* Recreate type of the composition of projection functions *)
let recreate_types ty_froms proj_functions =
let rec rec_types ty_froms =
match ty_froms with
| [(ts, ty_from)] ->
ty_app ts [ty_from; last_type proj_functions]
| (ts, ty_from) :: tl ->
let ty_to = rec_types tl in
ty_app ts [ty_from; ty_to]
| [] -> failwith "Not a correct type application. Please report."
in
rec_types ty_froms
(* Returns a list of pairs of vsymbol for array axiom definition *)
let rec create_index_list ty_froms =
match ty_froms with
| ty :: tl ->
let var_i : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh "x") ty in
let i : Term.term = Term.t_var var_i in
let l = create_index_list tl in
(var_i, i) :: l
| [] -> []
(* Applying array to indices: term[i][j][k]....[w]... *)
let rec recreate_term_applications select term var_l =
match var_l with
| i :: tl ->
let term_x = Term.t_app_infer select [term;i] in
recreate_term_applications select term_x tl
| [] -> term
(* Generate the list of projections possible for a term where a possible projection is
a list of functions that projects the result. *)
let rec list_projection_until_base_type map_projs t_to : Term.lsymbol list list =
let proj_functions = try Some (Ty.Mty.find t_to map_projs)
with | Not_found -> None in
match proj_functions with
| None -> [[]]
| Some lpfs ->
let lpfs_rec = List.map (fun x -> List.map (fun l -> x :: l)
(list_projection_until_base_type map_projs (Opt.get x.ls_value)))
lpfs in
List.fold_left (fun acc x -> acc @ x) [] lpfs_rec
let rec projections_for_term ls term proj_name applied_projs env map_projs =
(* Return declarations for projections of the term.
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to the term *)
match (Opt.get term.t_ty).ty_node with
| Tyapp (ts, [_t_from; _t_to]) when ts.ts_name.id_string = "map" -> begin
let (ty_froms, t_to) = detect_map_types (Opt.get term.t_ty) in
let pfs =
list_projection_until_base_type map_projs t_to
in
match pfs with
| [] | [[]]->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant ls term proj_name
| _ ->
List.fold_left
(fun ldecls proj_function ->
(* Newly introduced map with projected indices *)
let proj_map_name = ls.ls_name.id_string^"_proj_arr_constant"^proj_name in
let proj_map_id = Ident.id_fresh proj_map_name in
let proj_map_ty = Some (recreate_types ty_froms proj_function) in
let proj_map_ls = Term.create_lsymbol proj_map_id [] proj_map_ty in
let proj_map_decl = Decl.create_param_decl proj_map_ls in
let proj_map_t = Term.t_app proj_map_ls [] proj_map_ty in
(* The quantified variables i's *)
let var_l = create_index_list (List.map snd ty_froms) in
let map_theory = Env.read_theory env ["map"] "Map" in
let select = (ns_find_ls map_theory.th_export ["get"]) in
(* Indices: proj_map[i], term[i] *)
let term_idx_comp_app = recreate_term_applications select term (List.map snd var_l) in
let proj_map_idx_comp_app = recreate_term_applications select proj_map_t (List.map snd var_l) in
(* Formula f: forall i : t_from. proj_map[i] = pf_1(term[i]) *)
let term_idx_projected_t : Term.term =
List.fold_left (fun term_idx_comp_app proj_function ->
Term.t_app proj_function [term_idx_comp_app] proj_function.ls_value)
term_idx_comp_app proj_function in
let fla_to_be_quant = Term.t_equ proj_map_idx_comp_app term_idx_projected_t in
let fla_axiom = Term.t_forall_close (List.map fst var_l) [] fla_to_be_quant in
(* Axiom about projection: axiom f *)
let proj_axiom_name = ls.ls_name.id_string^"_proj_arr_axiom"^proj_name in
let proj_axiom_id = Decl.create_prsymbol (Ident.id_fresh proj_axiom_name) in
let proj_axiom = Decl.create_prop_decl Decl.Paxiom proj_axiom_id fla_axiom in
(* Recursively call projecting of the term proj_map -> proj_map_projections *)
let proj_name = proj_name^(List.fold_left
(fun acc x -> acc ^ get_record_field_suffix x)
"" proj_function) in
(*let applied_projs = Term.Sls.add proj_function applied_projs in*)
let proj_map_projections_defs =
introduce_constant ls proj_map_t proj_name in
List.append ldecls (
List.append [proj_map_decl;proj_axiom] proj_map_projections_defs)
)
[]
pfs
end
| _ ->
(* Non-map case *)
(* Find all projection functions for the term *)
let pfs = try (Some (Ty.Mty.find (Opt.get term.t_ty) map_projs)) with
| Not_found -> None in
match pfs with
| None ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant ls term proj_name
| Some pfs ->
(* Collect declarations for projections f of the form
f = pf_n .. pf_1 where pf_1 is an element of pfs *)
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant ls term proj_name
else
let t_applied = Term.t_app pf_1 [term] pf_1.ls_value in
let proj_name = proj_name^(get_record_field_suffix pf_1) in
let applied_projs = Term.Sls.add pf_1 applied_projs in
(* Return declarations for projections of t_applied = pf_1 term *)
let t_applied_projs =
projections_for_term ls t_applied proj_name applied_projs env map_projs in
List.append l t_applied_projs
)
[]
pfs
let intro_proj_for_ls env map_projs ls_projected =
(* Returns list of declarations for projection of ls_projected
if it has a label "model_projected", otherwise returns [].
......@@ -88,141 +260,10 @@ let intro_proj_for_ls env map_projs ls_projected =
match ls_projected.ls_value with
| None -> []
| Some _ ->
let introduce_constant t_rhs proj_name =
(* introduce new constant c and axiom stating c = t_rhs *)
let const_label = Slab.add model_label ls_projected.ls_name.id_label in
let const_label = append_to_model_element_name ~labels:const_label ~to_append:proj_name in
let const_loc = Opt.get ls_projected.ls_name.id_loc in
let const_name = ls_projected.ls_name.id_string^"_proj_constant_"^proj_name in
let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom_"^proj_name in
let id_new = Ident.id_user ~label:const_label const_name const_loc in
intro_const_equal_to_term ~term:t_rhs ~id_new:id_new ~axiom_name in
let rec projections_for_term term proj_name applied_projs map_projs =
(* Return declarations for projections of the term.
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to the term *)
let get_record_field_suffix projection =
try
get_model_element_name ~labels:projection.ls_name.id_label
with Not_found -> "" in
match (Opt.get term.t_ty).ty_node with
| Tyapp (ts, [t_from; t_to]) when ts.ts_name.id_string = "map" -> begin
(* If the term is of map type, check whether t_to (and t_from - to be done later) can be projected.
If it is so, for each projection pf_1 from t_to to t_res introduce new map with the elemements
equal to projections of the source map:
const proj_map: map t_from t_res
axiom proj_axiom :
(forall i : t_from. proj_map[i] = pf_1(term[i]))
-> continue recursively with m2 as a term (see comments for non-map case)
Problem: this introduces too many new constants => TODO: do either:
(1)
val proj_map_func (term: map t_from t_to) : map t_from t_res
ensures { forall i: t_from. pf_1(term[i]) = result[i] }
-> apply proj_map_func to term and continue the same way as in the non-map case
or
(2)
NOT: this does not work
function proj_map_func (term : map t_from t_to) : map t_from t_res
=
let proj_map = ref (Const.const 0) in
problem, cannot do for cycle through all the map proj_map
*)
try
let pfs = Ty.Mty.find t_to map_projs in
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
(* Newly introduced map with projected indices *)
let proj_map_name = ls_projected.ls_name.id_string^"_proj_arr_constant"^proj_name in
let proj_map_id = Ident.id_fresh proj_map_name in
let proj_map_ty = Some (ty_app ts [t_from; Opt.get pf_1.ls_value]) in
let proj_map_ls = Term.create_lsymbol proj_map_id [] proj_map_ty in
let proj_map_decl = Decl.create_param_decl proj_map_ls in
let proj_map_t = Term.t_app proj_map_ls [] proj_map_ty in
(* The quantified variable i *)
let var_i : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh "x") t_from in
let i : Term.term = Term.t_var var_i in
let map_theory = Env.read_theory env ["map"] "Map" in
let select = (ns_find_ls map_theory.th_export ["get"]) in
(* Indices: proj_map[i], term[i] *)
let proj_map_idx_t = Term.t_app_infer select [proj_map_t;i] in
let term_idx_t = Term.t_app_infer select [term;i] in
(* Formula f: forall i : t_from. proj_map[i] = pf_1(term[i]) *)
let term_idx_projected_t = Term.t_app pf_1 [term_idx_t] pf_1.ls_value in
let fla_to_be_quant = Term.t_equ proj_map_idx_t term_idx_projected_t in
let fla_axiom = Term.t_forall_close [var_i] [] fla_to_be_quant in
(* Axiom about projection: axiom f*)
let proj_axiom_name = ls_projected.ls_name.id_string^"_proj_arr_axiom"^proj_name in
let proj_axiom_id = Decl.create_prsymbol (Ident.id_fresh proj_axiom_name) in
let proj_axiom = Decl.create_prop_decl Decl.Paxiom proj_axiom_id fla_axiom in
(* Recursively call projecting of the term proj_map -> proj_map_projections *)
let proj_name = proj_name^(get_record_field_suffix pf_1) in
let applied_projs = Term.Sls.add pf_1 applied_projs in
let proj_map_projections_defs = projections_for_term proj_map_t proj_name applied_projs map_projs in
List.append l (List.append [proj_map_decl;proj_axiom] proj_map_projections_defs)
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant term proj_name
end
| _ ->
(* Non-map case *)
try
(* Find all projection functions for the term *)
let pfs = Ty.Mty.find (Opt.get term.t_ty) map_projs in
(* Collect declarations for projections f of the form
f = pf_n .. pf_1 where pf_1 is an element of pfs *)
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
let t_applied = Term.t_app pf_1 [term] pf_1.ls_value in
let proj_name = proj_name^(get_record_field_suffix pf_1) in
let applied_projs = Term.Sls.add pf_1 applied_projs in
(* Return declarations for projections of t_applied = pf_1 term *)
let t_applied_projs = projections_for_term t_applied proj_name applied_projs map_projs in
List.append l t_applied_projs
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant term proj_name
in
(* Create term from ls_projected *)
let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
projections_for_term t_projected "" Term.Sls.empty map_projs
projections_for_term ls_projected t_projected "" Term.Sls.empty env map_projs
let introduce_projs env map_projs decl =
match decl.d_node with
......
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