Adapt abs_interp to use ENUM_DOMAIN2 (this is a test...)

1 files changed, 44 insertions, 4 deletions

diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 60f2d3b..a372772 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -1,9 +1,41 @@
 open Ast
 open Formula
 open Util
-open Enum_domain
 
-module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
+module type ENUM_ENVIRONMENT_DOMAIN2 = sig
+    type t
+
+    type item = string
+
+    (* construction *)
+    val top           : (id * item list) list -> t
+    val bot           : (id * item list) list -> t
+    val is_bot        : t -> bool
+
+    (* variable management *)
+    val vars          : t -> (id * item list) list
+
+    val forgetvar     : t -> id -> t
+    val forgetvars    : t -> id list -> t
+    val project       : t -> id -> item list
+
+    (* set-theoretic operations *)
+    val join          : t -> t -> t   (* union *)
+    val meet          : t -> t -> t   (* intersection *)
+
+    val subset        : t -> t -> bool
+    val eq            : t -> t -> bool
+
+    (* abstract operations *)
+    val apply_cons    : t -> enum_cons -> t
+    val apply_cl      : t -> enum_cons list -> t
+    val assign        : t -> (id * id) list -> t
+
+    (* pretty-printing *)
+    val print         : Format.formatter -> t -> unit
+end
+
+module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
     exception Top
 
     type item = string
@@ -132,11 +164,19 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
 
     (*
       top : (id * item list) list -> t
+      bot : (id * item list) list -> t
     *)
     let top vars =
         let order = Hashtbl.create 12 in
         List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
         { vars; order; root = DTop }
+    let bot vars = let t = top vars in { t with root = DBot }
+
+    (*
+      is_bot : t -> bool
+    *)
+    let is_bot x = (x.root = DBot)
+
     (*
       vars : t -> (id * item list) list
     *)
@@ -243,8 +283,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
       apply_cl : t -> enum_cons list -> t
     *)
     let apply_cons v x =
-      let v = meet v (of_cons v x) in
-      if v.root = DBot then [] else [v]
+      meet v (of_cons v x)
+
     let apply_cl v ec =
         let rec cl_k = function
           | [] -> { v with root = DTop }