Commit baac0c6b authored by David Hauzar's avatar David Hauzar

Projections of indices of maps.

The transformation intro_projections_counterexmp now can project maps
with indices of types that should be projected (to type "t_to")
to maps with indices that are projections of indices of original maps
(they are of the type "t_to").
parent 113b783b
......@@ -35,7 +35,7 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
......
......@@ -12,13 +12,15 @@
open Ident
open Term
open Decl
open Theory
open Ty
(*
(* Debugging functions *)
let debug = Debug.register_info_flag "intro_projections_counterexmp"
~desc:"Print@ debugging@ messages@ about@ introducing@ projections@ for@ counterexamples."
let rec debug_print_terms terms =
vlet rec debug_print_terms terms =
match terms with
| [] -> ()
| term::tail ->
......@@ -65,7 +67,7 @@ let intro_const_equal_to_term
(* Return the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
let intro_proj_for_ls map_projs ls_projected =
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 [].
......@@ -101,36 +103,124 @@ let intro_proj_for_ls map_projs ls_projected =
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 term*)
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 pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name 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
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
(* 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
*)
introduce_constant term proj_name
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 pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name 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 pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name 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
......@@ -139,11 +229,11 @@ let intro_proj_for_ls map_projs ls_projected =
projections_for_term t_projected "" Term.Sls.empty map_projs
let introduce_projs map_projs decl =
let introduce_projs env map_projs decl =
match decl.d_node with
| Dparam ls_projected ->
(* Create declarations for a projections of ls_projected *)
let projection_decls = intro_proj_for_ls map_projs ls_projected in
let projection_decls = intro_proj_for_ls env map_projs ls_projected in
decl::projection_decls
(* TODO
......@@ -175,15 +265,15 @@ let build_projections_map projs =
in
Sls.fold build_map projs Ty.Mty.empty
let meta_transform2 projs =
let meta_transform2 env projs =
let map_projs = build_projections_map projs in
Trans.decl (introduce_projs map_projs) None
Trans.decl (introduce_projs env map_projs) None
let intro_projections_counterexmp =
Trans.on_tagged_ls meta_projection meta_transform2
let intro_projections_counterexmp env =
Trans.on_tagged_ls meta_projection (meta_transform2 env)
let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
let () = Trans.register_env_transform "intro_projections_counterexmp" intro_projections_counterexmp
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ with@ label@ model_projected@ \
and@ projectin@ f@ for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom@ \
c = f p."
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
val intro_projections_counterexmp : Task.task Trans.trans
val intro_projections_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that for each declared abstract function or predicate
p labeled with label "model_projected" creates a declaration of new
......
......@@ -11,7 +11,7 @@ let get_counterexmp task =
let ce_meta = Task.find_meta_tds task meta_get_counterexmp in
not (Theory.Stdecl.is_empty ce_meta.tds_set)
let prepare_for_counterexmp2 task =
let prepare_for_counterexmp2 env task =
if not (get_counterexmp task) then begin
(* Counter-example will not be queried, do nothing *)
Debug.dprintf debug "Not get ce@.";
......@@ -24,15 +24,15 @@ let prepare_for_counterexmp2 task =
(Trans.goal Introduction.intros)
(Trans.compose
Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp
Intro_projections_counterexmp.intro_projections_counterexmp
(Intro_projections_counterexmp.intro_projections_counterexmp env)
)
in
(Trans.apply comp_trans) task
end
let prepare_for_counterexmp = Trans.store prepare_for_counterexmp2
let prepare_for_counterexmp env = Trans.store (prepare_for_counterexmp2 env)
let () = Trans.register_transform "prepare_for_counterexmp" prepare_for_counterexmp
let () = Trans.register_env_transform "prepare_for_counterexmp" prepare_for_counterexmp
~desc:"Transformation@ that@ prepares@ the@ task@ for@ quering@ for@ \
the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \
when@ the@ solver@ will@ be@ asked@ for@ the@ counter-example."
......
......@@ -14,9 +14,9 @@ val get_counterexmp : Task.task -> bool
Returns true if counter-example should be get for the task.
*)
val prepare_for_counterexmp : Task.task Trans.trans
val prepare_for_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that prepares the task for quering for
Transformation that prepares the task for quering for
the counter-example model.
This transformation does so only when the solver will be asked
for the counter-example.
......
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