Merge 48377d9 into 7cee6ea

.travis.yml

@@ -37,6 +37,11 @@ matrix:
     dist: xenial
     python: 3.7
     env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"
+  - os: linux
+    sudo: required
+    dist: xenial
+    python: 3.7
+    env: PYSMT_SOLVER="optimsat"  PYSMT_GMPY="FALSE"
   - os: linux
     sudo: required
     dist: xenial
@@ -89,6 +94,9 @@ matrix:
   - os: linux
     python: 2.7
     env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="optimsat"  PYSMT_GMPY="FALSE"
   - os: linux
     python: 2.7
     env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"
@@ -148,6 +156,11 @@ matrix:
     language: generic
     python: 3.6
     env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9.4
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="optimsat"  PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
   - os: osx
     osx_image: xcode9.4
     language: generic
@@ -214,7 +227,6 @@ cache:
   #- ${HOME}/python_bindings
   - ${VIRTUAL_ENV}
 
-
 addons:
   apt:
     packages:
@@ -234,18 +246,14 @@ addons:
     - python3-all-dev
     - libmpc-dev
 
-
 before_install:
   - "./ci/travis_before_install.sh"
 
-
 install:
   - "./ci/travis_install.sh"
 
-
 script:
   - "./ci/travis_script.sh"
 
-
 after_success:
   - "./ci/travis_after_success.sh"

pysmt/cmd/check_version.py

@@ -28,7 +28,27 @@ def check_version(module):
             version_str = mathsat.msat_get_version()
             m = re.match(r"^MathSAT5 version (\d+\.\d+\.\d+) .*$", version_str)
             if m is not None:
+                # Do not confuse msat with optimsat
                 version = m.group(1)
+                c = None
+                try:
+                    c = mathsat.msat_objective
+                except AttributeError:
+                    pass
+                if c is not None:
+                    version = None
+
+        elif module == "optimsat":
+            import mathsat
+            version_str = mathsat.msat_get_version()
+            m = re.match(r"^MathSAT5 version (\d+\.\d+\.\d+) .*$", version_str)
+            if m is not None:
+                # Do not confuse msat with optimsat
+                version = m.group(1)
+                try:
+                    mathsat.msat_objective
+                except AttributeError:
+                    version = None
 
         elif module == "cudd":
             import repycudd

pysmt/cmd/install.py

@@ -23,7 +23,7 @@
 
 from pysmt.cmd.installers import MSatInstaller, Z3Installer, PicoSATInstaller
 from pysmt.cmd.installers import CVC4Installer, YicesInstaller, BtorInstaller
-from pysmt.cmd.installers import CuddInstaller
+from pysmt.cmd.installers import CuddInstaller, OptiMSatInstaller
 from pysmt.cmd.installers.base import solver_install_site
 
 from pysmt.environment import get_env
@@ -38,7 +38,8 @@
               Installer(YicesInstaller,   "2.6.0", {"yicespy_version": "f0768ffeec15ea310f830d10878971c9998454ac"}),
               Installer(BtorInstaller,    "2.4.1", {"lingeling_version": "bbc"}),
               Installer(PicoSATInstaller, "965", {"pypicosat_minor_version" : "1708010052"}),
-              Installer(CuddInstaller,    "2.0.3", {"git_version" : "75fe055c2a736a3ac3e971c1ade108b815edc96c"})]
+              Installer(CuddInstaller,    "2.0.3", {"git_version" : "75fe055c2a736a3ac3e971c1ade108b815edc96c"}),
+              Installer(OptiMSatInstaller, "1.5.0", {})]
 
 
 def get_requested_solvers():
@@ -50,7 +51,10 @@ def get_requested_solvers():
         keys = requested_solvers_str.split(",")
         requested_solvers = [x.lower().strip() for x in keys]
         if "all" in requested_solvers:
-            requested_solvers = [x.InstallerClass.SOLVER for x in INSTALLERS]
+            # Skip OptiMathSAT in the 'all' case because currently
+            # msat and optimsat cannot co-exist
+            requested_solvers = [x.InstallerClass.SOLVER for x in INSTALLERS
+                                 if x.InstallerClass.SOLVER != 'optimsat']
     return requested_solvers
 
 
@@ -200,6 +204,9 @@ def main():
     all_solvers = options.all_solvers
     for i in INSTALLERS:
         name = i.InstallerClass.SOLVER
