Commit 4b9104a7 authored by David Hauzar's avatar David Hauzar

Introducing new constant for all terms labeled by "model_projected".

Transformation intro_projections_counterexmp introduce new constant c
and axiom for all abstract functions and predicates p labeled with
label "model_projected", not only for these for that there exists
projection function. If the projection function does not exist,
the axiom states c = p, if there exists projection function f,
the axiom states c = f p.
parent d7a1a860
......@@ -13,7 +13,7 @@ open Ident
open Term
open Decl
(*
(*
(* Debugging functions *)
let debug = Debug.register_info_flag "intro_projections_counterexmp"
~desc:"Print@ debugging@ messages@ about@ introducing@ projections@ for@ counterexamples."
......@@ -22,7 +22,7 @@ let rec debug_print_terms terms =
match terms with
| [] -> ()
| term::tail ->
Pretty.print_term Format.str_formatter term;
debug_print_terms tail
......@@ -41,7 +41,7 @@ let label_model_proj = Ident.create_label "model_projected"
let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
~desc:"Declares@ the@ projection."
let intro_proj_for_ls map_projs ls_projected =
let intro_proj_for_ls map_projs ls_projected =
(* Returns list of declarations for projection of ls_projected
if it has a label "model_projected", otherwise returns [].
......@@ -53,52 +53,62 @@ let intro_proj_for_ls map_projs ls_projected =
The projection function for ls_declared is stored in map_projs
with key ls_projected.ls_value
@param map_projs maps types to projection function for these types
@param ls_projected the label symbol that should be projected
*)
if not (Slab.mem label_model_proj ls_projected.ls_name.id_label) then
(* ls_projected has not a label "model_projected" *)
[]
else
match ls_projected.ls_value with
| None -> []
| Some ty_projected ->
let create_proj_decls ls_projection =
(* Creates declarations for projection of ls_projected using
projection function ls_projection. *)
let create_proj_decls t_rhs =
(* Creates projection declarations. That is:
- declaration for new constant t_new_constant
- declaration for axiom stating that t_new_constant = t_rhs. *)
(* Create the projection *)
let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
let t_projection = Term.t_app ls_projection [t_projected] ls_projection.ls_value in
(* Create declaration of new constant *)
let name_new_constant = ls_projected.ls_name.id_string^"_proj_constant" in
let lab_new = Slab.add label_model Slab.empty in
let id_new = Ident.id_derive ~label:lab_new name_new_constant ls_projected.ls_name in
let ls_new_constant = Term.create_lsymbol id_new [] ls_projection.ls_value in
let ls_new_constant = Term.create_lsymbol id_new [] t_rhs.t_ty in
let decl_new_constant = Decl.create_param_decl ls_new_constant in
let t_new_constant = Term.t_app ls_new_constant [] ls_projection.ls_value in
(* Create the declaration of the axiom about the constant: t_new_constant = t_projection *)
let t_new_constant = Term.t_app ls_new_constant [] t_rhs.t_ty in
(* Create the declaration of the axiom about the constant: t_new_constant = t_rhs *)
let name_axiom = ls_projected.ls_name.id_string^"_proj_axiom" in
let id_axiom = Decl.create_prsymbol (Ident.id_fresh name_axiom) in
let fla_axiom = Term.t_equ t_new_constant t_projection in
let fla_axiom = Term.t_equ t_new_constant t_rhs in
let decl_axiom = Decl.create_prop_decl Decl.Paxiom id_axiom fla_axiom in
(* Add the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
in
try
let ls_proj = Ty.Mty.find ty_projected map_projs in
create_proj_decls ls_proj
with Not_found -> []
(* t_rhs is a term corresponding to
- ls_projected (the label symbol being projected) - if there is no
projection function for its type
- application of projection function f to ls_projected *)
let t_rhs =
let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
try
let f = Ty.Mty.find ty_projected map_projs in
Term.t_app f [t_projected] f.ls_value
with Not_found -> t_projected in
create_proj_decls t_rhs
let introduce_projs map_projs decl =
match decl.d_node with
| Dparam ls_projected ->
| Dparam ls_projected ->
(* Create declarations for a projection of ls_projected *)
let projection_decls = intro_proj_for_ls map_projs ls_projected in
decl::projection_decls
(* TODO
| Dlogic lslist ->
| Dlogic lslist ->
debug_decl decl;
let new_decls = List.fold_left (fun list (ls,_) -> list @ (intro_proj_for_ls map_projs ls)) [] lslist in
(* TODO *)
......@@ -110,28 +120,28 @@ let introduce_projs map_projs decl =
let build_projections_map projs =
(* Build map from types (Ty.ty) to projections (Term.lsymbol).
The type t maps to the projection function f if f has a single
argument of the type t.
argument of the type t.
*)
let build_map ls_proj proj_map =
match ls_proj.ls_args with
| [ty_proj_arg] ->
Ty.Mty.add ty_proj_arg ls_proj proj_map
Ty.Mty.add ty_proj_arg ls_proj proj_map
| _ -> assert false
in
Sls.fold build_map projs Ty.Mty.empty
let meta_transform2 projs =
let meta_transform2 projs =
let map_projs = build_projections_map projs in
Trans.decl (introduce_projs map_projs) None
let intro_projections_counterexmp =
let intro_projections_counterexmp =
Trans.on_tagged_ls meta_projection meta_transform2
let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ labeled@ with@ label@ \
model_projected@ for@ that@ it@ exists@ a@ projection@ function@ f@ creates@ declaration@ of@ \
new@ constant@ c@ and@ axiom@ stating@ that c = f p"
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ with@ label@ model_projected@ \
creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom;@ if@ there@ exists@ \
projection@ function@ f@ for@ p,@ the@ axiom@ is@ c = f p,@ otherwise@ it@ is@ c = p."
(*
Local Variables:
......
......@@ -11,26 +11,28 @@
val intro_projections_counterexmp : Task.task Trans.trans
(**
Transformation that for each declared abstract function and predicate
p labeled with label "model_projected" for that it exists a projection
function f creates declaration of new constant c and axiom stating that
c = f p
Transformation that for each declared abstract function or predicate
p labeled with label "model_projected" creates a declaration of new
constant c labeled with label "model" and declaration of new axiom.
If there exists a projection function f for p, the axiom states that
c = f p, otherwise it states that c = p.
Projection functions are functions tagged with meta "model_projection".
Function f is projection function for abstract function and predicate p
Projection functions are functions tagged with metas "model_projection"
and "inline : no" (the latter is needed just to prevent inlinng of this
function).
Function f is projection function for abstract function or predicate p
if f is tagged with meta "model_projection" and has a single argument
of the same type as is the type of p.
This transformation is needed in situations when we want to display not
value of a variable, but value of a projection function applied to a variable.
This is needed, e.g., in cases when the type of a variable is abstract.
Note that since Why3 supports namespaces (different projection functions
can have the same name) and input languages of solvers typically not,
Why3 renames projection functions to avoid name clashes.
This is why it is not possible to just store the name of the projection
function in a label and than query the solver directly for the value of
the projection.
Also, it means that this transformation should thus be executed before
this renaming.
Also, it means that this transformation must be executed before this renaming.
*)
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