From d7930da9a80caeb41ca7d51c76e092ac6417185d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Oct 2012 17:08:39 -0700
Subject: [PATCH] Added support for windows DLLs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 scripts/config-vs-debug.mk          |  5 +++++
 scripts/config-vs-release.mk        |  5 +++++
 scripts/mk_make.py                  |  2 +-
 scripts/mk_util.py                  | 16 ++++++++++++----
 src/api/dll/{z3.def => api_dll.def} |  0
 src/bindings/python/z3core.py       |  2 +-
 6 files changed, 24 insertions(+), 6 deletions(-)
 rename src/api/dll/{z3.def => api_dll.def} (100%)

diff --git a/scripts/config-vs-debug.mk b/scripts/config-vs-debug.mk
index c4ff2dba4..2c890f5de 100644
--- a/scripts/config-vs-debug.mk
+++ b/scripts/config-vs-debug.mk
@@ -12,4 +12,9 @@ LINK_FLAGS=/nologo /MDd
 LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:"8388608" /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
 LINK_OUT_FLAG=/Fe
 
+SO_EXT=.dll
+SLINK=cl
+SLINK_FLAGS=/nologo /LDd
+SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:"8388608" /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO
+SLINK_OUT_FLAG=/Fe
 
diff --git a/scripts/config-vs-release.mk b/scripts/config-vs-release.mk
index 5c3ee5885..89a4c0520 100644
--- a/scripts/config-vs-release.mk
+++ b/scripts/config-vs-release.mk
@@ -12,4 +12,9 @@ LINK_FLAGS=/nologo /MD
 LINK_EXTRA_FLAGS=/link /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:"8388608" /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
 LINK_OUT_FLAG=/Fe
 
+SO_EXT=.dll
+SLINK=cl
+SLINK_FLAGS=/nologo /LD
+SLINK_EXTRA_FLAGS=/link /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:"8388608" /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO
+SLINK_OUT_FLAG=/Fe
 
diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index f3ecdbdcd..da39fd709 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -62,6 +62,6 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe',
 add_lib('api', ['portfolio', 'user_plugin'])
 add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
 add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
-add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='libz3')
+add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3')
 
 mk_makefile()
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index cd49ee170..32faf2504 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -312,8 +312,10 @@ class DLLComponent(Component):
         global _Name2Component
         Component.mk_makefile(self, out)
         # generate rule for (SO_EXT)
-
-        dllfile = '%s$(SO_EXT)' % self.dll_name
+        if IS_WINDOW:
+            dllfile = '%s$(SO_EXT)' % self.dll_name
+        else:
+            dllfile = '%libs$(SO_EXT)' % self.dll_name
         out.write('%s:' % dllfile)
         deps = sort_components(self.deps)
         objs = []
@@ -334,7 +336,10 @@ class DLLComponent(Component):
         for dep in deps:
             c_dep = _Name2Component[dep]
             out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
-        out.write(' $(SLINK_EXTRA_FLAGS)\n')
+        out.write(' $(SLINK_EXTRA_FLAGS)')
+        if IS_WINDOW:
+            out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name))
+        out.write('\n')
         out.write('%s: %s\n\n' % (self.name, dllfile))
 
     # All DLLs are included in the all: rule
@@ -405,6 +410,9 @@ def mk_makefile():
             print "  compilation mode: Debug"
         else:
             print "  compilation mode: Release"
-        print "Type 'cd %s; make' to build Z3" % BUILD_DIR
+        if IS_WINDOW:
+            print "Type 'cd %s && nmake to build Z3" % BUILD_DIR
+        else:
+            print "Type 'cd %s; make' to build Z3" % BUILD_DIR
         
 
diff --git a/src/api/dll/z3.def b/src/api/dll/api_dll.def
similarity index 100%
rename from src/api/dll/z3.def
rename to src/api/dll/api_dll.def
diff --git a/src/bindings/python/z3core.py b/src/bindings/python/z3core.py
index 9d346ff90..26f344ff1 100644
--- a/src/bindings/python/z3core.py
+++ b/src/bindings/python/z3core.py
@@ -6,7 +6,7 @@ from z3consts import *
 
 def _find_lib():
   _dir = os.path.dirname(os.path.abspath(__file__))
-  libs = ['z3.dll', 'libz3.so', 'libz3.dylib']
+  libs = ['z3.dll', 'libz3.so', 'libz3.dylib', 'libz3.dll']
   if sys.maxsize > 2**32:
     locs = [_dir, '%s%s..%sx64%sexternal' % (_dir, os.sep, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)]
   else: