# Path: tests/utils.py
# class Configure:
#     """
#     This class provides a convenient context manager to initialize BMC test 
#     cases loading the model from a file and setting the most commonly used
#     fields in the testcase
#     """
#     
#     def __init__(self, testcase, location, model):
#         """
#         creates a new instance
#         :param testcase: the test case to initialize
#         :param location: the __file__ attribute of the module in which the 
#             testcase runs
#         :param model: a path relative to the testcase module from where to load
#             an smv model.
#         """
#         self.testcase = testcase
#         self.model    = current_directory(location)+model
#         
#     def __enter__(self):
#         """Performs what one would usually do in setUp"""
#         init_nusmv()
#         load_from_file(self.model)
#         go_bmc()
#         self.testcase.sexpfsm = master_bool_sexp_fsm()
#         self.testcase.befsm   = master_be_fsm()
#         self.testcase.enc     = self.testcase.befsm.encoding
#         self.testcase.mgr     = self.testcase.enc.manager
#     
#     def __exit__(self, type_, value, traceback):
#         """Performs what one would usually do in tearDown"""
#         bmc_exit()
#         deinit_nusmv()
# 
# Path: pynusmv/bmc/utils.py
# def get_symbol(name):
#     """
#     Conveniency method to retrieve a symbol (not necessarily a variable, it can
#     also be a DEFINE) by its name.
#     
#     :param name: a string version of the name of the symbol to retrieve
#     :return: a Node standing for the looked up symbol or None if it could not 
#         be found.
#     :raises ValueError: when the requested name cannot be found in the symbol
#         table
#     """
#     try:
#         sexpfsm = glob.master_bool_sexp_fsm()
#         return next(x for x in sexpfsm.symbols_list if str(x) == name)
#     except StopIteration:
#         #raised when the 'name' key could not be found, rethrow
#         raise ValueError("{} not found in the symbol table".format(name))
# 
# Path: pynusmv/sat.py
# class SatSolverFactory():
#     # =========================================================================
#     # ========== Utility functions ============================================
#     # =========================================================================
#     @staticmethod
#     def normalize_name(name):
#         """
#         :return: a normalized solver name corresponding to the given `name`.
#           (Only case should be changed)
#         :param name: the name (string) of the solver to normalize.
#         :raise: ValueError whenever the name corresponds to none of the 
#           available solvers
#         """
#         normalized = _sat.Sat_NormalizeSatSolverName(name)
#         if normalized is None:
#             raise ValueError("No such SAT solver available : {}".format(name))
#         else:
#             return normalized
# 
#     @staticmethod
#     def available_solvers():
#         """
#         :return: a list with the name of the solvers that can be instantiated
#         """
#         return set(_sat.Sat_GetAvailableSolversString().split())
#     
#     @staticmethod 
#     def print_available_solvers(stdio_file=utils.StdioFile.stdout()):
#         """
#         prints the list of available SAT solvers to the given stdio file 
#         """
#         _sat.Sat_PrintAvailableSolvers(stdio_file.handle)
#         
#     @staticmethod
#     def create(name='MiniSat', incremental=True, proof=True):
#         """
#         Creates a new sat solver corresponding to the given name and capabilities
#         :param name: the name of the solver to instanciate 
#         :param incremental: a flag indicating whether the instanciated solver
#         should have incremental capabilities
#         :param proof: a flag indicating whether the instanciated solver should
#         have proof logging capability.
#         :return: a new sat solver corresponding to the given name and capabilities
#         
#         :raise: Given that ZChaff does not support proof logging, this method
#           raises a ValueError when prooflogging is turned on and zchaff is passed
#           as name parameter.
#         """
#         if SatSolverFactory.normalize_name(name) == 'ZChaff' and proof:
#             raise ValueError("""
#                 Proof logging not supported when using the zchaff  SAT Solver. 
#                 Please retry using MiniSat
#                 """)
#         
#         if incremental:
#             if proof:
#                 return SatIncProofSolver(
#                                 _sat.Sat_CreateIncProofSolver(name))
#             else:
#                 return SatIncSolver(_sat.Sat_CreateIncSolver(name))
#         else:
#             if proof:
#                 return SatProofSolver(
#                                 _sat.Sat_CreateNonIncProofSolver(name))
#             else:
#                 return SatSolver(
#                                 _sat.Sat_CreateNonIncSolver(name))
#         raise Exception("Could not create solver")
# 
# class Polarity(IntEnum):
#     """
#     In general, a polarity is assigned to a formula and its variables. If this
#     were not done, this would potentially slow down the solver because the 
#     solver would unnecessarily try to assign values to many variables.
#     """
#     POSITIVE =  1
#     NEGATIVE = -1
#     NOT_SET  =  0


from unittest          import TestCase
from tests.utils       import Configure
from pynusmv.bmc.utils import get_symbol 
from pynusmv.sat       import SatSolverFactory , Polarity
 
 
class TestMultiBitsVariables(TestCase):
    
    def test_encode_to_bits(self):
        """
        Tests the encode_to_bits method in BeEnc
        """

