Implementation of disjunction domain seems to work.

1 files changed, 7 insertions, 8 deletions

diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
index 59ed1a0..96de8bc 100644
--- a/abstract/num_domain.ml
+++ b/abstract/num_domain.ml
@@ -6,18 +6,16 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
     type itv
 
     (* construction *)
-    val init        : t
-    val bottom      : t
-    val vbottom     : t -> t       (* bottom value with same environment *)
+    val top         : (id * bool) list -> t
+    val bottom      : (id * bool) list -> t
+    val vbottom     : t -> t       (* bottom value with same variables *)
     val is_bot      : t -> bool
 
     (* variable management *)
-    val addvar      : t -> id -> bool -> t     (* integer or real variable ? *)
-    val rmvar       : t -> id -> t
     val vars        : t -> (id * bool) list
 
     val forgetvar   : t -> id -> t             (* remove var from constraints *)
-    val var_itv     : t -> id -> itv
+    val project     : t -> id -> itv
 
     (* set-theoretic operations *)
     val join        : t -> t -> t       (* union *)
@@ -29,12 +27,13 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
     val eq          : t -> t -> bool
 
     (* abstract operation *)
-    val apply_ncl   : t -> num_cons list -> t
+    val apply_cons  : t -> num_cons -> t
+    val apply_cl    : t -> num_cons list -> t
     val assign      : 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_all   : Format.formatter -> t -> unit
     val print_itv   : Format.formatter -> itv -> unit
 end