Merge pull request #365 from pysmt/exceptions-common-father

Introduce PysmtException, from which all exceptions inherit. This also introduces hybrid exceptions that inherit both from the Standard Library and from PysmtException (i.e., PysmtValueError).

pysmt/cmd/install.py

@@ -25,6 +25,7 @@
 from pysmt.cmd.installers import CuddInstaller
 
 from pysmt.environment import get_env
+from pysmt.exceptions import PysmtException
 from pysmt import git_version
 
 # Build a list of installers, one for each solver
@@ -72,7 +73,7 @@ def check_installed(required_solvers, install_dir, bindings_dir, mirror_link):
     pypath_solvers = get_env().factory.all_solvers()
     for solver in required_solvers:
         if solver not in pypath_solvers:
-            raise Exception("Was expecting to find %s installed" % solver)
+            raise PysmtException("Was expecting to find %s installed" % solver)
 
     #
     # Output information

pysmt/configuration.py

@@ -43,6 +43,7 @@
 from warnings import warn
 
 from pysmt.logics import get_logic_by_name
+from pysmt.exceptions import PysmtIOError
 
 def configure_environment(config_filename, environment):
     """
@@ -52,7 +53,7 @@ def configure_environment(config_filename, environment):
     factory = environment.factory
 
     if not os.path.exists(config_filename):
-        raise IOError("File '%s' does not exists." % config_filename)
+        raise PysmtIOError("File '%s' does not exists." % config_filename)
 
     # We do not use variable inside the config file
     config = cp.RawConfigParser()

pysmt/constants.py

@@ -16,6 +16,7 @@
 
 import os
 from six import PY2
+from pysmt.exceptions import PysmtImportError
 # The environment variable can be used to force the configuration
 # of the Fraction class.
 #
@@ -38,7 +39,7 @@
     HAS_GMPY = True
 except ImportError as ex:
     if ENV_USE_GMPY is True:
-        raise ex
+        raise PysmtImportError(str(ex))
 
 if ENV_USE_GMPY is False:
     # Explicitely disable GMPY

pysmt/exceptions.py

@@ -19,69 +19,74 @@
 
 import pysmt.operators as op
 
-class UnknownSmtLibCommandError(Exception):
+
+class PysmtException(Exception):
+    """Base class for all custom exceptions of pySMT"""
+    pass
+
+class UnknownSmtLibCommandError(PysmtException):
     """Raised when the parser finds an unknown command."""
     pass
 
-class SolverReturnedUnknownResultError(Exception):
+class SolverReturnedUnknownResultError(PysmtException):
     """This exception is raised if a solver returns 'unknown' as a result"""
     pass
 
-class UnknownSolverAnswerError(Exception):
+class UnknownSolverAnswerError(PysmtException):
     """Raised when the a solver returns an invalid response."""
     pass
 
-class NoSolverAvailableError(Exception):
+class NoSolverAvailableError(PysmtException):
     """No solver is available for the selected Logic."""
     pass
 
-class NonLinearError(Exception):
+class NonLinearError(PysmtException):
     """The provided expression is not linear."""
     pass
 
-class UndefinedLogicError(Exception):
+class UndefinedLogicError(PysmtException):
     """This exception is raised if an undefined Logic is attempted to be used."""
     pass
 
-class InternalSolverError(Exception):
+class InternalSolverError(PysmtException):
     """Generic exception to capture errors provided by a solver."""
     pass
 
-class NoLogicAvailableError(Exception):
+class NoLogicAvailableError(PysmtException):
     """Generic exception to capture errors caused by missing support for logics."""
     pass
 
-class SolverRedefinitionError(Exception):
+class SolverRedefinitionError(PysmtException):
     """Exception representing errors caused by multiple defintion of solvers
        having the same name."""
     pass
 
-class SolverNotConfiguredForUnsatCoresError(Exception):
+class SolverNotConfiguredForUnsatCoresError(PysmtException):
     """
     Exception raised if a solver not configured for generating unsat
     cores is required to produce a core.
     """
     pass
 
-class SolverStatusError(Exception):
+class SolverStatusError(PysmtException):
     """
     Exception raised if a method requiring a specific solver status is
     incorrectly called in the wrong status.
     """
     pass
 
-class ConvertExpressionError(Exception):
+class ConvertExpressionError(PysmtException):
     """Exception raised if the converter cannot convert an expression."""
 
     def __init__(self, message=None, expression=None):
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.message = message
         self.expression=expression
 
     def __str__(self):
         return self.message
 
-class UnsupportedOperatorError(Exception):
+class UnsupportedOperatorError(PysmtException):
     """The expression contains an operator that is not supported.
 
     The argument node_type contains the unsupported operator id.
