1 files changed, 41 insertions, 0 deletions
diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
new file mode 100644
index 0000000..59ed1a0
--- /dev/null
+++ b/abstract/num_domain.ml
@@ -0,0 +1,41 @@
+open Ast
+open Formula
+
+module type NUMERICAL_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 -> 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
+
+    (* set-theoretic operations *)
+    val join        : t -> t -> t       (* union *)
+    val meet        : t -> t -> t       (* intersection *)
+    val widen       : t -> t -> t
+
+    (* order *)
+    val subset      : t -> t -> bool
+    val eq          : t -> t -> bool
+
+    (* abstract operation *)
+    val apply_ncl   : t -> num_cons list -> 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
+
+