Merge pull request #49 from pysmt/towards_python_3

Towards python 3

README.rst

@@ -52,6 +52,11 @@ Equalities and Uninterpreted Functions (EUF). The following solvers are supporte
 The library assumes that the python binding for the SMT Solver are installed
 and accessible from your PYTHONPATH. For Yices 2 we rely on pyices (https://github.com/cheshire/pyices).
 
+pySMT works on both Python 2 and Python 3. Some solvers support both
+versions (e.g., MathSAT) but in general, many solvers still support
+only Python 2.
+
+
 Usage
 =====
 

docs/CHANGES.rst

@@ -1,6 +1,15 @@
 Change Log
 ==========
 
+0.2.5: XXXXXXXXXX  -- YYYYYY
+----------------------------
+
+General:
+
+* Added support for Python 3. The library works with both Python 2 and
+  Python 3.
+
+
 0.2.4: 2015-03-15  -- PicoSAT
 -----------------------------
 

pysmt/cmd/install.py

@@ -1,5 +1,3 @@
-#!/usr/bin/env python
-
 # Copyright 2014 Andrea Micheli and Marco Gario
 #
 # Licensed under the Apache License, Version 2.0 (the "License");
@@ -14,7 +12,9 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
-import urllib2
+from six.moves.urllib import request as urllib2
+from six.moves import input
+
 import os
 import tarfile
 import sys
@@ -120,8 +120,8 @@ def download(url, file_name):
     u = urllib2.urlopen(url)
     f = open(file_name, 'wb')
     meta = u.info()
-    if len(meta.getheaders("Content-Length")) > 0:
-        file_size = int(meta.getheaders("Content-Length")[0])
+    if len(meta.get("Content-Length")) > 0:
+        file_size = int(meta.get("Content-Length"))
         print("Downloading: %s Bytes: %s" % (file_name, file_size))
 
     block_sz = 8192
@@ -132,17 +132,18 @@ def download(url, file_name):
             break
 
         f.write(buff)
-        if len(meta.getheaders("Content-Length")) > 0 and sys.stdout.isatty():
+        if len(meta.get("Content-Length")) > 0 and sys.stdout.isatty():
             count += len(buff)
             perc = (float(count) / float(file_size)) * 100.0
             str_perc = "%.1f%%" % perc
             sys.stdout.write('\r')
             sys.stdout.write(str_perc)
             sys.stdout.write(" " * (10 - len(str_perc)))
 
-    print ""
+    print("")
     f.close()
 
+
 ################################################################################
 # Installers
 
@@ -472,7 +473,7 @@ def print_welcome():
         (e.g., make and gcc).
 """
     print(msg)
-    res = raw_input("Continue? [Y]es/[N]o: ").lower()
+    res = input("Continue? [Y]es/[N]o: ").lower()
 
     if res != "y":
         exit(-1)

pysmt/configuration.py

@@ -39,7 +39,7 @@
 """
 
 import os.path
-import ConfigParser as cp
+import six.moves.configparser as cp
 from warnings import warn
 
 from pysmt.logics import get_logic_by_name
@@ -133,5 +133,5 @@ def write_environment_configuration(config_filename, environment):
 
 
     # Writing the configuration to file
-    with open(config_filename, 'wb') as configfile:
+    with open(config_filename, 'wt') as configfile:
         config.write(configfile)

pysmt/factory.py

@@ -24,6 +24,7 @@
 """
 
 from functools import partial
+from six import iteritems
 
 from pysmt.exceptions import NoSolverAvailableError, SolverRedefinitionError
 from pysmt.logics import QF_UFLIRA
@@ -239,7 +240,7 @@ def all_solvers(self, logic=None):
         """
         res = {}
         if logic is not None:
-            for s, v in self._all_solvers.iteritems():
+            for s, v in iteritems(self._all_solvers):
                 for l in v.LOGICS:
                     if logic <= l:
                         res[s] = v

pysmt/fnode.py

@@ -18,7 +18,7 @@
 """FNode are the building blocks of formulae."""
 import collections
 
-import shortcuts
+import pysmt.shortcuts
 from pysmt.operators import CONSTANTS
 from pysmt.operators import (FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF,
                              SYMBOL, FUNCTION,
@@ -69,16 +69,16 @@ def get_dependencies(self):
         return self.get_free_variables()
 
     def get_free_variables(self):
-        return shortcuts.get_free_variables(self)
+        return pysmt.shortcuts.get_free_variables(self)
 
     def get_sons(self):
         return self.args()
 
     def simplify(self):
-        return shortcuts.simplify(self)
+        return pysmt.shortcuts.simplify(self)
 
     def substitute(self, subs):
-        return shortcuts.substitute(self, subs=subs)
+        return pysmt.shortcuts.substitute(self, subs=subs)
 
     def is_constant(self, _type=None, value=None):
         if self.node_type() not in CONSTANTS:
@@ -184,7 +184,7 @@ def __repr__(self):
         return str(self)
 
     def serialize(self, threshold=None):
-        return shortcuts.serialize(self, threshold=threshold)
+        return pysmt.shortcuts.serialize(self, threshold=threshold)
 
     def is_quantifier(self):
         return self.is_exists() or self.is_forall()
@@ -223,54 +223,54 @@ def quantifier_vars(self):
 
     # Infix Notation
     def _apply_infix(self, right, function):
-        if shortcuts.get_env().enable_infix_notation:
+        if pysmt.shortcuts.get_env().enable_infix_notation:
             return function(self, right)
         else:
             raise Exception("Cannot use infix notation")
 
     def Implies(self, right):
-        return self._apply_infix(right, shortcuts.Implies)
+        return self._apply_infix(right, pysmt.shortcuts.Implies)
 
     def Iff(self, right):
-        return self._apply_infix(right, shortcuts.Iff)
+        return self._apply_infix(right, pysmt.shortcuts.Iff)
 
     def Equals(self, right):
-        return self._apply_infix(right, shortcuts.Equals)
+        return self._apply_infix(right, pysmt.shortcuts.Equals)
 
     def Ite(self, right):
-        return self._apply_infix(right, shortcuts.Ite)
+        return self._apply_infix(right, pysmt.shortcuts.Ite)
 
     def And(self, right):
-        return self._apply_infix(right, shortcuts.And)
+        return self._apply_infix(right, pysmt.shortcuts.And)
 
     def Or(self, right):
-        return self._apply_infix(right, shortcuts.Or)
+        return self._apply_infix(right, pysmt.shortcuts.Or)
 
     def __add__(self, right):
-        return self._apply_infix(right, shortcuts.Plus)
+        return self._apply_infix(right, pysmt.shortcuts.Plus)
 
     def __sub__(self, right):
-        return self._apply_infix(right, shortcuts.Minus)
+        return self._apply_infix(right, pysmt.shortcuts.Minus)
 
     def __mul__(self, right):
-        return self._apply_infix(right, shortcuts.Times)
+        return self._apply_infix(right, pysmt.shortcuts.Times)
 
     def __div__(self, right):
-        return self._apply_infix(right, shortcuts.Div)
+        return self._apply_infix(right, pysmt.shortcuts.Div)
 
     def __truediv__(self, right):
         return self.__div__(right)
 
     def __gt__(self, right):
-        return self._apply_infix(right, shortcuts.GT)
+        return self._apply_infix(right, pysmt.shortcuts.GT)
 
     def __ge__(self, right):
-        return self._apply_infix(right, shortcuts.GE)
+        return self._apply_infix(right, pysmt.shortcuts.GE)
 
     def __lt__(self, right):
-        return self._apply_infix(right, shortcuts.LT)
+        return self._apply_infix(right, pysmt.shortcuts.LT)
 
     def __le__(self, right):
-        return self._apply_infix(right, shortcuts.LE)
+        return self._apply_infix(right, pysmt.shortcuts.LE)
 
 # EOC FNode

pysmt/formula.py

@@ -34,6 +34,7 @@
 import pysmt.typing as types
 import pysmt.operators as op
 
+from pysmt.utils import is_integer
 from pysmt.fnode import FNode, FNodeContent
 from pysmt.exceptions import NonLinearError
 from pysmt.walkers.identitydag import IdentityDagWalker
@@ -313,7 +314,7 @@ def Real(self, value):
             val = value
         elif type(value) == tuple:
             val = Fraction(value[0], value[1])
-        elif type(value) == long or type(value) == int:
+        elif is_integer(value):
             val = Fraction(value, 1)
         elif type(value) == float:
             val = Fraction.from_float(value)
@@ -332,7 +333,7 @@ def Int(self, value):
         if value in self.int_constants:
             return self.int_constants[value]
 
-        if type(value) == long or type(value) == int:
+        if is_integer(value):
             n = self.create_node(node_type=op.INT_CONSTANT,
                                  args=tuple(),
                                  payload=value)
@@ -480,7 +481,7 @@ def Min(self, *args):
             a, b = exprs
             return self.Ite(self.LE(a, b), a, b)
         else:
-            h = len(exprs) / 2
+            h = len(exprs) // 2
             return self.Min(self.Min(exprs[0:h]), self.Min(exprs[h:]))
 
     def Max(self, *args):
@@ -493,7 +494,7 @@ def Max(self, *args):
             a, b = exprs
             return self.Ite(self.LE(a, b), b, a)
         else:
-            h = len(exprs) / 2
+            h = len(exprs) // 2
             return self.Max(self.Max(exprs[0:h]), self.Max(exprs[h:]))
 
 

pysmt/logics.py

@@ -244,7 +244,7 @@ def __ge__(self, other):
         return (other.__le__(self))
 
     def __gt__(self, other):
-        return other.__lt__(self)
+        return (other.__lt__(self))
 
 
 # Logics