Source code for pysmt.exceptions

# 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
#   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.
"""This module contains all custom exceptions of pySMT."""

import pysmt.operators as op

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