diff --git a/dune-project b/dune-project
index 48fa80dcef22b2e18c0772b6653cb27cd8fe0df3..ee105403ac7fb6420d212d0f640a8c3659652002 100644
--- a/dune-project
+++ b/dune-project
@@ -7,7 +7,7 @@
(using menhir 2.0)
(generate_opam_files true)
-(license LGPL)
+(license LGPL-2.0-or-later)
(authors "Pierre-Loic Garoche <ploc@garoche.net>"
"Xavier Thirioux <thirioux@enseeiht.fr>")
(maintainers "Pierre-Loic Garoche <ploc@garoche.net>"
diff --git a/lustrec.opam b/lustrec.opam
index c6305e6fd95ded6943fa7cb99cb17a9726eca931..a08dfd63d4a6ef511f00aab4da21fedbdd3f6d12 100644
--- a/lustrec.opam
+++ b/lustrec.opam
@@ -12,7 +12,7 @@ authors: [
"Pierre-Loic Garoche <ploc@garoche.net>"
"Xavier Thirioux <thirioux@enseeiht.fr>"
]
-license: "LGPL"
+license: "LGPL-2.0-or-later"
homepage: "https://gitlab.isae-supaero.fr/lustrec/lustrec"
bug-reports: "https://gitlab.isae-supaero.fr/lustrec/lustrec/-/issues"
depends: [
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index d7f96b3e3f625aa80782c9432e5d74ccb9a983db..d02de9f4916ff54cdb77b14cebb7836d8f1da207 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -447,7 +447,7 @@ module PrintSpec = struct
fmt
(f, mem_in', mem_out, mem_in))
| GhostAssign (v1, v2) ->
- pp_ghost (pp_assign m mem_in (pp_c_var_read m)) fmt (v1, vdecl_to_val v2)
+ pp_ghost (pp_assign m mem_in (pp_c_var_read m)) fmt (v1, v2)
let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index b6cc3e8cff6aa7c9250c5cbbf01028f5515900a3..4da14354099a1c63d6612a08e4a7aee65496d7c3 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -88,8 +88,8 @@ module PrintSpec = struct
inst
(pp_print_option pp_print_int)
i
- | GhostAssign (v1, v2) ->
- fprintf fmt "Ghost %s = %s" v1.var_id v2.var_id
+ | GhostAssign (v, e) ->
+ fprintf fmt "Ghost %s = %a" v.var_id (pp_val m) e
let pp_spec m =
let pp_expr fmt e = pp_expr m fmt e in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 93e430cd407d2d52b732966f710d800b9c3a3a47..d0adaa3677959c5a17cbce9f886e06c7e059d598 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -142,15 +142,8 @@ let rec eliminate_formula m elim =
| f ->
f
-let eliminate_spec m elim =
- List.map (fun (f, asrt) -> eliminate_formula m elim f, asrt)
-
-let eliminate_spec_instr m elim instr =
- { instr with instr_spec = eliminate_spec m elim instr.instr_spec }
-
let rec eliminate m elim instr =
let e_val = eliminate_val m elim in
- let instr = eliminate_spec_instr m elim instr in
match get_instr_desc instr with
| MLocalAssign (i, v) ->
update_instr_desc instr (MLocalAssign (i, e_val v))
@@ -411,6 +404,13 @@ let merge_elim elim1 elim2 =
let get_exprs elim = IMap.map (fun (_, e, _) -> e) elim
+let add_ghost_assign_spec i v spec =
+ (Predicate (GhostAssign (i, v)), false) :: spec
+
+let assign_comment m v e =
+ Format.(fprintf str_formatter "%s := %a" v.var_id (pp_val m) e);
+ MComment (Format.flush_str_formatter ())
+
(* see if elim has to take in account the provided instr: if so, update elim and
return the remove flag, otherwise, the expression should be kept and elim is
left untouched *)
@@ -472,9 +472,9 @@ let instrs_unfold m fanin elim instrs =
IMap.mem v.var_id elim ->
(* we transform the assignment into a comment in order to keep its
spec *)
- Format.(fprintf str_formatter "%s := %a" v.var_id (pp_val m) e);
- let instr = eliminate_spec_instr m elim_exprs instr in
- update_instr_desc instr (MComment (Format.flush_str_formatter ()))
+ { instr with
+ instr_spec = add_ghost_assign_spec v e instr.instr_spec;
+ instr_desc = assign_comment m v e }
| MBranch (g, hl) ->
let instr =
update_instr_desc
@@ -829,165 +829,166 @@ let predicate_spec_replace fvar = function
| p ->
p
-let is_reused_reassigned m fvar asg v =
- let r_asg = IMap.filter (fun _ n -> n > 1) asg in
- List.exists (fun v' -> v.var_id = v'.var_id) m.mstep.step_locals
- && List.exists (fun v' -> fvar v' = v && v <> v') m.mstep.step_locals
- && IMap.mem v.var_id r_asg
-
-let ghost_vd v = { v with var_id = "__" ^ v.var_id }
-
-let rec instr_spec_replace m fvar asg t =
- let aux instr = instr_spec_replace m fvar asg instr in
- (* rename reused vars that appears freely in the formula before
- substitution, *)
- (* to handle the fact that those vars can be modified in a way that the
- formula does not hold anymore *)
- let fv_m =
- VSet.fold
- (fun v fv_m ->
- if is_reused_reassigned m fvar asg v then
- IMap.add v.var_id (ghost_vd v) fv_m
- else fv_m)
- (fv_formula m VSet.empty t)
- IMap.empty
- in
- let fvar v = try IMap.find v.var_id fv_m with Not_found -> fvar v in
- let t' =
- match t with
- | Equal (e1, e2) ->
- Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
- | GEqual (e1, e2) ->
- GEqual (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
- | And f ->
- And (List.map aux f)
- | Or f ->
- Or (List.map aux f)
- | Imply (a, b) ->
- Imply (aux a, aux b)
- | Exists (xs, a) ->
- let fvar v = if List.mem v xs then v else fvar v in
- Exists (xs, instr_spec_replace m fvar asg a)
- | Forall (xs, a) ->
- let fvar v = if List.mem v xs then v else fvar v in
- Forall (xs, instr_spec_replace m fvar asg a)
- | Ternary (e, a, b) ->
- Ternary (expr_spec_replace fvar e, aux a, aux b)
- | Predicate p ->
- Predicate (predicate_spec_replace fvar p)
- | ExistsMem (f, a, b) ->
- ExistsMem (f, aux a, aux b)
- | f ->
- f
- in
- (* let fv_t = VSet.of_list (IMap.bindings fv_m |> List.split |> snd) in *)
- (* let fv = VSet.(elements (inter fv_t (fv_formula m empty t'))) in *)
- (* Exists (fv, t') *)
- t'
-
-let add_assigned v =
- IMap.update v.var_id (function Some n -> Some (n + 1) | None -> Some 1)
-
-let silly_asg i v =
- match v.value_desc with Var w -> w.var_id = i.var_id | _ -> false
+let rec instr_spec_replace fvar t =
+ let aux t = instr_spec_replace fvar t in
+ match t with
+ | Equal (e1, e2) ->
+ Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
+ | GEqual (e1, e2) ->
+ GEqual (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
+ | And f ->
+ And (List.map aux f)
+ | Or f ->
+ Or (List.map aux f)
+ | Imply (a, b) ->
+ Imply (aux a, aux b)
+ | Exists (xs, a) ->
+ let fvar v = if List.mem v xs then v else fvar v in
+ Exists (xs, instr_spec_replace fvar a)
+ | Forall (xs, a) ->
+ let fvar v = if List.mem v xs then v else fvar v in
+ Forall (xs, instr_spec_replace fvar a)
+ | Ternary (e, a, b) ->
+ Ternary (expr_spec_replace fvar e, aux a, aux b)
+ | Predicate p ->
+ Predicate (predicate_spec_replace fvar p)
+ | ExistsMem (f, a, b) ->
+ ExistsMem (f, aux a, aux b)
+ | f ->
+ f
-let rec instr_replace_var m fvar (asg, instrs) instr =
- let asg, instr_desc =
+let rec instr_replace_var m fvar instrs instr =
+ let instr_desc =
match instr.instr_desc with
| MLocalAssign (i, v) ->
let v = value_replace_var fvar v in
let i = fvar i in
- (if silly_asg i v then asg else add_assigned i asg), MLocalAssign (i, v)
+ MLocalAssign (i, v)
| MStateAssign (i, v) ->
- asg, MStateAssign (i, value_replace_var fvar v)
+ MStateAssign (i, value_replace_var fvar v)
| MStep (il, i, vl) ->
let il = List.map fvar il in
- ( List.fold_right add_assigned il asg,
- MStep (il, i, List.map (value_replace_var fvar) vl) )
+ MStep (il, i, List.map (value_replace_var fvar) vl)
| MBranch (g, hl) ->
- let asg, hl =
+ let hl =
List.fold_left
- (fun (asg', hl) (h, il) ->
- let asg'', il = instrs_replace_var m fvar asg il in
+ (fun hl (h, il) ->
+ let il = instrs_replace_var m fvar il in
(* Format.(printf "%s: before %a after %a@." h (IMap.pp
pp_print_int) asg (IMap.pp pp_print_int) asg''); *)
- ( IMap.union (fun _ n1 n2 -> Some (max n1 n2)) asg' asg'',
- (h, il) :: hl ))
- (IMap.empty, [])
+ (h, il) :: hl )
+ []
hl
in
(* Format.(printf "%a@." (IMap.pp pp_print_int) asg); *)
- asg, MBranch (value_replace_var fvar g, List.rev hl)
+ MBranch (value_replace_var fvar g, List.rev hl)
| MSetReset _
| MNoReset _
| MClearReset
| MResetAssign _
| MSpec _
| MComment _ ->
- asg, instr.instr_desc
+ instr.instr_desc
in
- let instr_spec =
- List.map
- (fun (f, asrt) -> instr_spec_replace m fvar asg f, asrt)
- instr.instr_spec
+ instr_cons { instr with instr_desc } instrs
+
+and instrs_replace_var m fvar instrs =
+ let instrs =
+ List.fold_left (instr_replace_var m fvar) [] instrs
+ in
+ List.rev instrs
+
+let add_ghost_assigns reuse instrs =
+ let is_reused_def v = Hashtbl.find_opt reuse v.var_id in
+ let add_reused vars i =
+ match is_reused_def i with
+ | None -> vars
+ | Some v -> VMap.add i v vars
+ in
+ let rec is_defining_reused vars instr =
+ match instr.instr_desc with
+ | MLocalAssign (i, _) -> add_reused vars i
+ | MStep (il, _, _) ->
+ List.fold_left add_reused vars il
+ | MBranch (_, hl) ->
+ List.fold_left (fun vars (_, instrs) ->
+ List.fold_left is_defining_reused vars instrs)
+ vars hl
+ | _ -> vars
in
- asg, instr_cons { instr with instr_desc; instr_spec } instrs
+ List.map (fun instr ->
+ let vars = is_defining_reused VMap.empty instr in
+ let instr_spec = VMap.fold (fun i v ->
+ add_ghost_assign_spec i (vdecl_to_val v))
+ vars instr.instr_spec
+ in
+ { instr with instr_spec }) instrs
+
+let ghost_vd v = { v with var_id = "__" ^ v.var_id }
-and instrs_replace_var m fvar asg instrs =
- let asg, instrs =
- List.fold_left (instr_replace_var m fvar) (asg, []) instrs
+let add_ghost_assigns_reassigned rasg instrs =
+ let _, instrs, _ =
+ List.fold_left (fun (rasg, instrs, fvar) instr ->
+ let rec aux rasg instr fvar =
+ match instr.instr_desc with
+ | MLocalAssign (i, _) when VSet.mem i rasg ->
+ VSet.remove i rasg,
+ add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) instr.instr_spec,
+ fun v -> if v = i then ghost_vd i else fvar v
+ | MStep (il, _, _) ->
+ let il = List.filter (fun i -> VSet.mem i rasg) il in
+ List.fold_left (fun (rasg, spec, fvar) i ->
+ VSet.remove i rasg,
+ add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec,
+ fun v -> if v = i then ghost_vd i else fvar v)
+ (rasg, instr.instr_spec, fvar) il
+ | MBranch (_, hl) ->
+ let rasg' = List.fold_left (fun rasg (_, instrs) ->
+ List.fold_left (fun rasg instr ->
+ let rasg, _, _ = aux rasg instr fvar in
+ rasg) rasg instrs) rasg hl
+ in
+ let rasg'' = VSet.diff rasg rasg' in
+ rasg',
+ VSet.fold (fun i spec ->
+ add_ghost_assign_spec (ghost_vd i) (vdecl_to_val i) spec)
+ rasg''
+ instr.instr_spec,
+ fun v -> if VSet.mem v rasg'' then ghost_vd v else fvar v
+ | _ -> rasg, instr.instr_spec, fvar
+ in
+ let rasg, instr_spec, fvar = aux rasg instr fvar in
+ let instr_spec = List.map (fun (t, b) ->
+ instr_spec_replace fvar t, b) instr_spec
+ in
+ rasg,
+ { instr with instr_spec } :: instrs,
+ fvar)
+ (rasg, [], fun v -> v) instrs
in
- asg, List.rev instrs
-
-let add_ghost_assign (firsts, spec) v =
- ( ISet.add v.var_id firsts,
- (Predicate (GhostAssign (ghost_vd v, v)), false) :: spec )
-
-let add_ghost_assigns m fvar asg instrs =
- let rec aux (firsts, instrs) instr =
- let firsts, instr =
- match instr.instr_desc with
- | MLocalAssign (i, _)
- when is_reused_reassigned m fvar asg i && not (ISet.mem i.var_id firsts)
- ->
- let firsts, instr_spec =
- add_ghost_assign (firsts, instr.instr_spec) i
- in
- firsts, { instr with instr_spec }
- | MStep (il, _, _) ->
- let firsts, instr_spec =
- List.fold_left
- (fun ((firsts, _) as acc) i ->
- if
- is_reused_reassigned m fvar asg i
- && not (ISet.mem i.var_id firsts)
- then add_ghost_assign acc i
- else acc)
- (firsts, instr.instr_spec)
- il
- in
- firsts, { instr with instr_spec }
- | MBranch (g, hl) ->
- let firsts, hl =
- List.fold_left
- (fun (firsts', hl) (h, il) ->
- let firsts, il = aux' firsts il in
- ISet.union firsts firsts', (h, il) :: hl)
- (ISet.empty, [])
- hl
- in
- firsts, { instr with instr_desc = MBranch (g, List.rev hl) }
- | _ ->
- firsts, instr
+ List.rev instrs
+
+module IntS = Set.Make(Int)
+
+let add_assigned k v =
+ VMap.update v (function
+ | Some (n, ks) as b ->
+ if k > IntS.max_elt ks then Some (n + 1, IntS.add k ks) else b
+ | None -> Some (1, IntS.singleton k))
+
+let silly_asg i v =
+ match v.value_desc with Var w -> w.var_id = i.var_id | _ -> false
+
+let step_replace_var m reuse step =
+ let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
+ let fvar v =
+ let f v =
+ let v' = fvar v in
+ let v'' = fvar v' in
+ v', v'.var_id <> v''.var_id
in
- firsts, instr :: instrs
- and aux' firsts instrs =
- let firsts, instrs = List.fold_left aux (firsts, []) instrs in
- firsts, List.rev instrs
+ fixpoint f v
in
- aux' ISet.empty instrs |> snd
-
-let step_replace_var m fvar step =
let step_locals =
List.fold_left
(fun res l ->
@@ -1001,21 +1002,58 @@ let step_replace_var m fvar step =
let step_checks =
List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks
in
- let asg, step_instrs =
- instrs_replace_var m fvar IMap.empty step.step_instrs
+ let rec asg_instr k asg instr =
+ match instr.instr_desc with
+ | MLocalAssign (i, v) ->
+ if silly_asg i v then asg else add_assigned k i asg
+ | MStep (il, _, _) ->
+ List.fold_right (add_assigned k) il asg
+ | MBranch (_, hl) ->
+ List.fold_left
+ (fun asg' (_, il) ->
+ let asg'' = List.fold_left (asg_instr k) asg il in
+ VMap.union (fun _ n1 n2 -> Some (max n1 n2)) asg' asg'')
+ VMap.empty
+ hl
+ | _ -> asg
+ in
+ let assigned asg instrs =
+ let asg, _ = List.fold_left (fun (asg, k) instr ->
+ asg_instr k asg instr, k + 1)
+ (asg, 0) instrs
+ in
+ asg
+ in
+ (* SSA *)
+ let step_instrs = add_ghost_assigns reuse step.step_instrs in
+ (* register the locations of assignments *)
+ let asg = assigned VMap.empty step_instrs in
+ (* let pp fmt (k, s) = *)
+ (* Format.(fprintf fmt "%n{@[%a}@]" k (pp_comma_list pp_print_int) (IntS.elements s)) *)
+ (* in *)
+ (* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
+ (* SSA *)
+ let step_instrs = instrs_replace_var m fvar step_instrs in
+ (* update the locations of assignments, consider as reassignments only the
+ ones appearing *after* the original one *)
+ let asg = assigned asg step_instrs in
+ (* Format.printf "APRES %a@." (VMap.pp pp) asg; *)
+ let rasg = VMap.fold (fun v (n, _) rasg ->
+ if n > 1 then VSet.add v rasg else rasg) asg VSet.empty
in
- let step_instrs = add_ghost_assigns m fvar asg step_instrs in
+ (* not SSA anymore *)
+ let step_instrs = add_ghost_assigns_reassigned rasg step_instrs in
+ (* not SSA anymore *)
{ step with step_checks; step_locals; step_instrs }
-let machine_replace_variables fvar m =
- { m with mstep = step_replace_var m fvar m.mstep }
+let machine_replace_variables reuse m =
+ { m with mstep = step_replace_var m reuse m.mstep }
let pp_reuse fmt reuse =
- Format.fprintf fmt "{ @[<hv>";
- Hashtbl.iter
- (fun v1 v2 -> Format.fprintf fmt "%s --> %s@ " v1 v2.var_id)
- reuse;
- Format.fprintf fmt "@]@;}"
+ let l = Hashtbl.to_seq reuse |> List.of_seq in
+ let pp_fun fmt (x, v) = Format.fprintf fmt "%s --> %s" x v.var_id in
+ Format.(fprintf fmt "{ @[<v 2>%a@] }"
+ (pp_print_list ~pp_sep:pp_print_comma pp_fun) l)
let machine_reuse_variables reuse m =
(* Some outputs may have been replaced by locals. We reverse such bindings. *)
@@ -1035,16 +1073,7 @@ let machine_reuse_variables reuse m =
m.mname.node_id
pp_reuse
reuse);
- let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
- let fvar v =
- let f v =
- let v' = fvar v in
- let v'' = fvar v' in
- v', v'.var_id <> v''.var_id
- in
- fixpoint f v
- in
- machine_replace_variables fvar m
+ machine_replace_variables reuse m
let machines_reuse_variables reuse_tables prog =
Log.report ~level:1 (fun fmt ->
@@ -1105,29 +1134,33 @@ and instrs_constant_assign var instrs =
false
instrs
-let rec instr_reduce branches instr1 cont =
+let rec instr_reduce m v branches instr1 cont =
match get_instr_desc instr1 with
- | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ })
- | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
+ | MLocalAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t) )
+ | MStateAssign (_, ({ value_desc = Cst (Const_tag c); _ } as t) ) ->
+ mkinstr ~instr_spec:(add_ghost_assign_spec v t []) (assign_comment m v t)
+ ::
instr1 :: (List.assoc c branches @ cont)
| MBranch (g, hl) ->
update_instr_desc
instr1
- (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
+ (MBranch (g, List.map (fun (h, b) ->
+ h,
+ instrs_reduce m v branches b []) hl))
:: cont
| _ ->
instr1 :: cont
-and instrs_reduce branches instrs cont =
+and instrs_reduce m v branches instrs cont =
match instrs with
| [] ->
cont
| [ i ] ->
- instr_reduce branches i cont
+ instr_reduce m v branches i cont
| i1 :: i2 :: q ->
- i1 :: instrs_reduce branches (i2 :: q) cont
+ i1 :: instrs_reduce m v branches (i2 :: q) cont
-let rec instrs_fusion instrs =
+let rec instrs_fusion m instrs =
match instrs with
| [] | [ _ ] ->
false, instrs
@@ -1136,19 +1169,20 @@ let rec instrs_fusion instrs =
| MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
( true,
instr_reduce
- (List.map (fun (h, b) -> h, snd (instrs_fusion b)) hl)
+ m v
+ (List.map (fun (h, b) -> h, snd (instrs_fusion m b)) hl)
{ i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
- (snd (instrs_fusion q)) )
+ (snd (instrs_fusion m q)) )
| _ ->
- let b, instrs = instrs_fusion (i2 :: q) in
+ let b, instrs = instrs_fusion m (i2 :: q) in
b, i1 :: instrs)
-let step_fusion step =
- let b, step_instrs = instrs_fusion step.step_instrs in
+let step_fusion m step =
+ let b, step_instrs = instrs_fusion m step.step_instrs in
b, { step with step_instrs }
let machine_fusion m =
- let b, mstep = step_fusion m.mstep in
+ let b, mstep = step_fusion m m.mstep in
b, { m with mstep }
let machines_fusion prog =
@@ -1194,19 +1228,6 @@ let machine_clean m =
let rec filter_instrs instrs =
List.filter_map
(fun instr ->
- let instr =
- {
- instr with
- instr_spec =
- List.map
- (fun (t, asrt) ->
- let fv =
- VSet.(elements (filter is_unused (fv_formula m empty t)))
- in
- Exists (fv, t), asrt)
- instr.instr_spec;
- }
- in
match get_instr_desc instr with
| MLocalAssign (v, _) ->
if is_used v then Some instr else None
diff --git a/src/spec_types.ml b/src/spec_types.ml
index bdfcb53bf4351961ab1b18aad7d298129f37e75c..3651b51a80ffaf975585a81ffa4eede105b46034 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -25,7 +25,7 @@ type 'a predicate_t =
| Reset of ident * ident * 'a
| MemoryPack of ident * ident option * int option
| MemoryPackBase of ident
- | GhostAssign of var_decl * var_decl
+ | GhostAssign of var_decl * 'a
type 'a formula_t =
| True
diff --git a/src/spec_types.mli b/src/spec_types.mli
index 41749288a07f70d7cd33fa084e28dbca562eb1e1..c4c43a89daeeb2a07d77d5a6c39b38d41fcdf768 100644
--- a/src/spec_types.mli
+++ b/src/spec_types.mli
@@ -25,7 +25,7 @@ type 'a predicate_t =
| Reset of ident * ident * 'a
| MemoryPack of ident * ident option * int option
| MemoryPackBase of ident
- | GhostAssign of var_decl * var_decl
+ | GhostAssign of var_decl * 'a
type 'a formula_t =
| True
diff --git a/strategy.ml b/strategy.ml
index c26cf0bf930219174e5821f708d842ffd030bdbd..b1cc5fea0f376d05117a06046c7db3defd1646a0 100644
--- a/strategy.ml
+++ b/strategy.ml
@@ -29,16 +29,6 @@ let is_pack (f : Lang.lfun) : bool =
true
with Not_found -> false
-(* (\* check that a given predicate name is a reset_cleared relation *\) *)
-(* let is_reset_cleared (f : Lang.lfun) : bool = *)
-(* let open Str in *)
-(* let r = regexp "_reset_cleared$" in *)
-(* let s = Repr.lfun f in *)
-(* try *)
-(* ignore (search_forward r s 0); *)
-(* true *)
-(* with Not_found -> false *)
-
(* tactical selection of the goal *)
let select_g (g : Lang.F.pred) : Tactical.selection =
let open Tactical in
@@ -161,24 +151,6 @@ class lustrec_transitions : Strategy.heuristic =
()
end
-(* (\* Reset Cleared heuristic *\) *)
-(* class lustrec_reset_cleared : Strategy.heuristic = *)
-(* object *)
-(* method id = "LustreC:ResetCleared" (\* required, must be unique *\) *)
-(* method title = "LustreC ResetCleared" *)
-(* method descr = "Custom goal transformations for reset_cleared relations" *)
-
-(* method search (push : Strategy.strategy -> unit) *)
-(* (sequent : Conditions.sequent) : unit = *)
-(* let goal = snd sequent in *)
-(* match Repr.pred goal with *)
-(* (\* if the goal is only a reset_cleared relation, unfold it *\) *)
-(* | Call (p, _) when is_reset_cleared p -> *)
-(* push (Auto.definition (select_g goal)) *)
-(* | _ -> *)
-(* () *)
-(* end *)
-
(* unfold f(es) in the given context (context is handled with side-effects) *)
let definition (context : WpContext.context) (f : Lang.lfun)
(es : Lang.F.term list) : Lang.F.term =
@@ -274,5 +246,4 @@ class lustrec_memory_packs : Strategy.heuristic =
(* Register the strategies *)
let () =
Strategy.register (new lustrec_transitions);
- (* Strategy.register (new lustrec_reset_cleared); *)
Strategy.register (new lustrec_memory_packs)