path: root/abstract/abs_domain.ml

open Ast
open Formula
open Num_domain
open Typing
open Util

module type ENVIRONMENT_DOMAIN = sig
    type t
    type itv

    (* construction *)
    val init              : t
    val bottom            : t
    val vbottom           : t -> t      (* bottom value with same environment *)
    val is_bot            : t -> bool

    (* variable management *)
    val addvar            : t -> id -> Typing.typ -> t
    val rmvar             : t -> id -> t
    val vars              : t -> (id * Typing.typ) list

    val forgetvar         : t -> id -> t
    val var_itv           : t -> id -> itv

    (* set_theoretic operations *)
    val join              : t -> t -> t   (* union *)
    val meet              : t -> t -> t   (* intersection *)
    val widen             : t -> t -> t

    val subset            : t -> t -> bool
    val eq                : t -> t -> bool

    (* abstract operations *)
    val apply_f           : t -> bool_expr -> t
    val apply_cl          : t -> conslist -> t
    val assign            : t -> (id * num_expr) list -> t

    (* pretty-printing *)
    val print_vars  : Format.formatter -> t -> id list -> unit
    val print_all   : Format.formatter -> t -> unit
    val print_itv   : Format.formatter -> itv -> unit

end

module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct

    type enum_valuation = (string * string) list

    module VMapKey = struct
      type t = enum_valuation VarMap.t
      let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b))
    end
    module VMap = Mapext.Make(VMapKey)

    type t = ND.t
    type itv = ND.itv

    let init = ND.init
    let bottom = ND.bottom
    let vbottom = ND.vbottom
    let is_bot = ND.is_bot

    let addvar x id ty = ND.addvar x id (ty = TReal)
    let rmvar = ND.rmvar
    let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x)

    let forgetvar = ND.forgetvar
    let var_itv = ND.var_itv

    let join = ND.join
    let meet = ND.meet
    let widen = ND.widen

    let subset = ND.subset
    let eq = ND.eq

    let rec apply_cl x (econs, cons, rest) = match rest with
        | CLTrue ->
          ND.apply_ncl x cons
        | CLFalse -> vbottom x
        | CLAnd(a, b) ->
          let y = apply_cl x (econs, cons, a) in
          apply_cl y (econs, cons, b)
        | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
          let y = apply_cl x (econs@eca, cons@ca, ra) in
          let z = apply_cl x (econs@ecb, cons@cb, rb) in
          join y z

    let apply_f x f = apply_cl x (conslist_of_f f)

    let assign = ND.assign

    let print_vars = ND.print_vars
    let print_all = ND.print_all
    let print_itv = ND.print_itv

end