# 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.