Version abc70930

18 files changed, 0 insertions, 4848 deletions

diff --git a/src/misc/mvc/module.make b/src/misc/mvc/module.make
deleted file mode 100644
index 23735ca2..00000000
--- a/src/misc/mvc/module.make
+++ /dev/null
@@ -1,16 +0,0 @@
-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
deleted file mode 100644
index 001b1c63..00000000
--- a/src/misc/mvc/mvc.c
+++ /dev/null
@@ -1,46 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
deleted file mode 100644
index 70834e0a..00000000
--- a/src/misc/mvc/mvc.h
+++ /dev/null
@@ -1,732 +0,0 @@
-/**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 "extra.h"
-#include "extra.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 int               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 DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-// 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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== 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 );
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/misc/mvc/mvcApi.c b/src/misc/mvc/mvcApi.c
deleted file mode 100644
index eb942f93..00000000
--- a/src/misc/mvc/mvcApi.c
+++ /dev/null
@@ -1,233 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 9cff99cd..00000000
--- a/src/misc/mvc/mvcCompare.c
+++ /dev/null
@@ -1,369 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index a9eae06e..00000000
--- a/src/misc/mvc/mvcContain.c
+++ /dev/null
@@ -1,173 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-
-/**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
deleted file mode 100644
index d8584446..00000000
--- a/src/misc/mvc/mvcCover.c
+++ /dev/null
@@ -1,251 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index e157879f..00000000
--- a/src/misc/mvc/mvcCube.c
+++ /dev/null
@@ -1,175 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 03643dcf..00000000
--- a/src/misc/mvc/mvcDivide.c
+++ /dev/null
@@ -1,436 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index ecdea75b..00000000
--- a/src/misc/mvc/mvcDivisor.c
+++ /dev/null
@@ -1,90 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 8a82f911..00000000
--- a/src/misc/mvc/mvcList.c
+++ /dev/null
@@ -1,362 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 910158e9..00000000
--- a/src/misc/mvc/mvcLits.c
+++ /dev/null
@@ -1,345 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 7b4ef2af..00000000
--- a/src/misc/mvc/mvcMan.c
+++ /dev/null
@@ -1,77 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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 );
-    Extra_MmFixedStop( p->pMan2 );
-    Extra_MmFixedStop( p->pMan4 );
-    Extra_MmFixedStop( p->pManC );
-    free( p );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/misc/mvc/mvcOpAlg.c b/src/misc/mvc/mvcOpAlg.c
deleted file mode 100644
index 65c02fa5..00000000
--- a/src/misc/mvc/mvcOpAlg.c
+++ /dev/null
@@ -1,163 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 0b34f1de..00000000
--- a/src/misc/mvc/mvcOpBool.c
+++ /dev/null
@@ -1,151 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 52ac76b3..00000000
--- a/src/misc/mvc/mvcPrint.c
+++ /dev/null
@@ -1,220 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 3c975cb3..00000000
--- a/src/misc/mvc/mvcSort.c
+++ /dev/null
@@ -1,141 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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
deleted file mode 100644
index 4b13b23d..00000000
--- a/src/misc/mvc/mvcUtils.c
+++ /dev/null
@@ -1,868 +0,0 @@
-/**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 DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**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                                ///
-////////////////////////////////////////////////////////////////////////
-
-