Version abc50904

18 files changed, 4849 insertions, 0 deletions

diff --git a/src/misc/mvc/module.make b/src/misc/mvc/module.make
new file mode 100644
index 00000000..23735ca2
--- /dev/null
+++ b/src/misc/mvc/module.make
@@ -0,0 +1,16 @@
+SRC +=  src/misc/mvc/mvc.c \
+    src/misc/mvc/mvcApi.c \
+    src/misc/mvc/mvcCompare.c \
+    src/misc/mvc/mvcContain.c \
+    src/misc/mvc/mvcCover.c \
+    src/misc/mvc/mvcCube.c \
+    src/misc/mvc/mvcDivide.c \
+    src/misc/mvc/mvcDivisor.c \
+    src/misc/mvc/mvcList.c \
+    src/misc/mvc/mvcLits.c \
+    src/misc/mvc/mvcMan.c \
+    src/misc/mvc/mvcOpAlg.c \
+    src/misc/mvc/mvcOpBool.c \
+    src/misc/mvc/mvcPrint.c \
+    src/misc/mvc/mvcSort.c \
+    src/misc/mvc/mvcUtils.c
diff --git a/src/misc/mvc/mvc.c b/src/misc/mvc/mvc.c
new file mode 100644
index 00000000..9430276c
--- /dev/null
+++ b/src/misc/mvc/mvc.c
@@ -0,0 +1,46 @@
+/**CFile****************************************************************
+
+  FileName    [mvc.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    []
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvc.c,v 1.3 2003/03/19 19:50:26 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
new file mode 100644
index 00000000..ee8c31be
--- /dev/null
+++ b/src/misc/mvc/mvc.h
@@ -0,0 +1,733 @@
+/**CFile****************************************************************
+
+  FileName    [mvc.h]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Data structure for MV cube/cover manipulation.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvc.h,v 1.10 2003/05/02 23:23:59 wjiang Exp $]
+
+***********************************************************************/
+
+#ifndef __MVC_H__
+#define __MVC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "util.h"
+#include "extra.h"
+//#include "vm.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// this is the only part of Mvc package, which should be modified
+// when compiling the package for other platforms
+
+// these parameters can be computed but setting them manually makes it faster
+#define BITS_PER_WORD         32                      // sizeof(Mvc_CubeWord_t) * 8 
+#define BITS_PER_WORD_MINUS   31                      // the same minus 1
+#define BITS_PER_WORD_LOG     5                       // log2(sizeof(Mvc_CubeWord_t) * 8)
+#define BITS_DISJOINT         ((Mvc_CubeWord_t)0x55555555)  // the mask of the type "01010101"
+#define BITS_FULL             ((Mvc_CubeWord_t)0xffffffff)  // the mask of the type "11111111"
+
+// uncomment this macro to switch to standard memory management
+//#define USE_SYSTEM_MEMORY_MANAGEMENT 
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// cube/list/cover/data
+typedef unsigned long              Mvc_CubeWord_t;
+typedef struct MvcCubeStruct       Mvc_Cube_t;
+typedef struct MvcListStruct       Mvc_List_t;
+typedef struct MvcCoverStruct      Mvc_Cover_t;
+typedef struct MvcDataStruct       Mvc_Data_t;
+typedef struct MvcManagerStruct    Mvc_Manager_t;
+
+// the cube data structure
+struct MvcCubeStruct
+{
+    Mvc_Cube_t *    pNext;        // the next cube in the linked list
+    unsigned        iLast   :  8; // the index of the last word
+    unsigned        nUnused :  6; // the number of unused bits in the last word
+    unsigned        fPrime  :  1; // marks the prime cube
+    unsigned        fEssen  :  1; // marks the essential cube
+    unsigned        nOnes   : 16; // the number of 1's in the bit data
+    Mvc_CubeWord_t  pData[1];     // the first Mvc_CubeWord_t filled with bit data
+};
+
+// the single-linked list of cubes in the cover
+struct MvcListStruct
+{
+    Mvc_Cube_t *    pHead;        // the first cube in the list
+    Mvc_Cube_t *    pTail;        // the last cube in the list
+    int             nItems;       // the number of cubes in the list
+};
+
+// the cover data structure
+struct MvcCoverStruct
+{
+    char            nWords;       // the number of machine words
+    char            nUnused;      // the number of unused bits in the last word
+    short           nBits;        // the number of used data bits in the cube
+    Mvc_List_t      lCubes;       // the single-linked list of cubes
+    Mvc_Cube_t **   pCubes;       // the array of cubes (for sorting)
+    int             nCubesAlloc;  // the size of allocated storage
+    int *           pLits;        // the counter of lit occurrances in cubes
+    Mvc_Cube_t *    pMask;        // the multipurpose mask
+    Mvc_Manager_t * pMem;         // the memory manager
+};
+
+// data structure to store information about MV variables
+struct MvcDataStruct
+{
+    Mvc_Manager_t * pMan;         // the memory manager
+//    Vm_VarMap_t *   pVm;          // the MV variable data
+    int             nBinVars;     // the number of binary variables
+    Mvc_Cube_t *    pMaskBin;     // the mask to select the binary bits only
+    Mvc_Cube_t **   ppMasks;      // the mask to select each MV variable
+    Mvc_Cube_t *    ppTemp[3];    // the temporary cubes
+};
+
+// the manager of covers and cubes (as of today, only managing memory)
+struct MvcManagerStruct
+{
+    Extra_MmFixed_t * pManC;        // the manager for covers
+    Extra_MmFixed_t * pMan1;        // the manager for 1-word cubes
+    Extra_MmFixed_t * pMan2;        // the manager for 2-word cubes
+    Extra_MmFixed_t * pMan4;        // the manager for 3-word cubes
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// reading data from the header of the cube
+#define Mvc_CubeReadNext(Cube)       ((Cube)->pNext)
+#define Mvc_CubeReadNextP(Cube)      (&(Cube)->pNext)
+#define Mvc_CubeReadLast(Cube)       ((Cube)->iLast)
+#define Mvc_CubeReadSize(Cube)       ((Cube)->nOnes)
+// setting data to the header of the cube
+#define Mvc_CubeSetNext(Cube,Next)   ((Cube)->pNext = (Next))
+#define Mvc_CubeSetLast(Cube,Last)   ((Cube)->iLast = (Last))
+#define Mvc_CubeSetSize(Cube,Size)   ((Cube)->nOnes = (Size))
+// checking the number of words
+
+#define Mvc_Cube1Words(Cube)         ((Cube)->iLast == 0) 
+#define Mvc_Cube2Words(Cube)         ((Cube)->iLast == 1) 
+#define Mvc_CubeNWords(Cube)         ((Cube)->iLast >  1) 
+// getting one data bit
+#define Mvc_CubeWhichWord(Bit)       ((Bit) >> BITS_PER_WORD_LOG)
+#define Mvc_CubeWhichBit(Bit)        ((Bit) &  BITS_PER_WORD_MINUS)
+// accessing individual bits
+#define Mvc_CubeBitValue(Cube, Bit) (((Cube)->pData[Mvc_CubeWhichWord(Bit)] &   (((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit)))) > 0)
+#define Mvc_CubeBitInsert(Cube, Bit) ((Cube)->pData[Mvc_CubeWhichWord(Bit)] |=  (((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit))))
+#define Mvc_CubeBitRemove(Cube, Bit) ((Cube)->pData[Mvc_CubeWhichWord(Bit)] &= ~(((Mvc_CubeWord_t)1)<<(Mvc_CubeWhichBit(Bit))))
+// accessing values of the binary variables
+#define Mvc_CubeVarValue(Cube, Var) (((Cube)->pData[Mvc_CubeWhichWord(2*(Var))] >> (Mvc_CubeWhichBit(2*(Var)))) & ((Mvc_CubeWord_t)3))
+
+// various macros
+
+// cleaning the data bits of the cube
+#define Mvc_Cube1BitClean( Cube )\
+          ((Cube)->pData[0] = 0)
+#define Mvc_Cube2BitClean( Cube )\
+         (((Cube)->pData[0] = 0),\
+          ((Cube)->pData[1] = 0))
+#define Mvc_CubeNBitClean( Cube  )\
+{\
+    int _i_;\
+    for( _i_ = (Cube)->iLast; _i_ >= 0; _i_--)\
+           (Cube)->pData[_i_] = 0;\
+}
+
+// cleaning the unused part of the lat word
+#define Mvc_CubeBitCleanUnused( Cube )\
+    ((Cube)->pData[(Cube)->iLast] &= (BITS_FULL >> (Cube)->nUnused))
+
+// filling the used data bits with 1's
+#define Mvc_Cube1BitFill( Cube )\
+           (Cube)->pData[0] = (BITS_FULL >> (Cube)->nUnused);
+#define Mvc_Cube2BitFill( Cube )\
+         (((Cube)->pData[0] =  BITS_FULL),\
+          ((Cube)->pData[1] = (BITS_FULL >> (Cube)->nUnused))) 
+#define Mvc_CubeNBitFill( Cube )\
+{\
+    int _i_;\
+    (Cube)->pData[(Cube)->iLast] = (BITS_FULL >> (Cube)->nUnused);\
+    for( _i_ = (Cube)->iLast - 1; _i_ >= 0; _i_-- )\
+        (Cube)->pData[_i_] =  BITS_FULL;\
+}
+
+// complementing the data bits
+#define Mvc_Cube1BitNot( Cube )\
+          ((Cube)->pData[0] ^= (BITS_FULL >> (Cube)->nUnused))
+#define Mvc_Cube2BitNot( Cube )\
+         (((Cube)->pData[0] ^=  BITS_FULL),\
+          ((Cube)->pData[1] ^= (BITS_FULL >> (Cube)->nUnused)))
+#define Mvc_CubeNBitNot( Cube )\
+{\
+    int _i_;\
+    (Cube)->pData[(Cube)->iLast] ^= (BITS_FULL >> (Cube)->nUnused);\
+    for( _i_ = (Cube)->iLast - 1; _i_ >= 0; _i_-- )\
+        (Cube)->pData[_i_] ^=  BITS_FULL;\
+}
+
+#define Mvc_Cube1BitCopy( Cube1, Cube2 )\
+         (((Cube1)->pData[0]) = ((Cube2)->pData[0]))
+#define Mvc_Cube2BitCopy( Cube1, Cube2 )\
+        ((((Cube1)->pData[0]) = ((Cube2)->pData[0])),\
+         (((Cube1)->pData[1])=  ((Cube2)->pData[1])))
+#define Mvc_CubeNBitCopy( Cube1, Cube2 )\
+{\
+    int _i_;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        ((Cube1)->pData[_i_]) = ((Cube2)->pData[_i_]);\
+}
+
+#define Mvc_Cube1BitOr( CubeR, Cube1, Cube2 )\
+         (((CubeR)->pData[0]) = ((Cube1)->pData[0] | (Cube2)->pData[0]))
+#define Mvc_Cube2BitOr( CubeR, Cube1, Cube2 )\
+        ((((CubeR)->pData[0]) = ((Cube1)->pData[0] | (Cube2)->pData[0])),\
+         (((CubeR)->pData[1]) = ((Cube1)->pData[1] | (Cube2)->pData[1])))
+#define Mvc_CubeNBitOr( CubeR, Cube1, Cube2 )\
+{\
+    int _i_;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] | (Cube2)->pData[_i_]));\
+}
+
+#define Mvc_Cube1BitExor( CubeR, Cube1, Cube2 )\
+         (((CubeR)->pData[0]) = ((Cube1)->pData[0] ^ (Cube2)->pData[0]))
+#define Mvc_Cube2BitExor( CubeR, Cube1, Cube2 )\
+        ((((CubeR)->pData[0]) = ((Cube1)->pData[0] ^ (Cube2)->pData[0])),\
+         (((CubeR)->pData[1]) = ((Cube1)->pData[1] ^ (Cube2)->pData[1])))
+#define Mvc_CubeNBitExor( CubeR, Cube1, Cube2 )\
+{\
+    int _i_;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] ^ (Cube2)->pData[_i_]));\
+}
+
+#define Mvc_Cube1BitAnd( CubeR, Cube1, Cube2 )\
+         (((CubeR)->pData[0]) = ((Cube1)->pData[0] & (Cube2)->pData[0]))
+#define Mvc_Cube2BitAnd( CubeR, Cube1, Cube2 )\
+        ((((CubeR)->pData[0]) = ((Cube1)->pData[0] & (Cube2)->pData[0])),\
+         (((CubeR)->pData[1]) = ((Cube1)->pData[1] & (Cube2)->pData[1])))
+#define Mvc_CubeNBitAnd( CubeR, Cube1, Cube2 )\
+{\
+    int _i_;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] & (Cube2)->pData[_i_]));\
+} 
+
+#define Mvc_Cube1BitSharp( CubeR, Cube1, Cube2 )\
+         (((CubeR)->pData[0]) = ((Cube1)->pData[0] & ~((Cube2)->pData[0])))
+#define Mvc_Cube2BitSharp( CubeR, Cube1, Cube2 )\
+        ((((CubeR)->pData[0]) = ((Cube1)->pData[0] & ~((Cube2)->pData[0]))),\
+         (((CubeR)->pData[1]) = ((Cube1)->pData[1] & ~((Cube2)->pData[1]))))
+#define Mvc_CubeNBitSharp( CubeR, Cube1, Cube2 )\
+{\
+    int _i_;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        (((CubeR)->pData[_i_]) = ((Cube1)->pData[_i_] & ~(Cube2)->pData[_i_]));\
+}  
+
+#define Mvc_Cube1BitEmpty( Res, Cube )\
+  (Res = ((Cube)->pData[0] == 0))
+#define Mvc_Cube2BitEmpty( Res, Cube )\
+  (Res = ((Cube)->pData[0] == 0 && (Cube)->pData[1] == 0))
+#define Mvc_CubeNBitEmpty( Res, Cube )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube)->iLast; _i_ >= 0; _i_--)\
+        if ( (Cube)->pData[_i_] )\
+           { Res = 0; break; }\
+}
+
+#define Mvc_Cube1BitEqual( Res, Cube1, Cube2 )\
+  (Res = (((Cube1)->pData[0]) == ((Cube2)->pData[0])))
+#define Mvc_Cube2BitEqual( Res, Cube1, Cube2 )\
+ (Res = ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) &&\
+         (((Cube1)->pData[1]) == ((Cube2)->pData[1]))))
+#define Mvc_CubeNBitEqual( Res, Cube1, Cube2 )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+         if (((Cube1)->pData[_i_]) != ((Cube2)->pData[_i_]))\
+              { Res = 0; break; }\
+}
+
+#define Mvc_Cube1BitLess( Res, Cube1, Cube2 )\
+  (Res = (((Cube1)->pData[0]) <  ((Cube2)->pData[0])))
+#define Mvc_Cube2BitLess( Res, Cube1, Cube2 )\
+ (Res = ((((Cube1)->pData[0]) <  ((Cube2)->pData[0])) ||\
+        ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) && (((Cube1)->pData[1]) <  ((Cube2)->pData[1])))))
+#define Mvc_CubeNBitLess( Res, Cube1, Cube2 )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+         if (((Cube1)->pData[_i_]) >= ((Cube2)->pData[_i_]))\
+             { Res = 0; break; }\
+}        
+
+#define Mvc_Cube1BitMore( Res, Cube1, Cube2 )\
+  (Res = (((Cube1)->pData[0]) >  ((Cube2)->pData[0])))
+#define Mvc_Cube2BitMore( Res, Cube1, Cube2 )\
+ (Res = ((((Cube1)->pData[0]) >  ((Cube2)->pData[0])) ||\
+        ((((Cube1)->pData[0]) == ((Cube2)->pData[0])) && (((Cube1)->pData[1]) >  ((Cube2)->pData[1])))))
+#define Mvc_CubeNBitMore( Res, Cube1, Cube2 )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if (((Cube1)->pData[_i_]) <= ((Cube2)->pData[_i_]))\
+             { Res = 0; break; }\
+}         
+
+#define Mvc_Cube1BitNotImpl( Res, Cube1, Cube2 )\
+  (Res = (((Cube1)->pData[0])  & ~((Cube2)->pData[0])))
+#define Mvc_Cube2BitNotImpl( Res, Cube1, Cube2 )\
+ (Res = ((((Cube1)->pData[0]) & ~((Cube2)->pData[0])) ||\
+         (((Cube1)->pData[1]) & ~((Cube2)->pData[1]))))
+#define Mvc_CubeNBitNotImpl( Res, Cube1, Cube2 )\
+{\
+    int _i_; Res = 0;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if (((Cube1)->pData[_i_]) & ~((Cube2)->pData[_i_]))\
+            { Res = 1; break; }\
+}         
+
+#define Mvc_Cube1BitDisjoint( Res, Cube1, Cube2 )\
+  (Res = ((((Cube1)->pData[0]) &  ((Cube2)->pData[0])) == 0 ))
+#define Mvc_Cube2BitDisjoint( Res, Cube1, Cube2 )\
+ (Res = (((((Cube1)->pData[0]) &  ((Cube2)->pData[0])) == 0 ) &&\
+         ((((Cube1)->pData[1]) &  ((Cube2)->pData[1])) == 0 )))
+#define Mvc_CubeNBitDisjoint( Res, Cube1, Cube2 )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if (((Cube1)->pData[_i_]) & ((Cube2)->pData[_i_]))\
+             { Res = 0; break; }\
+}             
+
+#define Mvc_Cube1BitEqualUnderMask( Res, Cube1, Cube2, Mask )\
+  (Res = ((((Cube1)->pData[0]) & ((Mask)->pData[0])) == (((Cube2)->pData[0]) & ((Mask)->pData[0]))))
+#define Mvc_Cube2BitEqualUnderMask( Res, Cube1, Cube2, Mask )\
+ (Res = (((((Cube1)->pData[0]) & ((Mask)->pData[0])) == (((Cube2)->pData[0]) & ((Mask)->pData[0])))  &&\
+         ((((Cube1)->pData[1]) & ((Mask)->pData[1])) == (((Cube2)->pData[1]) & ((Mask)->pData[1])))))
+#define Mvc_CubeNBitEqualUnderMask( Res, Cube1, Cube2, Mask )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if ((((Cube1)->pData[_i_]) & ((Mask)->pData[_i_])) != (((Cube2)->pData[_i_]) & ((Mask)->pData[_i_])))\
+            { Res = 0; break; }\
+}               
+
+#define Mvc_Cube1BitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
+  (Res = ((((Cube1)->pData[0]) | ((Mask)->pData[0])) == (((Cube2)->pData[0]) | ((Mask)->pData[0]))))
+#define Mvc_Cube2BitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
+ (Res = (((((Cube1)->pData[0]) | ((Mask)->pData[0])) == (((Cube2)->pData[0]) | ((Mask)->pData[0])))  &&\
+         ((((Cube1)->pData[1]) | ((Mask)->pData[1])) == (((Cube2)->pData[1]) | ((Mask)->pData[1])))))
+#define Mvc_CubeNBitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
+{\
+    int _i_; Res = 1;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if ((((Cube1)->pData[_i_]) | ((Mask)->pData[_i_])) != (((Cube2)->pData[_i_]) | ((Mask)->pData[_i_])))\
+            { Res = 0; break; }\
+}              
+
+#define Mvc_Cube1BitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
+  (Res = ((((Cube1)->pData[0]) & ((Cube2)->pData[0]) & ((Mask)->pData[0])) > 0))
+#define Mvc_Cube2BitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
+ (Res = (((((Cube1)->pData[0]) & ((Cube2)->pData[0]) & ((Mask)->pData[0])) > 0) ||\
+         ((((Cube1)->pData[1]) & ((Cube2)->pData[1]) & ((Mask)->pData[1])) > 0)))
+#define Mvc_CubeNBitIntersectUnderMask( Res, Cube1, Cube2, Mask)\
+{\
+    int _i_; Res = 0;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if (((Cube1)->pData[_i_]) & ((Cube2)->pData[_i_]) & ((Mask)->pData[_i_]))\
+           { Res = 1; break; }\
+}       
+
+#define Mvc_Cube1BitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
+  (Res = (((Mask)->pData[0]) & ((Cube1)->pData[0])  & ~((Cube2)->pData[0])))
+#define Mvc_Cube2BitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
+ (Res = ((((Mask)->pData[0]) & ((Cube1)->pData[0]) & ~((Cube2)->pData[0])) ||\
+         (((Mask)->pData[1]) & ((Cube1)->pData[1]) & ~((Cube2)->pData[1]))))
+#define Mvc_CubeNBitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
+{\
+    int _i_; Res = 0;\
+    for (_i_ = (Cube1)->iLast; _i_ >= 0; _i_--)\
+        if (((Mask)->pData[_i_]) & ((Cube1)->pData[_i_]) & ~((Cube2)->pData[_i_]))\
+            { Res = 1; break; }\
+}         
+
+// the following macros make no assumption about the cube's bitset size
+#define Mvc_CubeBitClean( Cube )\
+    if ( Mvc_Cube1Words(Cube) )      { Mvc_Cube1BitClean( Cube ); }\
+    else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitClean( Cube ); }\
+    else                             { Mvc_CubeNBitClean( Cube ); }
+#define Mvc_CubeBitFill( Cube )\
+    if ( Mvc_Cube1Words(Cube) )      { Mvc_Cube1BitFill( Cube ); }\
+    else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitFill( Cube ); }\
+    else                             { Mvc_CubeNBitFill( Cube ); }
+#define Mvc_CubeBitNot( Cube )\
+    if ( Mvc_Cube1Words(Cube) )      { Mvc_Cube1BitNot( Cube ); }\
+    else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitNot( Cube ); }\
+    else                             { Mvc_CubeNBitNot( Cube ); }
+#define Mvc_CubeBitCopy( Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitCopy( Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitCopy( Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitCopy( Cube1, Cube2 ); }
+#define Mvc_CubeBitOr( CubeR, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitOr( CubeR, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitOr( CubeR, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitOr( CubeR, Cube1, Cube2 ); }
+#define Mvc_CubeBitExor( CubeR, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitExor( CubeR, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitExor( CubeR, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitExor( CubeR, Cube1, Cube2 ); }
+#define Mvc_CubeBitAnd( CubeR, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitAnd( CubeR, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitAnd( CubeR, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitAnd( CubeR, Cube1, Cube2 ); }
+#define Mvc_CubeBitSharp( CubeR, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitSharp( CubeR, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitSharp( CubeR, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitSharp( CubeR, Cube1, Cube2 ); }
+#define Mvc_CubeBitEmpty( Res, Cube )\
+    if ( Mvc_Cube1Words(Cube) )      { Mvc_Cube1BitEmpty( Res, Cube ); }\
+    else if ( Mvc_Cube2Words(Cube) ) { Mvc_Cube2BitEmpty( Res, Cube ); }\
+    else                             { Mvc_CubeNBitEmpty( Res, Cube ); }
+#define Mvc_CubeBitEqual( Res, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitEqual( Res, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqual( Res, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitEqual( Res, Cube1, Cube2 ); }
+#define Mvc_CubeBitLess( Res, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitLess( Res, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitLess( Res, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitLess( Res, Cube1, Cube2 ); }
+#define Mvc_CubeBitMore( Res, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitMore( Res, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitMore( Res, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitMore( Res, Cube1, Cube2 ); }
+#define Mvc_CubeBitNotImpl( Res, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitNotImpl( Res, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitNotImpl( Res, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitNotImpl( Res, Cube1, Cube2 ); }
+#define Mvc_CubeBitDisjoint( Res, Cube1, Cube2 )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitDisjoint( Res, Cube1, Cube2 ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitDisjoint( Res, Cube1, Cube2 ); }\
+    else                             { Mvc_CubeNBitDisjoint( Res, Cube1, Cube2 ); }
+#define Mvc_CubeBitEqualUnderMask( Res, Cube1, Cube2, Mask )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitEqualUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqualUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else                             { Mvc_CubeNBitEqualUnderMask( Res, Cube1, Cube2, Mask ); }
+#define Mvc_CubeBitEqualOutsideMask( Res, Cube1, Cube2, Mask )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }\
+    else                             { Mvc_CubeNBitEqualOutsideMask( Res, Cube1, Cube2, Mask ); }
+#define Mvc_CubeBitIntersectUnderMask( Res, Cube1, Cube2, Mask )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else                             { Mvc_CubeNBitIntersectUnderMask( Res, Cube1, Cube2, Mask ); }
+#define Mvc_CubeBitNotImplUnderMask( Res, Cube1, Cube2, Mask )\
+    if ( Mvc_Cube1Words(Cube1) )     { Mvc_Cube1BitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else if ( Mvc_Cube2Words(Cube1) ){ Mvc_Cube2BitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }\
+    else                             { Mvc_CubeNBitNotImplUnderMask( Res, Cube1, Cube2, Mask ); }
+
+
+// managing linked lists
+#define Mvc_ListAddCubeHead( pList, pCube )\
+    {\
+        if ( pList->pHead == NULL )\
+        {\
+            Mvc_CubeSetNext( pCube, NULL );\
+            pList->pHead = pCube;\
+            pList->pTail = pCube;\
+        }\
+        else\
+        {\
+            Mvc_CubeSetNext( pCube, pList->pHead );\
+            pList->pHead = pCube;\
+        }\
+        pList->nItems++;\
+    }
+#define Mvc_ListAddCubeTail( pList, pCube )\
+    {\
+        if ( pList->pHead == NULL )\
+            pList->pHead = pCube;\
+        else\
+            Mvc_CubeSetNext( pList->pTail, pCube );\
+        pList->pTail    = pCube;\
+        Mvc_CubeSetNext( pCube, NULL );\
+        pList->nItems++;\
+    }
+#define Mvc_ListDeleteCube( pList, pPrev, pCube )\
+{\
+    if ( pPrev == NULL )\
+        pList->pHead = pCube->pNext;\
+    else\
+        pPrev->pNext = pCube->pNext;\
+    if ( pList->pTail == pCube )\
+    {\
+        assert( pCube->pNext == NULL );\
+        pList->pTail = pPrev;\
+    }\
+    pList->nItems--;\
+}
+
+// managing linked lists inside the cover
+#define Mvc_CoverAddCubeHead( pCover, pCube )\
+{\
+    Mvc_List_t * pList = &pCover->lCubes;\
+    Mvc_ListAddCubeHead( pList, pCube );\
+}
+#define Mvc_CoverAddCubeTail( pCover, pCube )\
+{\
+    Mvc_List_t * pList = &pCover->lCubes;\
+    Mvc_ListAddCubeTail( pList, pCube );\
+}
+#define Mvc_CoverDeleteCube( pCover, pPrev, pCube )\
+{\
+    Mvc_List_t * pList = &pCover->lCubes;\
+    Mvc_ListDeleteCube( pList, pPrev, pCube );\
+}
+
+
+
+
+
+
+// iterator through the cubes in the cube list
+#define Mvc_ListForEachCube( List, Cube )\
+    for ( Cube = List->pHead;\
+          Cube;\
+          Cube = Cube->pNext )
+#define Mvc_ListForEachCubeSafe( List, Cube, Cube2 )\
+    for ( Cube = List->pHead, Cube2 = (Cube? Cube->pNext: NULL);\
+          Cube;\
+          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
+
+// iterator through cubes in the cover
+#define Mvc_CoverForEachCube( Cover, Cube )\
+    for ( Cube = (Cover)->lCubes.pHead;\
+          Cube;\
+          Cube = Cube->pNext )
+#define Mvc_CoverForEachCubeWithIndex( Cover, Cube, Index )\
+    for ( Index = 0, Cube = (Cover)->lCubes.pHead;\
+          Cube;\
+          Index++, Cube = Cube->pNext )
+#define Mvc_CoverForEachCubeSafe( Cover, Cube, Cube2 )\
+    for ( Cube = (Cover)->lCubes.pHead, Cube2 = (Cube? Cube->pNext: NULL);\
+          Cube;\
+          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
+
+// iterator which starts from the given cube
+#define Mvc_CoverForEachCubeStart( Start, Cube )\
+    for ( Cube = Start;\
+          Cube;\
+          Cube = Cube->pNext )
+#define Mvc_CoverForEachCubeStartSafe( Start, Cube, Cube2 )\
+    for ( Cube = Start, Cube2 = (Cube? Cube->pNext: NULL);\
+          Cube;\
+          Cube = Cube2, Cube2 = (Cube? Cube->pNext: NULL) )
+
+
+// iterator through literals of the cube
+#define Mvc_CubeForEachBit( Cover, Cube, iBit, Value )\
+    for ( iBit = 0;\
+          iBit < Cover->nBits && ((Value = Mvc_CubeBitValue(Cube,iBit))>=0);\
+          iBit++ )
+// iterator through values of binary variables
+#define Mvc_CubeForEachVarValue( Cover, Cube, iVar, Value )\
+    for ( iVar = 0;\
+          iVar < Cover->nBits/2 && (Value = Mvc_CubeVarValue(Cube,iVar));\
+          iVar++ )
+
+
+// macros which work with memory
+// MEM_ALLOC: allocate the given number (Size) of items of type (Type)
+// MEM_FREE:  deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
+#define MEM_ALLOC( Manager, Type, Size )          ((Type *)malloc( (Size) * sizeof(Type) ))
+#define MEM_FREE( Manager, Type, Size, Pointer )  if ( Pointer ) { free(Pointer); Pointer = NULL; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== mvcApi.c ====================================================*/
+extern int              Mvc_CoverReadWordNum( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverReadBitNum( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverReadCubeNum( Mvc_Cover_t * pCover );
+extern Mvc_Cube_t *     Mvc_CoverReadCubeHead( Mvc_Cover_t * pCover );
+extern Mvc_Cube_t *     Mvc_CoverReadCubeTail( Mvc_Cover_t * pCover );
+extern Mvc_List_t *     Mvc_CoverReadCubeList( Mvc_Cover_t * pCover );
+extern int              Mvc_ListReadCubeNum( Mvc_List_t * pList );
+extern Mvc_Cube_t *     Mvc_ListReadCubeHead( Mvc_List_t * pList );
+extern Mvc_Cube_t *     Mvc_ListReadCubeTail( Mvc_List_t * pList );
+extern void             Mvc_CoverSetCubeNum( Mvc_Cover_t * pCover,int nItems );
+extern void             Mvc_CoverSetCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverSetCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverSetCubeList( Mvc_Cover_t * pCover, Mvc_List_t * pList );
+extern int              Mvc_CoverIsEmpty( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverIsTautology( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverIsBinaryBuffer( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverMakeEmpty( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverMakeTautology( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverCreateEmpty( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverCreateTautology( Mvc_Cover_t * pCover );
+/*=== mvcCover.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverAlloc( Mvc_Manager_t * pMem, int nBits );
+extern Mvc_Cover_t *    Mvc_CoverCreateConst( Mvc_Manager_t * pMem, int nBits, int  Phase );
+extern Mvc_Cover_t *    Mvc_CoverClone( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverDup( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverFree( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverAllocateMask( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverAllocateArrayLits( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverAllocateArrayCubes( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverDeallocateMask( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverDeallocateArrayLits( Mvc_Cover_t * pCover );
+/*=== mvcCube.c ====================================================*/
+extern Mvc_Cube_t *     Mvc_CubeAlloc( Mvc_Cover_t * pCover );
+extern Mvc_Cube_t *     Mvc_CubeDup( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CubeBitRemoveDcs( Mvc_Cube_t * pCube );
+/*=== mvcCompare.c ====================================================*/
+extern int              Mvc_CubeCompareInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
+extern int              Mvc_CubeCompareSizeAndInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
+extern int              Mvc_CubeCompareIntUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
+extern int              Mvc_CubeCompareIntOutsideMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
+extern int              Mvc_CubeCompareIntOutsideAndUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask );
+/*=== mvcDd.c ====================================================*/
+/*
+extern DdNode *         Mvc_CoverConvertToBdd( DdManager * dd, Mvc_Cover_t * pCover );
+extern DdNode *         Mvc_CoverConvertToZdd( DdManager * dd, Mvc_Cover_t * pCover );
+extern DdNode *         Mvc_CoverConvertToZdd2( DdManager * dd, Mvc_Cover_t * pCover );
+extern DdNode *         Mvc_CubeConvertToBdd( DdManager * dd, Mvc_Cube_t * pCube );
+extern DdNode *         Mvc_CubeConvertToZdd( DdManager * dd, Mvc_Cube_t * pCube );
+extern DdNode *         Mvc_CubeConvertToZdd2( DdManager * dd, Mvc_Cube_t * pCube );
+*/
+/*=== mvcDivisor.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverDivisor( Mvc_Cover_t * pCover );
+/*=== mvcDivide.c ====================================================*/
+extern void             Mvc_CoverDivide( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
+extern void             Mvc_CoverDivideInternal( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
+extern void             Mvc_CoverDivideByLiteral( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
+extern void             Mvc_CoverDivideByCube( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem );
+extern void             Mvc_CoverDivideByLiteralQuo( Mvc_Cover_t * pCover, int iLit );
+/*=== mvcList.c ====================================================*/
+// these functions are available as macros
+extern void             Mvc_ListAddCubeHead_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
+extern void             Mvc_ListAddCubeTail_( Mvc_List_t * pList, Mvc_Cube_t * pCube );
+extern void             Mvc_ListDeleteCube_( Mvc_List_t * pList, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverAddCubeHead_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverAddCubeTail_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverDeleteCube_( Mvc_Cover_t * pCover, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverAddDupCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverAddDupCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+// other functions
+extern void             Mvc_CoverAddLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverDeleteLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverList2Array( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverArray2List( Mvc_Cover_t * pCover );
+extern Mvc_Cube_t *     Mvc_ListGetTailFromHead( Mvc_Cube_t * pHead );
+/*=== mvcPrint.c ====================================================*/
+extern void             Mvc_CoverPrint( Mvc_Cover_t * pCover );
+extern void             Mvc_CubePrint( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+extern void             Mvc_CoverPrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover );
+extern void             Mvc_CubePrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+/*=== mvcSort.c ====================================================*/
+extern void             Mvc_CoverSort( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) );
+/*=== mvcUtils.c ====================================================*/
+extern void             Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp );
+extern int              Mvc_CoverSupportSizeBinary( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverSupportVarBelongs( Mvc_Cover_t * pCover, int iVar );
+extern void             Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube );
+extern int              Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover );
+extern void             Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverCommonCubeCover( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+extern int              Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube );
+extern int              Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] );
+extern Mvc_Cover_t *    Mvc_CoverRemap( Mvc_Cover_t * pCover, int * pVarsRem, int nVarsRem );
+extern void             Mvc_CoverInverse( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverRemoveDontCareLits( Mvc_Cover_t * pCover );
+extern Mvc_Cover_t *    Mvc_CoverCofactor( Mvc_Cover_t * pCover, int iValue, int iValueOther );
+extern Mvc_Cover_t *    Mvc_CoverFlipVar( Mvc_Cover_t * pCover, int iValue0, int iValue1 );
+extern Mvc_Cover_t *    Mvc_CoverUnivQuantify( Mvc_Cover_t * p, int iValueA0, int iValueA1, int iValueB0, int iValueB1 );
+extern Mvc_Cover_t **   Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar );
+extern int              Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue );
+//extern Mvc_Cover_t *    Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew );
+extern Mvc_Cover_t *    Mvc_CoverTranspose( Mvc_Cover_t * pCover );
+extern int              Mvc_UtilsCheckUnusedZeros( Mvc_Cover_t * pCover );
+/*=== mvcLits.c ====================================================*/
+extern int              Mvc_CoverAnyLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
+extern int              Mvc_CoverBestLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
+extern int              Mvc_CoverWorstLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask );
+extern Mvc_Cover_t *    Mvc_CoverBestLiteralCover( Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
+extern int              Mvc_CoverFirstCubeFirstLit( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverCountLiterals( Mvc_Cover_t * pCover );
+extern int              Mvc_CoverIsOneLiteral( Mvc_Cover_t * pCover );
+/*=== mvcOpAlg.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverAlgebraicMultiply( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+extern Mvc_Cover_t *    Mvc_CoverAlgebraicSubtract( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+extern int              Mvc_CoverAlgebraicEqual( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+/*=== mvcOpBool.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverBooleanOr( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+extern Mvc_Cover_t *    Mvc_CoverBooleanAnd( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+extern int              Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 );
+
+/*=== mvcContain.c ====================================================*/
+extern int              Mvc_CoverContain( Mvc_Cover_t * pCover );
+/*=== mvcTau.c ====================================================*/
+extern int              Mvc_CoverTautology( Mvc_Data_t * p, Mvc_Cover_t * pCover );
+/*=== mvcCompl.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverComplement( Mvc_Data_t * p, Mvc_Cover_t * pCover );
+/*=== mvcSharp.c ====================================================*/
+extern Mvc_Cover_t *    Mvc_CoverSharp( Mvc_Data_t * p, Mvc_Cover_t * pA, Mvc_Cover_t * pB );
+extern int              Mvc_CoverDist0Cubes( Mvc_Data_t * pData, Mvc_Cube_t * pA, Mvc_Cube_t * pB );
+extern void             Mvc_CoverIntersectCubes( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
+extern int              Mvc_CoverIsIntersecting( Mvc_Data_t * pData, Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
+extern void             Mvc_CoverAppendCubes( Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
+extern void             Mvc_CoverCopyAndAppendCubes( Mvc_Cover_t * pC1, Mvc_Cover_t * pC2 );
+extern void             Mvc_CoverRemoveCubes( Mvc_Cover_t * pC );
+
+/*=== mvcReshape.c ====================================================*/
+extern void             Mvc_CoverMinimizeByReshape( Mvc_Data_t * pData, Mvc_Cover_t * pCover );
+
+/*=== mvcMerge.c ====================================================*/
+extern void             Mvc_CoverDist1Merge( Mvc_Data_t * p, Mvc_Cover_t * pCover );
+
+/*=== mvcData.c ====================================================*/
+//extern Mvc_Data_t *     Mvc_CoverDataAlloc( Vm_VarMap_t * pVm, Mvc_Cover_t * pCover );
+//extern void             Mvc_CoverDataFree( Mvc_Data_t * p, Mvc_Cover_t * pCover );
+
+/*=== mvcMan.c ====================================================*/
+extern void             Mvc_ManagerFree( Mvc_Manager_t * p );
+extern Mvc_Manager_t *  Mvc_ManagerStart();
+extern Mvc_Manager_t *  Mvc_ManagerAllocCover();
+extern Mvc_Manager_t *  Mvc_ManagerAllocCube( int nWords );
+extern Mvc_Manager_t *  Mvc_ManagerFreeCover( Mvc_Cover_t * pCover );
+extern Mvc_Manager_t *  Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/mvc/mvcApi.c b/src/misc/mvc/mvcApi.c
new file mode 100644
index 00000000..1f51a235
--- /dev/null
+++ b/src/misc/mvc/mvcApi.c
@@ -0,0 +1,233 @@
+/**CFile****************************************************************
+
+  FileName    [mvcApi.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    []
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcApi.c,v 1.4 2003/04/03 06:31:48 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int          Mvc_CoverReadWordNum( Mvc_Cover_t * pCover )   { return pCover->nWords;         }
+int          Mvc_CoverReadBitNum( Mvc_Cover_t * pCover )    { return pCover->nBits;          }
+int          Mvc_CoverReadCubeNum( Mvc_Cover_t * pCover )   { return pCover->lCubes.nItems; }
+Mvc_Cube_t * Mvc_CoverReadCubeHead( Mvc_Cover_t * pCover )  { return pCover->lCubes.pHead;  }
+Mvc_Cube_t * Mvc_CoverReadCubeTail( Mvc_Cover_t * pCover )  { return pCover->lCubes.pTail;  }
+Mvc_List_t * Mvc_CoverReadCubeList( Mvc_Cover_t * pCover )  { return &pCover->lCubes;        }
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int          Mvc_ListReadCubeNum( Mvc_List_t * pList )   { return pList->nItems; }
+Mvc_Cube_t * Mvc_ListReadCubeHead( Mvc_List_t * pList )  { return pList->pHead;  }
+Mvc_Cube_t * Mvc_ListReadCubeTail( Mvc_List_t * pList )  { return pList->pTail;  }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void         Mvc_CoverSetCubeNum( Mvc_Cover_t * pCover,int nItems )           { pCover->lCubes.nItems = nItems; }
+void         Mvc_CoverSetCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) { pCover->lCubes.pHead = pCube;   }
+void         Mvc_CoverSetCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) { pCover->lCubes.pTail = pCube;   }
+void         Mvc_CoverSetCubeList( Mvc_Cover_t * pCover, Mvc_List_t * pList ) { pCover->lCubes = *pList;        }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverIsEmpty( Mvc_Cover_t * pCover )
+{
+    return Mvc_CoverReadCubeNum(pCover) == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverIsTautology( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int iBit, Value;
+
+    if ( Mvc_CoverReadCubeNum(pCover) != 1 )
+        return 0;
+
+    pCube = Mvc_CoverReadCubeHead( pCover );
+    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+        if ( Value == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cover is a binary buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverIsBinaryBuffer( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    if ( pCover->nBits != 2 )
+        return 0;
+    if ( Mvc_CoverReadCubeNum(pCover) != 1 )
+        return 0;
+    pCube = pCover->lCubes.pHead;
+    if ( Mvc_CubeBitValue(pCube, 0) == 0 && Mvc_CubeBitValue(pCube, 1) == 1 )
+        return 1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverMakeEmpty( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube, * pCube2;
+    Mvc_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+        Mvc_CubeFree( pCover, pCube );
+    pCover->lCubes.nItems = 0;
+    pCover->lCubes.pHead = NULL;
+    pCover->lCubes.pTail = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverMakeTautology( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCubeNew;
+    Mvc_CoverMakeEmpty( pCover );
+    pCubeNew = Mvc_CubeAlloc( pCover );
+    Mvc_CubeBitFill( pCubeNew );
+    Mvc_CoverAddCubeTail( pCover, pCubeNew );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverCreateEmpty( Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pCoverNew;
+    pCoverNew = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+    return pCoverNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverCreateTautology( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCubeNew;
+    Mvc_Cover_t * pCoverNew;
+    pCoverNew = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+    pCubeNew = Mvc_CubeAlloc( pCoverNew );
+    Mvc_CubeBitFill( pCubeNew );
+    Mvc_CoverAddCubeTail( pCoverNew, pCubeNew );
+    return pCoverNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcCompare.c b/src/misc/mvc/mvcCompare.c
new file mode 100644
index 00000000..c7999d40
--- /dev/null
+++ b/src/misc/mvc/mvcCompare.c
@@ -0,0 +1,369 @@
+/**CFile****************************************************************
+
+  FileName    [mvcCompare.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Various cube comparison functions.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcCompare.c,v 1.5 2003/04/03 23:25:41 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two cubes according to their integer value.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CubeCompareInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask )
+{
+    if ( Mvc_Cube1Words(pC1) )
+    {
+        if ( pC1->pData[0] < pC2->pData[0] )
+            return -1;
+        if ( pC1->pData[0] > pC2->pData[0] )
+            return 1;
+        return 0;
+    }
+    else if ( Mvc_Cube2Words(pC1) )
+    {
+        if ( pC1->pData[1] < pC2->pData[1] )
+            return -1;
+        if ( pC1->pData[1] > pC2->pData[1] )
+            return 1;
+        if ( pC1->pData[0] < pC2->pData[0] )
+            return -1;
+        if ( pC1->pData[0] > pC2->pData[0] )
+            return 1;
+        return 0;
+    }
+    else                            
+    {
+        int i = Mvc_CubeReadLast(pC1);
+        for(; i >= 0; i--)
+        {
+            if ( pC1->pData[i] < pC2->pData[i] )
+                return -1;
+            if ( pC1->pData[i] > pC2->pData[i] )
+                return 1;
+        }
+        return 0;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the cubes (1) by size, (2) by integer value.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CubeCompareSizeAndInt( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask )
+{
+    // compare the cubes by size
+    if ( Mvc_CubeReadSize( pC1 ) < Mvc_CubeReadSize( pC2 ) )
+        return 1;
+    if ( Mvc_CubeReadSize( pC1 ) > Mvc_CubeReadSize( pC2 ) )
+        return -1;
+    // the cubes have the same size
+
+    // compare the cubes as integers
+    if ( Mvc_Cube1Words( pC1 ) )
+    {
+        if ( pC1->pData[0] < pC2->pData[0] )
+            return -1;
+        if ( pC1->pData[0] > pC2->pData[0] )
+            return 1;
+        return 0;
+    }
+    else if ( Mvc_Cube2Words( pC1 ) )
+    {
+        if ( pC1->pData[1] < pC2->pData[1] )
+            return -1;
+        if ( pC1->pData[1] > pC2->pData[1] )
+            return 1;
+        if ( pC1->pData[0] < pC2->pData[0] )
+            return -1;
+        if ( pC1->pData[0] > pC2->pData[0] )
+            return 1;
+        return 0;
+    }
+    else                            
+    {
+        int i = Mvc_CubeReadLast( pC1 );
+        for(; i >= 0; i--)
+        {
+            if ( pC1->pData[i] < pC2->pData[i] )
+                return -1;
+            if ( pC1->pData[i] > pC2->pData[i] )
+                return 1;
+        }
+        return 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two cubes under the mask.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CubeCompareIntUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask )
+{
+    unsigned uBits1, uBits2;
+
+    // compare the cubes under the mask
+    if ( Mvc_Cube1Words(pC1) )
+    {
+        uBits1 = pC1->pData[0] & pMask->pData[0];
+        uBits2 = pC2->pData[0] & pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        // cubes are equal
+        return 0;
+    }
+    else if ( Mvc_Cube2Words(pC1) )
+    {
+        uBits1 = pC1->pData[1] & pMask->pData[1];
+        uBits2 = pC2->pData[1] & pMask->pData[1];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        uBits1 = pC1->pData[0] & pMask->pData[0];
+        uBits2 = pC2->pData[0] & pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        return 0;
+    }
+    else                            
+    {
+        int i = Mvc_CubeReadLast(pC1);
+        for(; i >= 0; i--)
+        {
+            uBits1 = pC1->pData[i] & pMask->pData[i];
+            uBits2 = pC2->pData[i] & pMask->pData[i];
+            if ( uBits1 < uBits2 )
+                return -1;
+            if ( uBits1 > uBits2 )
+                return 1;
+        }
+        return 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two cubes under the mask.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CubeCompareIntOutsideMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask )
+{
+    unsigned uBits1, uBits2;
+
+    // compare the cubes under the mask
+    if ( Mvc_Cube1Words(pC1) )
+    {
+        uBits1 = pC1->pData[0] | pMask->pData[0];
+        uBits2 = pC2->pData[0] | pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        // cubes are equal
+        return 0;
+    }
+    else if ( Mvc_Cube2Words(pC1) )
+    {
+        uBits1 = pC1->pData[1] | pMask->pData[1];
+        uBits2 = pC2->pData[1] | pMask->pData[1];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        uBits1 = pC1->pData[0] | pMask->pData[0];
+        uBits2 = pC2->pData[0] | pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        return 0;
+    }
+    else                            
+    {
+        int i = Mvc_CubeReadLast(pC1);
+        for(; i >= 0; i--)
+        {
+            uBits1 = pC1->pData[i] | pMask->pData[i];
+            uBits2 = pC2->pData[i] | pMask->pData[i];
+            if ( uBits1 < uBits2 )
+                return -1;
+            if ( uBits1 > uBits2 )
+                return 1;
+        }
+        return 0;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the cubes (1) outside the mask, (2) under the mask.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CubeCompareIntOutsideAndUnderMask( Mvc_Cube_t * pC1, Mvc_Cube_t * pC2, Mvc_Cube_t * pMask )
+{
+    unsigned uBits1, uBits2;
+
+    if ( Mvc_Cube1Words(pC1) )
+    {
+        // compare the cubes outside the mask
+        uBits1 = pC1->pData[0] & ~(pMask->pData[0]);
+        uBits2 = pC2->pData[0] & ~(pMask->pData[0]);
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+
+        // compare the cubes under the mask
+        uBits1 = pC1->pData[0] & pMask->pData[0];
+        uBits2 = pC2->pData[0] & pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+        // cubes are equal
+        // should never happen
+        assert( 0 );
+        return 0;
+    }
+    else if ( Mvc_Cube2Words(pC1) )
+    {
+        // compare the cubes outside the mask
+        uBits1 = pC1->pData[1] & ~(pMask->pData[1]);
+        uBits2 = pC2->pData[1] & ~(pMask->pData[1]);
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+
+        uBits1 = pC1->pData[0] & ~(pMask->pData[0]);
+        uBits2 = pC2->pData[0] & ~(pMask->pData[0]);
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+
+        // compare the cubes under the mask
+        uBits1 = pC1->pData[1] & pMask->pData[1];
+        uBits2 = pC2->pData[1] & pMask->pData[1];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+
+        uBits1 = pC1->pData[0] & pMask->pData[0];
+        uBits2 = pC2->pData[0] & pMask->pData[0];
+        if ( uBits1 < uBits2 )
+            return -1;
+        if ( uBits1 > uBits2 )
+            return 1;
+
+        // cubes are equal
+        // should never happen
+        assert( 0 );
+        return 0;
+    }
+    else                            
+    {
+        int i;
+
+        // compare the cubes outside the mask
+        for( i = Mvc_CubeReadLast(pC1); i >= 0; i-- )
+        {
+            uBits1 = pC1->pData[i] & ~(pMask->pData[i]);
+            uBits2 = pC2->pData[i] & ~(pMask->pData[i]);
+            if ( uBits1 < uBits2 )
+                return -1;
+            if ( uBits1 > uBits2 )
+                return 1;
+        }
+        // compare the cubes under the mask
+        for( i = Mvc_CubeReadLast(pC1); i >= 0; i-- )
+        {
+            uBits1 = pC1->pData[i] & pMask->pData[i];
+            uBits2 = pC2->pData[i] & pMask->pData[i];
+            if ( uBits1 < uBits2 )
+                return -1;
+            if ( uBits1 > uBits2 )
+                return 1;
+        }
+/*
+        {
+            Mvc_Cover_t * pCover;
+            pCover = Mvc_CoverAlloc( NULL, 96 );
+            Mvc_CubePrint( pCover, pC1 );
+            Mvc_CubePrint( pCover, pC2 );
+            Mvc_CubePrint( pCover, pMask );
+        }
+*/
+        // cubes are equal
+        // should never happen
+        assert( 0 );
+        return 0;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcContain.c b/src/misc/mvc/mvcContain.c
new file mode 100644
index 00000000..37b933b8
--- /dev/null
+++ b/src/misc/mvc/mvcContain.c
@@ -0,0 +1,173 @@
+/**CFile****************************************************************
+
+  FileName    [mvcContain.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Making the cover single-cube containment free.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcContain.c,v 1.4 2003/04/03 23:25:42 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Mvc_CoverRemoveDuplicates( Mvc_Cover_t * pCover );
+static void Mvc_CoverRemoveContained( Mvc_Cover_t * pCover );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the contained cubes.]
+
+  Description [Returns 1 if the cover has been changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int  Mvc_CoverContain( Mvc_Cover_t * pCover )
+{
+    int nCubes;
+    nCubes = Mvc_CoverReadCubeNum( pCover );
+    if ( nCubes < 2 )
+        return 0;
+    Mvc_CoverSetCubeSizes(pCover);
+    Mvc_CoverSort( pCover, NULL, Mvc_CubeCompareSizeAndInt );
+    Mvc_CoverRemoveDuplicates( pCover );
+    if ( nCubes > 1 )
+        Mvc_CoverRemoveContained( pCover );
+    return (nCubes != Mvc_CoverReadCubeNum(pCover));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes adjacent duplicated cubes from the cube list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverRemoveDuplicates( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pPrev, * pCube, * pCube2;
+    int  fEqual;
+
+    // set the first cube of the cover
+    pPrev = Mvc_CoverReadCubeHead(pCover);
+    // go through all the cubes after this one
+    Mvc_CoverForEachCubeStartSafe( Mvc_CubeReadNext(pPrev), pCube, pCube2 )
+    {
+        // compare the current cube with the prev cube
+        Mvc_CubeBitEqual( fEqual, pPrev, pCube );
+        if ( fEqual )
+        { // they are equal - remove the current cube
+            Mvc_CoverDeleteCube( pCover, pPrev, pCube );
+            Mvc_CubeFree( pCover, pCube );
+            // don't change the previous cube cube
+        }
+        else
+        { // they are not equal - update the previous cube
+            pPrev = pCube;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes contained cubes from the sorted cube list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverRemoveContained( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCubeBeg, * pCubeEnd, * pCubeLarge;
+    Mvc_Cube_t * pCube, * pCube2, * pPrev;
+    unsigned sizeCur;
+    int  Result;
+
+    // since the cubes are sorted by size, it is sufficient 
+    // to compare each cube with other cubes that have larger sizes
+    // if the given cube implies a larger cube, the larger cube is removed
+    pCubeBeg = Mvc_CoverReadCubeHead(pCover);
+    do
+    {
+        // get the current cube size
+        sizeCur = Mvc_CubeReadSize(pCubeBeg);
+
+        // initialize the end of the given size group
+        pCubeEnd = pCubeBeg;
+        // find the beginning of the next size group
+        Mvc_CoverForEachCubeStart( Mvc_CubeReadNext(pCubeBeg), pCube )
+        {
+            if ( sizeCur == Mvc_CubeReadSize(pCube) ) 
+                pCubeEnd = pCube;
+            else // pCube is the first cube in the new size group
+                break;
+        }
+        // if we could not find the next size group
+        // the containment check is finished
+        if ( pCube == NULL )
+            break;
+        // otherwise, pCubeBeg/pCubeEnd are the first/last cubes of the group
+
+        // go through all the cubes between pCubeBeg and pCubeEnd, inclusive,
+        // and for each of them, try removing cubes after pCubeEnd
+        Mvc_CoverForEachCubeStart( pCubeBeg, pCubeLarge )
+        {
+            pPrev = pCubeEnd;
+            Mvc_CoverForEachCubeStartSafe( Mvc_CubeReadNext(pCubeEnd), pCube, pCube2 )
+            {
+                // check containment
+                Mvc_CubeBitNotImpl( Result, pCube, pCubeLarge );
+                if ( !Result )
+                { // pCubeLarge implies pCube - remove pCube
+                    Mvc_CoverDeleteCube( pCover, pPrev, pCube );
+                    Mvc_CubeFree( pCover, pCube );
+                    // don't update the previous cube
+                }
+                else
+                {   // update the previous cube
+                    pPrev = pCube;
+                }
+            }
+            // quit, if the main cube was the last one of this size
+            if ( pCubeLarge == pCubeEnd )
+                break;
+        }
+
+        // set the beginning of the next group
+        pCubeBeg = Mvc_CubeReadNext(pCubeEnd);
+    }
+    while ( pCubeBeg );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcCover.c b/src/misc/mvc/mvcCover.c
new file mode 100644
index 00000000..bd9c4412
--- /dev/null
+++ b/src/misc/mvc/mvcCover.c
@@ -0,0 +1,251 @@
+/**CFile****************************************************************
+
+  FileName    [mvcCover.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Basic procedures to manipulate unate cube covers.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcCover.c,v 1.5 2003/04/09 18:02:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverAlloc( Mvc_Manager_t * pMem, int nBits )
+{
+    Mvc_Cover_t * p;
+    int nBitsInUnsigned;
+
+    nBitsInUnsigned  = 8 * sizeof(Mvc_CubeWord_t);
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    p                = (Mvc_Cover_t *)malloc( sizeof(Mvc_Cover_t) );
+#else
+    p                = (Mvc_Cover_t *)Extra_MmFixedEntryFetch( pMem->pManC );
+#endif
+    p->pMem          = pMem;
+    p->nBits         = nBits;
+    p->nWords        = nBits / nBitsInUnsigned + (int)(nBits % nBitsInUnsigned > 0);
+    p->nUnused       = p->nWords * nBitsInUnsigned - p->nBits;
+    p->lCubes.nItems = 0;
+    p->lCubes.pHead  = NULL;
+    p->lCubes.pTail  = NULL;
+    p->nCubesAlloc   = 0;
+    p->pCubes        = NULL;
+    p->pMask         = NULL;
+    p->pLits         = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverClone( Mvc_Cover_t * p )
+{
+    Mvc_Cover_t * pCover;
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    pCover                = (Mvc_Cover_t *)malloc( sizeof(Mvc_Cover_t) );
+#else
+    pCover                = (Mvc_Cover_t *)Extra_MmFixedEntryFetch( p->pMem->pManC );
+#endif
+    pCover->pMem          = p->pMem;
+    pCover->nBits         = p->nBits;
+    pCover->nWords        = p->nWords;
+    pCover->nUnused       = p->nUnused;
+    pCover->lCubes.nItems = 0;
+    pCover->lCubes.pHead  = NULL;
+    pCover->lCubes.pTail  = NULL;
+    pCover->nCubesAlloc   = 0;
+    pCover->pCubes        = NULL;
+    pCover->pMask         = NULL;
+    pCover->pLits         = NULL;
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverDup( Mvc_Cover_t * p )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    // clone the cover
+    pCover = Mvc_CoverClone( p );
+    // copy the cube list
+    Mvc_CoverForEachCube( p, pCube )
+    {
+        pCubeCopy = Mvc_CubeDup( p, pCube );
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverFree( Mvc_Cover_t * p )
+{
+    Mvc_Cube_t * pCube, * pCube2;
+    // recycle cube list
+    Mvc_CoverForEachCubeSafe( p, pCube, pCube2 )
+        Mvc_CubeFree( p, pCube );
+    // recycle other pointers
+    Mvc_CubeFree( p, p->pMask );
+    MEM_FREE( p->pMem, Mvc_Cube_t *, p->nCubesAlloc, p->pCubes );
+    MEM_FREE( p->pMem, int,          p->nBits,       p->pLits  );
+
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    free( p );
+#else
+    Extra_MmFixedEntryRecycle( p->pMem->pManC, (char *)p );
+#endif
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAllocateMask( Mvc_Cover_t * pCover ) 
+{ 
+    if ( pCover->pMask == NULL )
+        pCover->pMask = Mvc_CubeAlloc( pCover );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAllocateArrayLits( Mvc_Cover_t * pCover ) 
+{ 
+    if ( pCover->pLits == NULL )
+        pCover->pLits = MEM_ALLOC( pCover->pMem, int, pCover->nBits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAllocateArrayCubes( Mvc_Cover_t * pCover ) 
+{ 
+    if ( pCover->nCubesAlloc < pCover->lCubes.nItems )
+    {
+        if ( pCover->nCubesAlloc > 0 )
+            MEM_FREE( pCover->pMem, Mvc_Cube_t *, pCover->nCubesAlloc, pCover->pCubes );
+        pCover->nCubesAlloc = pCover->lCubes.nItems;
+        pCover->pCubes = MEM_ALLOC( pCover->pMem, Mvc_Cube_t *, pCover->nCubesAlloc );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDeallocateMask( Mvc_Cover_t * pCover ) 
+{ 
+    Mvc_CubeFree( pCover, pCover->pMask );
+    pCover->pMask = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDeallocateArrayLits( Mvc_Cover_t * pCover ) 
+{ 
+    if ( pCover->pLits )
+    {
+        MEM_FREE( pCover->pMem, int, pCover->nBits, pCover->pLits );
+        pCover->pLits = NULL;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcCube.c b/src/misc/mvc/mvcCube.c
new file mode 100644
index 00000000..d02fa270
--- /dev/null
+++ b/src/misc/mvc/mvcCube.c
@@ -0,0 +1,175 @@
+/**CFile****************************************************************
+
+  FileName    [mvcCube.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Manipulating unate cubes.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcCube.c,v 1.4 2003/04/03 06:31:49 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cube_t * Mvc_CubeAlloc( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+
+    assert( pCover->nWords >= 0 );
+    // allocate the cube
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    if ( pCover->nWords == 0 )
+        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) );
+    else
+        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
+#else
+    switch( pCover->nWords )
+    {
+    case 0:
+    case 1:
+        pCube = (Mvc_Cube_t *)Extra_MmFixedEntryFetch( pCover->pMem->pMan1 );
+        break;
+    case 2:
+        pCube = (Mvc_Cube_t *)Extra_MmFixedEntryFetch( pCover->pMem->pMan2 );
+        break;
+    case 3:
+    case 4:
+        pCube = (Mvc_Cube_t *)Extra_MmFixedEntryFetch( pCover->pMem->pMan4 );
+        break;
+    default:
+        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
+        break;
+    }
+#endif
+    // set the parameters charactering this cube
+    if ( pCover->nWords == 0 )
+        pCube->iLast   = pCover->nWords;
+    else
+        pCube->iLast   = pCover->nWords - 1;
+    pCube->nUnused = pCover->nUnused;
+    return pCube;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cube_t * Mvc_CubeDup( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    Mvc_Cube_t * pCubeCopy;
+    pCubeCopy = Mvc_CubeAlloc( pCover );
+    Mvc_CubeBitCopy( pCubeCopy, pCube );
+    return pCubeCopy;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    if ( pCube == NULL )
+        return;
+
+    // verify the parameters charactering this cube
+    assert( pCube->iLast == 0 || ((int)pCube->iLast) == pCover->nWords - 1 );
+    assert( ((int)pCube->nUnused) == pCover->nUnused );
+
+    // deallocate the cube
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    free( pCube );
+#else
+    switch( pCover->nWords )
+    {
+    case 0:
+    case 1:
+        Extra_MmFixedEntryRecycle( pCover->pMem->pMan1, (char *)pCube );
+        break;
+    case 2:
+        Extra_MmFixedEntryRecycle( pCover->pMem->pMan2, (char *)pCube );
+        break;
+    case 3:
+    case 4:
+        Extra_MmFixedEntryRecycle( pCover->pMem->pMan4, (char *)pCube );
+        break;
+    default:
+        free( pCube );
+        break;
+    }
+#endif
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the don't-care variable from the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CubeBitRemoveDcs( Mvc_Cube_t * pCube )
+{
+    unsigned Mask;
+    int i;
+    for ( i = Mvc_CubeReadLast(pCube); i >= 0; i-- )
+    {
+        // detect those variables that are different (not DCs)
+        Mask = (pCube->pData[i] ^ (pCube->pData[i] >> 1)) & BITS_DISJOINT; 
+        // create the mask of all that are different
+        Mask |= (Mask << 1);
+        // remove other bits from the set
+        pCube->pData[i] &= Mask;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcDivide.c b/src/misc/mvc/mvcDivide.c
new file mode 100644
index 00000000..6aa3d58d
--- /dev/null
+++ b/src/misc/mvc/mvcDivide.c
@@ -0,0 +1,436 @@
+/**CFile****************************************************************
+
+  FileName    [mvcDivide.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures for algebraic division.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcDivide.c,v 1.5 2003/04/26 20:41:36 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Mvc_CoverVerifyDivision( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t * pQuo, Mvc_Cover_t * pRem );
+
+int s_fVerbose = 0;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivide( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
+{
+    // check the number of cubes
+    if ( Mvc_CoverReadCubeNum( pCover ) < Mvc_CoverReadCubeNum( pDiv ) )
+    {
+        *ppQuo = NULL;
+        *ppRem = NULL;
+        return;
+    }
+
+    // make sure that support of pCover contains that of pDiv
+    if ( !Mvc_CoverCheckSuppContainment( pCover, pDiv ) )
+    {
+        *ppQuo = NULL;
+        *ppRem = NULL;
+        return;
+    }
+
+    // perform the general division
+    Mvc_CoverDivideInternal( pCover, pDiv, ppQuo, ppRem );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merge the cubes inside the groups.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideInternal( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
+{
+    Mvc_Cover_t * pQuo, * pRem;
+    Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
+    Mvc_Cube_t * pCube1, * pCube2;
+    int * pGroups, nGroups;    // the cube groups
+    int nCubesC, nCubesD, nMerges, iCubeC, iCubeD, iMerge;
+    int fSkipG, GroupSize, g, c, RetValue;
+    int nCubes;
+
+    // get cover sizes
+    nCubesD = Mvc_CoverReadCubeNum( pDiv );
+    nCubesC = Mvc_CoverReadCubeNum( pCover );
+
+    // check trivial cases
+    if ( nCubesD == 1 )
+    {
+        if ( Mvc_CoverIsOneLiteral( pDiv ) )
+            Mvc_CoverDivideByLiteral( pCover, pDiv, ppQuo, ppRem );
+        else
+            Mvc_CoverDivideByCube( pCover, pDiv, ppQuo, ppRem );
+        return;
+    }
+
+    // create the divisor and the remainder 
+    pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+    pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+
+    // get the support of the divisor
+    Mvc_CoverAllocateMask( pDiv );
+    Mvc_CoverSupport( pDiv, pDiv->pMask );
+
+    // sort the cubes of the divisor
+    Mvc_CoverSort( pDiv, NULL, Mvc_CubeCompareInt );
+    // sort the cubes of the cover
+    Mvc_CoverSort( pCover, pDiv->pMask, Mvc_CubeCompareIntOutsideAndUnderMask );
+
+    // allocate storage for cube groups
+    pGroups = MEM_ALLOC( pCover->pMem, int, nCubesC + 1 );
+
+    // mask contains variables in the support of Div
+    // split the cubes into groups using the mask
+    Mvc_CoverList2Array( pCover );
+    Mvc_CoverList2Array( pDiv );
+    pGroups[0] = 0;
+    nGroups    = 1;
+    for ( c = 1; c < nCubesC; c++ )
+    {
+        // get the cubes
+        pCube1 = pCover->pCubes[c-1];
+        pCube2 = pCover->pCubes[c  ];
+        // compare the cubes
+        Mvc_CubeBitEqualOutsideMask( RetValue, pCube1, pCube2, pDiv->pMask );
+        if ( !RetValue )
+            pGroups[nGroups++] = c;
+    }
+    // finish off the last group
+    pGroups[nGroups] = nCubesC;
+
+    // consider each group separately and decide
+    // whether it can produce a quotient cube
+    nCubes = 0;
+    for ( g = 0; g < nGroups; g++ )
+    {
+        // if the group has less than nCubesD cubes, 
+        // there is no way it can produce the quotient cube
+        // copy the cubes to the remainder
+        GroupSize = pGroups[g+1] - pGroups[g];
+        if ( GroupSize < nCubesD )
+        {
+            for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            {
+                pCubeCopy = Mvc_CubeDup( pRem, pCover->pCubes[c] );
+                Mvc_CoverAddCubeTail( pRem, pCubeCopy );
+                nCubes++;
+            }
+            continue;
+        }
+
+        // mark the cubes as those that should be added to the remainder
+        for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            Mvc_CubeSetSize( pCover->pCubes[c], 1 );
+
+        // go through the cubes in the group and at the same time
+        // go through the cubes in the divisor
+        iCubeD  = 0;
+        iCubeC  = 0;
+        pCubeD  = pDiv->pCubes[iCubeD++];
+        pCubeC  = pCover->pCubes[pGroups[g]+iCubeC++];
+        fSkipG  = 0;
+        nMerges = 0;
+
+        while ( 1 )
+        {
+            // compare the topmost cubes in F and in D
+            RetValue = Mvc_CubeCompareIntUnderMask( pCubeC, pCubeD, pDiv->pMask );
+            // cube are ordered in increasing order of their int value
+            if ( RetValue == -1 ) // pCubeC is above pCubeD
+            {  // cube in C should be added to the remainder
+                // check that there is enough cubes in the group
+                if ( GroupSize - iCubeC < nCubesD - nMerges )
+                {
+                    fSkipG = 1;
+                    break;
+                }
+                // get the next cube in the cover
+                pCubeC = pCover->pCubes[pGroups[g]+iCubeC++];
+                continue;
+            }
+            if ( RetValue == 1 ) // pCubeD is above pCubeC
+            { // given cube in D does not have a corresponding cube in the cover
+                fSkipG = 1;
+                break;
+            }
+            // mark the cube as the one that should NOT be added to the remainder
+            Mvc_CubeSetSize( pCubeC, 0 );
+            // remember this merged cube
+            iMerge = iCubeC-1;
+            nMerges++;
+
+            // stop if we considered the last cube of the group
+            if ( iCubeD == nCubesD )
+                break;
+
+            // advance the cube of the divisor
+            assert( iCubeD < nCubesD );
+            pCubeD = pDiv->pCubes[iCubeD++];
+
+            // advance the cube of the group
+            assert( pGroups[g]+iCubeC < nCubesC );
+            pCubeC = pCover->pCubes[pGroups[g]+iCubeC++];
+        }
+
+        if ( fSkipG )
+        { 
+            // the group has failed, add all the cubes to the remainder
+            for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+            {
+                pCubeCopy = Mvc_CubeDup( pRem, pCover->pCubes[c] );
+                Mvc_CoverAddCubeTail( pRem, pCubeCopy );
+                nCubes++;
+            }
+            continue;
+        }
+
+        // the group has worked, add left-over cubes to the remainder
+        for ( c = pGroups[g]; c < pGroups[g+1]; c++ )
+        {
+            pCubeC = pCover->pCubes[c];
+            if ( Mvc_CubeReadSize(pCubeC) )
+            {
+                pCubeCopy = Mvc_CubeDup( pRem, pCubeC );
+                Mvc_CoverAddCubeTail( pRem, pCubeCopy );
+                nCubes++;
+            }
+        }
+
+        // create the quotient cube
+        pCube1 = Mvc_CubeAlloc( pQuo );
+        Mvc_CubeBitSharp( pCube1, pCover->pCubes[pGroups[g]+iMerge], pDiv->pMask );
+        // add the cube to the quotient
+        Mvc_CoverAddCubeTail( pQuo, pCube1 );
+        nCubes += nCubesD;
+    }
+    assert( nCubes == nCubesC );
+
+    // deallocate the memory
+    MEM_FREE( pCover->pMem, int, nCubesC + 1, pGroups );
+
+    // return the results
+    *ppRem = pRem;
+    *ppQuo = pQuo;
+//    Mvc_CoverVerifyDivision( pCover, pDiv, pQuo, pRem );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Divides the cover by a cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByCube( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
+{
+    Mvc_Cover_t * pQuo, * pRem;
+    Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy;
+    int CompResult;
+
+    // get the only cube of D
+    assert( Mvc_CoverReadCubeNum(pDiv) == 1 );
+
+    // start the quotient and the remainder
+    pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+    pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+
+    // get the first and only cube of the divisor
+    pCubeD = Mvc_CoverReadCubeHead( pDiv );
+
+    // iterate through the cubes in the cover
+    Mvc_CoverForEachCube( pCover, pCubeC )
+    {
+        // check the containment of literals from pCubeD in pCube
+        Mvc_Cube2BitNotImpl( CompResult, pCubeD, pCubeC );
+        if ( !CompResult )
+        { // this cube belongs to the quotient
+            // alloc the cube
+            pCubeCopy = Mvc_CubeAlloc( pQuo );
+            // clean the support of D
+            Mvc_CubeBitSharp( pCubeCopy, pCubeC, pCubeD );
+            // add the cube to the quotient
+            Mvc_CoverAddCubeTail( pQuo, pCubeCopy );
+        }
+        else
+        { 
+            // copy the cube
+            pCubeCopy = Mvc_CubeDup( pRem, pCubeC );
+            // add the cube to the remainder
+            Mvc_CoverAddCubeTail( pRem, pCubeCopy );
+        }
+    }
+    // return the results
+    *ppRem = pRem;
+    *ppQuo = pQuo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divides the cover by a literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByLiteral( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t ** ppQuo, Mvc_Cover_t ** ppRem )
+{
+    Mvc_Cover_t * pQuo, * pRem;
+    Mvc_Cube_t * pCubeC, * pCubeCopy;
+    int iLit;
+
+    // get the only cube of D
+    assert( Mvc_CoverReadCubeNum(pDiv) == 1 );
+
+    // start the quotient and the remainder
+    pQuo = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+    pRem = Mvc_CoverAlloc( pCover->pMem, pCover->nBits );
+
+    // get the first and only literal in the divisor cube
+    iLit = Mvc_CoverFirstCubeFirstLit( pDiv );
+
+    // iterate through the cubes in the cover
+    Mvc_CoverForEachCube( pCover, pCubeC )
+    {
+        // copy the cube
+        pCubeCopy = Mvc_CubeDup( pCover, pCubeC );
+        // add the cube to the quotient or to the remainder depending on the literal
+        if ( Mvc_CubeBitValue( pCubeCopy, iLit ) )
+        {   // remove the literal
+            Mvc_CubeBitRemove( pCubeCopy, iLit );
+            // add the cube ot the quotient
+            Mvc_CoverAddCubeTail( pQuo, pCubeCopy );
+        }
+        else
+        {   // add the cube ot the remainder
+            Mvc_CoverAddCubeTail( pRem, pCubeCopy );
+        }
+    }
+    // return the results
+    *ppRem = pRem;
+    *ppQuo = pQuo;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the quotient of division by literal.]
+
+  Description [Reduces the cover to be the equal to the result of
+  division of the given cover by the literal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivideByLiteralQuo( Mvc_Cover_t * pCover, int iLit )
+{
+    Mvc_Cube_t * pCube, * pCube2, * pPrev;
+    // delete those cubes that do not have this literal
+    // remove this literal from other cubes
+    pPrev = NULL;
+    Mvc_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        if ( Mvc_CubeBitValue( pCube, iLit ) == 0 )
+        { // delete the cube from the cover
+            Mvc_CoverDeleteCube( pCover, pPrev, pCube );
+            Mvc_CubeFree( pCover, pCube );
+            // don't update the previous cube
+        }
+        else
+        { // delete this literal from the cube
+            Mvc_CubeBitRemove( pCube, iLit );
+            // update the previous cube
+            pPrev = pCube;
+        }
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the result of algebraic division is correct.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverVerifyDivision( Mvc_Cover_t * pCover, Mvc_Cover_t * pDiv, Mvc_Cover_t * pQuo, Mvc_Cover_t * pRem )
+{   
+    Mvc_Cover_t * pProd;
+    Mvc_Cover_t * pDiff;
+
+    pProd = Mvc_CoverAlgebraicMultiply( pDiv, pQuo );
+    pDiff = Mvc_CoverAlgebraicSubtract( pCover, pProd );
+
+    if ( Mvc_CoverAlgebraicEqual( pDiff, pRem ) )
+        printf( "Verification OKAY!\n" );
+    else
+    {
+        printf( "Verification FAILED!\n" );
+        printf( "pCover:\n" );
+        Mvc_CoverPrint( pCover );
+        printf( "pDiv:\n" );
+        Mvc_CoverPrint( pDiv );
+        printf( "pRem:\n" );
+        Mvc_CoverPrint( pRem );
+        printf( "pQuo:\n" );
+        Mvc_CoverPrint( pQuo );
+    }
+
+    Mvc_CoverFree( pProd );
+    Mvc_CoverFree( pDiff );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcDivisor.c b/src/misc/mvc/mvcDivisor.c
new file mode 100644
index 00000000..e92c3a65
--- /dev/null
+++ b/src/misc/mvc/mvcDivisor.c
@@ -0,0 +1,90 @@
+/**CFile****************************************************************
+
+  FileName    [mvcDivisor.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures for compute the quick divisor.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcDivisor.c,v 1.1 2003/04/03 15:34:08 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void  Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the quick divisor of the cover.]
+
+  Description [Returns NULL, if there is not divisor other than
+  trivial.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverDivisor( Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pKernel;
+    if ( Mvc_CoverReadCubeNum(pCover) <= 1 )
+        return NULL;
+    // allocate the literal array and count literals
+    if ( Mvc_CoverAnyLiteral( pCover, NULL ) == -1 )
+        return NULL;
+    // duplicate the cover
+    pKernel = Mvc_CoverDup(pCover);
+    // perform the kerneling
+    Mvc_CoverDivisorZeroKernel( pKernel );
+    assert( Mvc_CoverReadCubeNum(pKernel) );
+    return pKernel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a level-zero kernel.]
+
+  Description [Modifies the cover to contain one level-zero kernel.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover )
+{
+    int iLit;
+    // find any literal that occurs at least two times
+//    iLit = Mvc_CoverAnyLiteral( pCover, NULL );
+    iLit = Mvc_CoverWorstLiteral( pCover, NULL );
+//    iLit = Mvc_CoverBestLiteral( pCover, NULL );
+    if ( iLit == -1 )
+        return;
+    // derive the cube-free quotient
+    Mvc_CoverDivideByLiteralQuo( pCover, iLit ); // the same cover
+    Mvc_CoverMakeCubeFree( pCover );             // the same cover
+    // call recursively
+    Mvc_CoverDivisorZeroKernel( pCover );              // the same cover
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcList.c b/src/misc/mvc/mvcList.c
new file mode 100644
index 00000000..678ae9fd
--- /dev/null
+++ b/src/misc/mvc/mvcList.c
@@ -0,0 +1,362 @@
+/**CFile****************************************************************
+
+  FileName    [mvcList.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Manipulating list of cubes in the cover.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcList.c,v 1.4 2003/04/03 06:31:50 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_ListAddCubeHead_( Mvc_List_t * pList, Mvc_Cube_t * pCube )
+{
+    if ( pList->pHead == NULL )
+    {
+        Mvc_CubeSetNext( pCube, NULL );
+        pList->pHead = pCube;
+        pList->pTail = pCube;
+    }
+    else
+    {
+        Mvc_CubeSetNext( pCube, pList->pHead );
+        pList->pHead = pCube;
+    }
+    pList->nItems++;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_ListAddCubeTail_( Mvc_List_t * pList, Mvc_Cube_t * pCube )
+{
+    if ( pList->pHead == NULL )
+        pList->pHead = pCube;
+    else
+        Mvc_CubeSetNext( pList->pTail, pCube );
+    pList->pTail    = pCube;
+    Mvc_CubeSetNext( pCube, NULL );
+    pList->nItems++;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_ListDeleteCube_( Mvc_List_t * pList, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube )
+{
+    if ( pPrev == NULL ) // deleting the head cube
+        pList->pHead = Mvc_CubeReadNext(pCube);
+    else
+        pPrev->pNext = pCube->pNext;
+    if ( pList->pTail == pCube ) // deleting the tail cube
+    {
+        assert( Mvc_CubeReadNext(pCube) == NULL );
+        pList->pTail = pPrev;
+    }
+    pList->nItems--;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAddCubeHead_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    Mvc_List_t * pList = &pCover->lCubes;
+    if ( pList->pHead == NULL )
+    {
+        Mvc_CubeSetNext( pCube, NULL );
+        pList->pHead = pCube;
+        pList->pTail = pCube;
+    }
+    else
+    {
+        Mvc_CubeSetNext( pCube, pList->pHead );
+        pList->pHead = pCube;
+    }
+    pList->nItems++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAddCubeTail_( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    Mvc_List_t * pList = &pCover->lCubes;
+
+    if ( pList->pHead == NULL )
+        pList->pHead = pCube;
+    else
+        Mvc_CubeSetNext( pList->pTail, pCube );
+    pList->pTail    = pCube;
+    Mvc_CubeSetNext( pCube, NULL );
+    pList->nItems++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDeleteCube_( Mvc_Cover_t * pCover, Mvc_Cube_t * pPrev, Mvc_Cube_t * pCube )
+{
+    Mvc_List_t * pList = &pCover->lCubes;
+ 
+    if ( pPrev == NULL ) // deleting the head cube
+        pList->pHead = Mvc_CubeReadNext(pCube);
+    else
+        pPrev->pNext = pCube->pNext;
+    if ( pList->pTail == pCube ) // deleting the tail cube
+    {
+        assert( Mvc_CubeReadNext(pCube) == NULL );
+        pList->pTail = pPrev;
+    }
+    pList->nItems--;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAddDupCubeHead( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    Mvc_Cube_t * pCubeNew;
+    pCubeNew = Mvc_CubeAlloc( pCover );
+    Mvc_CubeBitCopy( pCubeNew, pCube );
+    Mvc_CoverAddCubeHead( pCover, pCubeNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAddDupCubeTail( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    Mvc_Cube_t * pCubeNew;
+    // copy the cube as part of this cover
+    pCubeNew = Mvc_CubeAlloc( pCover );
+    Mvc_CubeBitCopy( pCubeNew, pCube );
+    // clean the last bits of the new cube
+//    pCubeNew->pData[pCubeNew->iLast] &= (BITS_FULL >> pCubeNew->nUnused);
+    // add the cube at the end
+    Mvc_CoverAddCubeTail( pCover, pCubeNew );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverAddLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+//    int iBit, Value;
+//    assert( pCover->pLits );
+//    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+//        if ( Value )
+//            pCover->pLits[iBit] += Value;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverDeleteLiteralsOfCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+//    int iBit, Value;
+//    assert( pCover->pLits );
+//    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+//        if ( Value )
+//            pCover->pLits[iBit] -= Value;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the cubes from the list into the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverList2Array( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int Counter;
+    // resize storage if necessary
+    Mvc_CoverAllocateArrayCubes( pCover );
+    // iterate through the cubes
+    Counter = 0;
+    Mvc_CoverForEachCube( pCover, pCube )
+        pCover->pCubes[ Counter++ ] = pCube;
+    assert( Counter == Mvc_CoverReadCubeNum(pCover) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the cubes from the array into list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverArray2List( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int nCubes, i;
+
+    assert( pCover->pCubes );
+
+    nCubes = Mvc_CoverReadCubeNum(pCover);
+    if ( nCubes == 0 )
+        return;
+    if ( nCubes == 1 )
+    {
+        pCube    = pCover->pCubes[0];
+        pCube->pNext = NULL;
+        pCover->lCubes.pHead = pCover->lCubes.pTail = pCube;
+        return;
+    }
+    // set up the first cube
+    pCube = pCover->pCubes[0];
+    pCover->lCubes.pHead = pCube;
+    // set up the last cube
+    pCube = pCover->pCubes[nCubes-1];
+    pCube->pNext = NULL;
+    pCover->lCubes.pTail = pCube;
+
+    // link all cubes starting from the first one
+    for ( i = 0; i < nCubes - 1; i++ )
+        pCover->pCubes[i]->pNext = pCover->pCubes[i+1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the tail of the linked list given by the head.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cube_t * Mvc_ListGetTailFromHead( Mvc_Cube_t * pHead )
+{
+    Mvc_Cube_t * pCube, * pTail;
+    for ( pTail = pCube = pHead; 
+          pCube; 
+          pTail = pCube, pCube = Mvc_CubeReadNext(pCube) );
+    return pTail;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcLits.c b/src/misc/mvc/mvcLits.c
new file mode 100644
index 00000000..98211719
--- /dev/null
+++ b/src/misc/mvc/mvcLits.c
@@ -0,0 +1,345 @@
+/**CFile****************************************************************
+
+  FileName    [mvcLits.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Literal counting/updating procedures.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcLits.c,v 1.4 2003/04/03 06:31:50 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the any literal that occurs more than once.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverAnyLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask )
+{
+    Mvc_Cube_t * pCube;
+    int nWord, nBit, i;
+    int nLitsCur;
+    int fUseFirst = 0;
+
+    // go through each literal
+    if ( fUseFirst )
+    {
+        for ( i = 0; i < pCover->nBits; i++ )
+            if ( !pMask || Mvc_CubeBitValue(pMask,i) )
+            {
+                // get the word and bit of this literal
+                nWord = Mvc_CubeWhichWord(i);
+                nBit  = Mvc_CubeWhichBit(i);
+                // go through all the cubes
+                nLitsCur = 0;
+                Mvc_CoverForEachCube( pCover, pCube )
+                    if ( pCube->pData[nWord] & (1<<nBit) )
+                    {
+                        nLitsCur++;
+                        if ( nLitsCur > 1 )
+                            return i;
+                    }
+            }
+    }
+    else
+    {
+        for ( i = pCover->nBits - 1; i >=0; i-- )
+            if ( !pMask || Mvc_CubeBitValue(pMask,i) )
+            {
+                // get the word and bit of this literal
+                nWord = Mvc_CubeWhichWord(i);
+                nBit  = Mvc_CubeWhichBit(i);
+                // go through all the cubes
+                nLitsCur = 0;
+                Mvc_CoverForEachCube( pCover, pCube )
+                    if ( pCube->pData[nWord] & (1<<nBit) )
+                    {
+                        nLitsCur++;
+                        if ( nLitsCur > 1 )
+                            return i;
+                    }
+            }
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the most often occurring literal.]
+
+  Description [Find the most often occurring literal among those
+  that occur more than once.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverBestLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask )
+{
+    Mvc_Cube_t * pCube;
+    int nWord, nBit;
+    int i, iMax, nLitsMax, nLitsCur;
+    int fUseFirst = 1;
+
+    // go through each literal
+    iMax = -1;
+    nLitsMax = -1;
+    for ( i = 0; i < pCover->nBits; i++ )
+        if ( !pMask || Mvc_CubeBitValue(pMask,i) )
+        {
+            // get the word and bit of this literal
+            nWord = Mvc_CubeWhichWord(i);
+            nBit  = Mvc_CubeWhichBit(i);
+            // go through all the cubes
+            nLitsCur = 0;
+            Mvc_CoverForEachCube( pCover, pCube )
+                if ( pCube->pData[nWord] & (1<<nBit) )
+                    nLitsCur++;
+
+            // check if this is the best literal
+            if ( fUseFirst )
+            {
+                if ( nLitsMax < nLitsCur )
+                {
+                    nLitsMax = nLitsCur;
+                    iMax = i;
+                }
+            }
+            else
+            {
+                if ( nLitsMax <= nLitsCur )
+                {
+                    nLitsMax = nLitsCur;
+                    iMax = i;
+                }
+            }
+        }
+
+    if ( nLitsMax > 1 )
+        return iMax;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the most often occurring literal.]
+
+  Description [Find the most often occurring literal among those
+  that occur more than once.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverWorstLiteral( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask )
+{
+    Mvc_Cube_t * pCube;
+    int nWord, nBit;
+    int i, iMin, nLitsMin, nLitsCur;
+    int fUseFirst = 1;
+
+    // go through each literal
+    iMin = -1;
+    nLitsMin = 1000000;
+    for ( i = 0; i < pCover->nBits; i++ )
+        if ( !pMask || Mvc_CubeBitValue(pMask,i) )
+        {
+            // get the word and bit of this literal
+            nWord = Mvc_CubeWhichWord(i);
+            nBit  = Mvc_CubeWhichBit(i);
+            // go through all the cubes
+            nLitsCur = 0;
+            Mvc_CoverForEachCube( pCover, pCube )
+                if ( pCube->pData[nWord] & (1<<nBit) )
+                    nLitsCur++;
+
+            // skip the literal that does not occur or occurs once
+            if ( nLitsCur < 2 )
+                continue;
+
+            // check if this is the best literal
+            if ( fUseFirst )
+            {
+                if ( nLitsMin > nLitsCur )
+                {
+                    nLitsMin = nLitsCur;
+                    iMin = i;
+                }
+            }
+            else
+            {
+                if ( nLitsMin >= nLitsCur )
+                {
+                    nLitsMin = nLitsCur;
+                    iMin = i;
+                }
+            }
+        }
+
+    if ( nLitsMin < 1000000 )
+        return iMin;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverBestLiteralCover( Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
+{
+    Mvc_Cover_t * pCoverNew;
+    Mvc_Cube_t * pCubeNew;
+    Mvc_Cube_t * pCubeS;
+    int iLitBest;
+
+    // create the new cover
+    pCoverNew = Mvc_CoverClone( pCover );
+    // get the new cube
+    pCubeNew = Mvc_CubeAlloc( pCoverNew );
+    // clean the cube
+    Mvc_CubeBitClean( pCubeNew );
+
+    // get the first cube of pSimple
+    assert( Mvc_CoverReadCubeNum(pSimple) == 1 );
+    pCubeS = Mvc_CoverReadCubeHead( pSimple );
+    // find the best literal among those of pCubeS
+    iLitBest = Mvc_CoverBestLiteral( pCover, pCubeS );
+
+    // insert this literal into the cube
+    Mvc_CubeBitInsert( pCubeNew, iLitBest );
+    // add the cube to the cover
+    Mvc_CoverAddCubeTail( pCoverNew, pCubeNew );
+    return pCoverNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverFirstCubeFirstLit( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int iBit, Value;
+
+    // get the first cube
+    pCube = Mvc_CoverReadCubeHead( pCover );
+    // get the first literal
+    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+        if ( Value )
+            return iBit;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of literals in the cover.]
+
+  Description [Allocates storage for literal counters and fills it up
+  using the current information.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverCountLiterals( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int nWord, nBit;
+    int i, CounterTot, CounterCur;
+
+    // allocate/clean the storage for literals
+//    Mvc_CoverAllocateArrayLits( pCover );
+//    memset( pCover->pLits, 0, pCover->nBits * sizeof(int) );
+    // go through each literal
+    CounterTot = 0;
+    for ( i = 0; i < pCover->nBits; i++ )
+    {
+        // get the word and bit of this literal
+        nWord = Mvc_CubeWhichWord(i);
+        nBit  = Mvc_CubeWhichBit(i);
+        // go through all the cubes
+        CounterCur = 0;
+        Mvc_CoverForEachCube( pCover, pCube )
+            if ( pCube->pData[nWord] & (1<<nBit) )
+                CounterCur++;
+        CounterTot += CounterCur;
+    }
+    return CounterTot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of literals in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverIsOneLiteral( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int iBit, Counter, Value;
+    if ( Mvc_CoverReadCubeNum(pCover) != 1 )
+        return 0;
+    pCube = Mvc_CoverReadCubeHead(pCover);
+    // count literals
+    Counter = 0;
+    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+    {
+        if ( Value )
+        {
+            if ( Counter++ )
+                return 0;
+        }
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcMan.c b/src/misc/mvc/mvcMan.c
new file mode 100644
index 00000000..f2943e0c
--- /dev/null
+++ b/src/misc/mvc/mvcMan.c
@@ -0,0 +1,77 @@
+/**CFile****************************************************************
+
+  FileName    [mvcMan.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures working with the MVC memory manager.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcMan.c,v 1.3 2003/03/19 19:50:26 alanmi Exp $]
+
+***********************************************************************/
+
+#include <string.h>
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Manager_t * Mvc_ManagerStart()
+{
+    Mvc_Manager_t * p;
+    p = ALLOC( Mvc_Manager_t, 1 );
+    memset( p, 0, sizeof(Mvc_Manager_t) );
+    p->pMan1 = Extra_MmFixedStart( sizeof(Mvc_Cube_t)                              );
+    p->pMan2 = Extra_MmFixedStart( sizeof(Mvc_Cube_t) +     sizeof(Mvc_CubeWord_t) );
+    p->pMan4 = Extra_MmFixedStart( sizeof(Mvc_Cube_t) + 3 * sizeof(Mvc_CubeWord_t) );
+    p->pManC = Extra_MmFixedStart( sizeof(Mvc_Cover_t) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_ManagerFree( Mvc_Manager_t * p )
+{
+    Extra_MmFixedStop( p->pMan1, 0 );
+    Extra_MmFixedStop( p->pMan2, 0 );
+    Extra_MmFixedStop( p->pMan4, 0 );
+    Extra_MmFixedStop( p->pManC, 0 );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcOpAlg.c b/src/misc/mvc/mvcOpAlg.c
new file mode 100644
index 00000000..befccb70
--- /dev/null
+++ b/src/misc/mvc/mvcOpAlg.c
@@ -0,0 +1,163 @@
+/**CFile****************************************************************
+
+  FileName    [mvcOperAlg.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Miscellaneous operations on covers.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcOpAlg.c,v 1.4 2003/04/26 20:41:36 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Multiplies two disjoint-support covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverAlgebraicMultiply( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube1, * pCube2, * pCube;
+    int CompResult;
+
+    // covers should be the same base
+    assert( pCover1->nBits == pCover2->nBits );
+    // make sure that supports do not overlap
+    Mvc_CoverAllocateMask( pCover1 );
+    Mvc_CoverAllocateMask( pCover2 );
+    Mvc_CoverSupport( pCover1, pCover1->pMask );
+    Mvc_CoverSupport( pCover2, pCover2->pMask );
+    // check if the cubes are bit-wise disjoint
+    Mvc_CubeBitDisjoint( CompResult, pCover1->pMask, pCover2->pMask );
+    if ( !CompResult )
+        printf( "Mvc_CoverMultiply(): Cover supports are not disjoint!\n" );
+
+    // iterate through the cubes
+    pCover = Mvc_CoverClone( pCover1 );
+    Mvc_CoverForEachCube( pCover1, pCube1 )
+        Mvc_CoverForEachCube( pCover2, pCube2 )
+        { 
+            // create the product cube
+            pCube = Mvc_CubeAlloc( pCover );
+            // set the product cube equal to the product of the two cubes
+            Mvc_CubeBitOr( pCube, pCube1, pCube2 );
+            // add the cube to the cover
+            Mvc_CoverAddCubeTail( pCover, pCube );
+        }
+    return pCover;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Subtracts the second cover from the first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverAlgebraicSubtract( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube1, * pCube2, * pCube;
+    int fFound;
+    int CompResult;
+
+    // covers should be the same base
+    assert( pCover1->nBits == pCover2->nBits );
+
+    // iterate through the cubes
+    pCover = Mvc_CoverClone( pCover1 );
+    Mvc_CoverForEachCube( pCover1, pCube1 )
+    {
+        fFound = 0;
+        Mvc_CoverForEachCube( pCover2, pCube2 )
+        {
+            Mvc_CubeBitEqual( CompResult, pCube1, pCube2 );
+            if ( CompResult )
+            {
+                fFound = 1;
+                break;
+            }
+        }
+        if ( !fFound )
+        { 
+            // create the copy of the cube
+            pCube = Mvc_CubeDup( pCover, pCube1 );
+            // add the cube copy to the cover
+            Mvc_CoverAddCubeTail( pCover, pCube );
+        }
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverAlgebraicEqual( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cube_t * pCube1, * pCube2;
+    int fFound;
+    int CompResult;
+
+    // covers should be the same base
+    assert( pCover1->nBits == pCover2->nBits );
+    // iterate through the cubes
+    Mvc_CoverForEachCube( pCover1, pCube1 )
+    {
+        fFound = 0;
+        Mvc_CoverForEachCube( pCover2, pCube2 )
+        {
+            Mvc_CubeBitEqual( CompResult, pCube1, pCube2 );
+            if ( CompResult )
+            {
+                fFound = 1;
+                break;
+            }
+        }
+        if ( !fFound )
+            return 0;
+    }
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcOpBool.c b/src/misc/mvc/mvcOpBool.c
new file mode 100644
index 00000000..57b1a968
--- /dev/null
+++ b/src/misc/mvc/mvcOpBool.c
@@ -0,0 +1,151 @@
+/**CFile****************************************************************
+
+  FileName    [mvcProc.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Various boolean procedures working with covers.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcOpBool.c,v 1.4 2003/04/16 01:55:37 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverBooleanOr( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    // make sure the covers are compatible
+    assert( pCover1->nBits == pCover2->nBits );
+    // clone the cover
+    pCover = Mvc_CoverClone( pCover1 );
+    // create the cubes by making pair-wise products
+    // of cubes in pCover1 and pCover2
+    Mvc_CoverForEachCube( pCover1, pCube )
+    {
+        pCubeCopy = Mvc_CubeDup( pCover, pCube );
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+    }
+    Mvc_CoverForEachCube( pCover2, pCube )
+    {
+        pCubeCopy = Mvc_CubeDup( pCover, pCube );
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+    }
+    return pCover;
+}
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverBooleanAnd( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube1, * pCube2, * pCubeCopy;
+    // make sure the covers are compatible
+    assert( pCover1->nBits == pCover2->nBits );
+    // clone the cover
+    pCover = Mvc_CoverClone( pCover1 );
+    // create the cubes by making pair-wise products
+    // of cubes in pCover1 and pCover2
+    Mvc_CoverForEachCube( pCover1, pCube1 )
+    {
+        Mvc_CoverForEachCube( pCover2, pCube2 )
+        {
+            if ( Mvc_CoverDist0Cubes( p, pCube1, pCube2 ) )
+            {
+                pCubeCopy = Mvc_CubeAlloc( pCover );
+                Mvc_CubeBitAnd( pCubeCopy, pCube1, pCube2 );
+                Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+            }
+        }
+        // if the number of cubes in the new cover is too large
+        // try compressing them
+        if ( Mvc_CoverReadCubeNum( pCover ) > 500 )
+            Mvc_CoverContain( pCover );
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the two covers are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    Mvc_Cover_t * pSharp;
+
+    pSharp = Mvc_CoverSharp( p, pCover1, pCover2 );
+    if ( Mvc_CoverReadCubeNum( pSharp ) )
+    {
+Mvc_CoverContain( pSharp );
+printf( "Sharp \n" );
+Mvc_CoverPrint( pSharp );
+        Mvc_CoverFree( pSharp );
+        return 0;
+    }
+    Mvc_CoverFree( pSharp );
+
+    pSharp = Mvc_CoverSharp( p, pCover2, pCover1 );
+    if ( Mvc_CoverReadCubeNum( pSharp ) )
+    {
+Mvc_CoverContain( pSharp );
+printf( "Sharp \n" );
+Mvc_CoverPrint( pSharp );
+        Mvc_CoverFree( pSharp );
+        return 0;
+    }
+    Mvc_CoverFree( pSharp );
+
+    return 1;
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcPrint.c b/src/misc/mvc/mvcPrint.c
new file mode 100644
index 00000000..3a31235b
--- /dev/null
+++ b/src/misc/mvc/mvcPrint.c
@@ -0,0 +1,220 @@
+/**CFile****************************************************************
+
+  FileName    [mvcPrint.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Printing cubes and covers.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcPrint.c,v 1.6 2003/04/09 18:02:06 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+//#include "vm.h"
+//#include "vmInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Mvc_CubePrintBinary( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverPrint( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int i;
+    // print general statistics
+    printf( "The cover contains %d cubes (%d bits and %d words)\n", 
+        pCover->lCubes.nItems, pCover->nBits, pCover->nWords );
+    // iterate through the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubePrint( pCover, pCube );
+
+    if ( pCover->pLits )
+    {
+        for ( i = 0; i < pCover->nBits; i++ )
+            printf( " %d", pCover->pLits[i] );
+        printf( "\n" ); 
+    }
+    printf( "End of cover printout\n" ); 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CubePrint( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    int iBit, Value;
+    // iterate through the literals
+//    printf( "Size = %2d   ", Mvc_CubeReadSize(pCube) );
+    Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+        printf( "%c", '0' + Value );
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverPrintBinary( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int i;
+    // print general statistics
+    printf( "The cover contains %d cubes (%d bits and %d words)\n", 
+        pCover->lCubes.nItems, pCover->nBits, pCover->nWords );
+    // iterate through the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubePrintBinary( pCover, pCube );
+
+    if ( pCover->pLits )
+    {
+        for ( i = 0; i < pCover->nBits; i++ )
+            printf( " %d", pCover->pLits[i] );
+        printf( "\n" ); 
+    }
+    printf( "End of cover printout\n" ); 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CubePrintBinary( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    int iVar, Value;
+    // iterate through the literals
+//    printf( "Size = %2d   ", Mvc_CubeReadSize(pCube) );
+    Mvc_CubeForEachVarValue( pCover, pCube, iVar, Value )
+    {
+        assert( Value != 0 );
+        if ( Value == 3 )
+            printf( "-" );
+        else if ( Value == 1 )
+            printf( "0" );
+        else 
+            printf( "1" );
+    }
+    printf( "\n" );
+}
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverPrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    int i;
+    // print general statistics
+    printf( "The cover contains %d cubes (%d bits and %d words)\n", 
+        pCover->lCubes.nItems, pCover->nBits, pCover->nWords );
+    // iterate through the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubePrintMv( pData, pCover, pCube );
+
+    if ( pCover->pLits )
+    {
+        for ( i = 0; i < pCover->nBits; i++ )
+            printf( " %d", pCover->pLits[i] );
+        printf( "\n" ); 
+    }
+    printf( "End of cover printout\n" ); 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CubePrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
+{
+    int iLit, iVar;
+    // iterate through the literals
+    printf( "Size = %2d   ", Mvc_CubeReadSize(pCube) );
+    iVar = 0;
+    for ( iLit = 0; iLit < pData->pVm->nValuesIn; iLit++ )
+    {
+        if ( iLit == pData->pVm->pValuesFirst[iVar+1] )
+        {
+            printf( " " );
+            iVar++;
+        }
+        if ( Mvc_CubeBitValue( pCube, iLit ) )
+            printf( "%c", '0' + iLit - pData->pVm->pValuesFirst[iVar] );
+        else
+            printf( "-" );
+    }
+    printf( "\n" );
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcSort.c b/src/misc/mvc/mvcSort.c
new file mode 100644
index 00000000..1126b22a
--- /dev/null
+++ b/src/misc/mvc/mvcSort.c
@@ -0,0 +1,141 @@
+/**CFile****************************************************************
+
+  FileName    [mvcSort.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Sorting cubes in the cover with the mask.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [uC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcSort.c,v 1.5 2003/04/27 01:03:45 wjiang Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+Mvc_Cube_t * Mvc_CoverSort_rec( Mvc_Cube_t * pList, int nItems, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) );
+Mvc_Cube_t * Mvc_CoverSortMerge( Mvc_Cube_t * pList1, Mvc_Cube_t * pList2, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) );
+
+////////////////////////////////////////////////////////////////////////
+///                     FuNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts cubes using the given cost function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverSort( Mvc_Cover_t * pCover, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) )
+{
+    Mvc_Cube_t * pHead;
+    int nCubes;
+    // one cube does not need sorting
+    nCubes = Mvc_CoverReadCubeNum(pCover);
+    if ( nCubes <= 1 )
+        return;
+    // sort the cubes 
+    pHead = Mvc_CoverSort_rec( Mvc_CoverReadCubeHead(pCover), nCubes, pMask, pCompareFunc ); 
+    // insert the sorted list into the cover
+    Mvc_CoverSetCubeHead( pCover, pHead );
+    Mvc_CoverSetCubeTail( pCover, Mvc_ListGetTailFromHead(pHead) );
+    // make sure that the list is sorted in the increasing order
+    assert( pCompareFunc( Mvc_CoverReadCubeHead(pCover), Mvc_CoverReadCubeTail(pCover), pMask ) <= 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursive part of Mvc_CoverSort()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cube_t * Mvc_CoverSort_rec( Mvc_Cube_t * pList, int nItems, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) )
+{
+    Mvc_Cube_t * pList1, * pList2;
+    int nItems1, nItems2, i;
+
+    // trivial case
+    if ( nItems == 1 )
+    {
+        Mvc_CubeSetNext( pList, NULL );
+        return pList;
+    }
+
+    // select the new sizes
+    nItems1 = nItems/2;
+    nItems2 = nItems - nItems1;
+
+    // set the new beginnings
+    pList1 = pList2 = pList;
+    for ( i = 0; i < nItems1; i++ )
+        pList2 = Mvc_CubeReadNext( pList2 );
+
+    // solve recursively
+    pList1 = Mvc_CoverSort_rec( pList1, nItems1, pMask, pCompareFunc );
+    pList2 = Mvc_CoverSort_rec( pList2, nItems2, pMask, pCompareFunc );
+
+    // merge
+    return Mvc_CoverSortMerge( pList1, pList2, pMask, pCompareFunc );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two NULL-terminated linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cube_t * Mvc_CoverSortMerge( Mvc_Cube_t * pList1, Mvc_Cube_t * pList2, Mvc_Cube_t * pMask, int (* pCompareFunc)(Mvc_Cube_t *, Mvc_Cube_t *, Mvc_Cube_t *) )
+{
+    Mvc_Cube_t * pList = NULL, ** ppTail = &pList;
+    Mvc_Cube_t * pCube;
+    while ( pList1 && pList2 )
+    {
+        if ( pCompareFunc( pList1, pList2, pMask ) < 0 )
+        {
+            pCube = pList1;
+            pList1 = Mvc_CubeReadNext(pList1);
+        }
+        else
+        {
+            pCube = pList2;
+            pList2 = Mvc_CubeReadNext(pList2);
+        }
+        *ppTail = pCube;
+        ppTail = Mvc_CubeReadNextP(pCube);
+    }
+    *ppTail = pList1? pList1: pList2;
+    return pList;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c
new file mode 100644
index 00000000..3fb57276
--- /dev/null
+++ b/src/misc/mvc/mvcUtils.c
@@ -0,0 +1,868 @@
+/**CFile****************************************************************
+
+  FileName    [mvcUtils.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Various cover handling utilities.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: mvcUtils.c,v 1.7 2003/04/26 20:41:36 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mvc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int bit_count[256] = {
+  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+
+
+static void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, int iColOld, int iColNew );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp )
+{
+    Mvc_Cube_t * pCube;
+    // clean the support
+    Mvc_CubeBitClean( pSupp );
+    // collect the support
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubeBitOr( pSupp, pSupp, pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverSupportAnd( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp )
+{
+    Mvc_Cube_t * pCube;
+    // clean the support
+    Mvc_CubeBitFill( pSupp );
+    // collect the support
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubeBitAnd( pSupp, pSupp, pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverSupportSizeBinary( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pSupp;
+    int Counter, i, v0, v1;
+    // compute the support
+    pSupp = Mvc_CubeAlloc( pCover );
+    Mvc_CoverSupportAnd( pCover, pSupp );
+    Counter = pCover->nBits/2;
+    for ( i = 0; i < pCover->nBits/2; i++ )
+    {
+        v0 = Mvc_CubeBitValue( pSupp, 2*i   );
+        v1 = Mvc_CubeBitValue( pSupp, 2*i+1 );
+        if ( v0 && v1 )
+            Counter--;
+    }
+    Mvc_CubeFree( pCover, pSupp );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverSupportVarBelongs( Mvc_Cover_t * pCover, int iVar )
+{
+    Mvc_Cube_t * pSupp;
+    int RetValue, v0, v1;
+    // compute the support
+    pSupp = Mvc_CubeAlloc( pCover );
+    Mvc_CoverSupportAnd( pCover, pSupp );
+    v0 = Mvc_CubeBitValue( pSupp, 2*iVar   );
+    v1 = Mvc_CubeBitValue( pSupp, 2*iVar+1 );
+    RetValue = (int)( !v0 || !v1 );
+    Mvc_CubeFree( pCover, pSupp );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube )
+{
+    Mvc_Cube_t * pCube;
+    // clean the support
+    Mvc_CubeBitFill( pComCube );
+    // collect the support
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubeBitAnd( pComCube, pComCube, pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover )
+{
+    int Result;
+    // get the common cube
+    Mvc_CoverAllocateMask( pCover );
+    Mvc_CoverCommonCube( pCover, pCover->pMask );
+    // check whether the common cube is empty
+    Mvc_CubeBitEmpty( Result, pCover->pMask );
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    // get the common cube
+    Mvc_CoverAllocateMask( pCover );
+    Mvc_CoverCommonCube( pCover, pCover->pMask );
+    // remove this cube from the cubes in the cover
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubeBitSharp( pCube, pCube, pCover->pMask );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverCommonCubeCover( Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pRes;
+    Mvc_Cube_t * pCube;
+    // create the new cover
+    pRes = Mvc_CoverClone( pCover );
+    // get the new cube
+    pCube = Mvc_CubeAlloc( pRes );
+    // get the common cube
+    Mvc_CoverCommonCube( pCover, pCube );
+    // add the cube to the cover
+    Mvc_CoverAddCubeTail( pRes, pCube );
+    return pRes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the support of cover2 is contained in the support of cover1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 )
+{
+    int Result;
+    assert( pCover1->nBits == pCover2->nBits );
+    // set the supports
+    Mvc_CoverAllocateMask( pCover1 );
+    Mvc_CoverSupport( pCover1, pCover1->pMask );
+    Mvc_CoverAllocateMask( pCover2 );
+    Mvc_CoverSupport( pCover2, pCover2->pMask );
+    // check the containment
+    Mvc_CubeBitNotImpl( Result, pCover2->pMask, pCover1->pMask );
+    return !Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the cube sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    unsigned char * pByte, * pByteStart, * pByteStop;
+    int nBytes, nOnes;
+
+    // get the number of unsigned chars in the cube's bit strings
+    nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0);
+    // iterate through the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        // clean the counter of ones
+        nOnes = 0;
+        // set the starting and stopping positions
+        pByteStart = (unsigned char *)pCube->pData;
+        pByteStop  = pByteStart + nBytes;
+        // iterate through the positions
+        for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
+            nOnes += bit_count[*pByte];
+        // set the nOnes
+        Mvc_CubeSetSize( pCube, nOnes );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the cube sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube )
+{
+    unsigned char * pByte, * pByteStart, * pByteStop;
+    int nOnes, nBytes, nBits;
+    // get the number of unsigned chars in the cube's bit strings
+    nBits = (pCube->iLast + 1) * sizeof(Mvc_CubeWord_t) * 8 - pCube->nUnused;
+    nBytes = nBits / (8 * sizeof(unsigned char)) + (int)(nBits % (8 * sizeof(unsigned char)) > 0);
+    // clean the counter of ones
+    nOnes = 0;
+    // set the starting and stopping positions
+    pByteStart = (unsigned char *)pCube->pData;
+    pByteStop  = pByteStart + nBytes;
+    // iterate through the positions
+    for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
+        nOnes += bit_count[*pByte];
+    return nOnes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the differences in each cube pair in the cover.]
+
+  Description [Takes the cover (pCover) and the array where the
+  diff counters go (pDiffs). The array pDiffs should have as many
+  entries as there are different pairs of cubes in the cover: n(n-1)/2.
+  Fills out the array pDiffs with the following info: For each cube
+  pair, included in the array is the number of literals in both cubes
+  after they are made cube free.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] )
+{
+    Mvc_Cube_t * pCube1;
+    Mvc_Cube_t * pCube2;
+    Mvc_Cube_t * pMask;
+    unsigned char * pByte, * pByteStart, * pByteStop;
+    int nBytes, nOnes;
+    int nCubePairs;
+
+    // allocate a temporary mask
+    pMask = Mvc_CubeAlloc( pCover );
+    // get the number of unsigned chars in the cube's bit strings
+    nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0);
+    // iterate through the cubes
+    nCubePairs = 0;
+    Mvc_CoverForEachCube( pCover, pCube1 )
+    {
+        Mvc_CoverForEachCubeStart( Mvc_CubeReadNext(pCube1), pCube2 )
+        {
+            // find the bit-wise exor of cubes
+            Mvc_CubeBitExor( pMask, pCube1, pCube2 );
+            // set the starting and stopping positions
+            pByteStart = (unsigned char *)pMask->pData;
+            pByteStop  = pByteStart + nBytes;
+            // clean the counter of ones
+            nOnes = 0;
+            // iterate through the positions
+            for ( pByte = pByteStart; pByte < pByteStop; pByte++ )
+                nOnes += bit_count[*pByte];
+            // set the nOnes
+            pDiffs[nCubePairs++] = nOnes;
+        }
+    }
+    // deallocate the mask
+    Mvc_CubeFree( pCover, pMask );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new cover containing some literals of the old cover.]
+
+  Description [Creates the new cover containing the given number (nVarsRem)
+  literals of the old cover. All the bits of the new cover are initialized
+  to "1". The selected bits from the old cover are copied on top. The numbers
+  of the selected bits to copy are given in the array pVarsRem. The i-set
+  entry in this array is the index of the bit in the old cover which goes
+  to the i-th place in the new cover. If the i-th entry in pVarsRem is -1, 
+  it means that the i-th bit does not change (remains composed of all 1's).
+  This is a useful feature to speed up remapping covers, which are known
+  to depend only on a subset of input variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverRemap( Mvc_Cover_t * p, int * pVarsRem, int nVarsRem )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    int i;
+    // clone the cover
+    pCover = Mvc_CoverAlloc( p->pMem, nVarsRem );
+    // copy the cube list
+    Mvc_CoverForEachCube( p, pCube )
+    {
+        pCubeCopy = Mvc_CubeAlloc( pCover );
+        //Mvc_CubeBitClean( pCubeCopy );   //changed by wjiang
+        Mvc_CubeBitFill( pCubeCopy );      //changed by wjiang
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+    }
+    // copy the corresponding columns
+    for ( i = 0; i < nVarsRem; i++ )
+    {
+        if (pVarsRem[i] < 0) 
+            continue;     //added by wjiang
+        assert( pVarsRem[i] >= 0 && pVarsRem[i] < p->nBits );
+        Mvc_CoverCopyColumn( p, pCover, pVarsRem[i], i );
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copies a column from the old cover to the new cover.]
+
+  Description [Copies the column (iColOld) of the old cover (pCoverOld)
+  into the column (iColNew) of the new cover (pCoverNew). Assumes that 
+  the number of cubes is the same in both covers. Makes no assuptions 
+  about the current contents of the column in the new cover.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, 
+                         int iColOld, int iColNew )
+{
+    Mvc_Cube_t * pCubeOld, * pCubeNew;
+    int iWordOld, iWordNew, iBitOld, iBitNew;
+
+    assert( Mvc_CoverReadCubeNum(pCoverOld) == Mvc_CoverReadCubeNum(pCoverNew) );
+
+    // get the place of the old and new columns
+    iWordOld = Mvc_CubeWhichWord(iColOld);
+    iBitOld  = Mvc_CubeWhichBit(iColOld);
+    iWordNew = Mvc_CubeWhichWord(iColNew);
+    iBitNew  = Mvc_CubeWhichBit(iColNew);
+
+    // go through the cubes of both covers
+    pCubeNew = Mvc_CoverReadCubeHead(pCoverNew);
+    Mvc_CoverForEachCube( pCoverOld, pCubeOld )
+    {
+        if ( pCubeOld->pData[iWordOld] & (1<<iBitOld) )
+            pCubeNew->pData[iWordNew] |= (1<<iBitNew);
+        else
+            pCubeNew->pData[iWordNew] &= ~(1<<iBitNew);  // added by wjiang
+        pCubeNew = Mvc_CubeReadNext( pCubeNew );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mvc_CoverInverse( Mvc_Cover_t * pCover )
+{
+    Mvc_Cube_t * pCube;
+    // complement the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+        Mvc_CubeBitNot( pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This function dups the cover and removes DC literals from cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverRemoveDontCareLits( Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pCoverNew;
+    Mvc_Cube_t * pCube;
+
+    pCoverNew = Mvc_CoverDup( pCover );
+    Mvc_CoverForEachCube( pCoverNew, pCube )
+        Mvc_CubeBitRemoveDcs( pCube );
+    return pCoverNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cofactor w.r.t. to a binary var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverCofactor( Mvc_Cover_t * p, int iValue, int iValueOther )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    // clone the cover
+    pCover = Mvc_CoverClone( p );
+    // copy the cube list
+    Mvc_CoverForEachCube( p, pCube )
+        if ( Mvc_CubeBitValue( pCube, iValue ) )
+        {
+            pCubeCopy = Mvc_CubeDup( pCover, pCube );
+            Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+            Mvc_CubeBitInsert( pCubeCopy, iValueOther );
+        }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cover, in which the binary var is complemented.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverFlipVar( Mvc_Cover_t * p, int iValue0, int iValue1 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    int Value0, Value1, Temp;
+
+    assert( iValue0 + 1 == iValue1 ); // should be adjacent
+
+    // clone the cover
+    pCover = Mvc_CoverClone( p );
+    // copy the cube list
+    Mvc_CoverForEachCube( p, pCube )
+    {
+        pCubeCopy = Mvc_CubeDup( pCover, pCube );
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+
+        // get the bits
+        Value0 = Mvc_CubeBitValue( pCubeCopy, iValue0 );
+        Value1 = Mvc_CubeBitValue( pCubeCopy, iValue1 );
+
+        // if both bits are one, nothing to swap
+        if ( Value0 && Value1 )
+            continue;
+        // cannot be both zero because they belong to the same var
+        assert( Value0 || Value1 ); 
+
+        // swap the bits
+        Temp   = Value0;
+        Value0 = Value1;
+        Value1 = Temp;
+
+        // set the bits after the swap
+        if ( Value0 )
+            Mvc_CubeBitInsert( pCubeCopy, iValue0 );
+        else
+            Mvc_CubeBitRemove( pCubeCopy, iValue0 );
+
+        if ( Value1 )
+            Mvc_CubeBitInsert( pCubeCopy, iValue1 );
+        else
+            Mvc_CubeBitRemove( pCubeCopy, iValue1 );
+    }
+    return pCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cover derived by universal quantification.]
+
+  Description [Returns the cover computed by universal quantification
+  as follows: CoverNew = Univ(B) [Cover & (A==B)]. Removes the second 
+  binary var from the support (given by values iValueB0 and iValueB1). 
+  Leaves the first binary variable (given by values iValueA0 and iValueA1) 
+  in the support.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverUnivQuantify( Mvc_Cover_t * p, 
+    int iValueA0, int iValueA1, int iValueB0, int iValueB1 )
+{
+    Mvc_Cover_t * pCover;
+    Mvc_Cube_t * pCube, * pCubeCopy;
+    int ValueA0, ValueA1, ValueB0, ValueB1;
+
+    // clone the cover
+    pCover = Mvc_CoverClone( p );
+    // copy the cube list
+    Mvc_CoverForEachCube( p, pCube )
+    {
+        // get the bits
+        ValueA0 = Mvc_CubeBitValue( pCube, iValueA0 );
+        ValueA1 = Mvc_CubeBitValue( pCube, iValueA1 );
+        ValueB0 = Mvc_CubeBitValue( pCube, iValueB0 );
+        ValueB1 = Mvc_CubeBitValue( pCube, iValueB1 );
+
+        // cannot be both zero because they belong to the same var
+        assert( ValueA0 || ValueA1 ); 
+        assert( ValueB0 || ValueB1 ); 
+
+        // if the values of this var are different, do not add the cube
+        if ( ValueA0 != ValueB0 && ValueA1 != ValueB1 )
+            continue;
+
+        // create the cube
+        pCubeCopy = Mvc_CubeDup( pCover, pCube );
+        Mvc_CoverAddCubeTail( pCover, pCubeCopy );
+
+        // insert 1's into for the first var, if both have this value
+        if ( ValueA0 && ValueB0 )
+            Mvc_CubeBitInsert( pCubeCopy, iValueA0 );
+        else
+            Mvc_CubeBitRemove( pCubeCopy, iValueA0 );
+
+        if ( ValueA1 && ValueB1 )
+            Mvc_CubeBitInsert( pCubeCopy, iValueA1 );
+        else
+            Mvc_CubeBitRemove( pCubeCopy, iValueA1 );
+            
+        // insert 1's into for the second var (the cover does not depend on it)
+        Mvc_CubeBitInsert( pCubeCopy, iValueB0 );
+        Mvc_CubeBitInsert( pCubeCopy, iValueB1 );
+    }
+    return pCover;
+}
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cofactors of the cover.]
+
+  Description [Derives the cofactors w.r.t. a variable and also cubes
+  that do not depend on this variable.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar )
+{
+    Mvc_Cover_t ** ppCofs;
+    Mvc_Cube_t * pCube, * pCubeNew;
+    int i, nValues, iValueFirst, Res;
+
+    // start the covers for cofactors
+    iValueFirst = Vm_VarMapReadValuesFirst(pData->pVm, iVar);
+    nValues = Vm_VarMapReadValues(pData->pVm, iVar);
+    ppCofs = ALLOC( Mvc_Cover_t *, nValues + 1 );
+    for ( i = 0; i <= nValues; i++ )
+        ppCofs[i] = Mvc_CoverClone( pCover );
+
+    // go through the cubes
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        // if the literal if a full literal, add it to last "cofactor"
+        Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] );
+        if ( Res )
+        {
+            pCubeNew = Mvc_CubeDup(pCover, pCube);
+            Mvc_CoverAddCubeTail( ppCofs[nValues], pCubeNew );
+            continue;
+        }
+
+        // otherwise, add it to separate values
+        for ( i = 0; i < nValues; i++ )
+            if ( Mvc_CubeBitValue( pCube, iValueFirst + i ) )
+            {
+                pCubeNew = Mvc_CubeDup(pCover, pCube);
+                Mvc_CubeBitOr( pCubeNew, pCubeNew, pData->ppMasks[iVar] );
+                Mvc_CoverAddCubeTail( ppCofs[i], pCubeNew );
+            }
+    }
+    return ppCofs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the cubes with non-trivial literals with the given value.]
+
+  Description [The data and the cover are given (pData, pCover). Also given 
+  are the variable number and the number of a value of this variable.
+  This procedure returns the number of cubes having a non-trivial literal
+  of this variable that have the given value present.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue )
+{
+    Mvc_Cube_t * pCube;
+    int iValueFirst, Res, Counter;
+
+    Counter = 0;
+    iValueFirst = Vm_VarMapReadValuesFirst( pData->pVm, iVar );
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        // check if the given literal is the full literal
+        Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] );
+        if ( Res )
+            continue;
+        // this literal is not a full literal; check if it has this value
+        Counter += Mvc_CubeBitValue( pCube, iValueFirst + iValue );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the expanded cover.]
+
+  Description [The original cover is expanded by adding some variables.
+  These variables are the additional variables in pVmNew, compared to
+  pCvr->pVm. The resulting cover is the same as the original one, except
+  that it contains the additional variables present as full literals
+  in every cube.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew )
+{
+    Mvc_Cover_t * pCoverNew;
+    Mvc_Cube_t * pCube, * pCubeNew;
+    int i, iLast, iLastNew;
+
+    // create the new cover
+    pCoverNew = Mvc_CoverAlloc( pCover->pMem, Vm_VarMapReadValuesInNum(pVmNew) );
+
+    // get the cube composed of extra bits
+    Mvc_CoverAllocateMask( pCoverNew );
+    Mvc_CubeBitClean( pCoverNew->pMask );
+    for ( i = pCover->nBits; i < pCoverNew->nBits; i++ )
+        Mvc_CubeBitInsert( pCoverNew->pMask, i );
+
+    // get the indexes of the last words in both covers
+    iLast    = pCover->nWords?    pCover->nWords - 1: 0;
+    iLastNew = pCoverNew->nWords? pCoverNew->nWords - 1: 0;
+
+    // create the cubes of the new cover
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        pCubeNew = Mvc_CubeAlloc( pCoverNew );
+        Mvc_CubeBitClean( pCubeNew );
+        // copy the bits (cannot immediately use Mvc_CubeBitCopy, 
+        // because covers have different numbers of bits)
+        Mvc_CubeSetLast( pCubeNew, iLast );
+        Mvc_CubeBitCopy( pCubeNew, pCube );
+        Mvc_CubeSetLast( pCubeNew, iLastNew );
+        // add the extra bits
+        Mvc_CubeBitOr( pCubeNew, pCubeNew, pCoverNew->pMask );
+        // add the cube to the new cover
+        Mvc_CoverAddCubeTail( pCoverNew, pCubeNew );
+    }
+    return pCoverNew;
+}
+
+#endif
+
+/**Function*************************************************************
+
+  Synopsis    [Transposes the cube cover.]
+
+  Description [Returns the cube cover that looks like a transposed
+  matrix, compared to the matrix derived from the original cover.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mvc_Cover_t * Mvc_CoverTranspose( Mvc_Cover_t * pCover )
+{
+    Mvc_Cover_t * pRes;
+    Mvc_Cube_t * pCubeRes, * pCube;
+    int nWord, nBit, i, iCube;
+
+    pRes = Mvc_CoverAlloc( pCover->pMem, Mvc_CoverReadCubeNum(pCover) );
+    for ( i = 0; i < pCover->nBits; i++ )
+    {
+        // get the word and bit of this literal
+        nWord = Mvc_CubeWhichWord(i);
+        nBit  = Mvc_CubeWhichBit(i);
+        // get the transposed cube
+        pCubeRes = Mvc_CubeAlloc( pRes );
+        Mvc_CubeBitClean( pCubeRes );
+        iCube = 0;
+        Mvc_CoverForEachCube( pCover, pCube )
+        {
+            if ( pCube->pData[nWord] & (1<<nBit) )
+                Mvc_CubeBitInsert( pCubeRes, iCube );
+            iCube++;
+        }
+        Mvc_CoverAddCubeTail( pRes, pCubeRes ); 
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks that the cubes of the cover have 0's in unused bits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mvc_UtilsCheckUnusedZeros( Mvc_Cover_t * pCover )
+{
+    unsigned Unsigned;
+    Mvc_Cube_t * pCube;
+    int nCubes;
+
+    nCubes = 0;
+    Mvc_CoverForEachCube( pCover, pCube )
+    {
+        if ( pCube->nUnused == 0 )
+            continue;
+
+        Unsigned = ( pCube->pData[pCube->iLast] & 
+                    (BITS_FULL << (32-pCube->nUnused)) );
+        if( Unsigned )
+        {
+            printf( "Cube %2d out of %2d contains dirty bits.\n", nCubes, 
+                Mvc_CoverReadCubeNum(pCover) );
+        }
+        nCubes++;
+    }
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+