Source code for pysmt.decorators

# 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.
from functools import wraps
import warnings

import pysmt.exceptions

class deprecated(object):
    """This is a decorator which can be used to mark functions
    as deprecated. It will result in a warning being emmitted
    when the function is used."""

    def __init__(self, alternative=None):
        self.alternative = alternative

    def __call__(self, func):
        def newFunc(*args, **kwargs):
            alt = ""
            if self.alternative is not None:
                alt = " You should call %s() instead!" % self.alternative
            warnings.warn("Call to deprecated function %s().%s" % \
                          (func.__name__, alt),
            return func(*args, **kwargs)
        newFunc.__name__ = func.__name__
        newFunc.__doc__ = func.__doc__
        return newFunc

def clear_pending_pop(f):
    """Pop the solver stack (if necessary) before calling the function.

    Some functions (e.g., get_value) required the state of the solver
    to stay unchanged after a call to solve. Therefore, we can leave
    th solver in an intermediate state in which there is a formula
    asserted in the stack that is not needed (e.g., when solving under
    assumptions). In order to guarantee that methods operate on the
    correct set of formulae, all methods of the solver that rely on
    the assertion stack, need to be marked with this decorator.

    def clear_pending_pop_wrap(self, *args, **kwargs):
        if self.pending_pop:
            self.pending_pop = False
        return f(self, *args, **kwargs)
    return clear_pending_pop_wrap

def typecheck_result(f):
    """Performs type checking on the return value using the global environment"""

    def typecheck_result_wrap(*args, **kwargs):
        res = f(*args, **kwargs)
        res.get_type() # This raises an exception if an invalid type is found
    return typecheck_result_wrap

def catch_conversion_error(f):
    """Catch unknown operators errors and converts them into conversion error."""

    def catch_conversion_error_wrap(*args, **kwargs):
            res = f(*args, **kwargs)
        except pysmt.exceptions.UnsupportedOperatorError as ex:
            raise pysmt.exceptions.ConvertExpressionError(message=
                "Could not convert the input expression. " +
                "The formula contains unsupported operators. " +
                "The error was: %s" % ex.message,
        return res
    return catch_conversion_error_wrap

def assert_infix_enabled(f):
    """Raise an exception if infix notation is not enabled."""
    from functools import wraps
    from pysmt.exceptions import PysmtModeError
    INFIX_ERROR_MSG = """Infix notation is not enabled for the current environment.
Enable it by setting enable_infix_notation to True."""

    def assert_infix_enabled_wrap(*args, **kwargs):
        from pysmt.environment import get_env
        if not get_env().enable_infix_notation:
            raise PysmtModeError(INFIX_ERROR_MSG)
        return f(*args, **kwargs)
    return assert_infix_enabled_wrap