| # This file was automatically generated by SWIG (http://www.swig.org). | |
| # Version 2.0.11 | |
| # | |
| # Do not make changes to this file unless you know what you are doing--modify | |
| # the SWIG interface file instead. | |
| from sys import version_info | |
| if version_info >= (2,6,0): | |
| def swig_import_helper(): | |
| from os.path import dirname | |
| import imp | |
| fp = None | |
| try: | |
| fp, pathname, description = imp.find_module('_mathsat', [dirname(__file__)]) | |
| except ImportError: | |
| import _mathsat | |
| return _mathsat | |
| if fp is not None: | |
| try: | |
| _mod = imp.load_module('_mathsat', fp, pathname, description) | |
| finally: | |
| fp.close() | |
| return _mod | |
| _mathsat = swig_import_helper() | |
| del swig_import_helper | |
| else: | |
| import _mathsat | |
| del version_info | |
| try: | |
| _swig_property = property | |
| except NameError: | |
| pass # Python < 2.2 doesn't have 'property'. | |
| def _swig_setattr_nondynamic(self,class_type,name,value,static=1): | |
| if (name == "thisown"): return self.this.own(value) | |
| if (name == "this"): | |
| if type(value).__name__ == 'SwigPyObject': | |
| self.__dict__[name] = value | |
| return | |
| method = class_type.__swig_setmethods__.get(name,None) | |
| if method: return method(self,value) | |
| if (not static): | |
| self.__dict__[name] = value | |
| else: | |
| raise AttributeError("You cannot add attributes to %s" % self) | |
| def _swig_setattr(self,class_type,name,value): | |
| return _swig_setattr_nondynamic(self,class_type,name,value,0) | |
| def _swig_getattr(self,class_type,name): | |
| if (name == "thisown"): return self.this.own() | |
| method = class_type.__swig_getmethods__.get(name,None) | |
| if method: return method(self) | |
| raise AttributeError(name) | |
| def _swig_repr(self): | |
| try: strthis = "proxy of " + self.this.__repr__() | |
| except: strthis = "" | |
| return "<%s.%s; %s >" % (self.__class__.__module__, self.__class__.__name__, strthis,) | |
| try: | |
| _object = object | |
| _newclass = 1 | |
| except AttributeError: | |
| class _object : pass | |
| _newclass = 0 | |
| class msat_config(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_config, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_config, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_config_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_config_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_config_repr_get, _mathsat.msat_config_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_config() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_config | |
| __del__ = lambda self : None; | |
| msat_config_swigregister = _mathsat.msat_config_swigregister | |
| msat_config_swigregister(msat_config) | |
| class msat_env(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_env, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_env, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_env_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_env_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_env_repr_get, _mathsat.msat_env_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_env() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_env | |
| __del__ = lambda self : None; | |
| msat_env_swigregister = _mathsat.msat_env_swigregister | |
| msat_env_swigregister(msat_env) | |
| class msat_term(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_term, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_term, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_term_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_term_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_term_repr_get, _mathsat.msat_term_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_term() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_term | |
| __del__ = lambda self : None; | |
| msat_term_swigregister = _mathsat.msat_term_swigregister | |
| msat_term_swigregister(msat_term) | |
| class msat_decl(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_decl, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_decl, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_decl_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_decl_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_decl_repr_get, _mathsat.msat_decl_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_decl() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_decl | |
| __del__ = lambda self : None; | |
| msat_decl_swigregister = _mathsat.msat_decl_swigregister | |
| msat_decl_swigregister(msat_decl) | |
| class msat_type(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_type, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_type, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_type_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_type_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_type_repr_get, _mathsat.msat_type_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_type() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_type | |
| __del__ = lambda self : None; | |
| msat_type_swigregister = _mathsat.msat_type_swigregister | |
| msat_type_swigregister(msat_type) | |
| MSAT_UNKNOWN = _mathsat.MSAT_UNKNOWN | |
| MSAT_UNSAT = _mathsat.MSAT_UNSAT | |
| MSAT_SAT = _mathsat.MSAT_SAT | |
| MSAT_UNDEF = _mathsat.MSAT_UNDEF | |
| MSAT_FALSE = _mathsat.MSAT_FALSE | |
| MSAT_TRUE = _mathsat.MSAT_TRUE | |
| MSAT_TAG_ERROR = _mathsat.MSAT_TAG_ERROR | |
| MSAT_TAG_UNKNOWN = _mathsat.MSAT_TAG_UNKNOWN | |
| MSAT_TAG_TRUE = _mathsat.MSAT_TAG_TRUE | |
| MSAT_TAG_FALSE = _mathsat.MSAT_TAG_FALSE | |
| MSAT_TAG_AND = _mathsat.MSAT_TAG_AND | |
| MSAT_TAG_OR = _mathsat.MSAT_TAG_OR | |
| MSAT_TAG_NOT = _mathsat.MSAT_TAG_NOT | |
| MSAT_TAG_IFF = _mathsat.MSAT_TAG_IFF | |
| MSAT_TAG_PLUS = _mathsat.MSAT_TAG_PLUS | |
| MSAT_TAG_TIMES = _mathsat.MSAT_TAG_TIMES | |
| MSAT_TAG_FLOOR = _mathsat.MSAT_TAG_FLOOR | |
| MSAT_TAG_LEQ = _mathsat.MSAT_TAG_LEQ | |
| MSAT_TAG_EQ = _mathsat.MSAT_TAG_EQ | |
| MSAT_TAG_ITE = _mathsat.MSAT_TAG_ITE | |
| MSAT_TAG_INT_MOD_CONGR = _mathsat.MSAT_TAG_INT_MOD_CONGR | |
| MSAT_TAG_BV_CONCAT = _mathsat.MSAT_TAG_BV_CONCAT | |
| MSAT_TAG_BV_EXTRACT = _mathsat.MSAT_TAG_BV_EXTRACT | |
| MSAT_TAG_BV_NOT = _mathsat.MSAT_TAG_BV_NOT | |
| MSAT_TAG_BV_AND = _mathsat.MSAT_TAG_BV_AND | |
| MSAT_TAG_BV_OR = _mathsat.MSAT_TAG_BV_OR | |
| MSAT_TAG_BV_XOR = _mathsat.MSAT_TAG_BV_XOR | |
| MSAT_TAG_BV_ULT = _mathsat.MSAT_TAG_BV_ULT | |
| MSAT_TAG_BV_SLT = _mathsat.MSAT_TAG_BV_SLT | |
| MSAT_TAG_BV_ULE = _mathsat.MSAT_TAG_BV_ULE | |
| MSAT_TAG_BV_SLE = _mathsat.MSAT_TAG_BV_SLE | |
| MSAT_TAG_BV_COMP = _mathsat.MSAT_TAG_BV_COMP | |
| MSAT_TAG_BV_NEG = _mathsat.MSAT_TAG_BV_NEG | |
| MSAT_TAG_BV_ADD = _mathsat.MSAT_TAG_BV_ADD | |
| MSAT_TAG_BV_SUB = _mathsat.MSAT_TAG_BV_SUB | |
| MSAT_TAG_BV_MUL = _mathsat.MSAT_TAG_BV_MUL | |
| MSAT_TAG_BV_UDIV = _mathsat.MSAT_TAG_BV_UDIV | |
| MSAT_TAG_BV_SDIV = _mathsat.MSAT_TAG_BV_SDIV | |
| MSAT_TAG_BV_UREM = _mathsat.MSAT_TAG_BV_UREM | |
| MSAT_TAG_BV_SREM = _mathsat.MSAT_TAG_BV_SREM | |
| MSAT_TAG_BV_LSHL = _mathsat.MSAT_TAG_BV_LSHL | |
| MSAT_TAG_BV_LSHR = _mathsat.MSAT_TAG_BV_LSHR | |
| MSAT_TAG_BV_ASHR = _mathsat.MSAT_TAG_BV_ASHR | |
| MSAT_TAG_BV_ROL = _mathsat.MSAT_TAG_BV_ROL | |
| MSAT_TAG_BV_ROR = _mathsat.MSAT_TAG_BV_ROR | |
| MSAT_TAG_BV_ZEXT = _mathsat.MSAT_TAG_BV_ZEXT | |
| MSAT_TAG_BV_SEXT = _mathsat.MSAT_TAG_BV_SEXT | |
| MSAT_TAG_ARRAY_READ = _mathsat.MSAT_TAG_ARRAY_READ | |
| MSAT_TAG_ARRAY_WRITE = _mathsat.MSAT_TAG_ARRAY_WRITE | |
| MSAT_TAG_ARRAY_CONST = _mathsat.MSAT_TAG_ARRAY_CONST | |
| MSAT_TAG_FP_EQ = _mathsat.MSAT_TAG_FP_EQ | |
| MSAT_TAG_FP_LT = _mathsat.MSAT_TAG_FP_LT | |
| MSAT_TAG_FP_LE = _mathsat.MSAT_TAG_FP_LE | |
| MSAT_TAG_FP_NEG = _mathsat.MSAT_TAG_FP_NEG | |
| MSAT_TAG_FP_ADD = _mathsat.MSAT_TAG_FP_ADD | |
| MSAT_TAG_FP_SUB = _mathsat.MSAT_TAG_FP_SUB | |
| MSAT_TAG_FP_MUL = _mathsat.MSAT_TAG_FP_MUL | |
| MSAT_TAG_FP_DIV = _mathsat.MSAT_TAG_FP_DIV | |
| MSAT_TAG_FP_SQRT = _mathsat.MSAT_TAG_FP_SQRT | |
| MSAT_TAG_FP_ABS = _mathsat.MSAT_TAG_FP_ABS | |
| MSAT_TAG_FP_MIN = _mathsat.MSAT_TAG_FP_MIN | |
| MSAT_TAG_FP_MAX = _mathsat.MSAT_TAG_FP_MAX | |
| MSAT_TAG_FP_CAST = _mathsat.MSAT_TAG_FP_CAST | |
| MSAT_TAG_FP_ROUND_TO_INT = _mathsat.MSAT_TAG_FP_ROUND_TO_INT | |
| MSAT_TAG_FP_FROM_SBV = _mathsat.MSAT_TAG_FP_FROM_SBV | |
| MSAT_TAG_FP_FROM_UBV = _mathsat.MSAT_TAG_FP_FROM_UBV | |
| MSAT_TAG_FP_TO_BV = _mathsat.MSAT_TAG_FP_TO_BV | |
| MSAT_TAG_FP_AS_IEEEBV = _mathsat.MSAT_TAG_FP_AS_IEEEBV | |
| MSAT_TAG_FP_ISNAN = _mathsat.MSAT_TAG_FP_ISNAN | |
| MSAT_TAG_FP_ISINF = _mathsat.MSAT_TAG_FP_ISINF | |
| MSAT_TAG_FP_ISZERO = _mathsat.MSAT_TAG_FP_ISZERO | |
| MSAT_TAG_FP_ISSUBNORMAL = _mathsat.MSAT_TAG_FP_ISSUBNORMAL | |
| MSAT_TAG_FP_ISNORMAL = _mathsat.MSAT_TAG_FP_ISNORMAL | |
| MSAT_TAG_FP_ISNEG = _mathsat.MSAT_TAG_FP_ISNEG | |
| MSAT_TAG_FP_ISPOS = _mathsat.MSAT_TAG_FP_ISPOS | |
| MSAT_TAG_FP_FROM_IEEEBV = _mathsat.MSAT_TAG_FP_FROM_IEEEBV | |
| MSAT_TAG_INT_FROM_UBV = _mathsat.MSAT_TAG_INT_FROM_UBV | |
| MSAT_TAG_INT_FROM_SBV = _mathsat.MSAT_TAG_INT_FROM_SBV | |
| MSAT_TAG_INT_TO_BV = _mathsat.MSAT_TAG_INT_TO_BV | |
| class msat_model(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_model, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_model, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_model_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_model_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_model_repr_get, _mathsat.msat_model_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_model() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_model | |
| __del__ = lambda self : None; | |
| msat_model_swigregister = _mathsat.msat_model_swigregister | |
| msat_model_swigregister(msat_model) | |
| class msat_model_iterator(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_model_iterator, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_model_iterator, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_model_iterator_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_model_iterator_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_model_iterator_repr_get, _mathsat.msat_model_iterator_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_model_iterator() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_model_iterator | |
| __del__ = lambda self : None; | |
| msat_model_iterator_swigregister = _mathsat.msat_model_iterator_swigregister | |
| msat_model_iterator_swigregister(msat_model_iterator) | |
| MSAT_VISIT_PROCESS = _mathsat.MSAT_VISIT_PROCESS | |
| MSAT_VISIT_SKIP = _mathsat.MSAT_VISIT_SKIP | |
| MSAT_VISIT_ABORT = _mathsat.MSAT_VISIT_ABORT | |
| class msat_proof_manager(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_proof_manager, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_proof_manager, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_proof_manager_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_proof_manager_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_proof_manager_repr_get, _mathsat.msat_proof_manager_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_proof_manager() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_proof_manager | |
| __del__ = lambda self : None; | |
| msat_proof_manager_swigregister = _mathsat.msat_proof_manager_swigregister | |
| msat_proof_manager_swigregister(msat_proof_manager) | |
| class msat_proof(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_proof, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_proof, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_proof_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_proof_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_proof_repr_get, _mathsat.msat_proof_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_proof() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_proof | |
| __del__ = lambda self : None; | |
| msat_proof_swigregister = _mathsat.msat_proof_swigregister | |
| msat_proof_swigregister(msat_proof) | |
| def msat_get_version(): | |
| return _mathsat.msat_get_version() | |
| msat_get_version = _mathsat.msat_get_version | |
| def msat_last_error_message(*args): | |
| return _mathsat.msat_last_error_message(*args) | |
| msat_last_error_message = _mathsat.msat_last_error_message | |
| def msat_create_config(): | |
| return _mathsat.msat_create_config() | |
| msat_create_config = _mathsat.msat_create_config | |
| def msat_create_default_config(*args): | |
| return _mathsat.msat_create_default_config(*args) | |
| msat_create_default_config = _mathsat.msat_create_default_config | |
| def _msat_parse_config(*args): | |
| return _mathsat._msat_parse_config(*args) | |
| _msat_parse_config = _mathsat._msat_parse_config | |
| def msat_destroy_config(*args): | |
| return _mathsat.msat_destroy_config(*args) | |
| msat_destroy_config = _mathsat.msat_destroy_config | |
| def _msat_create_env(*args): | |
| return _mathsat._msat_create_env(*args) | |
| _msat_create_env = _mathsat._msat_create_env | |
| def _msat_create_shared_env(*args): | |
| return _mathsat._msat_create_shared_env(*args) | |
| _msat_create_shared_env = _mathsat._msat_create_shared_env | |
| def msat_destroy_env(*args): | |
| return _mathsat.msat_destroy_env(*args) | |
| msat_destroy_env = _mathsat.msat_destroy_env | |
| def _msat_gc_env(*args): | |
| return _mathsat._msat_gc_env(*args) | |
| _msat_gc_env = _mathsat._msat_gc_env | |
| def msat_set_option(*args): | |
| return _mathsat.msat_set_option(*args) | |
| msat_set_option = _mathsat.msat_set_option | |
| def msat_set_termination_test(*args): | |
| return _mathsat.msat_set_termination_test(*args) | |
| msat_set_termination_test = _mathsat.msat_set_termination_test | |
| def msat_get_bool_type(*args): | |
| return _mathsat.msat_get_bool_type(*args) | |
| msat_get_bool_type = _mathsat.msat_get_bool_type | |
| def msat_get_rational_type(*args): | |
| return _mathsat.msat_get_rational_type(*args) | |
| msat_get_rational_type = _mathsat.msat_get_rational_type | |
| def msat_get_integer_type(*args): | |
| return _mathsat.msat_get_integer_type(*args) | |
| msat_get_integer_type = _mathsat.msat_get_integer_type | |
| def msat_get_bv_type(*args): | |
| return _mathsat.msat_get_bv_type(*args) | |
| msat_get_bv_type = _mathsat.msat_get_bv_type | |
| def msat_get_array_type(*args): | |
| return _mathsat.msat_get_array_type(*args) | |
| msat_get_array_type = _mathsat.msat_get_array_type | |
| def msat_get_fp_type(*args): | |
| return _mathsat.msat_get_fp_type(*args) | |
| msat_get_fp_type = _mathsat.msat_get_fp_type | |
| def msat_get_fp_roundingmode_type(*args): | |
| return _mathsat.msat_get_fp_roundingmode_type(*args) | |
| msat_get_fp_roundingmode_type = _mathsat.msat_get_fp_roundingmode_type | |
| def msat_get_simple_type(*args): | |
| return _mathsat.msat_get_simple_type(*args) | |
| msat_get_simple_type = _mathsat.msat_get_simple_type | |
| def _msat_get_function_type(*args): | |
| return _mathsat._msat_get_function_type(*args) | |
| _msat_get_function_type = _mathsat._msat_get_function_type | |
| def msat_is_bool_type(*args): | |
| return _mathsat.msat_is_bool_type(*args) | |
| msat_is_bool_type = _mathsat.msat_is_bool_type | |
| def msat_is_rational_type(*args): | |
| return _mathsat.msat_is_rational_type(*args) | |
| msat_is_rational_type = _mathsat.msat_is_rational_type | |
| def msat_is_integer_type(*args): | |
| return _mathsat.msat_is_integer_type(*args) | |
| msat_is_integer_type = _mathsat.msat_is_integer_type | |
| def _msat_is_bv_type(*args): | |
| return _mathsat._msat_is_bv_type(*args) | |
| _msat_is_bv_type = _mathsat._msat_is_bv_type | |
| def _msat_is_array_type(*args): | |
| return _mathsat._msat_is_array_type(*args) | |
| _msat_is_array_type = _mathsat._msat_is_array_type | |
| def _msat_is_fp_type(*args): | |
| return _mathsat._msat_is_fp_type(*args) | |
| _msat_is_fp_type = _mathsat._msat_is_fp_type | |
| def msat_is_fp_roundingmode_type(*args): | |
| return _mathsat.msat_is_fp_roundingmode_type(*args) | |
| msat_is_fp_roundingmode_type = _mathsat.msat_is_fp_roundingmode_type | |
| def msat_type_equals(*args): | |
| return _mathsat.msat_type_equals(*args) | |
| msat_type_equals = _mathsat.msat_type_equals | |
| def msat_type_repr(*args): | |
| return _mathsat.msat_type_repr(*args) | |
| msat_type_repr = _mathsat.msat_type_repr | |
| def msat_declare_function(*args): | |
| return _mathsat.msat_declare_function(*args) | |
| msat_declare_function = _mathsat.msat_declare_function | |
| def msat_make_true(*args): | |
| return _mathsat.msat_make_true(*args) | |
| msat_make_true = _mathsat.msat_make_true | |
| def msat_make_false(*args): | |
| return _mathsat.msat_make_false(*args) | |
| msat_make_false = _mathsat.msat_make_false | |
| def msat_make_iff(*args): | |
| return _mathsat.msat_make_iff(*args) | |
| msat_make_iff = _mathsat.msat_make_iff | |
| def msat_make_or(*args): | |
| return _mathsat.msat_make_or(*args) | |
| msat_make_or = _mathsat.msat_make_or | |
| def msat_make_and(*args): | |
| return _mathsat.msat_make_and(*args) | |
| msat_make_and = _mathsat.msat_make_and | |
| def msat_make_not(*args): | |
| return _mathsat.msat_make_not(*args) | |
| msat_make_not = _mathsat.msat_make_not | |
| def msat_make_equal(*args): | |
| return _mathsat.msat_make_equal(*args) | |
| msat_make_equal = _mathsat.msat_make_equal | |
| def msat_make_eq(*args): | |
| return _mathsat.msat_make_eq(*args) | |
| msat_make_eq = _mathsat.msat_make_eq | |
| def msat_make_leq(*args): | |
| return _mathsat.msat_make_leq(*args) | |
| msat_make_leq = _mathsat.msat_make_leq | |
| def msat_make_plus(*args): | |
| return _mathsat.msat_make_plus(*args) | |
| msat_make_plus = _mathsat.msat_make_plus | |
| def msat_make_times(*args): | |
| return _mathsat.msat_make_times(*args) | |
| msat_make_times = _mathsat.msat_make_times | |
| def _msat_make_int_modular_congruence(*args): | |
| return _mathsat._msat_make_int_modular_congruence(*args) | |
| _msat_make_int_modular_congruence = _mathsat._msat_make_int_modular_congruence | |
| def msat_make_floor(*args): | |
| return _mathsat.msat_make_floor(*args) | |
| msat_make_floor = _mathsat.msat_make_floor | |
| def msat_make_number(*args): | |
| return _mathsat.msat_make_number(*args) | |
| msat_make_number = _mathsat.msat_make_number | |
| def msat_make_term_ite(*args): | |
| return _mathsat.msat_make_term_ite(*args) | |
| msat_make_term_ite = _mathsat.msat_make_term_ite | |
| def msat_make_constant(*args): | |
| return _mathsat.msat_make_constant(*args) | |
| msat_make_constant = _mathsat.msat_make_constant | |
| def msat_make_uf(*args): | |
| return _mathsat.msat_make_uf(*args) | |
| msat_make_uf = _mathsat.msat_make_uf | |
| def msat_make_array_read(*args): | |
| return _mathsat.msat_make_array_read(*args) | |
| msat_make_array_read = _mathsat.msat_make_array_read | |
| def msat_make_array_write(*args): | |
| return _mathsat.msat_make_array_write(*args) | |
| msat_make_array_write = _mathsat.msat_make_array_write | |
| def msat_make_array_const(*args): | |
| return _mathsat.msat_make_array_const(*args) | |
| msat_make_array_const = _mathsat.msat_make_array_const | |
| def msat_make_bv_number(*args): | |
| return _mathsat.msat_make_bv_number(*args) | |
| msat_make_bv_number = _mathsat.msat_make_bv_number | |
| def msat_make_bv_concat(*args): | |
| return _mathsat.msat_make_bv_concat(*args) | |
| msat_make_bv_concat = _mathsat.msat_make_bv_concat | |
| def msat_make_bv_extract(*args): | |
| return _mathsat.msat_make_bv_extract(*args) | |
| msat_make_bv_extract = _mathsat.msat_make_bv_extract | |
| def msat_make_bv_or(*args): | |
| return _mathsat.msat_make_bv_or(*args) | |
| msat_make_bv_or = _mathsat.msat_make_bv_or | |
| def msat_make_bv_xor(*args): | |
| return _mathsat.msat_make_bv_xor(*args) | |
| msat_make_bv_xor = _mathsat.msat_make_bv_xor | |
| def msat_make_bv_and(*args): | |
| return _mathsat.msat_make_bv_and(*args) | |
| msat_make_bv_and = _mathsat.msat_make_bv_and | |
| def msat_make_bv_not(*args): | |
| return _mathsat.msat_make_bv_not(*args) | |
| msat_make_bv_not = _mathsat.msat_make_bv_not | |
| def msat_make_bv_lshl(*args): | |
| return _mathsat.msat_make_bv_lshl(*args) | |
| msat_make_bv_lshl = _mathsat.msat_make_bv_lshl | |
| def msat_make_bv_lshr(*args): | |
| return _mathsat.msat_make_bv_lshr(*args) | |
| msat_make_bv_lshr = _mathsat.msat_make_bv_lshr | |
| def msat_make_bv_ashr(*args): | |
| return _mathsat.msat_make_bv_ashr(*args) | |
| msat_make_bv_ashr = _mathsat.msat_make_bv_ashr | |
| def msat_make_bv_zext(*args): | |
| return _mathsat.msat_make_bv_zext(*args) | |
| msat_make_bv_zext = _mathsat.msat_make_bv_zext | |
| def msat_make_bv_sext(*args): | |
| return _mathsat.msat_make_bv_sext(*args) | |
| msat_make_bv_sext = _mathsat.msat_make_bv_sext | |
| def msat_make_bv_plus(*args): | |
| return _mathsat.msat_make_bv_plus(*args) | |
| msat_make_bv_plus = _mathsat.msat_make_bv_plus | |
| def msat_make_bv_minus(*args): | |
| return _mathsat.msat_make_bv_minus(*args) | |
| msat_make_bv_minus = _mathsat.msat_make_bv_minus | |
| def msat_make_bv_neg(*args): | |
| return _mathsat.msat_make_bv_neg(*args) | |
| msat_make_bv_neg = _mathsat.msat_make_bv_neg | |
| def msat_make_bv_times(*args): | |
| return _mathsat.msat_make_bv_times(*args) | |
| msat_make_bv_times = _mathsat.msat_make_bv_times | |
| def msat_make_bv_udiv(*args): | |
| return _mathsat.msat_make_bv_udiv(*args) | |
| msat_make_bv_udiv = _mathsat.msat_make_bv_udiv | |
| def msat_make_bv_urem(*args): | |
| return _mathsat.msat_make_bv_urem(*args) | |
| msat_make_bv_urem = _mathsat.msat_make_bv_urem | |
| def msat_make_bv_sdiv(*args): | |
| return _mathsat.msat_make_bv_sdiv(*args) | |
| msat_make_bv_sdiv = _mathsat.msat_make_bv_sdiv | |
| def msat_make_bv_srem(*args): | |
| return _mathsat.msat_make_bv_srem(*args) | |
| msat_make_bv_srem = _mathsat.msat_make_bv_srem | |
| def msat_make_bv_ult(*args): | |
| return _mathsat.msat_make_bv_ult(*args) | |
| msat_make_bv_ult = _mathsat.msat_make_bv_ult | |
| def msat_make_bv_uleq(*args): | |
| return _mathsat.msat_make_bv_uleq(*args) | |
| msat_make_bv_uleq = _mathsat.msat_make_bv_uleq | |
| def msat_make_bv_slt(*args): | |
| return _mathsat.msat_make_bv_slt(*args) | |
| msat_make_bv_slt = _mathsat.msat_make_bv_slt | |
| def msat_make_bv_sleq(*args): | |
| return _mathsat.msat_make_bv_sleq(*args) | |
| msat_make_bv_sleq = _mathsat.msat_make_bv_sleq | |
| def msat_make_bv_rol(*args): | |
| return _mathsat.msat_make_bv_rol(*args) | |
| msat_make_bv_rol = _mathsat.msat_make_bv_rol | |
| def msat_make_bv_ror(*args): | |
| return _mathsat.msat_make_bv_ror(*args) | |
| msat_make_bv_ror = _mathsat.msat_make_bv_ror | |
| def msat_make_bv_comp(*args): | |
| return _mathsat.msat_make_bv_comp(*args) | |
| msat_make_bv_comp = _mathsat.msat_make_bv_comp | |
| def msat_make_fp_roundingmode_nearest_even(*args): | |
| return _mathsat.msat_make_fp_roundingmode_nearest_even(*args) | |
| msat_make_fp_roundingmode_nearest_even = _mathsat.msat_make_fp_roundingmode_nearest_even | |
| def msat_make_fp_roundingmode_zero(*args): | |
| return _mathsat.msat_make_fp_roundingmode_zero(*args) | |
| msat_make_fp_roundingmode_zero = _mathsat.msat_make_fp_roundingmode_zero | |
| def msat_make_fp_roundingmode_plus_inf(*args): | |
| return _mathsat.msat_make_fp_roundingmode_plus_inf(*args) | |
| msat_make_fp_roundingmode_plus_inf = _mathsat.msat_make_fp_roundingmode_plus_inf | |
| def msat_make_fp_roundingmode_minus_inf(*args): | |
| return _mathsat.msat_make_fp_roundingmode_minus_inf(*args) | |
| msat_make_fp_roundingmode_minus_inf = _mathsat.msat_make_fp_roundingmode_minus_inf | |
| def msat_make_fp_equal(*args): | |
| return _mathsat.msat_make_fp_equal(*args) | |
| msat_make_fp_equal = _mathsat.msat_make_fp_equal | |
| def msat_make_fp_lt(*args): | |
| return _mathsat.msat_make_fp_lt(*args) | |
| msat_make_fp_lt = _mathsat.msat_make_fp_lt | |
| def msat_make_fp_leq(*args): | |
| return _mathsat.msat_make_fp_leq(*args) | |
| msat_make_fp_leq = _mathsat.msat_make_fp_leq | |
| def msat_make_fp_neg(*args): | |
| return _mathsat.msat_make_fp_neg(*args) | |
| msat_make_fp_neg = _mathsat.msat_make_fp_neg | |
| def msat_make_fp_plus(*args): | |
| return _mathsat.msat_make_fp_plus(*args) | |
| msat_make_fp_plus = _mathsat.msat_make_fp_plus | |
| def msat_make_fp_minus(*args): | |
| return _mathsat.msat_make_fp_minus(*args) | |
| msat_make_fp_minus = _mathsat.msat_make_fp_minus | |
| def msat_make_fp_times(*args): | |
| return _mathsat.msat_make_fp_times(*args) | |
| msat_make_fp_times = _mathsat.msat_make_fp_times | |
| def msat_make_fp_div(*args): | |
| return _mathsat.msat_make_fp_div(*args) | |
| msat_make_fp_div = _mathsat.msat_make_fp_div | |
| def msat_make_fp_sqrt(*args): | |
| return _mathsat.msat_make_fp_sqrt(*args) | |
| msat_make_fp_sqrt = _mathsat.msat_make_fp_sqrt | |
| def msat_make_fp_abs(*args): | |
| return _mathsat.msat_make_fp_abs(*args) | |
| msat_make_fp_abs = _mathsat.msat_make_fp_abs | |
| def msat_make_fp_min(*args): | |
| return _mathsat.msat_make_fp_min(*args) | |
| msat_make_fp_min = _mathsat.msat_make_fp_min | |
| def msat_make_fp_max(*args): | |
| return _mathsat.msat_make_fp_max(*args) | |
| msat_make_fp_max = _mathsat.msat_make_fp_max | |
| def msat_make_fp_round_to_int(*args): | |
| return _mathsat.msat_make_fp_round_to_int(*args) | |
| msat_make_fp_round_to_int = _mathsat.msat_make_fp_round_to_int | |
| def msat_make_fp_cast(*args): | |
| return _mathsat.msat_make_fp_cast(*args) | |
| msat_make_fp_cast = _mathsat.msat_make_fp_cast | |
| def msat_make_fp_to_bv(*args): | |
| return _mathsat.msat_make_fp_to_bv(*args) | |
| msat_make_fp_to_bv = _mathsat.msat_make_fp_to_bv | |
| def msat_make_fp_from_sbv(*args): | |
| return _mathsat.msat_make_fp_from_sbv(*args) | |
| msat_make_fp_from_sbv = _mathsat.msat_make_fp_from_sbv | |
| def msat_make_fp_from_ubv(*args): | |
| return _mathsat.msat_make_fp_from_ubv(*args) | |
| msat_make_fp_from_ubv = _mathsat.msat_make_fp_from_ubv | |
| def msat_make_fp_as_ieeebv(*args): | |
| return _mathsat.msat_make_fp_as_ieeebv(*args) | |
| msat_make_fp_as_ieeebv = _mathsat.msat_make_fp_as_ieeebv | |
| def msat_make_fp_from_ieeebv(*args): | |
| return _mathsat.msat_make_fp_from_ieeebv(*args) | |
| msat_make_fp_from_ieeebv = _mathsat.msat_make_fp_from_ieeebv | |
| def msat_make_fp_isnan(*args): | |
| return _mathsat.msat_make_fp_isnan(*args) | |
| msat_make_fp_isnan = _mathsat.msat_make_fp_isnan | |
| def msat_make_fp_isinf(*args): | |
| return _mathsat.msat_make_fp_isinf(*args) | |
| msat_make_fp_isinf = _mathsat.msat_make_fp_isinf | |
| def msat_make_fp_iszero(*args): | |
| return _mathsat.msat_make_fp_iszero(*args) | |
| msat_make_fp_iszero = _mathsat.msat_make_fp_iszero | |
| def msat_make_fp_issubnormal(*args): | |
| return _mathsat.msat_make_fp_issubnormal(*args) | |
| msat_make_fp_issubnormal = _mathsat.msat_make_fp_issubnormal | |
| def msat_make_fp_isnormal(*args): | |
| return _mathsat.msat_make_fp_isnormal(*args) | |
| msat_make_fp_isnormal = _mathsat.msat_make_fp_isnormal | |
| def msat_make_fp_isneg(*args): | |
| return _mathsat.msat_make_fp_isneg(*args) | |
| msat_make_fp_isneg = _mathsat.msat_make_fp_isneg | |
| def msat_make_fp_ispos(*args): | |
| return _mathsat.msat_make_fp_ispos(*args) | |
| msat_make_fp_ispos = _mathsat.msat_make_fp_ispos | |
| def msat_make_fp_plus_inf(*args): | |
| return _mathsat.msat_make_fp_plus_inf(*args) | |
| msat_make_fp_plus_inf = _mathsat.msat_make_fp_plus_inf | |
| def msat_make_fp_minus_inf(*args): | |
| return _mathsat.msat_make_fp_minus_inf(*args) | |
| msat_make_fp_minus_inf = _mathsat.msat_make_fp_minus_inf | |
| def msat_make_fp_nan(*args): | |
| return _mathsat.msat_make_fp_nan(*args) | |
| msat_make_fp_nan = _mathsat.msat_make_fp_nan | |
| def msat_make_fp_rat_number(*args): | |
| return _mathsat.msat_make_fp_rat_number(*args) | |
| msat_make_fp_rat_number = _mathsat.msat_make_fp_rat_number | |
| def msat_make_fp_bits_number(*args): | |
| return _mathsat.msat_make_fp_bits_number(*args) | |
| msat_make_fp_bits_number = _mathsat.msat_make_fp_bits_number | |
| def msat_make_int_to_bv(*args): | |
| return _mathsat.msat_make_int_to_bv(*args) | |
| msat_make_int_to_bv = _mathsat.msat_make_int_to_bv | |
| def msat_make_int_from_ubv(*args): | |
| return _mathsat.msat_make_int_from_ubv(*args) | |
| msat_make_int_from_ubv = _mathsat.msat_make_int_from_ubv | |
| def msat_make_int_from_sbv(*args): | |
| return _mathsat.msat_make_int_from_sbv(*args) | |
| msat_make_int_from_sbv = _mathsat.msat_make_int_from_sbv | |
| def msat_make_term(*args): | |
| return _mathsat.msat_make_term(*args) | |
| msat_make_term = _mathsat.msat_make_term | |
| def msat_make_copy_from(*args): | |
| return _mathsat.msat_make_copy_from(*args) | |
| msat_make_copy_from = _mathsat.msat_make_copy_from | |
| def msat_term_id(*args): | |
| return _mathsat.msat_term_id(*args) | |
| msat_term_id = _mathsat.msat_term_id | |
| def msat_term_arity(*args): | |
| return _mathsat.msat_term_arity(*args) | |
| msat_term_arity = _mathsat.msat_term_arity | |
| def msat_term_get_arg(*args): | |
| return _mathsat.msat_term_get_arg(*args) | |
| msat_term_get_arg = _mathsat.msat_term_get_arg | |
| def msat_term_get_type(*args): | |
| return _mathsat.msat_term_get_type(*args) | |
| msat_term_get_type = _mathsat.msat_term_get_type | |
| def msat_term_is_true(*args): | |
| return _mathsat.msat_term_is_true(*args) | |
| msat_term_is_true = _mathsat.msat_term_is_true | |
| def msat_term_is_false(*args): | |
| return _mathsat.msat_term_is_false(*args) | |
| msat_term_is_false = _mathsat.msat_term_is_false | |
| def msat_term_is_boolean_constant(*args): | |
| return _mathsat.msat_term_is_boolean_constant(*args) | |
| msat_term_is_boolean_constant = _mathsat.msat_term_is_boolean_constant | |
| def msat_term_is_atom(*args): | |
| return _mathsat.msat_term_is_atom(*args) | |
| msat_term_is_atom = _mathsat.msat_term_is_atom | |
| def msat_term_is_number(*args): | |
| return _mathsat.msat_term_is_number(*args) | |
| msat_term_is_number = _mathsat.msat_term_is_number | |
| def _msat_term_to_number(*args): | |
| return _mathsat._msat_term_to_number(*args) | |
| _msat_term_to_number = _mathsat._msat_term_to_number | |
| def msat_term_is_and(*args): | |
| return _mathsat.msat_term_is_and(*args) | |
| msat_term_is_and = _mathsat.msat_term_is_and | |
| def msat_term_is_or(*args): | |
| return _mathsat.msat_term_is_or(*args) | |
| msat_term_is_or = _mathsat.msat_term_is_or | |
| def msat_term_is_not(*args): | |
| return _mathsat.msat_term_is_not(*args) | |
| msat_term_is_not = _mathsat.msat_term_is_not | |
| def msat_term_is_iff(*args): | |
| return _mathsat.msat_term_is_iff(*args) | |
| msat_term_is_iff = _mathsat.msat_term_is_iff | |
| def msat_term_is_term_ite(*args): | |
| return _mathsat.msat_term_is_term_ite(*args) | |
| msat_term_is_term_ite = _mathsat.msat_term_is_term_ite | |
| def msat_term_is_constant(*args): | |
| return _mathsat.msat_term_is_constant(*args) | |
| msat_term_is_constant = _mathsat.msat_term_is_constant | |
| def msat_term_is_uf(*args): | |
| return _mathsat.msat_term_is_uf(*args) | |
| msat_term_is_uf = _mathsat.msat_term_is_uf | |
| def msat_term_is_equal(*args): | |
| return _mathsat.msat_term_is_equal(*args) | |
| msat_term_is_equal = _mathsat.msat_term_is_equal | |
| def msat_term_is_leq(*args): | |
| return _mathsat.msat_term_is_leq(*args) | |
| msat_term_is_leq = _mathsat.msat_term_is_leq | |
| def msat_term_is_plus(*args): | |
| return _mathsat.msat_term_is_plus(*args) | |
| msat_term_is_plus = _mathsat.msat_term_is_plus | |
| def msat_term_is_times(*args): | |
| return _mathsat.msat_term_is_times(*args) | |
| msat_term_is_times = _mathsat.msat_term_is_times | |
| def _msat_term_is_int_modular_congruence(*args): | |
| return _mathsat._msat_term_is_int_modular_congruence(*args) | |
| _msat_term_is_int_modular_congruence = _mathsat._msat_term_is_int_modular_congruence | |
| def msat_term_is_floor(*args): | |
| return _mathsat.msat_term_is_floor(*args) | |
| msat_term_is_floor = _mathsat.msat_term_is_floor | |
| def msat_term_is_array_read(*args): | |
| return _mathsat.msat_term_is_array_read(*args) | |
| msat_term_is_array_read = _mathsat.msat_term_is_array_read | |
| def msat_term_is_array_write(*args): | |
| return _mathsat.msat_term_is_array_write(*args) | |
| msat_term_is_array_write = _mathsat.msat_term_is_array_write | |
| def msat_term_is_array_const(*args): | |
| return _mathsat.msat_term_is_array_const(*args) | |
| msat_term_is_array_const = _mathsat.msat_term_is_array_const | |
| def msat_term_is_bv_concat(*args): | |
| return _mathsat.msat_term_is_bv_concat(*args) | |
| msat_term_is_bv_concat = _mathsat.msat_term_is_bv_concat | |
| def _msat_term_is_bv_extract(*args): | |
| return _mathsat._msat_term_is_bv_extract(*args) | |
| _msat_term_is_bv_extract = _mathsat._msat_term_is_bv_extract | |
| def msat_term_is_bv_or(*args): | |
| return _mathsat.msat_term_is_bv_or(*args) | |
| msat_term_is_bv_or = _mathsat.msat_term_is_bv_or | |
| def msat_term_is_bv_xor(*args): | |
| return _mathsat.msat_term_is_bv_xor(*args) | |
| msat_term_is_bv_xor = _mathsat.msat_term_is_bv_xor | |
| def msat_term_is_bv_and(*args): | |
| return _mathsat.msat_term_is_bv_and(*args) | |
| msat_term_is_bv_and = _mathsat.msat_term_is_bv_and | |
| def msat_term_is_bv_not(*args): | |
| return _mathsat.msat_term_is_bv_not(*args) | |
| msat_term_is_bv_not = _mathsat.msat_term_is_bv_not | |
| def msat_term_is_bv_plus(*args): | |
| return _mathsat.msat_term_is_bv_plus(*args) | |
| msat_term_is_bv_plus = _mathsat.msat_term_is_bv_plus | |
| def msat_term_is_bv_minus(*args): | |
| return _mathsat.msat_term_is_bv_minus(*args) | |
| msat_term_is_bv_minus = _mathsat.msat_term_is_bv_minus | |
| def msat_term_is_bv_times(*args): | |
| return _mathsat.msat_term_is_bv_times(*args) | |
| msat_term_is_bv_times = _mathsat.msat_term_is_bv_times | |
| def msat_term_is_bv_neg(*args): | |
| return _mathsat.msat_term_is_bv_neg(*args) | |
| msat_term_is_bv_neg = _mathsat.msat_term_is_bv_neg | |
| def msat_term_is_bv_udiv(*args): | |
| return _mathsat.msat_term_is_bv_udiv(*args) | |
| msat_term_is_bv_udiv = _mathsat.msat_term_is_bv_udiv | |
| def msat_term_is_bv_urem(*args): | |
| return _mathsat.msat_term_is_bv_urem(*args) | |
| msat_term_is_bv_urem = _mathsat.msat_term_is_bv_urem | |
| def msat_term_is_bv_sdiv(*args): | |
| return _mathsat.msat_term_is_bv_sdiv(*args) | |
| msat_term_is_bv_sdiv = _mathsat.msat_term_is_bv_sdiv | |
| def msat_term_is_bv_srem(*args): | |
| return _mathsat.msat_term_is_bv_srem(*args) | |
| msat_term_is_bv_srem = _mathsat.msat_term_is_bv_srem | |
| def msat_term_is_bv_ult(*args): | |
| return _mathsat.msat_term_is_bv_ult(*args) | |
| msat_term_is_bv_ult = _mathsat.msat_term_is_bv_ult | |
| def msat_term_is_bv_uleq(*args): | |
| return _mathsat.msat_term_is_bv_uleq(*args) | |
| msat_term_is_bv_uleq = _mathsat.msat_term_is_bv_uleq | |
| def msat_term_is_bv_slt(*args): | |
| return _mathsat.msat_term_is_bv_slt(*args) | |
| msat_term_is_bv_slt = _mathsat.msat_term_is_bv_slt | |
| def msat_term_is_bv_sleq(*args): | |
| return _mathsat.msat_term_is_bv_sleq(*args) | |
| msat_term_is_bv_sleq = _mathsat.msat_term_is_bv_sleq | |
| def msat_term_is_bv_lshl(*args): | |
| return _mathsat.msat_term_is_bv_lshl(*args) | |
| msat_term_is_bv_lshl = _mathsat.msat_term_is_bv_lshl | |
| def msat_term_is_bv_lshr(*args): | |
| return _mathsat.msat_term_is_bv_lshr(*args) | |
| msat_term_is_bv_lshr = _mathsat.msat_term_is_bv_lshr | |
| def msat_term_is_bv_ashr(*args): | |
| return _mathsat.msat_term_is_bv_ashr(*args) | |
| msat_term_is_bv_ashr = _mathsat.msat_term_is_bv_ashr | |
| def _msat_term_is_bv_zext(*args): | |
| return _mathsat._msat_term_is_bv_zext(*args) | |
| _msat_term_is_bv_zext = _mathsat._msat_term_is_bv_zext | |
| def _msat_term_is_bv_sext(*args): | |
| return _mathsat._msat_term_is_bv_sext(*args) | |
| _msat_term_is_bv_sext = _mathsat._msat_term_is_bv_sext | |
| def _msat_term_is_bv_rol(*args): | |
| return _mathsat._msat_term_is_bv_rol(*args) | |
| _msat_term_is_bv_rol = _mathsat._msat_term_is_bv_rol | |
| def _msat_term_is_bv_ror(*args): | |
| return _mathsat._msat_term_is_bv_ror(*args) | |
| _msat_term_is_bv_ror = _mathsat._msat_term_is_bv_ror | |
| def msat_term_is_bv_comp(*args): | |
| return _mathsat.msat_term_is_bv_comp(*args) | |
| msat_term_is_bv_comp = _mathsat.msat_term_is_bv_comp | |
| def msat_term_is_fp_roundingmode_nearest_even(*args): | |
| return _mathsat.msat_term_is_fp_roundingmode_nearest_even(*args) | |
| msat_term_is_fp_roundingmode_nearest_even = _mathsat.msat_term_is_fp_roundingmode_nearest_even | |
| def msat_term_is_fp_roundingmode_zero(*args): | |
| return _mathsat.msat_term_is_fp_roundingmode_zero(*args) | |
| msat_term_is_fp_roundingmode_zero = _mathsat.msat_term_is_fp_roundingmode_zero | |
| def msat_term_is_fp_roundingmode_plus_inf(*args): | |
| return _mathsat.msat_term_is_fp_roundingmode_plus_inf(*args) | |
| msat_term_is_fp_roundingmode_plus_inf = _mathsat.msat_term_is_fp_roundingmode_plus_inf | |
| def msat_term_is_fp_roundingmode_minus_inf(*args): | |
| return _mathsat.msat_term_is_fp_roundingmode_minus_inf(*args) | |
| msat_term_is_fp_roundingmode_minus_inf = _mathsat.msat_term_is_fp_roundingmode_minus_inf | |
| def msat_term_is_fp_equal(*args): | |
| return _mathsat.msat_term_is_fp_equal(*args) | |
| msat_term_is_fp_equal = _mathsat.msat_term_is_fp_equal | |
| def msat_term_is_fp_lt(*args): | |
| return _mathsat.msat_term_is_fp_lt(*args) | |
| msat_term_is_fp_lt = _mathsat.msat_term_is_fp_lt | |
| def msat_term_is_fp_leq(*args): | |
| return _mathsat.msat_term_is_fp_leq(*args) | |
| msat_term_is_fp_leq = _mathsat.msat_term_is_fp_leq | |
| def msat_term_is_fp_neg(*args): | |
| return _mathsat.msat_term_is_fp_neg(*args) | |
| msat_term_is_fp_neg = _mathsat.msat_term_is_fp_neg | |
| def msat_term_is_fp_plus(*args): | |
| return _mathsat.msat_term_is_fp_plus(*args) | |
| msat_term_is_fp_plus = _mathsat.msat_term_is_fp_plus | |
| def msat_term_is_fp_minus(*args): | |
| return _mathsat.msat_term_is_fp_minus(*args) | |
| msat_term_is_fp_minus = _mathsat.msat_term_is_fp_minus | |
| def msat_term_is_fp_times(*args): | |
| return _mathsat.msat_term_is_fp_times(*args) | |
| msat_term_is_fp_times = _mathsat.msat_term_is_fp_times | |
| def msat_term_is_fp_div(*args): | |
| return _mathsat.msat_term_is_fp_div(*args) | |
| msat_term_is_fp_div = _mathsat.msat_term_is_fp_div | |
| def msat_term_is_fp_sqrt(*args): | |
| return _mathsat.msat_term_is_fp_sqrt(*args) | |
| msat_term_is_fp_sqrt = _mathsat.msat_term_is_fp_sqrt | |
| def msat_term_is_fp_abs(*args): | |
| return _mathsat.msat_term_is_fp_abs(*args) | |
| msat_term_is_fp_abs = _mathsat.msat_term_is_fp_abs | |
| def msat_term_is_fp_min(*args): | |
| return _mathsat.msat_term_is_fp_min(*args) | |
| msat_term_is_fp_min = _mathsat.msat_term_is_fp_min | |
| def msat_term_is_fp_max(*args): | |
| return _mathsat.msat_term_is_fp_max(*args) | |
| msat_term_is_fp_max = _mathsat.msat_term_is_fp_max | |
| def msat_term_is_fp_round_to_int(*args): | |
| return _mathsat.msat_term_is_fp_round_to_int(*args) | |
| msat_term_is_fp_round_to_int = _mathsat.msat_term_is_fp_round_to_int | |
| def msat_term_is_fp_cast(*args): | |
| return _mathsat.msat_term_is_fp_cast(*args) | |
| msat_term_is_fp_cast = _mathsat.msat_term_is_fp_cast | |
| def msat_term_is_fp_to_bv(*args): | |
| return _mathsat.msat_term_is_fp_to_bv(*args) | |
| msat_term_is_fp_to_bv = _mathsat.msat_term_is_fp_to_bv | |
| def msat_term_is_fp_from_sbv(*args): | |
| return _mathsat.msat_term_is_fp_from_sbv(*args) | |
| msat_term_is_fp_from_sbv = _mathsat.msat_term_is_fp_from_sbv | |
| def msat_term_is_fp_from_ubv(*args): | |
| return _mathsat.msat_term_is_fp_from_ubv(*args) | |
| msat_term_is_fp_from_ubv = _mathsat.msat_term_is_fp_from_ubv | |
| def msat_term_is_fp_as_ieeebv(*args): | |
| return _mathsat.msat_term_is_fp_as_ieeebv(*args) | |
| msat_term_is_fp_as_ieeebv = _mathsat.msat_term_is_fp_as_ieeebv | |
| def msat_term_is_fp_from_ieeebv(*args): | |
| return _mathsat.msat_term_is_fp_from_ieeebv(*args) | |
| msat_term_is_fp_from_ieeebv = _mathsat.msat_term_is_fp_from_ieeebv | |
| def msat_term_is_fp_isnan(*args): | |
| return _mathsat.msat_term_is_fp_isnan(*args) | |
| msat_term_is_fp_isnan = _mathsat.msat_term_is_fp_isnan | |
| def msat_term_is_fp_isinf(*args): | |
| return _mathsat.msat_term_is_fp_isinf(*args) | |
| msat_term_is_fp_isinf = _mathsat.msat_term_is_fp_isinf | |
| def msat_term_is_fp_iszero(*args): | |
| return _mathsat.msat_term_is_fp_iszero(*args) | |
| msat_term_is_fp_iszero = _mathsat.msat_term_is_fp_iszero | |
| def msat_term_is_fp_issubnormal(*args): | |
| return _mathsat.msat_term_is_fp_issubnormal(*args) | |
| msat_term_is_fp_issubnormal = _mathsat.msat_term_is_fp_issubnormal | |
| def msat_term_is_fp_isnormal(*args): | |
| return _mathsat.msat_term_is_fp_isnormal(*args) | |
| msat_term_is_fp_isnormal = _mathsat.msat_term_is_fp_isnormal | |
| def msat_term_is_fp_isneg(*args): | |
| return _mathsat.msat_term_is_fp_isneg(*args) | |
| msat_term_is_fp_isneg = _mathsat.msat_term_is_fp_isneg | |
| def msat_term_is_fp_ispos(*args): | |
| return _mathsat.msat_term_is_fp_ispos(*args) | |
| msat_term_is_fp_ispos = _mathsat.msat_term_is_fp_ispos | |
| def msat_term_is_int_to_bv(*args): | |
| return _mathsat.msat_term_is_int_to_bv(*args) | |
| msat_term_is_int_to_bv = _mathsat.msat_term_is_int_to_bv | |
| def msat_term_is_int_from_ubv(*args): | |
| return _mathsat.msat_term_is_int_from_ubv(*args) | |
| msat_term_is_int_from_ubv = _mathsat.msat_term_is_int_from_ubv | |
| def msat_term_is_int_from_sbv(*args): | |
| return _mathsat.msat_term_is_int_from_sbv(*args) | |
| msat_term_is_int_from_sbv = _mathsat.msat_term_is_int_from_sbv | |
| def msat_visit_term(*args): | |
| return _mathsat.msat_visit_term(*args) | |
| msat_visit_term = _mathsat.msat_visit_term | |
| def _msat_apply_substitution(*args): | |
| return _mathsat._msat_apply_substitution(*args) | |
| _msat_apply_substitution = _mathsat._msat_apply_substitution | |
| def msat_find_decl(*args): | |
| return _mathsat.msat_find_decl(*args) | |
| msat_find_decl = _mathsat.msat_find_decl | |
| def msat_term_get_decl(*args): | |
| return _mathsat.msat_term_get_decl(*args) | |
| msat_term_get_decl = _mathsat.msat_term_get_decl | |
| def msat_decl_id(*args): | |
| return _mathsat.msat_decl_id(*args) | |
| msat_decl_id = _mathsat.msat_decl_id | |
| def msat_decl_get_tag(*args): | |
| return _mathsat.msat_decl_get_tag(*args) | |
| msat_decl_get_tag = _mathsat.msat_decl_get_tag | |
| def msat_decl_get_return_type(*args): | |
| return _mathsat.msat_decl_get_return_type(*args) | |
| msat_decl_get_return_type = _mathsat.msat_decl_get_return_type | |
| def msat_decl_get_arity(*args): | |
| return _mathsat.msat_decl_get_arity(*args) | |
| msat_decl_get_arity = _mathsat.msat_decl_get_arity | |
| def msat_decl_get_arg_type(*args): | |
| return _mathsat.msat_decl_get_arg_type(*args) | |
| msat_decl_get_arg_type = _mathsat.msat_decl_get_arg_type | |
| def msat_decl_get_name(*args): | |
| return _mathsat.msat_decl_get_name(*args) | |
| msat_decl_get_name = _mathsat.msat_decl_get_name | |
| def msat_decl_repr(*args): | |
| return _mathsat.msat_decl_repr(*args) | |
| msat_decl_repr = _mathsat.msat_decl_repr | |
| def msat_term_repr(*args): | |
| return _mathsat.msat_term_repr(*args) | |
| msat_term_repr = _mathsat.msat_term_repr | |
| def msat_from_string(*args): | |
| return _mathsat.msat_from_string(*args) | |
| msat_from_string = _mathsat.msat_from_string | |
| def msat_from_smtlib1(*args): | |
| return _mathsat.msat_from_smtlib1(*args) | |
| msat_from_smtlib1 = _mathsat.msat_from_smtlib1 | |
| def msat_from_smtlib2(*args): | |
| return _mathsat.msat_from_smtlib2(*args) | |
| msat_from_smtlib2 = _mathsat.msat_from_smtlib2 | |
| def msat_to_smtlib1(*args): | |
| return _mathsat.msat_to_smtlib1(*args) | |
| msat_to_smtlib1 = _mathsat.msat_to_smtlib1 | |
| def msat_to_smtlib2(*args): | |
| return _mathsat.msat_to_smtlib2(*args) | |
| msat_to_smtlib2 = _mathsat.msat_to_smtlib2 | |
| def msat_to_smtlib2_ext(*args): | |
| return _mathsat.msat_to_smtlib2_ext(*args) | |
| msat_to_smtlib2_ext = _mathsat.msat_to_smtlib2_ext | |
| def msat_to_smtlib2_term(*args): | |
| return _mathsat.msat_to_smtlib2_term(*args) | |
| msat_to_smtlib2_term = _mathsat.msat_to_smtlib2_term | |
| def _msat_named_list_from_smtlib2(*args): | |
| return _mathsat._msat_named_list_from_smtlib2(*args) | |
| _msat_named_list_from_smtlib2 = _mathsat._msat_named_list_from_smtlib2 | |
| def _msat_named_list_to_smtlib2(*args): | |
| return _mathsat._msat_named_list_to_smtlib2(*args) | |
| _msat_named_list_to_smtlib2 = _mathsat._msat_named_list_to_smtlib2 | |
| def _msat_annotated_list_from_smtlib2(*args): | |
| return _mathsat._msat_annotated_list_from_smtlib2(*args) | |
| _msat_annotated_list_from_smtlib2 = _mathsat._msat_annotated_list_from_smtlib2 | |
| def _msat_annotated_list_to_smtlib2(*args): | |
| return _mathsat._msat_annotated_list_to_smtlib2(*args) | |
| _msat_annotated_list_to_smtlib2 = _mathsat._msat_annotated_list_to_smtlib2 | |
| def msat_push_backtrack_point(*args): | |
| return _mathsat.msat_push_backtrack_point(*args) | |
| msat_push_backtrack_point = _mathsat.msat_push_backtrack_point | |
| def msat_pop_backtrack_point(*args): | |
| return _mathsat.msat_pop_backtrack_point(*args) | |
| msat_pop_backtrack_point = _mathsat.msat_pop_backtrack_point | |
| def msat_num_backtrack_points(*args): | |
| return _mathsat.msat_num_backtrack_points(*args) | |
| msat_num_backtrack_points = _mathsat.msat_num_backtrack_points | |
| def msat_reset_env(*args): | |
| return _mathsat.msat_reset_env(*args) | |
| msat_reset_env = _mathsat.msat_reset_env | |
| def msat_assert_formula(*args): | |
| return _mathsat.msat_assert_formula(*args) | |
| msat_assert_formula = _mathsat.msat_assert_formula | |
| def msat_add_preferred_for_branching(*args): | |
| return _mathsat.msat_add_preferred_for_branching(*args) | |
| msat_add_preferred_for_branching = _mathsat.msat_add_preferred_for_branching | |
| def msat_clear_preferred_for_branching(*args): | |
| return _mathsat.msat_clear_preferred_for_branching(*args) | |
| msat_clear_preferred_for_branching = _mathsat.msat_clear_preferred_for_branching | |
| def msat_solve(*args): | |
| return _mathsat.msat_solve(*args) | |
| msat_solve = _mathsat.msat_solve | |
| def _msat_solve_with_assumptions(*args): | |
| return _mathsat._msat_solve_with_assumptions(*args) | |
| _msat_solve_with_assumptions = _mathsat._msat_solve_with_assumptions | |
| def _msat_all_sat(*args): | |
| return _mathsat._msat_all_sat(*args) | |
| _msat_all_sat = _mathsat._msat_all_sat | |
| def _msat_solve_diversify(*args): | |
| return _mathsat._msat_solve_diversify(*args) | |
| _msat_solve_diversify = _mathsat._msat_solve_diversify | |
| def _msat_get_asserted_formulas(*args): | |
| return _mathsat._msat_get_asserted_formulas(*args) | |
| _msat_get_asserted_formulas = _mathsat._msat_get_asserted_formulas | |
| def _msat_get_theory_lemmas(*args): | |
| return _mathsat._msat_get_theory_lemmas(*args) | |
| _msat_get_theory_lemmas = _mathsat._msat_get_theory_lemmas | |
| def msat_get_search_stats(*args): | |
| return _mathsat.msat_get_search_stats(*args) | |
| msat_get_search_stats = _mathsat.msat_get_search_stats | |
| def msat_create_itp_group(*args): | |
| return _mathsat.msat_create_itp_group(*args) | |
| msat_create_itp_group = _mathsat.msat_create_itp_group | |
| def msat_set_itp_group(*args): | |
| return _mathsat.msat_set_itp_group(*args) | |
| msat_set_itp_group = _mathsat.msat_set_itp_group | |
| def _msat_get_interpolant(*args): | |
| return _mathsat._msat_get_interpolant(*args) | |
| _msat_get_interpolant = _mathsat._msat_get_interpolant | |
| def msat_get_model_value(*args): | |
| return _mathsat.msat_get_model_value(*args) | |
| msat_get_model_value = _mathsat.msat_get_model_value | |
| def msat_create_model_iterator(*args): | |
| return _mathsat.msat_create_model_iterator(*args) | |
| msat_create_model_iterator = _mathsat.msat_create_model_iterator | |
| def msat_model_iterator_has_next(*args): | |
| return _mathsat.msat_model_iterator_has_next(*args) | |
| msat_model_iterator_has_next = _mathsat.msat_model_iterator_has_next | |
| def _msat_model_iterator_next(*args): | |
| return _mathsat._msat_model_iterator_next(*args) | |
| _msat_model_iterator_next = _mathsat._msat_model_iterator_next | |
| def msat_destroy_model_iterator(*args): | |
| return _mathsat.msat_destroy_model_iterator(*args) | |
| msat_destroy_model_iterator = _mathsat.msat_destroy_model_iterator | |
| def msat_get_model(*args): | |
| return _mathsat.msat_get_model(*args) | |
| msat_get_model = _mathsat.msat_get_model | |
| def msat_destroy_model(*args): | |
| return _mathsat.msat_destroy_model(*args) | |
| msat_destroy_model = _mathsat.msat_destroy_model | |
| def msat_model_eval(*args): | |
| return _mathsat.msat_model_eval(*args) | |
| msat_model_eval = _mathsat.msat_model_eval | |
| def msat_model_create_iterator(*args): | |
| return _mathsat.msat_model_create_iterator(*args) | |
| msat_model_create_iterator = _mathsat.msat_model_create_iterator | |
| def _msat_get_unsat_core(*args): | |
| return _mathsat._msat_get_unsat_core(*args) | |
| _msat_get_unsat_core = _mathsat._msat_get_unsat_core | |
| def msat_get_unsat_core_ext(*args): | |
| return _mathsat.msat_get_unsat_core_ext(*args) | |
| msat_get_unsat_core_ext = _mathsat.msat_get_unsat_core_ext | |
| def _msat_get_unsat_assumptions(*args): | |
| return _mathsat._msat_get_unsat_assumptions(*args) | |
| _msat_get_unsat_assumptions = _mathsat._msat_get_unsat_assumptions | |
| def msat_get_proof_manager(*args): | |
| return _mathsat.msat_get_proof_manager(*args) | |
| msat_get_proof_manager = _mathsat.msat_get_proof_manager | |
| def msat_destroy_proof_manager(*args): | |
| return _mathsat.msat_destroy_proof_manager(*args) | |
| msat_destroy_proof_manager = _mathsat.msat_destroy_proof_manager | |
| def msat_get_proof(*args): | |
| return _mathsat.msat_get_proof(*args) | |
| msat_get_proof = _mathsat.msat_get_proof | |
| def msat_proof_id(*args): | |
| return _mathsat.msat_proof_id(*args) | |
| msat_proof_id = _mathsat.msat_proof_id | |
| def msat_proof_is_term(*args): | |
| return _mathsat.msat_proof_is_term(*args) | |
| msat_proof_is_term = _mathsat.msat_proof_is_term | |
| def msat_proof_get_term(*args): | |
| return _mathsat.msat_proof_get_term(*args) | |
| msat_proof_get_term = _mathsat.msat_proof_get_term | |
| def msat_proof_get_name(*args): | |
| return _mathsat.msat_proof_get_name(*args) | |
| msat_proof_get_name = _mathsat.msat_proof_get_name | |
| def msat_proof_get_arity(*args): | |
| return _mathsat.msat_proof_get_arity(*args) | |
| msat_proof_get_arity = _mathsat.msat_proof_get_arity | |
| def msat_proof_get_child(*args): | |
| return _mathsat.msat_proof_get_child(*args) | |
| msat_proof_get_child = _mathsat.msat_proof_get_child | |
| class msat_dpll_callback(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_dpll_callback, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_dpll_callback, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_dpll_callback_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_dpll_callback_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_dpll_callback_repr_get, _mathsat.msat_dpll_callback_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_dpll_callback() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_dpll_callback | |
| __del__ = lambda self : None; | |
| msat_dpll_callback_swigregister = _mathsat.msat_dpll_callback_swigregister | |
| msat_dpll_callback_swigregister(msat_dpll_callback) | |
| class msat_ext_dpll_interface(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_ext_dpll_interface, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_ext_dpll_interface, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["new_var"] = _mathsat.msat_ext_dpll_interface_new_var_set | |
| __swig_getmethods__["new_var"] = _mathsat.msat_ext_dpll_interface_new_var_get | |
| if _newclass:new_var = _swig_property(_mathsat.msat_ext_dpll_interface_new_var_get, _mathsat.msat_ext_dpll_interface_new_var_set) | |
| __swig_setmethods__["set_decision_var"] = _mathsat.msat_ext_dpll_interface_set_decision_var_set | |
| __swig_getmethods__["set_decision_var"] = _mathsat.msat_ext_dpll_interface_set_decision_var_get | |
| if _newclass:set_decision_var = _swig_property(_mathsat.msat_ext_dpll_interface_set_decision_var_get, _mathsat.msat_ext_dpll_interface_set_decision_var_set) | |
| __swig_setmethods__["set_frozen"] = _mathsat.msat_ext_dpll_interface_set_frozen_set | |
| __swig_getmethods__["set_frozen"] = _mathsat.msat_ext_dpll_interface_set_frozen_get | |
| if _newclass:set_frozen = _swig_property(_mathsat.msat_ext_dpll_interface_set_frozen_get, _mathsat.msat_ext_dpll_interface_set_frozen_set) | |
| __swig_setmethods__["add_clause"] = _mathsat.msat_ext_dpll_interface_add_clause_set | |
| __swig_getmethods__["add_clause"] = _mathsat.msat_ext_dpll_interface_add_clause_get | |
| if _newclass:add_clause = _swig_property(_mathsat.msat_ext_dpll_interface_add_clause_get, _mathsat.msat_ext_dpll_interface_add_clause_set) | |
| __swig_setmethods__["solve"] = _mathsat.msat_ext_dpll_interface_solve_set | |
| __swig_getmethods__["solve"] = _mathsat.msat_ext_dpll_interface_solve_get | |
| if _newclass:solve = _swig_property(_mathsat.msat_ext_dpll_interface_solve_get, _mathsat.msat_ext_dpll_interface_solve_set) | |
| __swig_setmethods__["model_value"] = _mathsat.msat_ext_dpll_interface_model_value_set | |
| __swig_getmethods__["model_value"] = _mathsat.msat_ext_dpll_interface_model_value_get | |
| if _newclass:model_value = _swig_property(_mathsat.msat_ext_dpll_interface_model_value_get, _mathsat.msat_ext_dpll_interface_model_value_set) | |
| __swig_setmethods__["enqueue_assignment"] = _mathsat.msat_ext_dpll_interface_enqueue_assignment_set | |
| __swig_getmethods__["enqueue_assignment"] = _mathsat.msat_ext_dpll_interface_enqueue_assignment_get | |
| if _newclass:enqueue_assignment = _swig_property(_mathsat.msat_ext_dpll_interface_enqueue_assignment_get, _mathsat.msat_ext_dpll_interface_enqueue_assignment_set) | |
| __swig_setmethods__["remove_clauses_containing"] = _mathsat.msat_ext_dpll_interface_remove_clauses_containing_set | |
| __swig_getmethods__["remove_clauses_containing"] = _mathsat.msat_ext_dpll_interface_remove_clauses_containing_get | |
| if _newclass:remove_clauses_containing = _swig_property(_mathsat.msat_ext_dpll_interface_remove_clauses_containing_get, _mathsat.msat_ext_dpll_interface_remove_clauses_containing_set) | |
| __swig_setmethods__["reset"] = _mathsat.msat_ext_dpll_interface_reset_set | |
| __swig_getmethods__["reset"] = _mathsat.msat_ext_dpll_interface_reset_get | |
| if _newclass:reset = _swig_property(_mathsat.msat_ext_dpll_interface_reset_get, _mathsat.msat_ext_dpll_interface_reset_set) | |
| __swig_setmethods__["set_callback"] = _mathsat.msat_ext_dpll_interface_set_callback_set | |
| __swig_getmethods__["set_callback"] = _mathsat.msat_ext_dpll_interface_set_callback_get | |
| if _newclass:set_callback = _swig_property(_mathsat.msat_ext_dpll_interface_set_callback_get, _mathsat.msat_ext_dpll_interface_set_callback_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_ext_dpll_interface() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_ext_dpll_interface | |
| __del__ = lambda self : None; | |
| msat_ext_dpll_interface_swigregister = _mathsat.msat_ext_dpll_interface_swigregister | |
| msat_ext_dpll_interface_swigregister(msat_ext_dpll_interface) | |
| def msat_set_external_dpll_engine(*args): | |
| return _mathsat.msat_set_external_dpll_engine(*args) | |
| msat_set_external_dpll_engine = _mathsat.msat_set_external_dpll_engine | |
| def msat_dpll_callback_no_conflict_after_bcp(*args): | |
| return _mathsat.msat_dpll_callback_no_conflict_after_bcp(*args) | |
| msat_dpll_callback_no_conflict_after_bcp = _mathsat.msat_dpll_callback_no_conflict_after_bcp | |
| def msat_dpll_callback_model_found(*args): | |
| return _mathsat.msat_dpll_callback_model_found(*args) | |
| msat_dpll_callback_model_found = _mathsat.msat_dpll_callback_model_found | |
| def msat_dpll_callback_notify_assignment(*args): | |
| return _mathsat.msat_dpll_callback_notify_assignment(*args) | |
| msat_dpll_callback_notify_assignment = _mathsat.msat_dpll_callback_notify_assignment | |
| def msat_dpll_callback_notify_new_level(*args): | |
| return _mathsat.msat_dpll_callback_notify_new_level(*args) | |
| msat_dpll_callback_notify_new_level = _mathsat.msat_dpll_callback_notify_new_level | |
| def msat_dpll_callback_notify_backtrack(*args): | |
| return _mathsat.msat_dpll_callback_notify_backtrack(*args) | |
| msat_dpll_callback_notify_backtrack = _mathsat.msat_dpll_callback_notify_backtrack | |
| def msat_dpll_callback_ask_theory_reason(*args): | |
| return _mathsat.msat_dpll_callback_ask_theory_reason(*args) | |
| msat_dpll_callback_ask_theory_reason = _mathsat.msat_dpll_callback_ask_theory_reason | |
| MSAT_EXIST_ELIM_ALLSMT_FM = _mathsat.MSAT_EXIST_ELIM_ALLSMT_FM | |
| MSAT_EXIST_ELIM_VTS = _mathsat.MSAT_EXIST_ELIM_VTS | |
| class msat_exist_elim_options(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_exist_elim_options, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_exist_elim_options, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["toplevel_propagation"] = _mathsat.msat_exist_elim_options_toplevel_propagation_set | |
| __swig_getmethods__["toplevel_propagation"] = _mathsat.msat_exist_elim_options_toplevel_propagation_get | |
| if _newclass:toplevel_propagation = _swig_property(_mathsat.msat_exist_elim_options_toplevel_propagation_get, _mathsat.msat_exist_elim_options_toplevel_propagation_set) | |
| __swig_setmethods__["boolean_simplifications"] = _mathsat.msat_exist_elim_options_boolean_simplifications_set | |
| __swig_getmethods__["boolean_simplifications"] = _mathsat.msat_exist_elim_options_boolean_simplifications_get | |
| if _newclass:boolean_simplifications = _swig_property(_mathsat.msat_exist_elim_options_boolean_simplifications_get, _mathsat.msat_exist_elim_options_boolean_simplifications_set) | |
| __swig_setmethods__["remove_redundant_constraints"] = _mathsat.msat_exist_elim_options_remove_redundant_constraints_set | |
| __swig_getmethods__["remove_redundant_constraints"] = _mathsat.msat_exist_elim_options_remove_redundant_constraints_get | |
| if _newclass:remove_redundant_constraints = _swig_property(_mathsat.msat_exist_elim_options_remove_redundant_constraints_get, _mathsat.msat_exist_elim_options_remove_redundant_constraints_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_exist_elim_options() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_exist_elim_options | |
| __del__ = lambda self : None; | |
| msat_exist_elim_options_swigregister = _mathsat.msat_exist_elim_options_swigregister | |
| msat_exist_elim_options_swigregister(msat_exist_elim_options) | |
| def _msat_exist_elim(*args): | |
| return _mathsat._msat_exist_elim(*args) | |
| _msat_exist_elim = _mathsat._msat_exist_elim | |
| def _msat_exist_elim_model(*args): | |
| return _mathsat._msat_exist_elim_model(*args) | |
| _msat_exist_elim_model = _mathsat._msat_exist_elim_model | |
| def msat_aig_simplify(*args): | |
| return _mathsat.msat_aig_simplify(*args) | |
| msat_aig_simplify = _mathsat.msat_aig_simplify | |
| def msat_to_nnf(*args): | |
| return _mathsat.msat_to_nnf(*args) | |
| msat_to_nnf = _mathsat.msat_to_nnf | |
| def msat_lra_simplify(*args): | |
| return _mathsat.msat_lra_simplify(*args) | |
| msat_lra_simplify = _mathsat.msat_lra_simplify | |
| class msat_ic3(_object): | |
| __swig_setmethods__ = {} | |
| __setattr__ = lambda self, name, value: _swig_setattr(self, msat_ic3, name, value) | |
| __swig_getmethods__ = {} | |
| __getattr__ = lambda self, name: _swig_getattr(self, msat_ic3, name) | |
| __repr__ = _swig_repr | |
| __swig_setmethods__["repr"] = _mathsat.msat_ic3_repr_set | |
| __swig_getmethods__["repr"] = _mathsat.msat_ic3_repr_get | |
| if _newclass:repr = _swig_property(_mathsat.msat_ic3_repr_get, _mathsat.msat_ic3_repr_set) | |
| def __init__(self): | |
| this = _mathsat.new_msat_ic3() | |
| try: self.this.append(this) | |
| except: self.this = this | |
| __swig_destroy__ = _mathsat.delete_msat_ic3 | |
| __del__ = lambda self : None; | |
| msat_ic3_swigregister = _mathsat.msat_ic3_swigregister | |
| msat_ic3_swigregister(msat_ic3) | |
| MSAT_IC3_CONCRETE = _mathsat.MSAT_IC3_CONCRETE | |
| MSAT_IC3_IA = _mathsat.MSAT_IC3_IA | |
| MSAT_IC3_PARAMS = _mathsat.MSAT_IC3_PARAMS | |
| MSAT_IC3_PARAMS_IA = _mathsat.MSAT_IC3_PARAMS_IA | |
| MSAT_IC3_BMC = _mathsat.MSAT_IC3_BMC | |
| MSAT_IC3_CTIGAR = _mathsat.MSAT_IC3_CTIGAR | |
| MSAT_IC3_KINDUCTION = _mathsat.MSAT_IC3_KINDUCTION | |
| MSAT_IC3_PROP_UNKNOWN = _mathsat.MSAT_IC3_PROP_UNKNOWN | |
| MSAT_IC3_PROP_INVAR = _mathsat.MSAT_IC3_PROP_INVAR | |
| MSAT_IC3_PROP_LIVE = _mathsat.MSAT_IC3_PROP_LIVE | |
| MSAT_IC3_ERR_GENERIC = _mathsat.MSAT_IC3_ERR_GENERIC | |
| MSAT_IC3_ERR_INVALID_PROPERTY = _mathsat.MSAT_IC3_ERR_INVALID_PROPERTY | |
| MSAT_IC3_ERR_INVALID_STATE = _mathsat.MSAT_IC3_ERR_INVALID_STATE | |
| MSAT_IC3_ERR_MAX_BOUND = _mathsat.MSAT_IC3_ERR_MAX_BOUND | |
| MSAT_IC3_ERR_REFINEMENT_FAILURE = _mathsat.MSAT_IC3_ERR_REFINEMENT_FAILURE | |
| def msat_create_ic3(*args): | |
| return _mathsat.msat_create_ic3(*args) | |
| msat_create_ic3 = _mathsat.msat_create_ic3 | |
| def msat_destroy_ic3(*args): | |
| return _mathsat.msat_destroy_ic3(*args) | |
| msat_destroy_ic3 = _mathsat.msat_destroy_ic3 | |
| def msat_ic3_last_error_message(*args): | |
| return _mathsat.msat_ic3_last_error_message(*args) | |
| msat_ic3_last_error_message = _mathsat.msat_ic3_last_error_message | |
| def msat_ic3_set_verbosity(*args): | |
| return _mathsat.msat_ic3_set_verbosity(*args) | |
| msat_ic3_set_verbosity = _mathsat.msat_ic3_set_verbosity | |
| def msat_ic3_setopt(*args): | |
| return _mathsat.msat_ic3_setopt(*args) | |
| msat_ic3_setopt = _mathsat.msat_ic3_setopt | |
| def msat_ic3_parse_opts(*args): | |
| return _mathsat.msat_ic3_parse_opts(*args) | |
| msat_ic3_parse_opts = _mathsat.msat_ic3_parse_opts | |
| def msat_ic3_opthelp(*args): | |
| return _mathsat.msat_ic3_opthelp(*args) | |
| msat_ic3_opthelp = _mathsat.msat_ic3_opthelp | |
| def msat_ic3_set_search_bound_callback(*args): | |
| return _mathsat.msat_ic3_set_search_bound_callback(*args) | |
| msat_ic3_set_search_bound_callback = _mathsat.msat_ic3_set_search_bound_callback | |
| def msat_ic3_set_param_region_callbacks(*args): | |
| return _mathsat.msat_ic3_set_param_region_callbacks(*args) | |
| msat_ic3_set_param_region_callbacks = _mathsat.msat_ic3_set_param_region_callbacks | |
| def msat_ic3_add_state_var(*args): | |
| return _mathsat.msat_ic3_add_state_var(*args) | |
| msat_ic3_add_state_var = _mathsat.msat_ic3_add_state_var | |
| def msat_ic3_set_init(*args): | |
| return _mathsat.msat_ic3_set_init(*args) | |
| msat_ic3_set_init = _mathsat.msat_ic3_set_init | |
| def msat_ic3_set_trans(*args): | |
| return _mathsat.msat_ic3_set_trans(*args) | |
| msat_ic3_set_trans = _mathsat.msat_ic3_set_trans | |
| def msat_ic3_add_invar_property(*args): | |
| return _mathsat.msat_ic3_add_invar_property(*args) | |
| msat_ic3_add_invar_property = _mathsat.msat_ic3_add_invar_property | |
| def msat_ic3_add_property(*args): | |
| return _mathsat.msat_ic3_add_property(*args) | |
| msat_ic3_add_property = _mathsat.msat_ic3_add_property | |
| def msat_ic3_add_param(*args): | |
| return _mathsat.msat_ic3_add_param(*args) | |
| msat_ic3_add_param = _mathsat.msat_ic3_add_param | |
| def msat_ic3_add_predicate(*args): | |
| return _mathsat.msat_ic3_add_predicate(*args) | |
| msat_ic3_add_predicate = _mathsat.msat_ic3_add_predicate | |
| def msat_ic3_set_kzeno_time_var(*args): | |
| return _mathsat.msat_ic3_set_kzeno_time_var(*args) | |
| msat_ic3_set_kzeno_time_var = _mathsat.msat_ic3_set_kzeno_time_var | |
| def msat_ic3_set_kzeno_bound(*args): | |
| return _mathsat.msat_ic3_set_kzeno_bound(*args) | |
| msat_ic3_set_kzeno_bound = _mathsat.msat_ic3_set_kzeno_bound | |
| def msat_ic3_init(*args): | |
| return _mathsat.msat_ic3_init(*args) | |
| msat_ic3_init = _mathsat.msat_ic3_init | |
| def msat_ic3_add_init_constraint(*args): | |
| return _mathsat.msat_ic3_add_init_constraint(*args) | |
| msat_ic3_add_init_constraint = _mathsat.msat_ic3_add_init_constraint | |
| def msat_ic3_add_trans_constraint(*args): | |
| return _mathsat.msat_ic3_add_trans_constraint(*args) | |
| msat_ic3_add_trans_constraint = _mathsat.msat_ic3_add_trans_constraint | |
| def msat_ic3_num_state_vars(*args): | |
| return _mathsat.msat_ic3_num_state_vars(*args) | |
| msat_ic3_num_state_vars = _mathsat.msat_ic3_num_state_vars | |
| def _msat_ic3_get_state_var(*args): | |
| return _mathsat._msat_ic3_get_state_var(*args) | |
| _msat_ic3_get_state_var = _mathsat._msat_ic3_get_state_var | |
| def msat_ic3_get_init(*args): | |
| return _mathsat.msat_ic3_get_init(*args) | |
| msat_ic3_get_init = _mathsat.msat_ic3_get_init | |
| def msat_ic3_get_trans(*args): | |
| return _mathsat.msat_ic3_get_trans(*args) | |
| msat_ic3_get_trans = _mathsat.msat_ic3_get_trans | |
| def msat_ic3_num_properties(*args): | |
| return _mathsat.msat_ic3_num_properties(*args) | |
| msat_ic3_num_properties = _mathsat.msat_ic3_num_properties | |
| def msat_ic3_get_property(*args): | |
| return _mathsat.msat_ic3_get_property(*args) | |
| msat_ic3_get_property = _mathsat.msat_ic3_get_property | |
| def msat_ic3_get_property_kind(*args): | |
| return _mathsat.msat_ic3_get_property_kind(*args) | |
| msat_ic3_get_property_kind = _mathsat.msat_ic3_get_property_kind | |
| def msat_ic3_num_params(*args): | |
| return _mathsat.msat_ic3_num_params(*args) | |
| msat_ic3_num_params = _mathsat.msat_ic3_num_params | |
| def msat_ic3_get_param(*args): | |
| return _mathsat.msat_ic3_get_param(*args) | |
| msat_ic3_get_param = _mathsat.msat_ic3_get_param | |
| def msat_ic3_num_predicates(*args): | |
| return _mathsat.msat_ic3_num_predicates(*args) | |
| msat_ic3_num_predicates = _mathsat.msat_ic3_num_predicates | |
| def msat_ic3_get_predicate(*args): | |
| return _mathsat.msat_ic3_get_predicate(*args) | |
| msat_ic3_get_predicate = _mathsat.msat_ic3_get_predicate | |
| def msat_ic3_from_smtlib2(*args): | |
| return _mathsat.msat_ic3_from_smtlib2(*args) | |
| msat_ic3_from_smtlib2 = _mathsat.msat_ic3_from_smtlib2 | |
| def msat_ic3_to_smtlib2(*args): | |
| return _mathsat.msat_ic3_to_smtlib2(*args) | |
| msat_ic3_to_smtlib2 = _mathsat.msat_ic3_to_smtlib2 | |
| def msat_ic3_to_smtlib2_horn(*args): | |
| return _mathsat.msat_ic3_to_smtlib2_horn(*args) | |
| msat_ic3_to_smtlib2_horn = _mathsat.msat_ic3_to_smtlib2_horn | |
| def msat_ic3_to_smtlib2_horn_file(*args): | |
| return _mathsat.msat_ic3_to_smtlib2_horn_file(*args) | |
| msat_ic3_to_smtlib2_horn_file = _mathsat.msat_ic3_to_smtlib2_horn_file | |
| def msat_ic3_prove(*args): | |
| return _mathsat.msat_ic3_prove(*args) | |
| msat_ic3_prove = _mathsat.msat_ic3_prove | |
| def msat_ic3_witness(*args): | |
| return _mathsat.msat_ic3_witness(*args) | |
| msat_ic3_witness = _mathsat.msat_ic3_witness | |
| def msat_ic3_witness_loopback(*args): | |
| return _mathsat.msat_ic3_witness_loopback(*args) | |
| msat_ic3_witness_loopback = _mathsat.msat_ic3_witness_loopback | |
| def msat_ic3_stats(*args): | |
| return _mathsat.msat_ic3_stats(*args) | |
| msat_ic3_stats = _mathsat.msat_ic3_stats | |
| def MSAT_ERROR_CONFIG(*args): | |
| return _mathsat.MSAT_ERROR_CONFIG(*args) | |
| MSAT_ERROR_CONFIG = _mathsat.MSAT_ERROR_CONFIG | |
| def MSAT_ERROR_ENV(*args): | |
| return _mathsat.MSAT_ERROR_ENV(*args) | |
| MSAT_ERROR_ENV = _mathsat.MSAT_ERROR_ENV | |
| def MSAT_ERROR_TERM(*args): | |
| return _mathsat.MSAT_ERROR_TERM(*args) | |
| MSAT_ERROR_TERM = _mathsat.MSAT_ERROR_TERM | |
| def MSAT_ERROR_DECL(*args): | |
| return _mathsat.MSAT_ERROR_DECL(*args) | |
| MSAT_ERROR_DECL = _mathsat.MSAT_ERROR_DECL | |
| def MSAT_MAKE_ERROR_TERM(): | |
| return _mathsat.MSAT_MAKE_ERROR_TERM() | |
| MSAT_MAKE_ERROR_TERM = _mathsat.MSAT_MAKE_ERROR_TERM | |
| def MSAT_ERROR_TYPE(*args): | |
| return _mathsat.MSAT_ERROR_TYPE(*args) | |
| MSAT_ERROR_TYPE = _mathsat.MSAT_ERROR_TYPE | |
| def MSAT_ERROR_MODEL_ITERATOR(*args): | |
| return _mathsat.MSAT_ERROR_MODEL_ITERATOR(*args) | |
| MSAT_ERROR_MODEL_ITERATOR = _mathsat.MSAT_ERROR_MODEL_ITERATOR | |
| def MSAT_ERROR_MODEL(*args): | |
| return _mathsat.MSAT_ERROR_MODEL(*args) | |
| MSAT_ERROR_MODEL = _mathsat.MSAT_ERROR_MODEL | |
| def msat_parse_config(data_or_file): | |
| if hasattr(data_or_file, 'read'): | |
| data_or_file = data_or_file.read() | |
| return _msat_parse_config(data_or_file) | |
| def msat_parse_config_file(f): | |
| return _msat_parse_config(f.read()) | |
| def msat_create_env(conf=None, other=None): | |
| try: | |
| if conf is None: | |
| cfg = msat_create_config() | |
| elif hasattr(conf, 'iteritems'): | |
| cfg = msat_create_config() | |
| for (k, v) in conf.iteritems(): | |
| msat_set_option(cfg, k, v) | |
| elif hasattr(conf, 'read'): | |
| cfg = _msat_parse_config(conf.read()) | |
| else: | |
| try: | |
| cfg = conf + "" | |
| except: | |
| cfg = conf | |
| else: | |
| if '=' not in cfg: | |
| cfg = msat_create_default_config(cfg) | |
| else: | |
| cfg = msat_parse_config(cfg) | |
| if other is not None: | |
| return _msat_create_shared_env(cfg, other) | |
| else: | |
| return _msat_create_env(cfg) | |
| finally: | |
| if cfg is not conf: | |
| msat_destroy_config(cfg) | |
| msat_create_shared_env = msat_create_env | |
| def msat_get_function_type(env, param_types, return_type): | |
| return _msat_get_function_type(env, param_types, len(param_types), return_type) | |
| def msat_model_iterator_next(i): | |
| "returns a tuple (term, value)" | |
| t = msat_term() | |
| v = msat_term() | |
| _msat_model_iterator_next(i, t, v) | |
| return (t, v) | |
| def msat_all_sat(env, important, callback): | |
| return _msat_all_sat(env, important, len(important), callback) | |
| def msat_solve_diversify(env, diversifiers, callback): | |
| return _msat_solve_diversify(env, diversifiers, len(diversifiers), callback) | |
| def msat_get_asserted_formulas(env): | |
| return _msat_get_asserted_formulas(env, 0) | |
| def msat_get_unsat_core(env): | |
| return _msat_get_unsat_core(env, 0) | |
| def msat_get_theory_lemmas(env): | |
| return _msat_get_theory_lemmas(env, 0) | |
| def msat_solve_with_assumptions(env, assumptions): | |
| return _msat_solve_with_assumptions(env, assumptions, len(assumptions)) | |
| def msat_get_unsat_assumptions(env): | |
| return _msat_get_unsat_assumptions(env, 0) | |
| def msat_get_interpolant(env, groups_of_a): | |
| return _msat_get_interpolant(env, groups_of_a, len(groups_of_a)) | |
| def msat_from_smtlib1_file(env, fileobj): | |
| return _msat_from_smtlib1(env, fileobj.read()) | |
| def msat_from_smtlib2_file(env, fileobj): | |
| return _msat_from_smtlib2(env, fileobj.read()) | |
| def msat_term_to_number(env, term): | |
| return _msat_term_to_number(env, term, 0) | |
| def msat_make_int_modular_congruence(env, modulus, t1, t2): | |
| return _msat_make_int_modular_congruence(env, str(modulus), t1, t2) | |
| def msat_term_is_int_modular_congruence(env, term): | |
| "returns a tuple (res, number)" | |
| return _msat_term_is_int_modular_congruence(env, term, 0) | |
| def msat_is_bv_type(env, tp): | |
| "returns a tuple (res, width)" | |
| return _msat_is_bv_type(env, tp, None) | |
| def msat_is_array_type(env, tp): | |
| "returns a tuple (res, indextp, elemtp)" | |
| return _msat_is_array_type(env, tp, None, None) | |
| def msat_is_fp_type(env, tp): | |
| "returns a tuple (res, exp_width, mant_width)" | |
| return _msat_is_fp_type(env, tp, None, None) | |
| def msat_term_is_bv_extract(env, term): | |
| "returns a tuple (res, msb, lsb)" | |
| return _msat_term_is_bv_extract(env, term, None, None) | |
| def msat_term_is_bv_zext(env, term): | |
| "returns a tuple (res, amount)" | |
| return _msat_term_is_bv_zext(env, term, None) | |
| def msat_term_is_bv_sext(env, term): | |
| "returns a tuple (res, amount)" | |
| return _msat_term_is_bv_sext(env, term, None) | |
| def msat_term_is_bv_rol(env, term): | |
| "returns a tuple (res, amount)" | |
| return _msat_term_is_bv_rol(env, term, None) | |
| def msat_term_is_bv_ror(env, term): | |
| "returns a tuple (res, amount)" | |
| return _msat_term_is_bv_ror(env, term, None) | |
| def msat_named_list_from_smtlib2(env, data): | |
| ret = _msat_named_list_from_smtlib2(env, data, 0, 0, 0) | |
| if ret is not None: | |
| ret = [p[0] for p in ret], [p[1] for p in ret] | |
| return ret | |
| def msat_named_list_from_smtlib2_file(env, f): | |
| return msat_named_list_from_smtlib2(env, f.read()) | |
| def msat_named_list_to_smtlib2(env, names, terms): | |
| return _msat_named_list_to_smtlib2(env, len(names), names, terms) | |
| def msat_named_list_to_smtlib2_file(env, names, terms, out): | |
| data = msat_named_list_to_smtlib2(env, names, terms) | |
| out.write(data) | |
| def msat_annotated_list_from_smtlib2(env, data): | |
| return _msat_annotated_list_from_smtlib2(env, data, 0, 0, 0) | |
| def msat_annotated_list_from_smtlib2_file(env, f): | |
| return msat_annotated_list_from_smtlib2(env, f.read()) | |
| def msat_annotated_list_to_smtlib2(env, terms, annots): | |
| return _msat_annotated_list_to_smtlib2(env, len(terms), terms, annots) | |
| def msat_annotated_list_to_smtlib2_file(env, terms, annots, out): | |
| data = msat_annotated_list_to_smtlib2(env, terms, annots) | |
| out.write(data) | |
| def msat_gc_env(env, tokeep): | |
| return _msat_gc_env(env, tokeep, len(tokeep)) | |
| # add suitable __eq__, __hash__ and __str__ methods to the msat classes | |
| def _term_hash(self): | |
| return msat_term_id(self) | |
| msat_term.__hash__ = _term_hash | |
| del _term_hash | |
| def _term_eq(self, other): | |
| return isinstance(other, msat_term) and msat_term_id(self) == msat_term_id(other) | |
| msat_term.__eq__ = _term_eq | |
| del _term_eq | |
| def _term_str(self): | |
| if MSAT_ERROR_TERM(self): return "<ERROR>" | |
| return msat_term_repr(self) | |
| msat_term.__str__ = _term_str | |
| del _term_str | |
| def _decl_hash(self): | |
| return msat_decl_id(self) | |
| msat_decl.__hash__ = _decl_hash | |
| del _decl_hash | |
| def _decl_eq(self, other): | |
| return isinstance(other, msat_decl) and msat_decl_id(self) == msat_decl_id(other) | |
| msat_decl.__eq__ = _decl_eq | |
| del _decl_eq | |
| def msat_exist_elim(env, formula, to_elim, algo, | |
| toplevel_propagation=True, | |
| boolean_simplifications=True, | |
| remove_redundant_constraints=True): | |
| opts = msat_exist_elim_options() | |
| opts.toplevel_propagation = toplevel_propagation | |
| opts.boolean_simplifications = boolean_simplifications | |
| opts.remove_redundant_constraints = remove_redundant_constraints | |
| return _msat_exist_elim(env, formula, to_elim, len(to_elim), algo, opts) | |
| def msat_exist_elim_model(env, formula, to_elim, model, model_values=None): | |
| if model_values is None: | |
| model_vars, model_values = [], [] | |
| for (k, v) in model.iteritems(): | |
| model_vars.append(k) | |
| model_values.append(v) | |
| else: | |
| model_vars = model | |
| return _msat_exist_elim_model(env, formula, to_elim, len(to_elim), | |
| model_vars, model_values, len(model_vars)) | |
| def msat_apply_substitution(env, term, to_subst, values=None): | |
| if values is None: | |
| m = to_subst | |
| to_subst = [] | |
| values = [] | |
| if hasattr(m, 'iteritems'): | |
| for (k, v) in m.iteritems(): | |
| to_subst.append(k) | |
| values.append(v) | |
| else: | |
| # assume m is a sequence of (k, v) pairs | |
| for (k, v) in m: | |
| to_subst.append(k) | |
| values.append(v) | |
| return _msat_apply_substitution(env, term, len(to_subst), to_subst, values) | |
| def msat_ic3_get_state_var(s, idx): | |
| return _msat_ic3_get_state_var(s, idx, None, None) | |
| # This file is compatible with both classic and new-style classes. | |