# Path: pynusmv/utils.py
# class PointerWrapper(object):
# 
#     """
#     Superclass wrapper for NuSMV pointers.
# 
#     Every pointer to a NuSMV structure is wrapped in a PointerWrapper
#     or in a subclass of PointerWrapper.
#     Every subclass instance takes a pointer to a NuSMV structure as constructor
#     parameter.
# 
#     It is the responsibility of PointerWrapper and its subclasses to free
#     the wrapped pointer. Some pointers have to be freed like `bdd_ptr`,
#     but other do not have to be freed since NuSMV takes care of this;
#     for example, `BddFrm_ptr` does not have to be freed.
#     To ensure that a pointer is freed only once, PyNuSMV ensures that
#     any pointer is wrapped by only one PointerWrapper (or subclass of it)
#     if the pointer have to be freed.
# 
#     """
# 
#     def __init__(self, pointer, freeit=False):
#         """
#         Create a new PointerWrapper.
# 
#         :param pointer: the pointer to wrap
#         :param freeit: whether the pointer has to be freed when this wrapper
#                        is destroyed
# 
#         """
#         self._ptr = pointer
#         self._freeit = freeit
#         _register_wrapper(self)
# 
#     def _free(self):
#         """
#         Every subclass must implement `_free` if there is something to free.
# 
#         """
#         pass
# 
#     def __del__(self):
#         if self._freeit and self._ptr is not None:
#             self._free()
# 
# 
#     def __hash__(self):
#         """
#         Makes this object hashable.
# 
#         .. warning::
# 
#             Beware it uses the pointer to implement the hashing function.
#             So it is IDENTITY dependent (in C) and not value dependant.
# 
#         :return: an object that can serve as key to perform the lookup in a dict.
#         """
#         return self._ptr.__hash__()
# 
#     def __eq__(self, other):
#         """
#         Equality test between two objects.
# 
#         .. warning::
# 
#             Beware it uses the pointer to implement the hashing function.
#             So it is IDENTITY dependent (in C) and not value dependant.
# 
#         :return: True iff the two object are the same
#         """
#         return self._ptr == other._ptr
# 
# Path: pynusmv/exception.py
# class MissingManagerError(PyNuSMVError):
# 
#     """
#     Exception for missing BDD manager.
# 
#     """
#     pass