# Path: tests/utils.py
# class Configure:
#     """
#     This class provides a convenient context manager to initialize BMC test 
#     cases loading the model from a file and setting the most commonly used
#     fields in the testcase
#     """
#     
#     def __init__(self, testcase, location, model):
#         """
#         creates a new instance
#         :param testcase: the test case to initialize
#         :param location: the __file__ attribute of the module in which the 
#             testcase runs
#         :param model: a path relative to the testcase module from where to load
#             an smv model.
#         """
#         self.testcase = testcase
#         self.model    = current_directory(location)+model
#         
#     def __enter__(self):
#         """Performs what one would usually do in setUp"""
#         init_nusmv()
#         load_from_file(self.model)
#         go_bmc()
#         self.testcase.sexpfsm = master_bool_sexp_fsm()
#         self.testcase.befsm   = master_be_fsm()
#         self.testcase.enc     = self.testcase.befsm.encoding
#         self.testcase.mgr     = self.testcase.enc.manager
#     
#     def __exit__(self, type_, value, traceback):
#         """Performs what one would usually do in tearDown"""
#         bmc_exit()
#         deinit_nusmv()
# 
# Path: pynusmv/bmc/utils.py
# def get_symbol(name):
#     """
#     Conveniency method to retrieve a symbol (not necessarily a variable, it can
#     also be a DEFINE) by its name.
#     
#     :param name: a string version of the name of the symbol to retrieve
#     :return: a Node standing for the looked up symbol or None if it could not 
#         be found.
#     :raises ValueError: when the requested name cannot be found in the symbol
#         table
#     """
#     try:
#         sexpfsm = glob.master_bool_sexp_fsm()
#         return next(x for x in sexpfsm.symbols_list if str(x) == name)
#     except StopIteration:
#         #raised when the 'name' key could not be found, rethrow
#         raise ValueError("{} not found in the symbol table".format(name))
# 
# Path: pynusmv/sat.py
# class SatSolverFactory():
#     # =========================================================================
#     # ========== Utility functions ============================================
#     # =========================================================================
#     @staticmethod
#     def normalize_name(name):
#         """
#         :return: a normalized solver name corresponding to the given `name`.
#           (Only case should be changed)
#         :param name: the name (string) of the solver to normalize.
#         :raise: ValueError whenever the name corresponds to none of the 
#           available solvers
#         """
#         normalized = _sat.Sat_NormalizeSatSolverName(name)
#         if normalized is None:
#             raise ValueError("No such SAT solver available : {}".format(name))
#         else:
#             return normalized
# 
#     @staticmethod
#     def available_solvers():
#         """
#         :return: a list with the name of the solvers that can be instantiated
#         """
#         return set(_sat.Sat_GetAvailableSolversString().split())
#     
#     @staticmethod 
#     def print_available_solvers(stdio_file=utils.StdioFile.stdout()):
#         """
#         prints the list of available SAT solvers to the given stdio file 
#         """
#         _sat.Sat_PrintAvailableSolvers(stdio_file.handle)
#         
#     @staticmethod
#     def create(name='MiniSat', incremental=True, proof=True):
#         """
#         Creates a new sat solver corresponding to the given name and capabilities
#         :param name: the name of the solver to instanciate 
#         :param incremental: a flag indicating whether the instanciated solver
#         should have incremental capabilities
#         :param proof: a flag indicating whether the instanciated solver should
#         have proof logging capability.
#         :return: a new sat solver corresponding to the given name and capabilities
#         
#         :raise: Given that ZChaff does not support proof logging, this method
#           raises a ValueError when prooflogging is turned on and zchaff is passed
#           as name parameter.
#         """
#         if SatSolverFactory.normalize_name(name) == 'ZChaff' and proof:
#             raise ValueError("""
#                 Proof logging not supported when using the zchaff  SAT Solver. 
#                 Please retry using MiniSat
#                 """)
#         
#         if incremental:
#             if proof:
#                 return SatIncProofSolver(
#                                 _sat.Sat_CreateIncProofSolver(name))
#             else:
#                 return SatIncSolver(_sat.Sat_CreateIncSolver(name))
#         else:
#             if proof:
#                 return SatProofSolver(
#                                 _sat.Sat_CreateNonIncProofSolver(name))
#             else:
#                 return SatSolver(
#                                 _sat.Sat_CreateNonIncSolver(name))
#         raise Exception("Could not create solver")
# 
# class Polarity(IntEnum):
#     """
#     In general, a polarity is assigned to a formula and its variables. If this
#     were not done, this would potentially slow down the solver because the 
#     solver would unnecessarily try to assign values to many variables.
#     """
#     POSITIVE =  1
#     NEGATIVE = -1
#     NOT_SET  =  0


# Path: tests/pynusmv/testBeMultiBitsVariables.py
from unittest          import TestCase
from tests.utils       import Configure
from pynusmv.bmc.utils import get_symbol 
from pynusmv.sat       import SatSolverFactory , Polarity

 
 
class TestMultiBitsVariables(TestCase):
    
    def test_encode_to_bits(self):
        """
        Tests the encode_to_bits method in BeEnc
        """

        with Configure(self, __file__, "/models/multibit.smv"):