Version abc60407

8 files changed, 112 insertions, 33 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c68c74e2..e0f0df99 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -154,6 +154,7 @@ struct Abc_Ntk_t_
     Abc_NtkFunc_t    ntkFunc;       // functionality of the network
     char *           pName;         // the network name
     char *           pSpec;         // the name of the spec file if present
+    int              Id;            // network ID
     // name representation 
     stmm_table *     tName2Net;     // the table hashing net names into net pointer
     stmm_table *     tObj2Name;     // the table hashing PI/PO/latch pointers into names
@@ -210,7 +211,7 @@ struct Abc_Ntk_t_
 // maximum/minimum operators
 #define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
-#define ABC_INFINITY      (10000000)
+#define ABC_INFINITY      (100000000)
 
 // transforming floats into ints and back
 static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
@@ -439,10 +440,10 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose );
+extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
-extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti );
-extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
+extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
 extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
 extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
 extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
@@ -492,6 +493,8 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
@@ -554,7 +557,7 @@ extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly, int fReorder, int fVerbose );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@@ -584,7 +587,7 @@ extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode,
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcProve.c ==========================================================*/
-extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose );
+extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -607,8 +610,8 @@ extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose );
-extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose );
+extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
@@ -623,6 +626,7 @@ extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
 extern int                Abc_SopGetCubeNum( char * pSop );
@@ -672,6 +676,19 @@ extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
 extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
 extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
