Boolector: Upgrade to 3.0.1-pre (7f5d32) (#514)

Boolector: Upgrade to 3.0.1-pre (7f5d32)
pysmt · Jan 27, 2019 · 3798ed50b90ffa37663002abccf8dd72e5c387ee · 3798ed5
1 parent d3fcb7d
commit 3798ed50b90ffa37663002abccf8dd72e5c387ee
diff --git a/ci/travis_before_install.sh b/ci/travis_before_install.sh
@@ -63,8 +63,11 @@ fi
 python ${DIR}/check_python_version.py "${TRAVIS_PYTHON_VERSION}"
 # Install latest version of SWIG
-  
-git clone https://github.com/swig/swig.git
-  
-cd swig
-  
-git checkout rel-3.0.12
-  
-./autogen.sh && ./configure && make
-  
-sudo make install
+  
+if [ "${PYSMT_SOLVER}" == "bdd" ] || [ "${PYSMT_SOLVER}" == "cvc4" ] || [ "${PYSMT_SOLVER}" == "btor" ] || [ "${PYSMT_SOLVER}" == "all" ]
+  
+then
+  
+    git clone https://github.com/swig/swig.git
+  
+    cd swig
+  
+    git checkout rel-3.0.12
+  
+    ./autogen.sh && ./configure && make
+  
+    sudo make install
+  
+fi
diff --git a/ci/travis_install.sh b/ci/travis_install.sh
@@ -50,16 +50,16 @@ then
    $PIP_INSTALL gmpy2;
 fi
+  
+
+  
+#
+  
+# Install Solvers
+  
+#
 # Adding Python 3.7 library path to GCC search
 if [ "${TRAVIS_PYTHON_VERSION}" == "3.7" ]; then
    export LIBRARY_PATH="/opt/python/3.7.1/lib:${LIBRARY_PATH}"
    export CPATH="/opt/python/3.7.1/include/python3.7m:${CPATH}"
 fi
-  
-
-  
-#
-  
-# Install Solvers
-  
-#
 if [ "${PYSMT_CUSTOM_BINDINGS_PATH}" == "TRUE" ]; then
    PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER}_${TRAVIS_OS_NAME}"
    PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER_FOLDER//,/$'_'}"

diff --git a/pysmt/cmd/check_version.py b/pysmt/cmd/check_version.py
@@ -38,7 +38,7 @@ def check_version(module):
                version = m.group(1)
        elif module == "btor":
-  
-            import boolector
+  
+            import pyboolector
            version = "OK" # Just checking if import succeeds
        elif module == "cvc4":

diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
@@ -41,15 +41,16 @@
              {"osx": "10.14.1", "commit": "d6df51951f4c"}),
    Installer(YicesInstaller,   "2.6.0",
              {"yicespy_version": "f0768ffeec15ea310f830d10878971c9998454ac"}),
-  
-    Installer(BtorInstaller,    "2.4.1",
-  
-              {"lingeling_version": "bbc"}),
+  
+    Installer(BtorInstaller,    "3.0.1-pre",
+  
+              {"git_version" : "8062caf14f797a3aa85bf310705973468874e127"}),
    Installer(PicoSATInstaller, "965",
              {"pypicosat_minor_version" : "1708010052"}),
    Installer(CuddInstaller,    "2.0.3",
              {"git_version" : "ecb03d6d231273343178f566cc4d7258dcce52b4"}),
 ]
+  
+
 def get_requested_solvers():
    """Parses the PYSMT_SOLVER env variable to extract requirements to fulfill"""

diff --git a/pysmt/cmd/installers/btor.py b/pysmt/cmd/installers/btor.py
@@ -11,21 +11,27 @@
 # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 # See the License for the specific language governing permissions and
 # limitations under the License.
-  
-import sys
 import os
