Restart anew ; done nonrelational stuff, interpret remains, intervals domain remains

1 files changed, 28 insertions, 0 deletions

diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
new file mode 100644
index 0000000..a0f082f
--- /dev/null
+++ b/abstract/value_domain.ml
@@ -0,0 +1,28 @@
+module type VALUE_DOMAIN = sig
+	type t
+
+	(* constructors *)
+	val top		: t
+	val bottom	: t
+	val const	: Z.t -> t
+	val rand	: Z.t -> Z.t -> t
+
+	(* order *)
+	val subset	: t -> t -> bool
+
+	(* set-theoretic operations *)
+	val join	: t -> t -> t   (* union *)
+	val meet	: t -> t -> t	(* intersection *)
+	val widen	: t -> t -> t
+
+	(* arithmetic operations *)
+	val neg		: t -> t
+	val add		: t -> t -> t
+	val sub		: t -> t -> t
+	val mul		: t -> t -> t
+	val div		: t -> t -> t
+	val rem		: t -> t -> t
+
+	(* boolean test *)
+	val leq		: t -> t -> t * t	(* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+end