open Ast
open Formula
open Num_domain
open Enum_domain
open Varenv
module type ENVIRONMENT_DOMAIN = sig
type t
type itv
(* constructors *)
val top : varenv -> t
val bottom : varenv -> t
val is_top : t -> bool
val is_bot : t -> bool
(* variable management *)
val varenv : t -> varenv
val forgetvar : t -> id -> t
val forgetvars : t -> id list -> t
val nproject : t -> id -> itv (* numerical project *)
val eproject : t -> id -> item list
(* set-theoretic operations *)
val join : t -> t -> t
val meet : t -> t -> t
val widen : t -> t -> t
val subset : t -> t -> bool
val eq : t -> t -> bool
(* abstract operations *)
val apply_ec : t -> enum_cons -> t
val apply_ecl : t -> enum_cons list -> t
val apply_nc : t -> num_cons -> t
val apply_ncl : t -> num_cons list -> t
val eassign : t -> (id * id) list -> t
val nassign : t -> (id * num_expr) list -> t
(* pretty-printing *)
val print : Format.formatter -> t -> unit
val print_vars : Format.formatter -> t -> id list -> unit
val print_itv : Format.formatter -> itv -> unit
end
module NumDomainOnly(ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
struct
type t = varenv * ND.t
type itv = ND.itv
let top ve = (ve, ND.top ve.nvars)
let bottom ve = (ve, ND.top ve.nvars)
let is_top (_, x) = ND.is_top x
let is_bot (_, x) = ND.is_bot x
let varenv (ve, x) = ve
let forgetvar (ve, x) id =
if List.exists (fun (i, _) -> i = id) ve.nvars
then (ve, ND.forgetvar x id)
else (ve, x)
let forgetvars (ve, x) ids =
(ve, List.fold_left ND.forgetvar x
(List.filter (fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids))
let nproject (_, x) id = ND.project x id
let eproject (ve, _) id = List.assoc id ve.evars
let join (ve, a) (_, b) = (ve, ND.join a b)
let meet (ve, a) (_, b) = (ve, ND.meet a b)
let widen (ve, a) (_, b) = (ve, ND.widen a b)
let subset (_, a) (_, b) = ND.subset a b
let eq (_, a) (_, b) = ND.eq a b
let apply_ec x _ = x
let apply_ecl x _ = x
let apply_nc (ve, x) c = (ve, ND.apply_cons x c)
let apply_ncl (ve, x) cl = (ve, ND.apply_cl x cl)
let eassign x _ = x
let nassign (ve, x) ex = (ve, ND.assign x ex)
let print fmt (_, x) = ND.print fmt x
let print_vars fmt (ve, x) ids =
ND.print_vars fmt x
(List.filter
(fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids)
let print_itv = ND.print_itv
end
module NumEnumDomain
(ED : ENUM_ENVIRONMENT_DOMAIN)(ND : NUMERICAL_ENVIRONMENT_DOMAIN)
: ENVIRONMENT_DOMAIN
= struct
type t =
| V of varenv * ED.t * ND.t
| Bot of varenv
type itv = ND.itv
let strict = function
| V(ve, enum, num) as x ->
if ND.is_bot num || ED.is_bot enum
then Bot ve
else x
| b -> b
let strict_apply f x = match x with
| V(ve, enum, num) ->
begin
try strict (f (ve, enum, num))
with Enum_domain.Bot -> Bot ve
end
| Bot ve -> Bot ve
let top ve = V(ve, ED.top ve.evars, ND.top ve.nvars)
let bottom ve = Bot ve
let is_top x = match strict x with
| Bot _ -> false
| V(_, enum, num) -> ED.is_top enum && ND.is_top num
let is_bot x = match strict x with
| Bot _ -> true
| _ -> false
let varenv = function
| Bot x -> x
| V(ve, _, _) -> ve
let forgetvar x id =
strict_apply (fun (ve, enum, num) ->
if List.exists (fun (id2, _) -> id2 = id) ve.evars
then V(ve, ED.forgetvar enum id, num)
else V(ve, enum, ND.forgetvar num id))
x
let forgetvars x ids =
strict_apply (fun (ve, enum, num) ->
let efv, nfv = List.fold_left
(fun (efv, nfv) id ->
if List.exists (fun (id2, _) -> id2 = id) ve.evars
then id::efv, nfv
else efv, id::nfv)
([], []) ids
in
V(ve, ED.forgetvars enum efv, List.fold_left ND.forgetvar num nfv))
x
let nproject x id = match x with
| V(ve, enum, num) ->
ND.project num id
| Bot ve -> ND.project (ND.bottom ve.nvars) id
let eproject x id = match x with
| V(ve, enum, num) ->
ED.project enum id
| Bot ve -> []
let join x y = match strict x, strict y with
| Bot _, a | a, Bot _ -> a
| V(ve, enum, num), V(_, enum', num') ->
V(ve, ED.join enum enum', ND.join num num')
let meet x y = match strict x, strict y with
| Bot ve, a | a, Bot ve -> Bot ve
| V(ve, enum, num), V(_, enum', num') ->
try
strict (V(ve, ED.meet enum enum', ND.meet num num'))
with Enum_domain.Bot -> Bot ve
let widen x y = match strict x, strict y with
| Bot _, a | a, Bot _ -> a
| V(ve, enum, num), V(_, enum', num') ->
V(ve, ED.join enum enum', ND.widen num num')
let subset x y = match strict x, strict y with
| Bot _, a -> true
| V(_, _, _), Bot _ -> false
| V(_, enum, num), V(_, enum', num') ->
ED.subset enum enum' && ND.subset num num'
let eq x y = match strict x, strict y with
| Bot _, Bot _ -> true
| V(_, enum, num), V(_, enum', num') ->
ED.eq enum enum' && ND.eq num num'
| _ -> false
let apply_ec x f =
strict_apply
(fun (ve, enum, num) -> V(ve, ED.apply_cl enum [f], num))
x
let apply_ecl x f =
strict_apply (fun (ve, enum, num) -> V(ve, ED.apply_cl enum f, num)) x
let apply_nc x f =
strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cons num f)) x
let apply_ncl x f =
strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cl num f)) x
let eassign x ass =
strict_apply (fun (ve, enum, num) -> V(ve, ED.assign enum ass, num)) x
let nassign x ass =
strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.assign num ass)) x
let print_itv = ND.print_itv
let print fmt x = match strict x with
| Bot _ -> Format.fprintf fmt "⊥"
| V(_, enum, num) ->
Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
let print_vars fmt x vars = match strict x with
| Bot _ -> Format.fprintf fmt "⊥"
| V(ve, enum, num) ->
let nvars = List.filter
(fun v -> List.exists (fun (x, _) -> x = v) ve.nvars)
vars
in
Format.fprintf fmt "@[<hov 1>(%a,@ " ED.print enum;
ND.print_vars fmt num nvars;
Format.printf ")@]"
end