-  
-from pysmt.cmd.installers.base import SolverInstaller, TemporaryPath
+  
+from pysmt.cmd.installers.base import SolverInstaller
 class BtorInstaller(SolverInstaller):
    SOLVER = "btor"
    def __init__(self, install_dir, bindings_dir, solver_version,
-  
-                 mirror_link=None, lingeling_version=None):
-  
-        archive_name = "boolector-%s-with-lingeling-%s.tar.bz2" % \
-  
-                       (solver_version, lingeling_version)
-  
-        native_link = "http://fmv.jku.at/boolector/{archive_name}"
+  
+                 mirror_link=None, git_version=None):
+  
+        native_link = "https://github.com/Boolector/boolector/archive/%s.tar.gz"
+  
+        archive_name = "boolector-%s.tar.gz"
+  
+
+  
+        if git_version:
+  
+            native_link = native_link % git_version
+  
+            archive_name = archive_name % git_version
+  
+        else:
+  
+            native_link = native_link % solver_version
+  
+            archive_name = archive_name % solver_version
+  
+
        SolverInstaller.__init__(self, install_dir=install_dir,
                                 bindings_dir=bindings_dir,
                                 solver_version=solver_version,
@@ -34,53 +40,60 @@ def __init__(self, install_dir, bindings_dir, solver_version,
                                 mirror_link=mirror_link)
    def compile(self):
-  
-        import glob
+  
+        # Unpack
+  
+        SolverInstaller.untar(os.path.join(self.base_dir, self.archive_name),
+  
+                              self.extract_path)
+  
+
        # Build lingeling
-  
-        lingeling_archive = glob.glob(os.path.join(self.extract_path,
-  
-                                                   "archives", "lingeling-*.tar.gz"))[0]
-  
-        SolverInstaller.untar(lingeling_archive, self.extract_path)
-  
-        lingeling_dir = glob.glob(os.path.join(self.extract_path,
-  
-                                               "lingeling*"))[0]
-  
-        SolverInstaller.mv(lingeling_dir,
-  
-                           os.path.join(self.extract_path, "lingeling"))
-  
-        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 ./contrib/setup-lingeling.sh",
+  
+                            directory=self.extract_path)
        # Build Btor
-  
-        boolector_archive = glob.glob(os.path.join(self.extract_path,
-  
-                                                   "archives", "boolector-*.tar.gz"))[0]
-  
-        SolverInstaller.untar(boolector_archive, self.extract_path)
-  
-        boolector_dir = glob.glob(os.path.join(self.extract_path,
-  
-                                               "boolector*"))[0]
-  
-        SolverInstaller.mv(boolector_dir,
-  
-                           os.path.join(self.extract_path, "boolector"))
+  
+        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()
+  
+        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)
-  
-        SolverInstaller.run("bash ./configure.sh -python",
-  
-                          directory=os.path.join(self.extract_path, "boolector"))
-  
-        SolverInstaller.run("make",
-  
-                          directory=os.path.join(self.extract_path, "boolector"))
+  
+        # Build Boolector Solver
+  
+        SolverInstaller.run("bash ./configure.sh --python",
+  
+                            directory=self.extract_path)
-  
-        # Redo this step to make sure the correct version of python is used
-  
-        SolverInstaller.run_python("setup.py build_ext -b build -t build/api/python/tmp",
-  
-                                   directory=os.path.join(self.extract_path, "boolector"))
+  
+        SolverInstaller.run("make -j2",
+  
+                            directory=os.path.join(self.extract_path, "build"))
    def move(self):
-  
-        bdir = os.path.join(self.extract_path, "boolector/build")
-  
-        for f in os.listdir(bdir):
-  
-            if f.startswith("boolector") and f.endswith(".so"):
-  
-                SolverInstaller.mv(os.path.join(bdir, f), self.bindings_dir)
+  
+        libdir = os.path.join(self.extract_path, "build", "lib")
+  
+        for f in os.listdir(libdir):
+  
+            if f.startswith("pyboolector") and f.endswith(".so"):
+  
+                SolverInstaller.mv(os.path.join(libdir, f),
+  
+                                   self.bindings_dir)
+  
+
    def get_installed_version(self):
+  
+        import re
+  
+
        res = self.get_installed_version_script(self.bindings_dir, "btor")
        version = None
        if res == "OK":
-  
-            vfile = os.path.join(self.extract_path, "boolector", "VERSION")
+  
+            vfile = os.path.join(self.extract_path, "CMakeLists.txt")
            try:
                with open(vfile) as f:
-  
-                    version = f.read().strip()
+  
+                    content = f.read().strip()
+  
+                    m = re.search('set\(VERSION "(.*)"\)', content)
+  
+                if m is not None:
+  
+                    version = m.group(1)
            except OSError:
+  
+                print("File not found")
+  
+                return None
+  
+            except IOError:
+  
+                print("IO Error")
                return None
        return version
diff --git a/pysmt/cmd/installers/cvc4.py b/pysmt/cmd/installers/cvc4.py
@@ -16,7 +16,7 @@
 import os
 import sys
-  
-from pysmt.cmd.installers.base import SolverInstaller, TemporaryPath
+  
+from pysmt.cmd.installers.base import SolverInstaller
 class CVC4Installer(SolverInstaller):