1 files changed, 30 insertions, 0 deletions
diff --git a/src/constraint.mli b/src/constraint.mli
new file mode 100644
index 00000000..3fb3d2f6
--- /dev/null
+++ b/src/constraint.mli
@@ -0,0 +1,30 @@
+type nexp
+type t
+
+type smt_result = Unknown of t list | Unsat of t
+       
+val call_z3 : t -> smt_result
+
+val string_of : t -> string
+                                           
+val implies : t -> t -> t
+val conj : t -> t -> t
+val disj : t -> t -> t
+val negate : t -> t
+val branch : t list -> t
+val literal : bool -> t
+
+val lt : nexp -> nexp -> t
+val lteq : nexp -> nexp -> t
+val gt : nexp -> nexp -> t
+val gteq : nexp -> nexp -> t
+val eq : nexp -> nexp -> t
+val neq : nexp -> nexp -> t
+
+val pow2 : nexp -> nexp
+val add : nexp -> nexp -> nexp
+val sub : nexp -> nexp -> nexp
+val mult : nexp -> nexp -> nexp
+
+val constant : Big_int.big_int -> nexp
+val variable : int -> nexp