from pynusmv_lower_interface.nusmv.dd import dd as nsdd
from pynusmv_lower_interface.nusmv.node import node as nsnode
from pynusmv_lower_interface.nusmv.compile.symb_table import symb_table as nssymb_table
from pynusmv_lower_interface.nusmv.enc.bdd import bdd as nsbddEnc
from pynusmv_lower_interface.nusmv.utils import utils as nsutils
from pynusmv_lower_interface.nusmv.cinit import cinit as nscinit
from pynusmv_lower_interface.nusmv.opt import opt as nsopt
from .utils import PointerWrapper
from .exception import MissingManagerError
        from .fsm import BddFsm
            from .glob import prop_database
        from .fsm import BddFsm
            from .glob import prop_database
                   `window{2, 3, 4}`,
                   `window{2, 3, 4}_converge`,
                   `group_sift`,
                   `group_sift_converge`,
                   `annealing`,
                   `genetic`,
                   `exact`,
                   `linear`,
                   `linear_converge`,
                   `same` (the previously chosen method)
    :type method: :class:`str`

    :raise: a :exc:`MissingManagerError
            <pynusmv.exception.MissingManagerError>` if the manager is missing

    .. note:: For more information on reordering methods, see NuSMV manual.

    """
    if DDmanager is None:
        DDmanager_ptr = nscinit.cvar.dd_manager
    else:
        DDmanager_ptr = DDmanager._ptr
    if DDmanager_ptr is None:
        raise MissingManagerError("Missing manager")
    method = nsdd.StringConvertToDynOrderType(method)
    if method == nsdd.CUDD_REORDER_NONE:
        method = nsdd.CUDD_REORDER_SIFT
    nsdd.dd_reorder(DDmanager_ptr, method, nsdd.DEFAULT_MINSIZE)



# Path: pynusmv/utils.py
# class PointerWrapper(object):
# 
#     """
#     Superclass wrapper for NuSMV pointers.
# 
#     Every pointer to a NuSMV structure is wrapped in a PointerWrapper
#     or in a subclass of PointerWrapper.
#     Every subclass instance takes a pointer to a NuSMV structure as constructor
#     parameter.
# 
#     It is the responsibility of PointerWrapper and its subclasses to free
#     the wrapped pointer. Some pointers have to be freed like `bdd_ptr`,
#     but other do not have to be freed since NuSMV takes care of this;
#     for example, `BddFrm_ptr` does not have to be freed.
#     To ensure that a pointer is freed only once, PyNuSMV ensures that
#     any pointer is wrapped by only one PointerWrapper (or subclass of it)
#     if the pointer have to be freed.
# 
#     """
# 
#     def __init__(self, pointer, freeit=False):
#         """
#         Create a new PointerWrapper.
# 
#         :param pointer: the pointer to wrap
#         :param freeit: whether the pointer has to be freed when this wrapper
#                        is destroyed
# 
#         """
#         self._ptr = pointer
#         self._freeit = freeit
#         _register_wrapper(self)
# 
#     def _free(self):
#         """
#         Every subclass must implement `_free` if there is something to free.
# 
#         """
#         pass
# 
#     def __del__(self):
#         if self._freeit and self._ptr is not None:
#             self._free()
# 
# 
#     def __hash__(self):
#         """
#         Makes this object hashable.
# 
#         .. warning::
# 
#             Beware it uses the pointer to implement the hashing function.
#             So it is IDENTITY dependent (in C) and not value dependant.
# 
#         :return: an object that can serve as key to perform the lookup in a dict.
#         """
#         return self._ptr.__hash__()
# 
#     def __eq__(self, other):
#         """
#         Equality test between two objects.
# 
#         .. warning::
# 
#             Beware it uses the pointer to implement the hashing function.
#             So it is IDENTITY dependent (in C) and not value dependant.
# 
#         :return: True iff the two object are the same
#         """
#         return self._ptr == other._ptr
# 
# Path: pynusmv/exception.py
# class MissingManagerError(PyNuSMVError):
# 
#     """
#     Exception for missing BDD manager.
# 
#     """
#     pass


# Path: pynusmv/dd.py
from pynusmv_lower_interface.nusmv.dd import dd as nsdd
from pynusmv_lower_interface.nusmv.node import node as nsnode
from pynusmv_lower_interface.nusmv.compile.symb_table import symb_table as nssymb_table
from pynusmv_lower_interface.nusmv.enc.bdd import bdd as nsbddEnc
from pynusmv_lower_interface.nusmv.utils import utils as nsutils
from pynusmv_lower_interface.nusmv.cinit import cinit as nscinit
from pynusmv_lower_interface.nusmv.opt import opt as nsopt
from .utils import PointerWrapper
from .exception import MissingManagerError
        from .fsm import BddFsm
            from .glob import prop_database
        from .fsm import BddFsm
            from .glob import prop_database

                   `window{2, 3, 4}`,
                   `window{2, 3, 4}_converge`,
                   `group_sift`,
                   `group_sift_converge`,
                   `annealing`,
                   `genetic`,
                   `exact`,
                   `linear`,
                   `linear_converge`,
                   `same` (the previously chosen method)
    :type method: :class:`str`

    :raise: a :exc:`MissingManagerError
            <pynusmv.exception.MissingManagerError>` if the manager is missing

    .. note:: For more information on reordering methods, see NuSMV manual.

    """
    if DDmanager is None:
        DDmanager_ptr = nscinit.cvar.dd_manager
    else:
        DDmanager_ptr = DDmanager._ptr
    if DDmanager_ptr is None:
        raise MissingManagerError("Missing manager")
    method = nsdd.StringConvertToDynOrderType(method)
    if method == nsdd.CUDD_REORDER_NONE:
        method = nsdd.CUDD_REORDER_SIFT
    nsdd.dd_reorder(DDmanager_ptr, method, nsdd.DEFAULT_MINSIZE)



class BDD(PointerWrapper):