Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/ml/META.in

@@ -1,11 +1,11 @@
 # META file for the "z3" package:
-version = "VERSION"
+version = "@VERSION@"
 description = "Z3 Theorem Prover (OCaml API)"
 requires = "num"
 archive(byte) = "z3ml.cma"
 archive(native) = "z3ml.cmxa"
 archive(byte,plugin) = "z3ml.cma"
-archive(native,plugin) = "z3ml.cmxa"
+archive(native,plugin) = "z3ml.cmxs"
 archive(byte,toploop) = "z3ml.cma"
 archive(native,toploop) = "z3ml.cmxa"
-linkopts = "-cclib -lz3"
+linkopts = "-cclib @LEXTRA@"

src/api/ml/Makefile

@@ -1,10 +0,0 @@
-# This is a temporary support file for emacs annotations. 
-# It does not compile the Z3 ML API; this will be built 
-# in the top-level build directory.
-
-all: 
-	ocamlbuild -cflag -annot z3.cmxa
-
-doc: *.ml
-	mkdir -p doc
-	ocamldoc -html -d doc -I _build -sort *.mli -hide Z3

src/api/ml/README

@@ -4,8 +4,10 @@ refer to previous releases of Z3.
 On Windows, there are no less than four different ports of OCaml. The Z3 build 
 system assumes that either the win32 or the win64 port is installed. This means
 that OCaml will use `cl' as the underlying C compiler and not the cygwin or
-mingw compilers. 
+mingw compilers.
 
-By default, a make target called `ocamlfind_install' is added. This installs Z3
-into the ocamlfind package repository such that programs can be compiled via 
-ocamlfind.
+OCamlfind: When ocamlfind is found, the `install' target will install the Z3
+OCaml bindings into the ocamlfind site-lib directory. The installed package is
+linked against the (dynamic) libz3 and it adds $(PREFIX)/lib to the library
+include paths. On Windows, there is no $(PREFIX), so the build directory is
+used instead (see META.in).

src/api/ml/z3native_stubs.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    z3native_stubs.h
+
+Abstract:
+
+    DLL/SO/DYLIB export macros.
+
+Author:
+
+    Christoph (cwinter) 2015-12-12
+
+Notes:
+
+--*/
+
+#ifndef Z3NATIVE_STUBS_H_
+#define Z3NATIVE_STUBS_H_
+
+#if defined _WIN32 || defined __CYGWIN__
+  #ifdef __GNUC__
+    #define DLL_PUBLIC __attribute__ ((dllexport))
+  #else
+    #define DLL_PUBLIC __declspec(dllexport)
+  #endif
+  #define DLL_LOCAL
+#else
+  #if __GNUC__ >= 4
+    #define DLL_PUBLIC __attribute__ ((visibility ("default")))
+    #define DLL_LOCAL  __attribute__ ((visibility ("hidden")))
+  #else
+    #define DLL_PUBLIC
+    #define DLL_LOCAL
+  #endif
+#endif
+	
+#endif

src/api/python/z3.py

@@ -285,6 +285,9 @@ class AstRef(Z3PPObject):
     def __repr__(self):
         return obj_to_string(self)
 
+    def __eq__(self, other):
+        return self.eq(other)
+
     def __hash__(self):
         return self.hash()
 
@@ -531,6 +534,10 @@ class SortRef(AstRef):
         """
         return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
 
+    def __hash__(self):
+        """ Hash code. """
+        AstRef.__hash__(self)
+
 def is_sort(s):
     """Return `True` if `s` is a Z3 sort.
     
@@ -793,6 +800,10 @@ class ExprRef(AstRef):
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
 
+    def __hash__(self):
+        """ Hash code. """
+        AstRef.__hash__(self)
+
     def __ne__(self, other):
         """Return a Z3 expression that represents the constraint `self != other`.