Isolate numerical part of domain. Next: isolate numerical part of equations.

1 files changed, 88 insertions, 0 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
new file mode 100644
index 0000000..ddc34ab
--- /dev/null
+++ b/abstract/abs_domain.ml
@@ -0,0 +1,88 @@
+open Ast
+open Formula
+open Num_domain
+open Typing
+
+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 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 (cons, rest) = match rest with
+        | CLTrue ->
+          ND.apply_ncl x cons
+        | CLFalse -> vbottom x
+        | CLAnd(a, b) ->
+          let y = apply_cl x (cons, a) in
+          apply_cl y (cons, b)
+        | CLOr((ca, ra), (cb, rb)) ->
+          let y = apply_cl x (cons@ca, ra) in
+          let z = apply_cl x (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