Commit b9e80472 authored by MARCHE Claude's avatar MARCHE Claude

Fix issue #263

parent dc8d92b8
......@@ -88,17 +88,17 @@ Line 37:
x23, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "399" } }] } }
"val" : "1768" } }] } }
Line 38:
x23, [[@introduced], [@field:0:contents],
[@model_trace:x23]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "401" } }] } }
"val" : "1770" } }] } }
x23 at 'Old, [[@introduced], [@field:0:contents],
[@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "399" } }] } }
"val" : "1768" } }] } }
y at 'Old, [[@introduced], [@field:0:contents],
[@at:'Old], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Record" ,
......@@ -111,11 +111,11 @@ y, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 42:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "400" } }] } }
"val" : "1769" } }] } }
Line 43:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "401" } }] } }
"val" : "1770" } }] } }
bench/ce/ref_mono.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref_mono.mlw:
......@@ -166,59 +166,59 @@ Counter-example model:File ref_mono.mlw:
Line 9:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6083" } }] } }
"val" : "7100" } }] } }
Line 11:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
Line 35:
y, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18248" } }] } }
"val" : "21299" } }] } }
Line 38:
x at 'Old, [[@introduced], [@field:0:contents], [@at:'Old],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
x, [[@introduced], [@field:0:contents],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
Line 45:
x, [[@introduced], [@field:0:contents], [@at:'Old],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
Line 49:
x, [[@introduced], [@field:0:contents],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
Line 51:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6083" } }] } }
"val" : "7100" } }] } }
Line 52:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
x at M, [[@introduced], [@field:0:contents],
[@at:M], [@model_trace:x],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
Line 54:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
bench/ce/ref_mono.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref_mono.mlw:
......
......@@ -88,17 +88,17 @@ Line 37:
x23, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "399" } }] } }
"val" : "1768" } }] } }
Line 38:
x23, [[@introduced], [@field:0:contents],
[@model_trace:x23]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "401" } }] } }
"val" : "1770" } }] } }
x23 at 'Old, [[@introduced], [@field:0:contents],
[@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "399" } }] } }
"val" : "1768" } }] } }
y at 'Old, [[@introduced], [@field:0:contents],
[@at:'Old], [@model_trace:y],
[@at:'Old:loc:location] = {"type" : "Record" ,
......@@ -111,11 +111,11 @@ y, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
Line 42:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "400" } }] } }
"val" : "1769" } }] } }
Line 43:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "401" } }] } }
"val" : "1770" } }] } }
bench/ce/ref_mono.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref_mono.mlw:
......@@ -166,59 +166,59 @@ Counter-example model:File ref_mono.mlw:
Line 9:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6083" } }] } }
"val" : "7100" } }] } }
Line 11:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
Line 35:
y, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "18248" } }] } }
"val" : "21299" } }] } }
Line 38:
x at 'Old, [[@introduced], [@field:0:contents], [@at:'Old],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
x, [[@introduced], [@field:0:contents],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
Line 45:
x, [[@introduced], [@field:0:contents], [@at:'Old],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
Line 49:
x, [[@introduced], [@field:0:contents],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
Line 51:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6083" } }] } }
"val" : "7100" } }] } }
Line 52:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
[@at:L:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "-6084" } }] } }
"val" : "-7101" } }] } }
x at M, [[@introduced], [@field:0:contents],
[@at:M], [@model_trace:x],
[@at:M:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "12166" } }] } }
"val" : "14200" } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
Line 54:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "6082" } }] } }
"val" : "7099" } }] } }
bench/ce/ref_mono.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File ref_mono.mlw:
......
......@@ -14,6 +14,8 @@ a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
Line 12:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -14,6 +14,8 @@ a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
Line 12:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -14,6 +14,8 @@ a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
Line 12:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -14,6 +14,8 @@ a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "4" }
Line 12:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -470,7 +470,7 @@ let print_task args ?old:_ fmt task =
let inv_trig = Task.on_tagged_ls meta_invalid_trigger task in
let show,cast = Task.on_meta meta_printer_option
check_options (false,true) task in
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let cntexample = Inlining.get_counterexmp task in
let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
let vc_info = {vc_inside = false; vc_loc = None; vc_func_name = None} in
let info = {
......
......@@ -697,7 +697,7 @@ let meta_incremental =
~desc:"Internal@ use@ only"
let print_task version args ?old:_ fmt task =
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let cntexample = Inlining.get_counterexmp task in
let incremental =
let incr_meta = Task.find_meta_tds task meta_incremental in
not (Theory.Stdecl.is_empty incr_meta.Task.tds_set)
......
......@@ -440,7 +440,7 @@ let t_shape_task ~version ~expl t =
| SV4 ->
let open Decl in
let introduced id = Ident.Sattr.mem
Introduction.intro_attr
Inlining.intro_attr
id.Ident.id_attrs in
let do_td td = match td.Theory.td_node with
| Theory.Decl d ->
......
......@@ -15,6 +15,17 @@ open Decl
open Theory
open Task
let intro_attr = Ident.create_attribute "introduced"
let meta_get_counterexmp =
Theory.register_meta_excl "get_counterexmp" [Theory.MTstring]
~desc:"Set@ when@ counter-example@ should@ be@ get."
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 rec relocate loc t =
t_map (relocate loc) (t_attr_set ?loc t.t_attrs t)
......@@ -86,20 +97,24 @@ let meta = Theory.register_meta "inline:no" [Theory.MTlsymbol]
~desc:"Disallow@ the@ inlining@ of@ the@ given@ function/predicate@ symbol."
let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls =
let trans notls =
Trans.fold_map (fold in_goal notdeft notdeff notls) Mls.empty None in
if use_meta then
Trans.on_tagged_ls meta (fun sls ->
let notls ls = Sls.mem ls sls || notls ls in
trans notls)
else
trans notls
let all = t ~use_meta:true ~in_goal:false
~notdeft:Util.ffalse ~notdeff:Util.ffalse ~notls:Util.ffalse
let goal = t ~use_meta:true ~in_goal:true
~notdeft:Util.ffalse ~notdeff:Util.ffalse ~notls:Util.ffalse
Trans.bind (Trans.store get_counterexmp)
(fun for_counterexample ->
let trans notls =
Trans.fold_map (fold in_goal notdeft notdeff notls) Mls.empty None in
if use_meta then
Trans.on_tagged_ls meta (fun sls ->
let notls ls = Sls.mem ls sls || notls ~for_counterexample ls in
trans notls)
else
trans (notls ~for_counterexample))
let all =
t ~use_meta:true ~in_goal:false ~notdeft:Util.ffalse ~notdeff:Util.ffalse
~notls:(fun ~for_counterexample:_ _ -> false)
let goal =
t ~use_meta:true ~in_goal:true ~notdeft:Util.ffalse ~notdeff:Util.ffalse
~notls:(fun ~for_counterexample:_ _ -> false)
(* inline_trivial *)
......@@ -120,8 +135,14 @@ let notdeft t = match t.t_node with
| Tapp (_,tl) -> not (trivial tl)
| _ -> true
let trivial = t ~use_meta:true ~in_goal:false
~notdeft:notdeft ~notdeff:notdeft ~notls:Util.ffalse
let trivial =
let notls ~for_counterexample ls =
(* do not inline things like `let result = ... in ...`
when counterexamples are wanted. These are recognized
as having the attribute `introduced` *)
for_counterexample && ls.ls_args = [] &&
Ident.(Sattr.mem intro_attr ls.ls_name.id_attrs) in
t ~use_meta:true ~in_goal:false ~notdeft:notdeft ~notdeff:notdeft ~notls
let () =
Trans.register_transform "inline_all" all
......
......@@ -11,8 +11,16 @@
(** Inline non-recursive definitions *)
val intro_attr : Ident.attribute
val meta : Theory.meta
val get_counterexmp : Task.task -> bool
(**
Returns true if counterexample should be get for the task.
*)
(** {2 Generic inlining} *)
val t :
......@@ -20,7 +28,7 @@ val t :
?in_goal:bool ->
notdeft:(Term.term -> bool) ->
notdeff:(Term.term -> bool) ->
notls :(Term.lsymbol -> bool) ->
notls :(for_counterexample:bool -> Term.lsymbol -> bool) ->
Task.task Trans.trans
(** [t ~use_meta ~in_goal ~notdeft ~notdeff ~notls] returns a transformation
......
......@@ -84,14 +84,13 @@ let rec dequant pos f = t_attr_copy f (match f.t_node with
and dequant_if_case pos f = if case f then dequant pos f else f
let intro_attr = Ident.create_attribute "introduced"
let intro_attrs = Sattr.singleton intro_attr
let intro_attrs = Sattr.singleton Inlining.intro_attr
let compat ls vs =
ls.ls_args = [] &&
Opt.equal ty_equal ls.ls_value (Some vs.vs_ty) &&
Opt.equal Loc.equal ls.ls_name.id_loc vs.vs_name.id_loc &&
Sattr.equal ls.ls_name.id_attrs (Sattr.add intro_attr vs.vs_name.id_attrs)
Sattr.equal ls.ls_name.id_attrs (Sattr.add Inlining.intro_attr vs.vs_name.id_attrs)
let ls_of_vs mal vs = match mal with
| Theory.MAls ls :: mal when compat ls vs -> ls, mal
......@@ -121,7 +120,7 @@ let rec intros kn pr mal expl f =
(* f is going to be removed, preserve its attributes and location in f2 *)
let f2 = t_attr_copy f f2 in
let fl = Split_goal.split_intro_right ?known_map:kn (dequant false f1) in
let idx = id_fresh "H" ~attrs:(Sattr.singleton intro_attr) in
let idx = id_fresh "H" ~attrs:intro_attrs in
let add (subst,dl) f =
let svs = Mvs.set_diff (t_freevars Mvs.empty f) subst in
let subst, dl = Mvs.fold (fun vs _ (subst,dl) ->
......@@ -206,7 +205,7 @@ let rec generalize hd =
if pl = [] then [], Some hd else
let expl = get_expls f in
let get_vs {ls_name = id; ls_value = oty} =
let attrs = Sattr.remove intro_attr id.id_attrs in
let attrs = Sattr.remove Inlining.intro_attr id.id_attrs in
let id = id_fresh ~attrs ?loc:id.id_loc id.id_string in
create_vsymbol id (Opt.get oty) in
let set_vs vs ls f =
......@@ -233,11 +232,11 @@ let rec generalize hd =
| Theory.Decl ({d_node =
( Dparam ({ls_args = []; ls_value = Some _} as ls)
| Dlogic [{ls_args = []; ls_value = Some _} as ls, _])} as d)
when Sattr.mem intro_attr ls.ls_name.id_attrs ->
when Sattr.mem Inlining.intro_attr ls.ls_name.id_attrs ->
let pl, task = apply_prev generalize hd in
d::pl, Task.add_meta task meta_intro_ls [Theory.MAls ls]
| Theory.Decl ({d_node = Dprop (Paxiom, pr, _)} as d)
when Sattr.mem intro_attr pr.pr_name.id_attrs ->
when Sattr.mem Inlining.intro_attr pr.pr_name.id_attrs ->
let pl, task = apply_prev generalize hd in
d::pl, Task.add_meta task meta_intro_pr [Theory.MApr pr]
(* We only reattach the local premises right before the goal.
......@@ -264,7 +263,7 @@ let rec eliminate_exists_aux pr t =
| Tquant (Texists, q) ->
let vsl, _, t' = t_open_quant q in
let intro_var subst vs =
let id = id_clone ~attrs:(Sattr.singleton intro_attr) vs.vs_name in
let id = id_clone ~attrs:intro_attrs vs.vs_name in
let ls =
create_lsymbol id [] (Some vs.vs_ty)
in
......@@ -288,7 +287,7 @@ let () = Trans.register_transform
~desc:"Replace axioms of the form 'exists x. P' by 'constant x axiom P'."
let subst_filter ls =
Sattr.mem intro_attr ls.ls_name.id_attrs &&
Sattr.mem Inlining.intro_attr ls.ls_name.id_attrs &&
not (relevant_for_counterexample ls.ls_name)
let simplify_intros =
......
......@@ -27,8 +27,6 @@
*)
val intro_attr : Ident.attribute
val intros :
?known_map:Decl.known_map -> Decl.prsymbol -> Term.term -> Decl.decl list
(** [intros ?known_map G f] returns the declarations after introducing
......
......@@ -9,22 +9,12 @@
(* *)
(********************************************************************)
open Task
let debug = Debug.register_info_flag "prepare_for_counterexmp"
~desc:"Print@ debugging@ messages@ about@ preparing@ the@ task@ \
for@ getting@ counter-example."
let meta_get_counterexmp =
Theory.register_meta_excl "get_counterexmp" [Theory.MTstring]
~desc:"Set@ when@ counter-example@ should@ be@ get."
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 env task =
if not (get_counterexmp task) then begin
if not (Inlining.get_counterexmp task) then begin
(* Counter-example will not be queried, do nothing *)
Debug.dprintf debug "Not get ce@.";
task
......
......@@ -9,11 +9,6 @@
(* *)
(********************************************************************)
val get_counterexmp : Task.task -> bool
(**
Returns true if counter-example should be get for the task.
*)
val prepare_for_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that prepares the task for querying for
......
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