+/*=== abcTrace.c ==========================================================*/
+extern void               Abc_HManStart();
+extern void               Abc_HManStop();
+extern int                Abc_HManIsRunning();
+extern int                Abc_HManGetNewNtkId();
+extern void               Abc_HManAddObj( Abc_Obj_t * pObj );
+extern void               Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern void               Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin );
+extern void               Abc_HManRemoveFanins( Abc_Obj_t * pObj );
+extern void               Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto );
+extern void               Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu );
+extern int                Abc_HManPopulate( Abc_Ntk_t * pNtk );
+extern int                Abc_HManVerify( int NtkIdOld, int NtkIdNew );
 /*=== abcUtil.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f2f50f77..7eb62416 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -807,6 +807,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
         Abc_AigAndDelete( pMan, pFanout );
         // remove the fanins of the old fanout
         Abc_ObjRemoveFanins( pFanout );
+        Abc_HManRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
         assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 59dff196..60e847d0 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -50,6 +50,7 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
+    Abc_HManAddFanin( pObj, pFanin );
 }
 
 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index cb20cec3..da50a9aa 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_MUX_CUBES   100000
+
 static int         Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 
 ////////////////////////////////////////////////////////////////////////
@@ -205,6 +207,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Obj_t * pNode;
+    Extra_MmFlex_t * pManNew;
     DdManager * dd = pNtk->pManFunc;
     DdNode * bFunc;
     Vec_Str_t * vCube;
@@ -217,10 +220,8 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 
     assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
-    // allocate the new manager
-    pNtk->pManFunc = Extra_MmFlexStart();
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // create the new manager
+    pManNew = Extra_MmFlexStart();
 
     // go through the objects
     vCube = Vec_StrAlloc( 100 );
@@ -228,17 +229,30 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
-        if ( pNode->pData == NULL )
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
+        if ( pNode->pNext == NULL )
         {
+            Extra_MmFlexStop( pManNew, 0 );
+            Abc_NtkCleanNext( pNtk );
+//            printf( "Converting from BDDs to SOPs has failed.\n" );
             Vec_StrFree( vCube );
-            Cudd_Quit( dd );
             return 0;
         }
-        Cudd_RecursiveDeref( dd, bFunc );
     }
     Vec_StrFree( vCube );
 
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // set the new manager
+    pNtk->pManFunc = pManNew;
+    // transfer from next to data
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = pNode->pNext;
+        pNode->pNext = NULL;
+    }
+
     // check for remaining references in the package
     Extra_StopManager( dd );
     return 1;
@@ -339,6 +353,13 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
         assert( 0 );
     }
 
+    if ( nCubes > ABC_MUX_CUBES )
+    {
+        Cudd_RecursiveDerefZdd( dd, zCover );
+        printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
+        return NULL;
+    }
+
     // allocate memory for the cover
     if ( pMan )
         pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
@@ -468,6 +489,8 @@ void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
         (*pnCubes)++;
         return;
     }
+    if ( (*pnCubes) > ABC_MUX_CUBES )
+        return;
     extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
     Abc_CountZddCubes_rec( dd, zC0, pnCubes );
     Abc_CountZddCubes_rec( dd, zC1, pnCubes );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index d289cd35..737d63c2 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pFanin)->pCopy );
     // collect the CO nodes
     Abc_NtkFinalize( pNtk, pNtkNew );
-    // fix the problem with CO pointing directing to CIs
+    // fix the problem with CO pointing directly to CIs
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate EXDC 
     if ( pNtk->pExdc )
@@ -101,7 +101,8 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk, fDirect);
+        if ( !Abc_NtkBddToSop(pNtk, fDirect) )
+            return NULL;
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
         Abc_NtkSopToBdd(pNtk);
     }
@@ -157,7 +158,10 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk,0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk,0) )
+            return NULL;
+    }
 
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 0692819b..60ad2412 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -50,6 +50,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     memset( pNtk, 0, sizeof(Abc_Ntk_t) );
     pNtk->ntkType     = Type;
     pNtk->ntkFunc     = Func;
+    pNtk->Id          = !Abc_HManIsRunning()? 0 : Abc_HManGetNewNtkId();
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
     pNtk->vLats       = Vec_PtrAlloc( 100 );
@@ -136,6 +137,14 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Vec_PtrPush( pNtkNew->vCis, pObjNew );
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_HManAddProto( Abc_NtkConst1(pNtk)->pCopy, Abc_NtkConst1(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // transfer the names
     Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
     Abc_ManTimeDup( pNtk, pNtkNew );
@@ -407,6 +416,11 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index d6adfeb2..0ffe3298 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -50,6 +50,8 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
     pObj->pNtk = pNtk;
     pObj->Type = Type;
     pObj->Id   = -1;
+    if ( pNtk->ntkType != ABC_NTK_NETLIST )
+        Abc_HManAddObj( pObj );
     return pObj;
 }
 
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 1e59b17b..d5cc65f1 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -61,7 +61,7 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
 
   Description []
                
@@ -92,7 +92,7 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -108,7 +108,7 @@ char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -124,7 +124,7 @@ char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the AND2 cover.]
+  Synopsis    [Creates the AND2 cover.]
 
   Description []
                
@@ -147,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input AND cover.]
+  Synopsis    [Creates the multi-input AND cover.]
 
   Description []
                
@@ -169,7 +169,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NAND cover.]
+  Synopsis    [Creates the multi-input NAND cover.]
 
   Description []
                
@@ -191,7 +191,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -213,7 +213,7 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -238,7 +238,7 @@ char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NOR cover.]
+  Synopsis    [Creates the multi-input NOR cover.]
 
   Description []
                
@@ -259,7 +259,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover.]
+  Synopsis    [Creates the multi-input XOR cover.]
 
   Description []
                
@@ -276,7 +276,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover (special case).]
+  Synopsis    [Creates the multi-input XOR cover (special case).]
 
   Description []
                
@@ -296,7 +296,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XNOR cover.]
+  Synopsis    [Creates the multi-input XNOR cover.]
 
   Description []
                
@@ -313,7 +313,24 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the inv cover.]
+  Synopsis    [Creates the MUX cover.]
+
+  Description [The first input of MUX is the control. The second input
+  is DATA1. The third input is DATA0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateMux( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister(pMan, "11- 1\n0-1 1\n");
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the inv cover.]
 
   Description []
                
@@ -329,7 +346,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the buf cover.]
+  Synopsis    [Creates the buf cover.]
 
   Description []