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