Remove now-unused ApronDomain.BoxProd

Author: sim642

src/cdomains/apron/apronDomain.apron.ml

@@ -856,111 +856,3 @@ struct
 
   let unmarshal (m: marshal) = Oct.Abstract1.of_oct @@ OctagonD.unmarshal m
 end
-
-(** Lift [D] to a non-reduced product with box.
-    Both are updated in parallel, but [D] answers to queries.
-    Box domain is used to filter out non-relational invariants for output. *)
-module BoxProd0 (D: S3) = (* TODO: remove? *)
-struct
-  module BoxD = D2 (IntervalManager)
-
-  include Printable.Prod (BoxD) (D)
-
-  let equal (_, d1) (_, d2) = D.equal d1 d2
-  let hash (_, d) = D.hash d
-  let compare (_, d1) (_, d2) = D.compare d1 d2
-
-  let leq (_, d1) (_, d2) = D.leq d1 d2
-  let join (b1, d1) (b2, d2) = (BoxD.join b1 b2, D.join d1 d2)
-  let meet (b1, d1) (b2, d2) = (BoxD.meet b1 b2, D.meet d1 d2)
-  let widen (b1, d1) (b2, d2) = (BoxD.widen b1 b2, D.widen d1 d2)
-  let narrow (b1, d1) (b2, d2) = (BoxD.narrow b1 b2, D.narrow d1 d2)
-
-  let top () = (BoxD.top (), D.top ())
-  let bot () = (BoxD.bot (), D.bot ())
-  let is_top (_, d) = D.is_top d
-  let is_bot (_, d) = D.is_bot d
-  let top_env env = (BoxD.top_env env, D.top_env env)
-  let bot_env env = (BoxD.bot_env env, D.bot_env env)
-  let is_top_env (_, d) = D.is_top_env d
-  let is_bot_env (_, d) = D.is_bot_env d
-  let unify (b1, d1) (b2, d2) = (BoxD.unify b1 b2, D.unify d1 d2)
-  let copy (b, d) = (BoxD.copy b, D.copy d)
-
-  type marshal = BoxD.marshal * D.marshal
-
-  let marshal (b, d) = (BoxD.marshal b, D.marshal d)
-  let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d)
-
-  let mem_var (_, d) v = D.mem_var d v
-  let vars (_, d) = D.vars d
-
-  let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2)
-
-  let add_vars_with (b, d) vs =
-    BoxD.add_vars_with b vs;
-    D.add_vars_with d vs
-  let remove_vars_with (b, d) vs =
-    BoxD.remove_vars_with b vs;
-    D.remove_vars_with d vs
-  let remove_filter_with (b, d) f =
-    BoxD.remove_filter_with b f;
-    D.remove_filter_with d f
-  let keep_filter_with (b, d) f =
-    BoxD.keep_filter_with b f;
-    D.keep_filter_with d f
-  let keep_vars_with (b, d) vs =
-    BoxD.keep_vars_with b vs;
-    D.keep_vars_with d vs
-  let forget_vars_with (b, d) vs =
-    BoxD.forget_vars_with b vs;
-    D.forget_vars_with d vs
-  let assign_exp_with ask (b, d) v e no_ov =
-    BoxD.assign_exp_with ask b v e no_ov;
-    D.assign_exp_with ask d v e no_ov
-  let assign_exp_parallel_with ask (b, d) ves no_ov =
-    BoxD.assign_exp_parallel_with ask b ves no_ov;
-    D.assign_exp_parallel_with ask d ves no_ov
-  let assign_var_with (b, d) v e =
-    BoxD.assign_var_with b v e;
-    D.assign_var_with d v e
-  let assign_var_parallel_with (b, d) vvs =
-    BoxD.assign_var_parallel_with b vvs;
-    D.assign_var_parallel_with d vvs
-  let assign_var_parallel' (b, d) vs v's =
-    (BoxD.assign_var_parallel' b vs v's, D.assign_var_parallel' d vs v's)
-  let substitute_exp_with ask (b, d) v e no_ov =
-    BoxD.substitute_exp_with ask b v e no_ov;
-    D.substitute_exp_with ask d v e no_ov
-  let substitute_exp_parallel_with ask (b, d) ves no_ov =
-    BoxD.substitute_exp_parallel_with ask b ves no_ov;
-    D.substitute_exp_parallel_with ask d ves no_ov
-  let substitute_var_with (b, d) v1 v2 =
-    BoxD.substitute_var_with b v1 v2;
-    D.substitute_var_with d v1 v2
-  let meet_tcons ask (b, d) c e = (BoxD.meet_tcons ask b c e, D.meet_tcons ask d c e)
-  let to_lincons_array (_, d) = D.to_lincons_array d
-  let of_lincons_array a = (BoxD.of_lincons_array a, D.of_lincons_array a)
-
-  let cil_exp_of_lincons1 = D.cil_exp_of_lincons1
-  let assert_inv ask (b, d) e n no_ov = (BoxD.assert_inv ask b e n no_ov, D.assert_inv ask d e n no_ov)
-  let eval_int ask (_, d) = D.eval_int ask d
-
-  let invariant (b, d) =
-    (* diff via lincons *)
-    let lcb = D.to_lincons_array (D.of_lincons_array (BoxD.to_lincons_array b)) in (* convert through D to make lincons use the same format *)
-    let lcd = D.to_lincons_array d in
-    Lincons1Set.(diff (of_earray lcd) (of_earray lcb))
-    |> (if Oct.manager_is_oct D.Man.mgr then Lincons1Set.simplify else Fun.id)
-    |> Lincons1Set.elements
-end
-
-module BoxProd (D: S3): RD =
-struct
-  module V = D.V
-  type var = V.t
-  module BP0 = BoxProd0 (D)
-  module Tracked = SharedFunctions.Tracked
-  include BP0
-  include AOpsPureOfImperative (BP0)
-end