Cint.ml

      Lang.iter_confident_literals
        (fun p -> domain <- Dom.assume_literal p domain) (Lang.F.e_prop p)

    method private simplify ~is_goal p =
      let pool = Lang.get_pool () in

      let reduce op var_domain base =
        let dom =
          match Lang.F.repr base with
          | Kint z -> Ival.inject_singleton z
          | _ ->
              try Tmap.find base domain
              with Not_found -> Ival.top
        in
        var_domain := Ival.backward_comp_int_left op !var_domain dom
      in
      let rec reduce_on_neg var var_domain t =
        match Lang.F.repr t with
        | _ when not (is_prop t) -> ()
        | Leq(a,b) when Lang.F.equal a var ->
            reduce Abstract_interp.Comp.Le var_domain b
        | Leq(b,a) when Lang.F.equal a var ->
            reduce Abstract_interp.Comp.Ge var_domain b
        | Lt(a,b) when Lang.F.equal a var ->
            reduce Abstract_interp.Comp.Lt var_domain b
        | Lt(b,a) when Lang.F.equal a var ->
            reduce Abstract_interp.Comp.Gt var_domain b
        | And l -> List.iter (reduce_on_neg var var_domain) l
        | Not p -> reduce_on_pos var var_domain p
        | _ -> ()
      and reduce_on_pos var var_domain t =
        match Lang.F.repr t with
        | Neq _ | Leq _ | Lt _ -> reduce_on_neg var var_domain (e_not t)
        | Imply (l,p) -> List.iter (reduce_on_neg var var_domain) l;
            reduce_on_pos var var_domain p
        | Or l -> List.iter (reduce_on_pos var var_domain) l;
        | Not p -> reduce_on_neg var var_domain p
        | _ -> ()
      in
      (* [~term_pol] gives the polarity of the term [t] from the top level.
                     That informs about how should be considered the quantifiers
                     of [t]
      *)
      let rec walk ~term_pol t =
        let walk_flip_pol t = walk ~term_pol:(Polarity.flip term_pol) t
        and walk_same_pol t = walk ~term_pol t
        and walk_both_pol t = walk ~term_pol:Polarity.Both t
        in
        match repr t with
        | _ when not (is_prop t) -> t
        | Bind((Forall|Exists),_,_) ->
            let ctx,t = e_open ~pool ~lambda:false t in
            let ctx_with_dom =
              List.map (fun ((quant,var) as qv)  -> match tau_of_var var with
                  | Int ->
                      let tvar = (e_var var) in
                      let var_domain = ref Ival.top in
                      if quant = Forall
                      then reduce_on_pos tvar var_domain t
                      else reduce_on_neg tvar var_domain t;
                      domain <- Dom.add tvar !var_domain domain;
                      qv, Some (tvar, var_domain)
                  | _ -> qv, None) ctx
            in
            let t = walk_same_pol t in
            let f_close t = function
              | (quant,var), None -> e_bind quant var t
              | (quant,var), Some (tvar,var_domain) ->
                  domain <- Dom.remove tvar domain;
                  (** Bonus: Add additionnal hypothesis in forall when we could deduce
                      better constraint on the variable *)
                  let add_bonus = match term_pol with
                    | Polarity.Both -> false
                    | _ -> (term_pol=Polarity.Pos) = (quant=Forall)
                  in
                  let t = reduce_bound ~add_bonus quant var tvar !var_domain t in
                  e_bind quant var t
            in
            List.fold_left f_close t ctx_with_dom
        | Fun(g,[a]) ->
            (** Here we simplifies the cints which are redoundant *)
            begin try
                let ubound = c_int_bounds_ival (is_cint g) in
                let dom = (Tmap.find a domain) in
                if Ival.is_included dom ubound
                then e_true
                else t
              with Not_found -> t
            end
        | Imply (l1,l2) -> e_imply (List.map walk_flip_pol l1) (walk_same_pol l2)
        | Not p -> e_not (walk_flip_pol p)
        | And _ | Or _ -> Lang.F.QED.f_map walk_same_pol t
        | _ ->
            Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
      Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))

    method simplify_exp (e : term) = e

    method simplify_hyp p = self#simplify ~is_goal:false p

    method simplify_goal p = self#simplify ~is_goal:true p

    method simplify_branch p = p

    method infer = []
  end


let mask_simplifier =
  let update x m ctx =
    Tmap.insert (fun _ m old -> if Integer.lt m old then (*better*) m else old)
      x m ctx
  and rewrite ctx e =
    let reduce m x = match F.repr x with
      | Kint v -> F.e_zint (Integer.logand m v)
      | _ -> x
    and collect ctx d x = try
        let m = Tmap.find x ctx in
        match d with
        | None -> Some m
        | Some m0 -> if Integer.lt m m0 then Some m else d
      with Not_found -> d
    in
    match F.repr e with
    | Fun(f,es) when f == f_land ->
        begin
          match List.fold_left (collect ctx) None es with
          | None -> raise Not_found
          | Some m -> F.e_fun f_land (List.map (reduce m) es)
        end
    | _ -> raise Not_found
  in
  object

    (** Must be 2^n-1 *)
    val mutable magnitude : Integer.t Tmap.t = Tmap.empty

    method name = "Rewrite unsigned masks"
    method copy = {< magnitude = magnitude >}

    method target _ = ()
    method infer = []
    method fixpoint = ()

    method assume p =
      Lang.iter_confident_literals
        (fun p -> match F.repr p with
           | Fun(f,[x]) -> begin
               try
                 let iota = is_cint f in
                 if not (Ctypes.signed iota) then
                   magnitude <- update x (snd (Ctypes.bounds iota)) magnitude
               with Not_found -> ()
             end
           | _ -> ()) (F.e_prop p)

    method simplify_exp e =
      if Tmap.is_empty magnitude then e else
        Lang.e_subst (rewrite magnitude) e

    method simplify_hyp p =
      if Tmap.is_empty magnitude then p else
        Lang.p_subst (rewrite magnitude) p

    method simplify_branch p =
      if Tmap.is_empty magnitude then p else
        Lang.p_subst (rewrite magnitude) p

    method simplify_goal p =
      if Tmap.is_empty magnitude then p else
        Lang.p_subst (rewrite magnitude) p

  end

(* -------------------------------------------------------------------------- *)