+        if all_solvers and name == 'optimsat':
+            continue # Skip OptiMathSAT in the --all case because currently
+                     # msat and optimsat cannot co-exist
         if all_solvers or getattr(options, name):
             solvers_to_install.append(i)
 

pysmt/cmd/installers/__init__.py

@@ -19,6 +19,7 @@
 from pysmt.cmd.installers.btor import BtorInstaller
 from pysmt.cmd.installers.pico import PicoSATInstaller
 from pysmt.cmd.installers.bdd import CuddInstaller
+from pysmt.cmd.installers.optimsat import OptiMSatInstaller
 
 assert MSatInstaller and Z3Installer and CVC4Installer and YicesInstaller
-assert BtorInstaller and PicoSATInstaller and CuddInstaller
+assert BtorInstaller and PicoSATInstaller and CuddInstaller and OptiMSatInstaller

pysmt/cmd/installers/optimsat.py

@@ -0,0 +1,84 @@
+# Copyright 2014 Andrea Micheli and Marco Gario
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# 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 os
+import glob
+
+from pysmt.cmd.installers.base import SolverInstaller
+
+
+class OptiMSatInstaller(SolverInstaller):
+
+    SOLVER = "optimsat"
+
+    def __init__(self, install_dir, bindings_dir, solver_version,
+                 mirror_link=None):
+        # Getting the right archive name
+        os_name = self.os_name
+        arch = str(self.bits) + "-bit"
+        ext = "tar.gz"
+        if os_name == "windows":
+            ext = "zip"
+            arch += "-mingw"
+        elif os_name == "darwin":
+            os_name = "macos"
+
+        archive_name = "optimathsat-%s-%s-%s.%s" % (solver_version, os_name,
+                                                    arch, ext)
+
+        native_link = "http://optimathsat.disi.unitn.it/releases/optimathsat-%s/{archive_name}" % solver_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.python_bindings_dir = os.path.join(self.extract_path, "python")
+
+
+    def compile(self):
+        setup_py_url = "https://github.com/pysmt/solvers_patches/raw/master/optimsat/setup.py"
+        # Overwrite setup.py with the patched version
+        setup_py = os.path.join(self.python_bindings_dir, "setup.py")
+        SolverInstaller.mv(setup_py, setup_py + ".original")
+        SolverInstaller.do_download(setup_py_url, setup_py)
+
+        # Run setup.py to compile the bindings
+        SolverInstaller.mv(os.path.join(self.python_bindings_dir, 'mathsat_python_wrap.c'),
+                           os.path.join(self.python_bindings_dir, 'mathsat_python_wrap.cpp'))
+        SolverInstaller.run_python("./setup.py build", self.python_bindings_dir)
+
+
+    def move(self):
+        pdir = self.python_bindings_dir
+        bdir = os.path.join(pdir, "build")
+        sodir = glob.glob(bdir + "/lib.*")[0]
+        libdir = os.path.join(self.python_bindings_dir, "../lib")
+
+        # First, we need the SWIG-generated wrapper
+        for f in os.listdir(sodir):
+            if f.endswith(".so") or f.endswith(".pyd"):
+                SolverInstaller.mv(os.path.join(sodir, f), self.bindings_dir)
+        SolverInstaller.mv(os.path.join(pdir, "mathsat.py"), self.bindings_dir)
+
+        # Since MathSAT 5.5.0 we also need the SO/DLL/DYLIB of mathsat in the PATH
+        # Under Windows, we also need the DLLs of MPIR in the PATH
+        for f in os.listdir(libdir):
+            if f.endswith(".so") or f.endswith(".dll") or f.endswith(".dylib"):
+                SolverInstaller.mv(os.path.join(libdir, f), self.bindings_dir)
+
+    def get_installed_version(self):
+        return self.get_installed_version_script(self.bindings_dir, "optimsat")

pysmt/exceptions.py

@@ -147,3 +147,15 @@ def __str__(self):
 
 class PysmtIOError(PysmtException, IOError):
     pass
+
+class PysmtInfinityError(PysmtException):
+    """Infinite value in expressions."""
+    pass
+
+class PysmtInfinitesimalError(PysmtException):
+    """Infinite value in expressions."""
+    pass
+
+class PysmtUnboundedOptimizationError(PysmtException):
+    """Infinite optimal value in optimization."""
+    pass