Merge pull request #432 from pysmt/cython/smtlib_parser

Cython/smtlib parser

.travis.yml

@@ -52,7 +52,8 @@ env:
   matrix:
     - PYSMT_SOLVER="all"   PYSMT_GMPY="TRUE"
     - PYSMT_SOLVER="all"   PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"
+    - PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"
+    - PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"
     - PYSMT_SOLVER="msat"  PYSMT_GMPY="FALSE"
     - PYSMT_SOLVER="z3"    PYSMT_GMPY="FALSE"
     - PYSMT_SOLVER="cvc4"  PYSMT_GMPY="FALSE"

ci/travis_install.sh

@@ -32,10 +32,10 @@ then
 fi
 
 pip install six
+pip install cython;
 
 if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == "btor" ];
 then
-    pip install cython;
     pip install python-coveralls;
 fi
 

docs/getting_started.rst

@@ -65,6 +65,15 @@ system environment variables ``PYSMT_GMPY2`` to ``True`` or
 ``False``. If this is set to true and the gmpy library cannot be
 imported, an exception will be thrown.
 
+Cython
+""""""
+
+PySMT supports the use of `Cython <http://cython.org/>`_ in order to
+improve the performances of some internal component. If Cython is
+installed, this will be used (by default) to compile the SMT-LIB
+parser. The use of Cython can be controlled by setting the environment
+variable ``PYSMT_CYTHON`` to ``True`` or ``False``. If set to false,
+the default pure python implementation will be used.
 
 
 Hello World

pysmt/configuration.py

@@ -17,7 +17,7 @@
 #
 """Utils to configure pySMT.
 
-The following is an example of configuratoin file.
+The following is an example of configuration file.
 
 [global]
 use_infix_notation: true

pysmt/smtlib/parser/__init__.py

@@ -0,0 +1,124 @@
+#
+# This file is part of pySMT.
+#
+#   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
+
+from pysmt.exceptions import PysmtImportError
+#
+# Try to import the Cython version of the parser.
+# Fall-back on the pure-python version if:
+#  - Cython is not installed
+#  - There is an error in the handling of the pyx file and the use of
+#    Cython was not specified (unset env variable)
+#
+ENV_USE_CYTHON = os.environ.get("PYSMT_CYTHON")
+if ENV_USE_CYTHON is not None:
+    ENV_USE_CYTHON = ENV_USE_CYTHON.lower() in ["true", "1"]
+
+HAS_CYTHON = False
+try:
+    import pyximport
+    HAS_CYTHON = True
+except ImportError as ex:
+    if ENV_USE_CYTHON:
+        raise PysmtImportError(str(ex))
+
+if HAS_CYTHON and (ENV_USE_CYTHON or ENV_USE_CYTHON is None):
+    USE_CYTHON = True
+else:
+    USE_CYTHON = False
+
+if USE_CYTHON:
+    try:
+        pyximport.install()
+        from pysmt.smtlib.parser.parser import *
+    except ImportError as ex:
+        if ENV_USE_CYTHON is None:
+            # If not specified, fall-ack
+            USE_CYTHON = False
+        else:
+            raise PysmtImportError(str(ex))
+
+if not USE_CYTHON:
+    from pysmt.smtlib.parser.parser import *
+else:
+    # pyximport.install() would be sufficient if we had a .pyx file
+    # However, we currently are not annotating the .py file for cython,
+    # and therefore our .pyx file would be a copy of the .py file.
+    #
+    # To avoid code duplication, we tell cython to compile the .py file
+    # and load the resulting .so file. Cython does not support this flow,
+    # therfore we need to have a couple of work-arounds.
+    #
+    # 1. Call to pyximport.install(): Functions in pyximport expect to
+    # find a global object called pyxargs. This is created within
+    # install(). We could call uninstall() afterwards, to avoid
+    # enabling cython globally.
+    #
+    # 2. build_dir: Also this variable is set in install(). We use the
+    # default value, that is a folder in the home-dir.
+    #
+    # 3. load_dynamic will load the module but not extend the globald
+    # directory. We rely on the fact that the loading has been already
+    # performed and call the import * explicitely
+    #
+    # Since the .so is compiled outside of the PYTHON_PATH, there is
+    # no ambiguity when importing the parser: the only way to load the
+    # cython version is by the so_path that targets .pyxbld .
+    #
+    import imp
+    pyx = pyximport.install()
+    pyximport.uninstall(*pyx)
+    build_dir = os.path.join(os.path.expanduser('~'), '.pyxbld')
+    path = os.path.join(os.path.dirname(__file__), "parser.py")
+    name="pysmt.smtlib.parser.parser"
+
+    so_path = pyximport.build_module(name, path,
+                                     pyxbuild_dir=build_dir)
+    mod = imp.load_dynamic(name, so_path)
+    assert mod.__file__ == so_path, (mod.__file__, so_path)
+    # print(so_path)
+    from pysmt.smtlib.parser.parser import *
+
+
+# End of preamble
+
+#
+#
+#
+if __name__ == "__main__":
+    import sys
+
+    def main():
+        """Simple testing script"""
+        args = sys.argv
+        out = None
+        if len(args) == 3:
+            out = args[2]
+        elif len(args) != 2:
+            print("Usage %s <file.smt2> [out.smt2]" % args[0])
+            exit(1)
+
+        fname = args[1]
+
+        parser = SmtLibParser()
+        res = parser.get_script_fname(fname)
+        assert res is not None
+        print("Done")
+        if out is not None:
+            res.to_file(out, daggify=True)
+    main()

pysmt/smtlib/parser.py → pysmt/smtlib/parser/parser.py

@@ -1312,27 +1312,3 @@ def _ext_rotate_right(self, x, y):
         return self.env.formula_manager.BVRor(x, y.simplify().constant_value())
 
 # EOC SmtLibZ3Parser
-
-
-if __name__ == "__main__":
-    import sys
-
-    def main():
-        """Simple testing script"""
-        args = sys.argv
-        out = None
-        if len(args) == 3:
-            out = args[2]
-        elif len(args) != 2:
-            print("Usage %s <file.smt2> [out.smt2]" % args[0])
-            exit(1)
-
-        fname = args[1]
-
-        parser = SmtLibParser()
-        res = parser.get_script_fname(fname)
-        assert res is not None
-        print("Done")
-        if out is not None:
-            res.to_file(out, daggify=True)
-    main()

pysmt/utils.py

@@ -77,3 +77,14 @@ def quote(name, style='|'):
         return "%s%s%s" % (style, name, style)
     else:
         return name
+
+
+def open_(fname):
+    """Transparently handle .bz2 files."""
+    if fname.endswith(".bz2"):
+        import bz2
+        if PY2:
+            return bz2.BZ2File(fname, "r")
+        else:
+            return bz2.open(fname, "rt")
+    return open(fname)