def __init__(self, install_dir, bindings_dir, solver_version,
                 mirror_link=None, yicespy_version='HEAD'):

        self.needs_compilation = False
        if self.os_name == "darwin" or self.needs_compilation:
            sysctl = self.run("sysctl -a", get_output=True, suppress_stderr=True)
            if 'hw.optional.avx2_0: 1' in sysctl:
                # No need to compile, see http://yices.csl.sri.com/faq.html
                pack = "x86_64-apple-darwin16.7.0-static-gmp"
            else:
                self.needs_compilation = True
                pack = "src"
        else:
            pack = "x86_64-pc-linux-gnu-static-gmp"

        archive_name = "yices-%s-%s.tar.gz" % (solver_version, pack)
        native_link = "http://yices.csl.sri.com/releases/{solver_version}/{archive_name}"
        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
                                 archive_name=archive_name,
                                 native_link=native_link,
                                 mirror_link=mirror_link)

        self.extract_path = os.path.join(self.base_dir, "yices-%s" % self.solver_version)
        self.yices_path = os.path.join(self.bindings_dir, "yices_bin")
        self.yicespy_git_version = yicespy_version

    def __init__(self, install_dir, bindings_dir, solver_version,
                 mirror_link=None):

        # Getting the right archive name
        os_name = self.os_name
        arch = self.architecture
        ext = "tar.gz"
        if os_name == "windows":
            ext = "zip"
            arch = "msvc"
            if self.architecture == "x86_64":
                os_name = "win64"
            else:
                os_name = "win32"
        elif os_name == "darwin":
            os_name = "darwin-libcxx"

        archive_name = "mathsat-%s-%s-%s.%s" % (solver_version, os_name,
                                                arch, ext)

        native_link = "http://mathsat.fbk.eu/download.php?file={archive_name}"

        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
                                 archive_name=archive_name,
                                 native_link = native_link,
                                 mirror_link=mirror_link)

        self.python_bindings_dir = os.path.join(self.extract_path, "python")

    def compile(self):
        # Select the correct Makefile to be used
        makefile = "Makefile"
        if self.architecture == "x86_64":
            makefile = "Makefile_64bit"

        # Find python-config
        command = self.find_python_config()
        if command is None:
            raise OSError("No installation of python-config found on this system."
                          " Please install python-config for this version of python.")
        print("Found python-config in %s" % command)

        # Build the pycudd
        prefix = None
        p = subprocess.Popen([command, '--includes'], stdout=subprocess.PIPE, stderr=None)
        prefix = p.stdout.read()
        if PY2:
            pass # Prefix is already a string
        else:
            # > PY3 Prefix is binary data
            prefix = prefix.decode()

        if not prefix or len(prefix) == 0:
            prefix = "/usr"

        SolverInstaller.run("make -C %s -f %s PYTHON_INCL=%s" %
                            (self.extract_path, makefile, prefix))

    def compile(self):
        # Unpack
        SolverInstaller.untar(os.path.join(self.base_dir, self.archive_name),
                              self.extract_path)

        # Build lingeling
        SolverInstaller.run("bash ./contrib/setup-lingeling.sh",
                            directory=self.extract_path)

        # Build Btor
        SolverInstaller.run("bash ./contrib/setup-btor2tools.sh",
                            directory=self.extract_path)

        # Inject Python library and include paths into CMake because Boolector
        # search system can be fooled in some systems
        import distutils.sysconfig as sysconfig
        PYTHON_LIBRARY = sysconfig.get_config_var('LIBDIR')
        PYTHON_INCLUDE_DIR = sysconfig.get_python_inc()
        CMAKE_OPTS = ' -DPYTHON_LIBRARY=' + PYTHON_LIBRARY
        CMAKE_OPTS += ' -DPYTHON_INCLUDE_DIR=' + PYTHON_INCLUDE_DIR

        # Build Boolector Solver
        SolverInstaller.run("bash ./configure.sh --python",
                            directory=self.extract_path,
                            env_variables={"CMAKE_OPTS": CMAKE_OPTS})

        SolverInstaller.run("make -j2",
                            directory=os.path.join(self.extract_path, "build"))

    def __init__(self, install_dir, bindings_dir, solver_version,
                 mirror_link=None, osx=None, git_version=None, commit=None):
        arch = self.architecture
        if arch == "x86_64":
            arch = "x64"

        system = self.os_name
        if system == "linux":
            system = "ubuntu-14.04"
        elif system == "darwin":
            system = "osx-%s" % osx
        elif system == "windows":
            system = "win"

        if git_version is None:
            # Stable versions template
            archive_name = "z3-%s.%s-%s-%s.zip" % (solver_version, commit, arch, system)
            native_link = "https://github.com/Z3Prover/z3/releases/download/z3-" + solver_version + "/{archive_name}"
            # print(native_link)
        else:
            # Nightly build template
            archive_name = "z3-%s.%s-%s-%s.zip" % (solver_version, git_version, arch, system)
            native_link = "https://github.com/pysmt/Z3bin/blob/master/nightly/{archive_name}?raw=true"

        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
                                 archive_name=archive_name,
                                 native_link=native_link,
                                 mirror_link=mirror_link)

    def compile(self):
        # Prepare an empty folder for installing yices
        SolverInstaller.clean_dir(self.yices_path)

        SolverInstaller.run("bash ./install-yices %s" % self.yices_path,
                            directory=self.extract_path)

        self.install_yicespy()

 def __init__(self, install_dir, bindings_dir, solver_version, mirror_link=None):
     SolverInstaller.__init__(
         self,
         install_dir=install_dir,
         bindings_dir=bindings_dir,
         solver_version=solver_version,
         mirror_link=mirror_link,
     )

 def __init__(self, install_dir, bindings_dir, solver_version,
              mirror_link=None):
     archive_name = "boolector-%s-with-lingeling-b85.tar.bz2" % solver_version
     native_link = "http://fmv.jku.at/boolector/{archive_name}"
     SolverInstaller.__init__(self, install_dir=install_dir,
                              bindings_dir=bindings_dir,
                              solver_version=solver_version,
                              archive_name=archive_name,
                              native_link=native_link,
                              mirror_link=mirror_link)

 def __init__(self, install_dir, bindings_dir, solver_version,
              pypicosat_minor_version, mirror_link=None):
     self.pypicosat_minor_version = pypicosat_minor_version
     self.complete_version = None
     SolverInstaller.__init__(self, install_dir=install_dir,
                              bindings_dir=bindings_dir,
                              solver_version=solver_version,
                              mirror_link=mirror_link,
                              native_link=None,
                              archive_name=None)

    def move(self):
        libdir = "lib.%s-%s-%s" % (self.os_name, self.architecture,
                                   self.python_version)
        bdir = os.path.join(self.extract_path, "build")
        sodir = os.path.join(bdir, libdir)

        for f in os.listdir(sodir):
            if f.endswith(".so"):
                SolverInstaller.mv(os.path.join(sodir, f), self.bindings_dir)
        SolverInstaller.mv(os.path.join(self.extract_path, "picosat.py"), self.bindings_dir)

    def compile(self):
        # Select the correct Makefile to be used
        makefile = "Makefile"
        if self.architecture == "x86_64":
            makefile = "Makefile_64bit"

        import distutils.sysconfig as sysconfig
        PYTHON_INCLUDE_DIR = sysconfig.get_python_inc()
        SolverInstaller.run("make -C %s -f %s PYTHON_INCL=-I%s" %
                            (self.extract_path, makefile, PYTHON_INCLUDE_DIR))

 def __init__(self, install_dir, bindings_dir, solver_version,
              mirror_link=None, git_version='HEAD'):
     archive_name = "repycudd-%s.tar.gz" % git_version
     native_link = "https://codeload.github.com/pysmt/repycudd/tar.gz/%s" % git_version
     SolverInstaller.__init__(self, install_dir=install_dir,
                              bindings_dir=bindings_dir,
                              solver_version=solver_version,
                              archive_name=archive_name,
                              native_link=native_link,
                              mirror_link=mirror_link)
     self.git_version = git_version

 def __init__(self, install_dir, bindings_dir, solver_version,
              mirror_link=None, git_version='HEAD'):
     archive_name = "CVC4-%s.tar.gz" % git_version
     native_link = "https://codeload.github.com/CVC4/CVC4/tar.gz/%s" % (git_version)
     SolverInstaller.__init__(self, install_dir=install_dir,
                              bindings_dir=bindings_dir,
                              solver_version=solver_version,
                              archive_name=archive_name,
                              native_link=native_link,
                              mirror_link=mirror_link)
     self.git_version = git_version
     self.bin_path = os.path.join(self.bindings_dir, "CVC4_bin")

    def __init__(self, install_dir, bindings_dir, solver_version,
                 mirror_link=None):
        pack = "x86_64-unknown-linux-gnu-static-gmp"
        archive_name = "yices-%s-%s.tar.gz" % (solver_version, pack)
        native_link = "http://yices.csl.sri.com/cgi-bin/yices2-newnewdownload.cgi?file={archive_name}&accept=I+Agree"
        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
                                 archive_name=archive_name,
                                 native_link=native_link,
                                 mirror_link=mirror_link)

        self.extract_path = os.path.join(self.base_dir, "yices-%s" % self.solver_version)
        self.yices_path = os.path.join(self.bindings_dir, "yices_bin")

    def move(self):
        libdir = "lib.%s-%s-%s" % (self.os_name, self.architecture,
                                   self.python_version)
        if self.os_name == "darwin":
            osx_version = ".".join(platform.mac_ver()[0].split(".")[:2])
            libdir = libdir.replace("darwin", "macosx-%s" % osx_version)
        pdir = self.python_bindings_dir
        bdir = os.path.join(pdir, "build")
        sodir = os.path.join(bdir, libdir)

        for f in os.listdir(sodir):
            if f.endswith(".so"):
                SolverInstaller.mv(os.path.join(sodir, f), self.bindings_dir)
        SolverInstaller.mv(os.path.join(pdir, "mathsat.py"), self.bindings_dir)

    def download(self):
        self.complete_version = "%s.%s" % (self.solver_version,
                                           self.pypicosat_minor_version)
        pypi_link = "http://pypi.python.org/pypi/pyPicoSAT/%s/json" % self.complete_version
        response = urllib2.urlopen(pypi_link)
        reader = codecs.getreader("utf-8")
        pypi_json = json.load(reader(response))

        self.native_link = pypi_json["urls"][0]["url"]
        self.archive_name = pypi_json["urls"][0]["filename"]
        self.archive_path = os.path.join(self.base_dir, self.archive_name)
        self.extract_path = os.path.join(self.base_dir, self.archive_name[:-7])

        SolverInstaller.download(self)

    def compile(self):
        # Prepare the building system
        SolverInstaller.run("bash autogen.sh", directory=self.extract_path)

        # Build ANTLR
        SolverInstaller.run("bash get-antlr-3.4",
                            directory=os.path.join(self.extract_path, "contrib"))

        # Configure and build CVC4
        config = "./configure --prefix={bin_path} \
                              --enable-language-bindings=python \
                              --with-antlr-dir={dir_path}/antlr-3.4 ANTLR={dir_path}/antlr-3.4/bin/antlr3;\
                  make; \
                  make install ".format(bin_path=self.bin_path, dir_path=self.extract_path)
        if os.path.exists(sys.executable+"-config"):
            pyconfig = {"PYTHON_CONFIG": sys.executable+"-config"}
        else:
            pyconfig = {}
        SolverInstaller.run(config,
                            directory=self.extract_path,
                            env_variables=pyconfig)

        # Fix the paths of the bindings
        SolverInstaller.run("cp CVC4.so.3.0.0 _CVC4.so",
                            directory=os.path.join(self.bin_path, "lib/pyshared"))

    def __init__(self, install_dir, bindings_dir, solver_version,
                 mirror_link=None):
        archive_name = "mathsat-%s-%s-%s.tar.gz" % (solver_version,
                                                    self.os_name,
                                                    self.architecture)
        native_link = "http://mathsat.fbk.eu/download.php?file={archive_name}"
        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
                                 archive_name=archive_name,
                                 native_link = native_link,
                                 mirror_link=mirror_link)

        self.python_bindings_dir = os.path.join(self.extract_path, "python")

    def compile(self):
        # Build ANTLR
        SolverInstaller.run("bash get-antlr-3.4",
                            directory=os.path.join(self.extract_path, "contrib"))

        # Build ABC
        # SolverInstaller.run("bash get-abc",
        #                     directory=os.path.join(self.extract_path, "contrib"))
        # Build GLPK
        # We could configure with --gpl --best, but this takes forever to build

        # Inject Python library and include paths into CMake because CVC4 search
        # system can be fooled in some systems
        import distutils.sysconfig as sysconfig
        PYTHON_LIBRARY = sysconfig.get_config_var('LIBDIR')
        PYTHON_INCLUDE_DIR = sysconfig.get_python_inc()
        SolverInstaller.run(['sed', '-i',
                             's|cmake_opts=""|cmake_opts="-DPYTHON_LIBRARY=' + PYTHON_LIBRARY + ' -DPYTHON_INCLUDE_DIR=' + PYTHON_INCLUDE_DIR + '"|g',
                             './configure.sh'], directory=self.extract_path)

        # Configure and build CVC4
        config_cmd = "./configure.sh --language-bindings=python \
                                     --python%s" % self.python_version[0]

        if os.path.exists(sys.executable+"-config"):
            pyconfig = {"PYTHON_CONFIG": sys.executable+"-config"}
        else:
            pyconfig = {}

        SolverInstaller.run(config_cmd, directory=self.extract_path,
                            env_variables=pyconfig)
        SolverInstaller.run("make", directory=self.build_path,
                            env_variables=pyconfig)

    def compile(self):
        # First build
        SolverInstaller.run("make", directory=self.extract_path)

        # Reconfigure and build python bindings
        SolverInstaller.run("bash ./configure.sh -fPIC",
                          directory=os.path.join(self.extract_path, "lingeling"))
        SolverInstaller.run("make",
                          directory=os.path.join(self.extract_path, "lingeling"))

        SolverInstaller.run("bash ./configure -python",
                          directory=os.path.join(self.extract_path, "boolector"))
        SolverInstaller.run("make",
                          directory=os.path.join(self.extract_path, "boolector"))