Commit 24a6ca4b authored by Sylvain Dailler's avatar Sylvain Dailler

Simplification in counterexample transformations

parent 8c2dc271
......@@ -61,7 +61,7 @@ let add_old attr_str =
else attr_str
with Not_found -> attr_str ^ "@old"
let model_trace_for_postcondition ~attrs =
let model_trace_for_postcondition ~attrs trace_attr =
(* Modifies the model_trace attribute of a term in the postcondition:
- if term corresponds to the initial value of a function
parameter, model_trace attribute will have postfix @old
......@@ -69,18 +69,14 @@ let model_trace_for_postcondition ~attrs =
Returns attrs with model_trace attribute modified if there
exist model_trace attribute in attrs, attrs otherwise.
*)
match get_model_trace_attr ~attrs with
| trace_attr ->
let attr_str = add_old trace_attr.attr_string in
if attr_str = trace_attr.attr_string then
attrs
else
let other_attrs = Sattr.remove trace_attr attrs in
Sattr.add
(Ident.create_attribute attr_str)
other_attrs
| exception Not_found ->
attrs
let attr_str = add_old trace_attr.attr_string in
if attr_str = trace_attr.attr_string then
attrs
else
let other_attrs = Sattr.remove trace_attr attrs in
Sattr.add
(Ident.create_attribute attr_str)
other_attrs
(* Preid table necessary to avoid duplication of *_vc_constant *)
module Hprid = Exthtbl.Make (struct
......@@ -89,7 +85,6 @@ module Hprid = Exthtbl.Make (struct
let hash p = Exthtbl.hash p
end)
(* Used to generate duplicate vc_constant and axioms for counterex generation.
This function is always called when the term is in negative position or
under a positive term that is not introducible. This means it never change the
......@@ -117,22 +112,25 @@ let rec do_intro info vc_loc vc_map vc_var t =
should be in counterexample, introduce new constant in location
loc with all attributes necessary for collecting it for
counterexample and make it equal to the variable *)
if Ident.has_a_model_attr ls then
let const_attr = if info.vc_pre_or_post then
model_trace_for_postcondition ~attrs:ls.id_attrs
else
ls.id_attrs in
let const_name = ls.id_string^"_vc_constant" in
let axiom_name = ls.id_string^"_vc_axiom" in
(* Create a new id here to check the couple name, location. *)
let id_new = Ident.id_user ~attrs:const_attr const_name loc in
(* The following check is used to avoid duplication of
*_vc_constant_n. We keep track of the preids that have already
been duplicated in vc_map. Note that we need to do it before
these preid are casted to lsymbol (by Term.create_lsymbol)
because those integrates a unique hash that would make identical
preid different lsymbol *)
if (Hprid.mem vc_map id_new) then
begin match Ident.get_model_trace_attr ~attrs:ls.id_attrs with
| tr_attr ->
let const_attr =
if info.vc_pre_or_post then
model_trace_for_postcondition ~attrs:ls.id_attrs tr_attr
else
ls.id_attrs
in
let const_name = ls.id_string^"_vc_constant" in
let axiom_name = ls.id_string^"_vc_axiom" in
(* Create a new id here to check the couple name, location. *)
let id_new = Ident.id_user ~attrs:const_attr const_name loc in
(* The following check is used to avoid duplication of
*_vc_constant_n. We keep track of the preids that have already
been duplicated in vc_map. Note that we need to do it before
these preid are casted to lsymbol (by Term.create_lsymbol)
because those integrates a unique hash that would make
identical preid different lsymbol *)
if (Hprid.mem vc_map id_new) then
[]
else
begin
......@@ -140,8 +138,8 @@ let rec do_intro info vc_loc vc_map vc_var t =
intro_const_equal_to_term
~term:t ~id_new:id_new ~axiom_name
end
else
[]
| exception Not_found -> []
end
end
else [] in
match t.t_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