Merge pull request #385 from fontealpina/master

Windows: Add support for installing Z3

appveyor.yml

@@ -9,18 +9,45 @@ environment:
     - PYTHON: "C:\\Python27"
       PYTHON_VERSION: "2.7.8"
       PYTHON_ARCH: "32"
+      PYSMT_SOLVER: "None"
 
-    # - PYTHON: "C:\\Python27-x64"
-    #   PYTHON_VERSION: "2.7.8"
-    #   PYTHON_ARCH: "64"
+    - PYTHON: "C:\\Python27-x64"
+      PYTHON_VERSION: "2.7.8"
+      PYTHON_ARCH: "64"
+      PYSMT_SOLVER: "None"
 
-    # - PYTHON: "C:\\Python34"
-    #   PYTHON_VERSION: "3.4.1"
-    #   PYTHON_ARCH: "32"
+    - PYTHON: "C:\\Python35"
+      PYTHON_VERSION: "3.5.2"
+      PYTHON_ARCH: "32"
+      PYSMT_SOLVER: "None"
 
-    - PYTHON: "C:\\Python34-x64"
-      PYTHON_VERSION: "3.4.1"
+    - PYTHON: "C:\\Python35-x64"
+      PYTHON_VERSION: "3.5.2"
       PYTHON_ARCH: "64"
+      PYSMT_SOLVER: "None"
+
+
+    - PYTHON: "C:\\Python27"
+      PYTHON_VERSION: "2.7.8"
+      PYTHON_ARCH: "32"
+      PYSMT_SOLVER: "z3"
+
+    - PYTHON: "C:\\Python27-x64"
+      PYTHON_VERSION: "2.7.8"
+      PYTHON_ARCH: "64"
+      PYSMT_SOLVER: "z3"
+
+    - PYTHON: "C:\\Python35"
+      PYTHON_VERSION: "3.5.2"
+      PYTHON_ARCH: "32"
+      PYSMT_SOLVER: "z3"
+
+    - PYTHON: "C:\\Python35-x64"
+      PYTHON_VERSION: "3.5.2"
+      PYTHON_ARCH: "64"
+      PYSMT_SOLVER: "z3"
+
+
 
 install:
   - ECHO "Filesystem root:"
@@ -44,11 +71,19 @@ install:
 
   - "%CMD_IN_ENV% pip install -r dev-requirements.txt"
 
-# MG: Build is where we probably want to build the solvers
-build: false  # Not a C# project, build stuff at the test step instead.
+  # Install the solvers
+  - "%CMD_IN_ENV% python install.py --confirm-agreement"
+
+  # Set the pythonpath
+  - "python install.py --env > bindings_path.txt"
+  - "SET /p BINDINGS_CMD=<bindings_path.txt"
+  - "%BINDINGS_CMD%"
+  - ECHO "PythonPath=%PYTHONPATH%"
+
+build: false
 
 test_script:
-  # Build the compiled extension and run the project tests
+  - "%CMD_IN_ENV% python install.py --check"
   - "%CMD_IN_ENV% nosetests -v "
 
 # after_test:

pysmt/cmd/install.py

@@ -17,6 +17,7 @@
 import os
 import argparse
 import sys
+import platform
 
 from collections import namedtuple
 
@@ -133,12 +134,14 @@ def parse_options():
                         action='store_true', default=False,
                         help='Confirm that you agree with the licenses of the\
                         solvers and skip the interactive question')
-
+
+    install_path_default = os.path.join("~", ".smt_solvers")
     parser.add_argument('--install-path', dest='install_path',
-                        type=str, default="~/.smt_solvers",
+                        type=str, default=install_path_default,
                         help='The folder to use for the installation')
 
-    py_bindings = "~/.smt_solvers/python-bindings-%d.%d" % sys.version_info[0:2]
+    py_bindings = os.path.join(install_path_default, 
+                               "python-bindings-%d.%d" % sys.version_info[0:2])
     parser.add_argument('--bindings-path', dest='bindings_path',
                         type=str, default=py_bindings,
                         help='The folder to use for the bindings')
@@ -214,7 +217,10 @@ def main():
 
     elif options.env:
         bindings_dir= os.path.expanduser(options.bindings_path)
-        print("export PYTHONPATH=\""+ bindings_dir + ":${PYTHONPATH}\"")
+        if platform.system().lower() == "windows":
+            print("set PYTHONPATH=" + bindings_dir + ";%PYTHONPATH%")
+        else:
+            print("export PYTHONPATH=\"" + bindings_dir + ":${PYTHONPATH}\"")
 
     else:
         if len(solvers_to_install) == 0:

pysmt/cmd/installers/base.py

@@ -18,6 +18,7 @@
 import zipfile
 import tarfile
 import six
+import struct
 
 from contextlib import contextmanager
 
@@ -75,7 +76,11 @@ def os_name(self):
 
     @property
     def architecture(self):
-        return platform.machine()
+        bits = 8 * struct.calcsize("P")
+        if bits == 64:
+            return "x86_64"
+        else:
+            return "x86"
 
     @property
     def python_version(self):

pysmt/cmd/installers/z3.py

@@ -35,6 +35,8 @@ def __init__(self, install_dir, bindings_dir, solver_version,
             system = "ubuntu-14.04"
         elif system == "darwin":
             system = "osx-%s" % osx
+        elif system == "windows":
+            system = "win"
 
         archive_name = "z3-%s-%s-%s.zip" % (solver_version, arch, system)
         native_link = "https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/{archive_name}"
@@ -62,6 +64,9 @@ def move(self):
             files += [ "libz3.so" ]
         elif self.os_name == "darwin":
             files += [ "libz3.a", "libz3.dylib" ]
+        elif self.os_name == "windows":
+            files += [ "libz3.dll", "libz3.lib" ]
+
         for f in files:
             SolverInstaller.mv(os.path.join(bpath, f), self.bindings_dir)