1#
2# This file is part of pySMT.
3#
4#   Copyright 2014 Andrea Micheli and Marco Gario
5#
6#   Licensed under the Apache License, Version 2.0 (the "License");
7#   you may not use this file except in compliance with the License.
8#   You may obtain a copy of the License at
9#
10#       http://www.apache.org/licenses/LICENSE-2.0
11#
12#   Unless required by applicable law or agreed to in writing, software
13#   distributed under the License is distributed on an "AS IS" BASIS,
14#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15#   See the License for the specific language governing permissions and
16#   limitations under the License.
17#
18from functools import wraps
19import warnings
20
21import pysmt.exceptions
22
23class deprecated(object):
24    """This is a decorator which can be used to mark functions
25    as deprecated. It will result in a warning being emmitted
26    when the function is used."""
27
28    def __init__(self, alternative=None):
29        self.alternative = alternative
30
31    def __call__(self, func):
32        def newFunc(*args, **kwargs):
33            alt = ""
34            if self.alternative is not None:
35                alt = " You should call %s() instead!" % self.alternative
36            warnings.warn("Call to deprecated function %s().%s" % \
37                          (func.__name__, alt),
38                          category=DeprecationWarning,
39                          stacklevel=2)
40            return func(*args, **kwargs)
41        newFunc.__name__ = func.__name__
42        newFunc.__doc__ = func.__doc__
43        newFunc.__dict__.update(func.__dict__)
44        return newFunc
45
46
47def clear_pending_pop(f):
48    """Pop the solver stack (if necessary) before calling the function.
49
50    Some functions (e.g., get_value) required the state of the solver
51    to stay unchanged after a call to solve. Therefore, we can leave
52    th solver in an intermediate state in which there is a formula
53    asserted in the stack that is not needed (e.g., when solving under
54    assumptions). In order to guarantee that methods operate on the
55    correct set of formulae, all methods of the solver that rely on
56    the assertion stack, need to be marked with this decorator.
57    """
58
59    @wraps(f)
60    def clear_pending_pop_wrap(self, *args, **kwargs):
61        if self.pending_pop:
62            self.pending_pop = False
63            self.pop()
64        return f(self, *args, **kwargs)
65    return clear_pending_pop_wrap
66
67
68def typecheck_result(f):
69    """Performs type checking on the return value using the global environment"""
70
71    @wraps(f)
72    def typecheck_result_wrap(*args, **kwargs):
73        res = f(*args, **kwargs)
74        res.get_type() # This raises an exception if an invalid type is found
75    return typecheck_result_wrap
76
77
78def catch_conversion_error(f):
79    """Catch unknown operators errors and converts them into conversion error."""
80
81    @wraps(f)
82    def catch_conversion_error_wrap(*args, **kwargs):
83        try:
84            res = f(*args, **kwargs)
85        except pysmt.exceptions.UnsupportedOperatorError as ex:
86            raise pysmt.exceptions.ConvertExpressionError(message=
87                "Could not convert the input expression. " +
88                "The formula contains unsupported operators. " +
89                "The error was: %s" % ex.message,
90            expression=ex.expression)
91        return res
92    return catch_conversion_error_wrap
93
94
95def assert_infix_enabled(f):
96    """Raise an exception if infix notation is not enabled."""
97    from functools import wraps
98    from pysmt.exceptions import PysmtModeError
99    INFIX_ERROR_MSG = """Infix notation is not enabled for the current environment.
100Enable it by setting enable_infix_notation to True."""
101
102    @wraps(f)
103    def assert_infix_enabled_wrap(*args, **kwargs):
104        from pysmt.environment import get_env
105        if not get_env().enable_infix_notation:
106            raise PysmtModeError(INFIX_ERROR_MSG)
107        return f(*args, **kwargs)
108    return assert_infix_enabled_wrap
109