@@ -90,7 +95,7 @@ class UnsupportedOperatorError(Exception):
     def __init__(self, message=None, node_type=None, expression=None):
         if message is None:
             message = "Unsupported operator '%s' (node_type: %d)" % (op.op_to_str(node_type), node_type)
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.message = message
         self.expression = expression
         self.node_type = node_type
@@ -99,17 +104,37 @@ def __str__(self):
         return self.message
 
 
-class SolverAPINotFound(Exception):
+class SolverAPINotFound(PysmtException):
     """The Python API of the selected solver cannot be found."""
     pass
 
 
-class UndefinedSymbolError(Exception):
+class UndefinedSymbolError(PysmtException):
     """The given Symbol is not in the FormulaManager."""
 
     def __init__(self, name):
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.name = name
 
     def __str__(self):
         return "'%s' is not defined!" % self.name
+
+class PysmtModeError(PysmtException):
+    """The current mode is not supported for this operation"""
+    pass
+
+
+class PysmtImportError(PysmtException, ImportError):
+    pass
+
+class PysmtValueError(PysmtException, ValueError):
+    pass
+
+class PysmtTypeError(PysmtException, TypeError):
+    pass
+
+class PysmtSyntaxError(PysmtException, SyntaxError):
+    pass
+
+class PysmtIOError(PysmtException, IOError):
+    pass

pysmt/fnode.py

@@ -47,6 +47,7 @@
 from pysmt.utils import twos_complement
 from pysmt.constants import (Fraction, is_python_integer,
                              is_python_rational, is_python_boolean)
+from pysmt.exceptions import PysmtValueError, PysmtModeError
 
 
 FNodeContent = collections.namedtuple("FNodeContent",
@@ -145,8 +146,8 @@ def is_constant(self, _type=None, value=None):
                     if not c.is_constant():
                         return False
                 if _type is not None or value is not None:
-                    raise ValueError("constant type and value checking is " \
-                                     "not available for array values")
+                    raise PysmtValueError("constant type and value checking " \
+                                          "is not available for array values")
                 return True
             return False
         if _type is not None:
@@ -657,7 +658,7 @@ def _apply_infix(self, right, function, bv_function=None):
                 right = mgr.Real(right)
             return function(self, right)
         else:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
 
     def Implies(self, right):
         return self._apply_infix(right, _mgr().Implies)
@@ -673,9 +674,9 @@ def Ite(self, then_, else_):
             if isinstance(then_, FNode) and isinstance(else_, FNode):
                 return _mgr().Ite(self, then_, else_)
             else:
-                raise Exception("Cannot infix ITE with implicit argument types.")
+                raise PysmtModeError("Cannot infix ITE with implicit argument types.")
         else:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
 
     def And(self, right):
         return self._apply_infix(right, _mgr().And)
@@ -807,14 +808,14 @@ def __neg__(self):
 
     def __invert__(self):
         if not _env().enable_infix_notation:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
         if _is_bv(self):
             return _mgr().BVNot(self)
         return _mgr().Not(self)
 
     def __getitem__(self, idx):
         if not _env().enable_infix_notation:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
         if isinstance(idx, slice):
             end = idx.stop
             start = idx.start