Version abc51222

author: Alan Mishchenko <alanmi@berkeley.edu> 2005-12-22 08:01:00 -0800
committer: Alan Mishchenko <alanmi@berkeley.edu> 2005-12-22 08:01:00 -0800
commit: 457e243e588e7ed5f39251784335e254a0c9e711 (patch)
tree: 751d7b416e66e416983760d0b95d79bb24371309 /src
parent: 37f19d8dfb17605abab38110beec5fc17413e635 (diff)
download: abc-457e243e588e7ed5f39251784335e254a0c9e711.tar.gz
abc-457e243e588e7ed5f39251784335e254a0c9e711.tar.bz2
abc-457e243e588e7ed5f39251784335e254a0c9e711.zip
39 files changed, 3935 insertions, 72 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e43ee31b..e0a27f9a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -209,8 +209,9 @@ struct Abc_Ntk_t_
 #define ABC_INFINITY      (10000000)
 
 // transforming floats into ints and back
-static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);           }
-static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);         }
+static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
+static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);             }
+static inline int         Abc_BitWordNum( int nBits )                { return nBits/32 + ((nBits%32) > 0);  }
 
 // checking the network type
 static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST; }
@@ -570,7 +571,7 @@ extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
 extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
-extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
+extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
@@ -600,12 +601,13 @@ extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int n
 extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
-extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 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_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 742c8c8d..2ab3842f 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -93,27 +93,41 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
     DdNode * bSum, * bCube, * bTemp, * bVar;
     char * pCube;
     int nVars, Value, v;
+    extern int Abc_SopIsExorType( char * pSop );
+
     // start the cover
     nVars = Abc_SopGetVarNum(pSop);
-    // check the logic function of the node
     bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
-    Abc_SopForEachCube( pSop, nVars, pCube )
+    if ( Abc_SopIsExorType(pSop) )
+    {
+        for ( v = 0; v < nVars; v++ )
+        {
+            bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+    }
+    else
     {
-        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
-        Abc_CubeForEachVar( pCube, Value, v )
+        // check the logic function of the node
+        Abc_SopForEachCube( pSop, nVars, pCube )
         {
-            if ( Value == '0' )
-                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
-            else if ( Value == '1' )
-                bVar = Cudd_bddIthVar( dd, v );
-            else
-                continue;
-            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
+            bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
+            Abc_CubeForEachVar( pCube, Value, v )
+            {
+                if ( Value == '0' )
+                    bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+                else if ( Value == '1' )
+                    bVar = Cudd_bddIthVar( dd, v );
+                else
+                    continue;
+                bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
+                Cudd_RecursiveDeref( dd, bTemp );
+            }
+            bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
+            Cudd_Ref( bSum );
             Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bCube );
         }
-        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   Cudd_Ref( bSum );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bCube );
     }
     // complement the result if necessary
     bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
@@ -246,16 +260,18 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
     if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
     {
+        if ( fMode == -1 ) // if the phase is not known, write constant 1
+            fMode = 1;
         Vec_StrFill( vCube, nFanins, '-' );
         Vec_StrPush( vCube, '\0' );
         if ( pMan )
             pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
         else
             pSop = ALLOC( char, nFanins + 4 );
-        if ( bFuncOn == Cudd_ReadLogicZero(dd) )
-            sprintf( pSop, "%s 0\n", vCube->pArray );
+        if ( bFuncOn == Cudd_ReadOne(dd) )
+            sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
         else
-            sprintf( pSop, "%s 1\n", vCube->pArray );
+            sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
         return pSop;
     }
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 53f8c1e9..65cc6e2e 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
         if ( !Abc_NodeIsConst(pObj) )
         {
             Abc_NtkDupObj( pNtkNew, pObj );
-            pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
+            pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL );
         }
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
             pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index dc69f651..4152dd0a 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -156,13 +156,14 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 {
     char * pSop;
     int i;
     pSop = Abc_SopStart( pMan, 1, nVars );
     for ( i = 0; i < nVars; i++ )
-        pSop[i] = '1';
+        pSop[i] = '1' - (pfCompl? pfCompl[i] : 0);
+    pSop[nVars + 1] = '1';
     return pSop;
 }
 
@@ -275,6 +276,26 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the multi-input XOR cover (special case).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
+{
+    char * pSop;
+    pSop = Abc_SopCreateAnd( pMan, nVars, NULL );
+    pSop[nVars+1] = 'x';
+    assert( pSop[nVars+2] == '\n' );
+    return pSop;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Starts the multi-input XNOR cover.]
 
   Description []
@@ -402,9 +423,9 @@ int Abc_SopGetVarNum( char * pSop )
 int Abc_SopGetPhase( char * pSop )
 {
     int nVars = Abc_SopGetVarNum( pSop );
-    if ( pSop[nVars+1] == '0' )
+    if ( pSop[nVars+1] == '0' || pSop[nVars+1] == 'n' )
         return 0;
-    if ( pSop[nVars+1] == '1' )
+    if ( pSop[nVars+1] == '1' || pSop[nVars+1] == 'x' )
         return 1;
     assert( 0 );
     return -1;
@@ -453,6 +474,10 @@ void Abc_SopComplement( char * pSop )
                 *(pCur - 1) = '1';
             else if ( *(pCur - 1) == '1' )
                 *(pCur - 1) = '0';
+            else if ( *(pCur - 1) == 'x' )
+                *(pCur - 1) = 'n';
+            else if ( *(pCur - 1) == 'n' )
+                *(pCur - 1) = 'x';
             else
                 assert( 0 );
         }
@@ -474,7 +499,7 @@ bool Abc_SopIsComplement( char * pSop )
     char * pCur;
     for ( pCur = pSop; *pCur; pCur++ )
         if ( *pCur == '\n' )
-            return (int)(*(pCur - 1) == '0');
+            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
     assert( 0 );
     return 0;
 }
@@ -616,6 +641,27 @@ bool Abc_SopIsOrType( char * pSop )
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_SopIsExorType( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+            return (int)(*(pCur - 1) == 'x' || *(pCur - 1) == 'n');
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 bool Abc_SopCheck( char * pSop, int nFanins )
 {
     char * pCubes, * pCubesOld;
@@ -638,7 +684,7 @@ bool Abc_SopCheck( char * pSop, int nFanins )
             fFound0 = 1;
         else if ( *pCubes == '1' )
             fFound1 = 1;
-        else
+        else if ( *pCubes != 'x' && *pCubes != 'n' )
         {
             fprintf( stdout, "Abc_SopCheck: SOP has a strange character in the output part of its cube.\n" );
             return 0;
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 8e1615d7..9d95fade 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -76,6 +76,8 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
     assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         assert( pNode->pData );
         nCubes += Abc_SopGetCubeNum( pNode->pData );
     }
@@ -153,6 +155,8 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         assert( pNode->pData );
         nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0;
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b6de6cbf..71b76cf6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -77,6 +77,7 @@ static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -173,6 +174,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -648,6 +650,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     int c;
+    int fListNodes;
     int fProfile;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -655,12 +658,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fProfile = 1;
+    fListNodes = 0;
+    fProfile   = 1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fListNodes ^= 1;
+            break;
         case 'p':
             fProfile ^= 1;
             break;
@@ -701,12 +708,13 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // process all COs
-    Abc_NtkPrintLevel( pOut, pNtk, fProfile );
+    Abc_NtkPrintLevel( pOut, pNtk, fProfile, fListNodes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_level [-ph] <node>\n" );
+    fprintf( pErr, "usage: print_level [-nph] <node>\n" );
     fprintf( pErr, "\t        prints information about node level and cone size\n" );
+    fprintf( pErr, "\t-n    : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
     fprintf( pErr, "\t-p    : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     fprintf( pErr, "\tnode  : (optional) one node to consider\n");
@@ -732,6 +740,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fVerbose;
     extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
+    extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -759,6 +768,11 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+
+    // print support information
+    Abc_NtkPrintStrSupports( pNtk );
+    return 0;
+
     if ( !Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "This command works only for combinational networks.\n" );
@@ -3649,11 +3663,102 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fVerbose;
+    int fUseInvs;
+    int nFaninMax;
+    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    fUseInvs = 1;
+    nFaninMax = 128;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFaninMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nFaninMax < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fUseInvs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+    // run the command
+    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" );
+    fprintf( pErr, "\t         specilized AND/OR/EXOR decomposition\n" );
+    fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-i     : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3676,6 +3781,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+//    Abc_NtkDeriveEsops( pNtk );
+//    Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
+    printf( "This command is currently not used.\n" );
+
+/*
     // run the command
     pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
     if ( pNtkRes == NULL )
@@ -3685,6 +3802,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
     return 0;
 
 usage:
@@ -3696,7 +3814,6 @@ usage:
 
 
 
-
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 1adbfef7..fed89dbb 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -102,6 +102,42 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
 
 /**Function*************************************************************
 
+  Synopsis    [Randomizes the node positions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    int i, Signature;
+    if ( Vec_PtrSize(vSuper) < 3 )
+        return;
+    pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 );
+    pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 );
+    if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+        return;
+    // some reordering will be performed
+    Signature = rand();
+    for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- )
+    {
+        pNode1 = Vec_PtrEntry( vSuper, i );
+        pNode2 = Vec_PtrEntry( vSuper, i-1 );
+        if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+            return;
+        if ( Signature & (1 << (i % 10)) )
+            continue;
+        Vec_PtrWriteEntry( vSuper, i,   pNode2 );
+        Vec_PtrWriteEntry( vSuper, i-1, pNode1 );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Rebalances the multi-input node rooted at pNodeOld.]
 
   Description []
@@ -143,6 +179,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     assert( vSuper->nSize > 1 );
     while ( vSuper->nSize > 1 )
     {
+        // randomize the node positions
+//        Abc_NodeBalanceRandomize( vSuper );
+        // pull out the last two nodes
         pNode1 = Vec_PtrPop(vSuper);
         pNode2 = Vec_PtrPop(vSuper);
         Abc_VecObjPushUniqueOrderByLevel( vSuper, Abc_AigAnd(pMan, pNode1, pNode2) );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index bfc992ef..d59f21a0 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
 {
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
-    Fraig_Man_t * pMan;
+    Fraig_Man_t * pMan; 
     // check if EXDC is present
     if ( fExdc && pNtk->pExdc == NULL )
         fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 82325619..6791f08c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -79,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
             fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkHasBdd(pNtk) )
-        fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
+        fprintf( pFile, "  bdd  = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
     else if ( Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
@@ -423,10 +423,26 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
+void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes )
 {
     Abc_Obj_t * pNode;
-    int i, Length;
+    int i, k, Length;
+
+    if ( fListNodes )
+    {
+        int nLevels;
+        nLevels = Abc_NtkGetLevelNum(pNtk);
+        printf( "Nodes by level:\n" );
+        for ( i = 0; i <= nLevels; i++ )
+        {
+            printf( "%2d : ", i );
+            Abc_NtkForEachNode( pNtk, pNode, k )
+                if ( (int)pNode->Level == i )
+                    printf( " %s", Abc_ObjName(pNode) );
+            printf( "\n" );
+        }
+        return;
+    }
 
     // print the delay profile
     if ( fProfile && Abc_NtkHasMapping(pNtk) )
@@ -716,6 +732,34 @@ void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints info for each output cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "Structural support info:\n" );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+        printf( "%20s :  Cone = %5d.  Supp = %5d.\n", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index ab594667..b3b30d9a 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -109,6 +109,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     // print stats
     if ( fVerbose )
         Rwr_ManPrintStats( pManRwr );
+//        Rwr_ManPrintStatsFile( pManRwr );
     // delete the managers
     Rwr_ManStop( pManRwr );
     Cut_ManStop( pManCut );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 1a35d143..4a65659c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int  Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int  Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,6 +57,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     // load clauses into the solver
     clk = clock();
     pSat = Abc_NtkMiterSatCreate( pNtk );
+    if ( pSat == NULL )
+        return 1;
 //    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
@@ -69,7 +71,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     {
         solver_delete( pSat );
 //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return -1;
+        return 1;
     }
 
     // solve the miter
@@ -143,13 +145,19 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
         // derive SOPs for both phases of the node
         Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
         // add the clauses to the solver
-        Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
+        if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
+        {
+            solver_delete( pSat );
+            return NULL;
+        }
     }
-    // add clauses for each PO
-//    Abc_NtkForEachPo( pNtk, pNode, i )
-//        Abc_NodeAddClausesTop( pSat, pNode, vVars );
-
-    Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
+    // add clauses for the POs
+    if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
+    {
+        solver_delete( pSat );
+        return NULL;
+    }
+//    Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
 
     // delete
     Vec_StrFree( vCube );
@@ -169,7 +177,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
     int i, c, nFanins;
@@ -177,6 +185,16 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
 
     nFanins = Abc_ObjFaninNum( pNode );
     assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
+
+    if ( nFanins == 0 )
+    {
+        vVars->nSize = 0;
+        if ( Abc_SopIsConst1(pSop1) )
+            Vec_IntPush( vVars, toLit(pNode->Id) );
+        else
+            Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
  
     // add clauses for the negative phase
     for ( c = 0; ; c++ )
@@ -195,7 +213,8 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
                 Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
 
     // add clauses for the positive phase
@@ -215,8 +234,10 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
                 Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
+    return 1;
 }
 
 /**Function*************************************************************
@@ -230,7 +251,7 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
 
@@ -240,29 +261,33 @@ void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
     else
     {
         vVars->nSize = 0;
         Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
 
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLit(pNode->Id) );
-    solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
 
 
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index d1734d88..72f4215b 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -29,6 +29,7 @@
 // static functions
 static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
+static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 
 extern char *      Mio_GateReadSop( void * pGate );
@@ -182,6 +183,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
 {
     int fUseFactor = 1;
     char * pSop;
+    extern int Abc_SopIsExorType( char * pSop );
 
     assert( Abc_ObjIsNode(pNode) );
 
@@ -203,6 +205,10 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
     if ( Abc_NodeIsConst(pNode) )
         return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) );
 
+    // consider the special case of EXOR function
+    if ( Abc_SopIsExorType(pSop) )
+        return Abc_NodeStrashExor( pNtkNew, pNode, pSop );
+
     // decide when to use factoring
     if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
         return Abc_NodeStrashFactor( pNtkNew, pNode, pSop );
@@ -254,6 +260,37 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pS
 
 /**Function*************************************************************
 
+  Synopsis    [Strashed n-input XOR function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Aig_t * pMan = pNtkNew->pManFunc;
+    Abc_Obj_t * pFanin, * pSum;
+    int i, nFanins;
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pFanin = Abc_ObjFanin( pNode, i );
+        pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy );
+    }
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Abc_ObjNot(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Strashes one logic node using its SOP.]
 
   Description []
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index bbaca5a9..f20855ab 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1245,6 +1245,12 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling SIS.\n" );
+    }
+
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk);
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
@@ -1375,6 +1381,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling MVSIS.\n" );
+    }
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk);
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 2f74c2a5..9b7fb49f 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -245,7 +245,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop )
     argc = *argcp;
     argv = *argvp;
     stopit = 0;
-    for ( ; *loop < 20; ( *loop )++ )
+    for ( ; *loop < 200; ( *loop )++ )
     {
         if ( argc == 0 )
             return 0;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1330d114..69b60000 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -44,6 +44,7 @@ static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -81,6 +82,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_gml",     IoCommandWriteGml,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
 }
 
 /**Function*************************************************************
@@ -1383,6 +1385,69 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    char * FileName;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[util_optind];
+
+    // derive the netlist
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    if ( pNtkTemp == NULL )
+    {
+        fprintf( pAbc->Out, "Writing PLA has failed.\n" );
+        return 0;
+    }
+    Io_WriteVerilog( pNtkTemp, FileName );
+    Abc_NtkDelete( pNtkTemp );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write a very special subset of Verilog\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.h b/src/base/io/io.h
index cb8678b3..286b570c 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -90,6 +90,8 @@ extern void               Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
 extern void               Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost );
 /*=== abcWritePla.c ==========================================================*/
 extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteVerilog.c ==========================================================*/
+extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 510167a8..d8ad8f71 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -127,7 +127,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
                 // assign the cover
                 if ( strcmp(pType, "AND") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "OR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "NAND") == 0 )
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index e23bfdb7..b8a2ed01 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -504,7 +504,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
             Vec_StrAppend( p->vCubes, vTokens->pArray[0] );
             // check the char 
             Char = ((char *)vTokens->pArray[1])[0];
-            if ( Char != '0' && Char != '1' )
+            if ( Char != '0' && Char != '1' && Char != 'x' && Char != 'n' )
             {
                 p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
                 sprintf( p->sError, "The output character in the constant cube is wrong." );
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 63345fd7..a2a2f527 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -191,7 +191,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( strncmp( pObj->pData, "And", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( pObj->pData, "Or", 2 ) == 0 )
             Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 )
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
new file mode 100644
index 00000000..f56da052
--- /dev/null
+++ b/src/base/io/ioWriteVerilog.c
@@ -0,0 +1,445 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteVerilog.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to output a special subset of Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+
+    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogCheckNtk(pNtk) )
+    {
+        printf( "Io_WriteVerilog(): Can write Verilog for a very special subset of logic networks.\n" );
+        printf( "The current network is not in the subset; writing Verilog is not performed.\n" );
+        return;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+        printf( "Io_WriteVerilog(): Warning: only combinational portion is being written.\n" );
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // write the equations for the network
+    Io_WriteVerilogInt( pFile, pNtk );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    // write inputs and outputs
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "module %s (\n   ", Abc_NtkName(pNtk) );
+    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    fprintf( pFile, ",\n   " );
+    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    fprintf( pFile, "  );\n" );
+    // write inputs, outputs and wires
+    fprintf( pFile, "  input" );
+    Io_WriteVerilogPis( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  output" );
+    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  wire" );
+    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    // write the nodes
+    Io_WriteVerilogNodes( pFile, pNtk );
+    // finalize the file
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachCi( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanout0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCiNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachCo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCoNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        nNodes++;
+    }
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nCubes, nFanins, Counter, nDigits, fPadZeros;
+    char * pName;
+    extern int Abc_SopIsExorType( char * pSop );
+
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    Counter = 1;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        nCubes = Abc_SopGetCubeNum(pObj->pData);
+        if ( Abc_SopIsAndType(pObj->pData) )
+            pName = "ts_and", fPadZeros = 1;
+        else if ( Abc_SopIsExorType(pObj->pData) )
+            pName = "ts_xor", fPadZeros = 1;
+        else // if ( Abc_SopIsOrType(pObj->pData) )
+            pName = "ts_or",  fPadZeros = 0;
+
+        assert( nCubes < 2 );
+        if ( nCubes == 0 )
+        {
+            fprintf( pFile, "  ts_gnd g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+        }
+        else if ( nCubes == 1 && nFanins == 0 )
+        {
+            fprintf( pFile, "  ts_vdd g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+        }
+        else if ( nFanins == 1 && Abc_SopIsInv(pObj->pData) )
+        {
+            fprintf( pFile, "  ts_inv g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+        }
+        else if ( nFanins == 1 )
+        {
+            fprintf( pFile, "  ts_buf g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+        }
+        else if ( nFanins <= 4 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 4, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 4, fPadZeros );
+        }
+        else if ( nFanins <= 6 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 6, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 6, fPadZeros );
+        }
+        else if ( nFanins == 7 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 7, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 7, fPadZeros );
+        }
+        else if ( nFanins == 8 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 8, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 8, fPadZeros );
+        }
+        else if ( nFanins <= 16 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 16, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 16, fPadZeros );
+        }
+        else if ( nFanins <= 32 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 32, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 32, fPadZeros );
+        }
+        else if ( nFanins <= 64 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 64, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 64, fPadZeros );
+        }
+        else if ( nFanins <= 128 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 128, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 128, fPadZeros );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 2;
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+    }
+    for ( ; i < nInMax; i++ )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+    }
+    fprintf( pFile, ");\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    char * pSop;
+    int i, k, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_SopGetCubeNum(pObj->pData) > 1 )
+        {
+            printf( "Node %s contains a cover with more than one cube.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins < 2 )
+            continue;
+        pSop = pObj->pData;
+        for ( k = 0; k < nFanins; k++ )
+            if ( pSop[k] != '1' )
+            {
+                printf( "Node %s contains a cover with non-positive literals.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the name for writing the Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+{
+    static char Buffer[20];
+    char * pName;
+    pName = Abc_ObjName(pObj);
+    if ( pName[0] != '[' )
+        return pName;
+    // replace opening bracket by the escape sign and closing bracket by space
+    // as a result of this transformation, the length of the name does not change
+    strcpy( Buffer, pName );
+    Buffer[0] = '\\';
+    Buffer[strlen(Buffer)-1] = ' ';
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c
index f4eefa8c..b951fd8f 100644
--- a/src/map/fpga/fpgaUtils.c
+++ b/src/map/fpga/fpgaUtils.c
@@ -51,11 +51,11 @@ static Fpga_Man_t * s_pMan = NULL;
 ***********************************************************************/
 Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv )
 {
-    Fpga_NodeVec_t * vNodes, * vNodesCo;
+    Fpga_NodeVec_t * vNodes;//, * vNodesCo;
     Fpga_Node_t * pNode;
     int i;
     // collect the CO nodes by level
-    vNodesCo = Fpga_MappingOrderCosByLevel( pMan );
+//    vNodesCo = Fpga_MappingOrderCosByLevel( pMan );
     // start the array
     vNodes = Fpga_NodeVecAlloc( 100 );
     // collect the PIs
@@ -66,17 +66,17 @@ Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv )
         pNode->fMark0 = 1;
     }
     // perform the traversal
-//    for ( i = 0; i < pMan->nOutputs; i++ )
-//        Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
-    for ( i = 0; i < vNodesCo->nSize; i++ )
-        for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
-            Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
+//    for ( i = vNodesCo->nSize - 1; i >= 0 ; i-- )
+//        for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
+//            Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv );
     // clean the node marks
     for ( i = 0; i < vNodes->nSize; i++ )
         vNodes->pArray[i]->fMark0 = 0;
 //    for ( i = 0; i < pMan->nOutputs; i++ )
 //        Fpga_MappingUnmark_rec( Fpga_Regular(pMan->pOutputs[i]) );
-    Fpga_NodeVecFree( vNodesCo );
+//    Fpga_NodeVecFree( vNodesCo );
     return vNodes;
 }
 
@@ -954,7 +954,7 @@ Fpga_NodeVec_t * Fpga_MappingOrderCosByLevel( Fpga_Man_t * pMan )
     Fpga_Node_t * pNode;
     Fpga_NodeVec_t * vNodes;
     int i, nLevels;
-    // get the largest node
+    // get the largest level of a CO
     nLevels = Fpga_MappingMaxLevel( pMan );
     // allocate the array of nodes
     vNodes = Fpga_NodeVecAlloc( nLevels + 1 );
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 3856c04e..70e1070b 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -129,6 +129,7 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
 extern void              Rwr_ManStop( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
+extern void              Rwr_ManPrintStatsFile( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
 extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 1d306e7e..115065f5 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -179,6 +179,29 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Rwr_ManPrintStatsFile( Rwr_Man_t * p )
+{
+    FILE * pTable;
+    pTable = fopen( "stats.txt", "a+" );
+    fprintf( pTable, "%d ", p->nCutsGood );
+    fprintf( pTable, "%d ", p->nSubgraphs );
+    fprintf( pTable, "%d ", p->nNodesRewritten );
+    fprintf( pTable, "%d", p->nNodesGained );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Rwr_ManReadDecs( Rwr_Man_t * p )
 {
     return p->pGraph;
diff --git a/src/opt/xyz/module.make b/src/opt/xyz/module.make
new file mode 100644
index 00000000..ae7dab0f
--- /dev/null
+++ b/src/opt/xyz/module.make
@@ -0,0 +1,8 @@
+SRC +=    src/opt/xyz/xyzBuild.c \
+    src/opt/xyz/xyzCore.c \
+    src/opt/xyz/xyzMan.c \
+    src/opt/xyz/xyzMinEsop.c \
+    src/opt/xyz/xyzMinMan.c \
+    src/opt/xyz/xyzMinSop.c \
+    src/opt/xyz/xyzMinUtil.c \
+    src/opt/xyz/xyzTest.c 
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
new file mode 100644
index 00000000..f18686ff
--- /dev/null
+++ b/src/opt/xyz/xyz.h
@@ -0,0 +1,94 @@
+/**CFile****************************************************************
+
+  FileName    [xyz.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Xyz_Man_t_  Xyz_Man_t;
+typedef struct Xyz_Obj_t_  Xyz_Obj_t;
+
+// storage for node information
+struct Xyz_Obj_t_
+{
+    Min_Cube_t *      pCover[3];    // pos/neg/esop
+    Vec_Int_t *       vSupp;        // computed support (all nodes except CIs)
+};
+
+// storage for additional information
+struct Xyz_Man_t_
+{
+    // general characteristics
+    int               nFaninMax;    // the number of vars
+    int               nCubesMax;    // the limit on the number of cubes in the intermediate covers
+    int               nWords;       // the number of words
+    Vec_Int_t *       vFanCounts;   // fanout counts
+    Vec_Ptr_t *       vObjStrs;     // object structures
+    void *            pMemory;      // memory for the internal data strctures
+    Min_Man_t *       pManMin;      // the cub manager
+    // arrays to map local variables
+    Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
+    Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
+    Vec_Int_t *       vPairs0;      // the first var in each pair of common vars
+    Vec_Int_t *       vPairs1;      // the second var in each pair of common vars
+    Vec_Int_t *       vTriv0;       // trival support of the first node
+    Vec_Int_t *       vTriv1;       // trival support of the second node
+    // statistics
+    int               nSupps;       // supports created
+    int               nSuppsMax;    // the maximum number of supports
+    int               nBoundary;    // the boundary size
+    int               nNodes;       // the number of nodes processed
+};
+
+static inline Xyz_Obj_t *  Abc_ObjGetStr( Abc_Obj_t * pObj )                       { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
+
+static inline void         Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec )    { Abc_ObjGetStr(pObj)->vSupp = vVec;   }
+static inline Vec_Int_t *  Abc_ObjGetSupp( Abc_Obj_t * pObj )                      { return Abc_ObjGetStr(pObj)->vSupp;   }
+
+static inline void         Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj )                    { return Abc_ObjGetStr(pObj)->pCover[2]; }
+
+static inline void         Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol )                    { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== xyzBuild.c ==========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
+/*=== xyzCore.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+/*=== xyzMan.c ============================================================*/
+extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
+extern void        Xyz_ManFree( Xyz_Man_t * p );
+extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
+/*=== xyzTest.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzBuild.c b/src/opt/xyz/xyzBuild.c
new file mode 100644
index 00000000..e32721e7
--- /dev/null
+++ b/src/opt/xyz/xyzBuild.c
@@ -0,0 +1,379 @@
+/**CFile****************************************************************
+
+  FileName    [xyzBuild.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Network construction procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
+{
+    Vec_Int_t * vLits;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    int i, iFanin, Lit;
+    // create empty cube
+    if ( pCube->nLits == 0 )
+        return Abc_NodeCreateConst1(pNtkNew);
+    // get the literals of this cube
+    vLits = Vec_IntAlloc( 10 );
+    Min_CubeGetLits( pCube, vLits );
+    assert( pCube->nLits == (unsigned)vLits->nSize );
+    // create special case when there is only one literal
+    if ( pCube->nLits == 1 )
+    {
+        iFanin = Vec_IntEntry(vLits,0);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntFree( vLits );
+        if ( Lit == 1 )// negative
+            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
+        return pFanin->pCopy;
+    }
+    assert( pCube->nLits > 1 );
+    // create the AND cube
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < vLits->nSize; i++ )
+    {
+        iFanin = Vec_IntEntry(vLits,i);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntWriteEntry( vLits, i, Lit==1 );
+        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+    }
+    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    Vec_IntFree( vLits );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
+    Vec_Int_t * vSupp;
+    int Entry, nCubes, i;
+
+    if ( Abc_ObjIsCi(pObj) )
+        return pObj->pCopy;
+    assert( Abc_ObjIsNode(pObj) );
+    // skip if already computed
+    if ( pObj->pCopy )
+        return pObj->pCopy;
+
+    // get the support and the cover
+    vSupp  = Abc_ObjGetSupp( pObj ); 
+    pCover = Abc_ObjGetCover2( pObj );
+    assert( vSupp );
+/*
+    if ( pCover &&  pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 )
+    {
+        printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) );
+        Min_CoverWrite( stdout, pCover );
+    }
+*/
+/*
+    // print the support of this node
+    printf( "{ " );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+        printf( "%d ", Entry );
+    printf( "}  cubes = %d\n", Min_CoverCountCubes( pCover ) );
+*/
+    // process the fanins
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 );
+    }
+
+    // for each cube, construct the node
+    nCubes = Min_CoverCountCubes( pCover );
+    if ( nCubes == 0 )
+        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
+    else if ( nCubes == 1 )
+        pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp );
+    else
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Min_CoverForEachCube( pCover, pCube )
+        {
+            pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp );
+            Abc_ObjAddFanin( pNodeNew, pFaninNew );
+        }
+        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
+    }
+/*
+    printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
+    }
+    printf( "\n" );
+    Min_CoverWrite( stdout, pCover );
+*/
+    pObj->pCopy = pNodeNew;
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // reconstruct the network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 );
+//        printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id );
+    }
+    // add the COs
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkXyzDerive: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
+{
+    assert( pObj->pCopy );
+    if ( !fCompl )
+        return pObj->pCopy;
+    if ( pObj->pCopy->pCopy == NULL )
+        pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+    return pObj->pCopy->pCopy;
+ }
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
+{
+    Vec_Int_t * vLits;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    int i, iFanin, Lit;
+    // create empty cube
+    if ( pCube->nLits == 0 )
+        return Abc_NodeCreateConst1(pNtkNew);
+    // get the literals of this cube
+    vLits = Vec_IntAlloc( 10 );
+    Min_CubeGetLits( pCube, vLits );
+    assert( pCube->nLits == (unsigned)vLits->nSize );
+    // create special case when there is only one literal
+    if ( pCube->nLits == 1 )
+    {
+        iFanin = Vec_IntEntry(vLits,0);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntFree( vLits );
+//        if ( Lit == 1 )// negative
+//            return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
+//        return pFanin->pCopy;
+        return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 );
+    }
+    assert( pCube->nLits > 1 );
+    // create the AND cube
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < vLits->nSize; i++ )
+    {
+        iFanin = Vec_IntEntry(vLits,i);
+        pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
+        Lit = Min_CubeGetVar(pCube, iFanin);
+        assert( Lit == 1 || Lit == 2 );
+        Vec_IntWriteEntry( vLits, i, Lit==1 );
+//        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) );
+    }
+//    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL );
+    Vec_IntFree( vLits );
+    return pNodeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
+{
+    Min_Cube_t * pCover, * pCube;
+    Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
+    Vec_Int_t * vSupp;
+    int Entry, nCubes, i;
+
+    // skip if already computed
+    if ( pObj->pCopy )
+        return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
+    assert( Abc_ObjIsNode(pObj) );
+
+    // get the support and the cover
+    vSupp  = Abc_ObjGetSupp( pObj ); 
+    pCover = Abc_ObjGetCover2( pObj );
+    assert( vSupp );
+
+    // process the fanins
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFanin = Abc_NtkObj(pObj->pNtk, Entry);
+        Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 );
+    }
+
+    // for each cube, construct the node
+    nCubes = Min_CoverCountCubes( pCover );
+    if ( nCubes == 0 )
+        pNodeNew = Abc_NodeCreateConst0(pNtkNew);
+    else if ( nCubes == 1 )
+        pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp );
+    else
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Min_CoverForEachCube( pCover, pCube )
+        {
+            pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
+            Abc_ObjAddFanin( pNodeNew, pFaninNew );
+        }
+        pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
+    }
+
+    pObj->pCopy = pNodeNew;
+    return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the decomposed network.]
+
+  Description [The resulting network contains only pure AND/OR/EXOR gates
+  and inverters. This procedure is usedful to generate Verilog.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pNodeNew;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // reconstruct the network
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
+    }
+    // add the COs
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
new file mode 100644
index 00000000..a48f749e
--- /dev/null
+++ b/src/opt/xyz/xyzCore.c
@@ -0,0 +1,697 @@
+/**CFile****************************************************************
+
+  FileName    [xyzCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
+static int         Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
+static void        Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
+
+static int         Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
+static int         Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
+static int         Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+static int         Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+static int         Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+static int         Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Xyz_Man_t * p;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // create the manager
+    p = Xyz_ManAlloc( pNtk, nFaninMax );
+    pNtk->pManCut = p;
+
+    // perform mapping
+    Abc_NtkXyzCovers( p, pNtk, fVerbose );
+
+    // derive the final network
+    if ( fUseInvs )
+        pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
+    else
+        pNtkNew = Abc_NtkXyzDerive( p, pNtk );
+
+    Xyz_ManFree( p );
+    pNtk->pManCut = NULL;
+
+    // make sure that everything is okay
+    if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkXyz: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the supports.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int i, clk = clock();
+
+    // start the manager
+    p->vFanCounts = Abc_NtkFanoutCounts(pNtk);
+
+    // set trivial cuts for the constant and the CIs
+    pObj = Abc_NtkConst1(pNtk);
+    pObj->fMarkA = 1;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->fMarkA = 1;
+
+    // perform iterative decomposition
+    for ( i = 0; ; i++ )
+    {
+        if ( fVerbose )
+        printf( "Iter %d : ", i+1 );
+        if ( Abc_NtkXyzCoversOne(p, pNtk, fVerbose) )
+            break;
+    }
+
+    // clean the cut-point markers
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = 0;
+
+if ( fVerbose )
+{
+PRT( "Total", clock() - clk );
+}
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the supports.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vBoundary;
+    int i, clk = clock();
+    int Counter = 0;
+    int fStop = 1;
+
+    // array to collect the nodes in the new boundary
+    vBoundary = Vec_PtrAlloc( 100 );
+
+    // start from the COs and mark visited nodes using pObj->fMarkB
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // skip the solved nodes (including the CIs)
+        pObj = Abc_ObjFanin0(pObj);
+        if ( pObj->fMarkA )
+        {
+            Counter++;
+            continue;
+        } 
+
+        // traverse the cone starting from this node
+        Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+        if ( Abc_ObjGetSupp(pObj) == NULL )
+            fStop = 0;
+        else
+            Counter++;
+
+/*
+        printf( "%-15s : ", Abc_ObjName(pObj) ); 
+        printf( "lev = %5d  ", pObj->Level );
+        if ( Abc_ObjGetSupp(pObj) == NULL )
+        {
+            printf( "\n" );
+            continue;
+        }
+        printf( "supp = %3d  ", Abc_ObjGetSupp(pObj)->nSize ); 
+        printf( "esop = %3d  ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); 
+        printf( "\n" );
+*/
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // clean visited nodes
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkB = 0;
+
+    // create the new boundary
+    p->nBoundary = 0;
+    Vec_PtrForEachEntry( vBoundary, pObj, i )
+    {
+        if ( !pObj->fMarkA )
+        {
+            pObj->fMarkA = 1;
+            p->nBoundary++;
+        }
+    }
+    Vec_PtrFree( vBoundary );
+
+if ( fVerbose )
+{
+    printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d  Bound = %4d  ", 
+        Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary );
+PRT( "T", clock() - clk );
+}
+    return fStop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary )
+{
+    Abc_Obj_t * pObj0, * pObj1;
+    // return if the support is already computed
+    if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) )
+        return;
+    // mark as visited
+    pObj->fMarkB = 1;
+    // get the fanins
+    pObj0 = Abc_ObjFanin0(pObj);
+    pObj1 = Abc_ObjFanin1(pObj);
+    // solve for the fanins
+    Abc_NtkXyzCovers_rec( p, pObj0, vBoundary );
+    Abc_NtkXyzCovers_rec( p, pObj1, vBoundary );
+    // skip the node that spaced out
+    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||     // fanin is not ready
+         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||     // fanin is not ready
+         !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) )  // node's support or covers cannot be computed
+    {
+        // save the nodes of the future boundary
+        if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
+            Vec_PtrPush( vBoundary, pObj0 );
+        if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) )
+            Vec_PtrPush( vBoundary, pObj1 );
+        return;
+    }
+    // consider dropping the fanin supports
+//    Abc_NodeXyzDropData( p, pObj0 );
+//    Abc_NodeXyzDropData( p, pObj1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 )
+{
+    Vec_Int_t * vSupp;
+    int k0, k1;
+
+    assert( vSupp0 && vSupp1 );
+    Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
+    Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
+    Vec_IntClear( p->vPairs0 );
+    Vec_IntClear( p->vPairs1 );
+
+    vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize );
+    for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
+    {
+        if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
+        {
+            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
+            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
+            Vec_IntPush( p->vPairs0, k0 );
+            Vec_IntPush( p->vPairs1, k1 );
+            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
+            k0++; k1++;
+        }
+        else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
+        {
+            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
+            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
+            k0++;
+        }
+        else 
+        {
+            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
+            Vec_IntPush( vSupp, vSupp1->pArray[k1] );
+            k1++;
+        }
+    }
+    for ( ; k0 < vSupp0->nSize; k0++ )
+    {
+        Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
+        Vec_IntPush( vSupp, vSupp0->pArray[k0] );
+    }
+    for ( ; k1 < vSupp1->nSize; k1++ )
+    {
+        Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
+        Vec_IntPush( vSupp, vSupp1->pArray[k1] );
+    }
+/*
+    printf( "Zero : " );
+    for ( k0 = 0; k0 < vSupp0->nSize; k0++ )
+        printf( "%d ", vSupp0->pArray[k0] );
+    printf( "\n" );
+
+    printf( "One  : " );
+    for ( k1 = 0; k1 < vSupp1->nSize; k1++ )
+        printf( "%d ", vSupp1->pArray[k1] );
+    printf( "\n" );
+
+    printf( "Sum  : " );
+    for ( k0 = 0; k0 < vSupp->nSize; k0++ )
+        printf( "%d ", vSupp->pArray[k0] );
+    printf( "\n" );
+    printf( "\n" );
+*/
+    return vSupp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
+{
+    Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1;
+    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
+
+    if ( pObj0->fMarkA )  Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
+    if ( pObj1->fMarkA )  Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
+
+    // get the resulting support
+    vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
+    vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
+    vSupp  = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
+
+    // quit if support if too large
+    if ( vSupp->nSize > p->nFaninMax )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+   
+    // get the covers
+    pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
+    pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
+
+    // complement the first if needed
+    if ( !Abc_ObjFaninC0(pObj) )
+        pCover0 = pCov0;
+    else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+        pCover0 = pCov0->pNext;
+    else
+        pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
+
+    // complement the second if needed
+    if ( !Abc_ObjFaninC1(pObj) )
+        pCover1 = pCov1;
+    else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+        pCover1 = pCov1->pNext;
+    else
+        pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
+
+    // derive and minimize the cover (quit if too large)
+    if ( !Abc_NodeXyzProductEsop( p, pCover0, pCover1, vSupp->nSize ) )
+    {
+        pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
+        Min_CoverRecycle( p->pManMin, pCover );
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // minimize the cover
+    Min_EsopMinimize( p->pManMin );
+    pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
+
+    // quit if the cover is too large
+    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+    {
+        Min_CoverRecycle( p->pManMin, pCover );
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // count statistics
+    p->nSupps++;
+    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
+
+    // set the covers
+    assert( Abc_ObjGetSupp(pObj) == NULL );
+    Abc_ObjSetSupp( pObj, vSupp );
+    Abc_ObjSetCover2( pObj, pCover );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
+{
+    Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1;
+    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
+    int fCompl0, fCompl1;
+
+    if ( pObj0->fMarkA )  Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
+    if ( pObj1->fMarkA )  Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
+
+    // get the resulting support
+    vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
+    vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
+    vSupp  = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
+
+    // quit if support if too large
+    if ( vSupp->nSize > p->nFaninMax )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // get the complemented attributes
+    fCompl0 = Abc_ObjFaninC0(pObj);
+    fCompl1 = Abc_ObjFaninC1(pObj);
+   
+    // prepare the positive cover
+    pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
+    pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
+
+    // derive and minimize the cover (quit if too large)
+    if ( !pCover0 || !pCover1 )
+        pCoverP = NULL;
+    else if ( !Abc_NodeXyzProductSop( p, pCover0, pCover1, vSupp->nSize ) )
+    {
+        pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
+        Min_CoverRecycle( p->pManMin, pCoverP );
+        pCoverP = NULL;
+    }
+    else
+    {
+        Min_SopMinimize( p->pManMin );
+        pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
+        // quit if the cover is too large
+        if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax )
+        {
+            Min_CoverRecycle( p->pManMin, pCoverP );
+            pCoverP = NULL;
+        }
+    }
+   
+    // prepare the negative cover
+    pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
+    pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
+
+    // derive and minimize the cover (quit if too large)
+    if ( !pCover0 || !pCover1 )
+        pCoverN = NULL;
+    else if ( !Abc_NodeXyzUnionSop( p, pCover0, pCover1, vSupp->nSize ) )
+    {
+        pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
+        Min_CoverRecycle( p->pManMin, pCoverN );
+        pCoverN = NULL;
+    }
+    else
+    {
+        Min_SopMinimize( p->pManMin );
+        pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
+        // quit if the cover is too large
+        if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax )
+        {
+            Min_CoverRecycle( p->pManMin, pCoverN );
+            pCoverN = NULL;
+        }
+    }
+
+    if ( pCoverP == NULL && pCoverN == NULL )
+    {
+        Vec_IntFree( vSupp );
+        return 0;
+    }
+
+    // count statistics
+    p->nSupps++;
+    p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
+
+    // set the covers
+    assert( Abc_ObjGetSupp(pObj) == NULL );
+    Abc_ObjSetSupp( pObj, vSupp );
+    Abc_ObjSetCover( pObj, pCoverP, 0 );
+    Abc_ObjSetCover( pObj, pCoverN, 1 );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    int i, Val0, Val1;
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    if ( pCover0 == NULL || pCover1 == NULL )
+        return 1;
+
+    // go through the cube pairs
+    Min_CoverForEachCube( pCover0, pCube0 )
+    Min_CoverForEachCube( pCover1, pCube1 )
+    {
+        // go through the support variables of the cubes
+        for ( i = 0; i < p->vPairs0->nSize; i++ )
+        {
+            Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
+            Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
+            if ( (Val0 & Val1) == 0 )
+                break;
+        }
+        // check disjointness
+        if ( i < p->vPairs0->nSize )
+            continue;
+
+        if ( p->pManMin->nCubes >= p->nCubesMax )
+            return 0;
+
+        // create the product cube
+        pCube = Min_CubeAlloc( p->pManMin );
+
+        // add the literals
+        pCube->nLits = 0;
+        for ( i = 0; i < nSupp; i++ )
+        {
+            if ( p->vComTo0->pArray[i] == -1 )
+                Val0 = 3;
+            else
+                Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+
+            if ( p->vComTo1->pArray[i] == -1 )
+                Val1 = 3;
+            else
+                Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+
+            if ( (Val0 & Val1) == 3 )
+                continue;
+
+            Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
+            pCube->nLits++;
+        }
+        // add the cube to storage
+        while ( Min_EsopAddCube( p->pManMin, pCube ) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
+{
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
+{
+    Min_Cube_t * pCube, * pCube0, * pCube1;
+    int i, Val0, Val1;
+
+    // clean storage
+    Min_ManClean( p->pManMin, nSupp );
+    if ( pCover0 )
+    {
+        Min_CoverForEachCube( pCover0, pCube0 )
+        {
+            // create the cube
+            pCube = Min_CubeAlloc( p->pManMin );
+            pCube->nLits = 0;
+            for ( i = 0; i < p->vComTo0->nSize; i++ )
+            {
+                if ( p->vComTo0->pArray[i] == -1 )
+                    continue;
+                Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+                if ( Val0 == 3 )
+                    continue;
+                Min_CubeXorVar( pCube, i, Val0 ^ 3 );
+                pCube->nLits++;
+            }
+            if ( p->pManMin->nCubes >= p->nCubesMax )
+                return 0;
+            // add the cube to storage
+            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+        }
+    }
+    if ( pCover1 )
+    {
+        Min_CoverForEachCube( pCover1, pCube1 )
+        {
+            // create the cube
+            pCube = Min_CubeAlloc( p->pManMin );
+            pCube->nLits = 0;
+            for ( i = 0; i < p->vComTo1->nSize; i++ )
+            {
+                if ( p->vComTo1->pArray[i] == -1 )
+                    continue;
+                Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+                if ( Val1 == 3 )
+                    continue;
+                Min_CubeXorVar( pCube, i, Val1 ^ 3 );
+                pCube->nLits++;
+            }
+            if ( p->pManMin->nCubes >= p->nCubesMax )
+                return 0;
+            // add the cube to storage
+            while ( Min_EsopAddCube( p->pManMin, pCube ) );
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
+{
+    return 1;
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
new file mode 100644
index 00000000..22950bfd
--- /dev/null
+++ b/src/opt/xyz/xyzInt.h
@@ -0,0 +1,631 @@
+/**CFile****************************************************************
+
+  FileName    [xyzInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Min_Man_t_  Min_Man_t;
+typedef struct Min_Cube_t_ Min_Cube_t;
+
+struct Min_Man_t_
+{
+    int               nVars;          // the number of vars
+    int               nWords;         // the number of words
+    Extra_MmFixed_t * pMemMan;        // memory manager for cubes
+    // temporary cubes
+    Min_Cube_t *      pOne0;          // tautology cube
+    Min_Cube_t *      pOne1;          // tautology cube
+    Min_Cube_t *      pTriv0[2];      // trivial cube
+    Min_Cube_t *      pTriv1[2];      // trivial cube
+    Min_Cube_t *      pTemp;          // cube for computing the distance
+    Min_Cube_t *      pBubble;        // cube used as a separator
+    // temporary storage for the new cover
+    int               nCubes;         // the number of cubes
+    Min_Cube_t **     ppStore;        // storage for cubes by number of literals
+};
+
+struct Min_Cube_t_
+{
+    Min_Cube_t *      pNext;          // the pointer to the next cube in the cover
+    unsigned          nVars    : 10;  // the number of variables
+    unsigned          nWords   : 12;  // the number of machine words
+    unsigned          nLits    : 10;  // the number of literals in the cube
+    unsigned          uData[1];       // the bit-data for the cube
+};
+
+
+// iterators through the entries in the linked lists of cubes
+#define Min_CoverForEachCube( pCover, pCube )                   \
+    for ( pCube = pCover;                                       \
+          pCube;                                                \
+          pCube = pCube->pNext )
+#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )       \
+    for ( pCube = pCover,                                       \
+          pCube2 = pCube? pCube->pNext: NULL;                   \
+          pCube;                                                \
+          pCube = pCube2,                                       \
+          pCube2 = pCube? pCube->pNext: NULL )
+#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev )       \
+    for ( pCube = pCover,                                       \
+          ppPrev = &(pCover);                                   \
+          pCube;                                                \
+          ppPrev = &pCube->pNext,                               \
+          pCube = pCube->pNext )
+
+// macros to get hold of bits and values in the cubes
+static inline int  Min_CubeHasBit( Min_Cube_t * p, int i )              { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0;     }
+static inline void Min_CubeSetBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] |= (1<<((i) & 31));                 }
+static inline void Min_CubeXorBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] ^= (1<<((i) & 31));                 }
+static inline int  Min_CubeGetVar( Min_Cube_t * p, int Var )            { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
+static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31));     }
+
+/*=== xyzMinEsop.c ==========================================================*/
+extern void         Min_EsopMinimize( Min_Man_t * p );
+extern int          Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+/*=== xyzMinSop.c ==========================================================*/
+extern void         Min_SopMinimize( Min_Man_t * p );
+extern int          Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+/*=== xyzMinMan.c ==========================================================*/
+extern Min_Man_t *  Min_ManAlloc( int nVars );
+extern void         Min_ManClean( Min_Man_t * p, int nSupp );
+extern void         Min_ManFree( Min_Man_t * p );
+/*=== xyzMinUtil.c ==========================================================*/
+extern void         Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
+extern void         Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
+extern void         Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
+extern void         Min_CoverCheck( Min_Man_t * p );
+extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
+extern void         Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
+extern int          Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
+    pCube->pNext  = NULL;
+    pCube->nVars  = p->nVars;
+    pCube->nWords = p->nWords;
+    pCube->nLits  = 0;
+    memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube representing elementary var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
+{
+    Min_Cube_t * pCube;
+    pCube = Min_CubeAlloc( p );
+    Min_CubeXorBit( pCube, iVar*2+fCompl );
+    pCube->nLits = 1;
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
+{
+    Min_Cube_t * pCube;
+    pCube = Min_CubeAlloc( p );
+    memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the cube cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2;
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+        Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubeCountLits( Min_Cube_t * pCube )
+{
+    unsigned uData;
+    int Count = 0, i, w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Count++;
+    }
+    return Count;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
+{
+    unsigned uData;
+    int i, w;
+    Vec_IntClear( vLits );
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Vec_IntPush( vLits, w*16 + i/2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    int Count = 0;
+    Min_CoverForEachCube( pCover, pCube )
+        Count++;
+    return Count;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    unsigned uData;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] & pCube1->uData[i];
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( uData != 0x55555555 )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the disjoint variables of the two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
+{
+    unsigned uData;
+    int i, w;
+    Vec_IntClear( vVars );
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        uData  = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
+        uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
+        if ( uData == 0 )
+            continue;
+        for ( i = 0; i < 32; i += 2 )
+            if ( uData & (1 << i) )
+                Vec_IntPush( vVars, w*16 + i/2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
+{
+    unsigned uData;
+    int i, fFound = 0;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] ^ pCube1->uData[i];
+        if ( uData == 0 )
+        {
+            if ( pTemp ) pTemp->uData[i] = 0;
+            continue;
+        }
+        if ( fFound )
+            return 0;
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( (uData & (uData-1)) > 0 ) // more than one 1
+            return 0;
+        if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
+        fFound = 1;
+    }
+    if ( fFound == 0 )
+    {
+        printf( "\n" );
+        Min_CubeWrite( stdout, pCube0 );
+        Min_CubeWrite( stdout, pCube1 );
+        printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are disjoint.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
+{
+    unsigned uData;//, uData2;
+    int i, k, Var0 = -1, Var1 = -1;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+    {
+        uData = pCube0->uData[i] ^ pCube1->uData[i];
+        if ( uData == 0 )
+            continue;
+        if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
+            return 0;
+        uData = (uData | (uData >> 1)) & 0x55555555;
+        if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
+            return 0;
+        for ( k = 0; k < 32; k += 2 )
+            if ( uData & (1 << k) )
+            {
+                if ( Var0 == -1 )
+                    Var0 = 16 * i + k/2;
+                else if ( Var1 == -1 )
+                    Var1 = 16 * i + k/2;
+                else
+                    return 0;
+            }
+        /*
+        if ( Var0 >= 0 )
+        {
+            uData &= 0xFFFF;
+            uData2 = (uData >> 16);
+            if ( uData && uData2 )
+                return 0;
+            if ( uData )
+            {
+            }
+            uData }= uData2;
+            uData &= 0x
+        }
+        */
+    }
+    if ( Var0 >= 0 && Var1 >= 0 )
+    {
+        *pVar0 = Var0;
+        *pVar1 = Var1;
+        return 1;
+    }
+    if ( Var0 == -1 || Var1 == -1 )
+    {
+        printf( "\n" );
+        Min_CubeWrite( stdout, pCube0 );
+        Min_CubeWrite( stdout, pCube1 );
+        printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    Min_Cube_t * pCube;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    pCube = Min_CubeAlloc( p );
+    for ( i = 0; i < p->nWords; i++ )
+        pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
+    pCube->nLits = Min_CubeCountLits( pCube );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    Min_Cube_t * pCube;
+    int i;
+    assert( pCube0->nVars == pCube1->nVars );
+    pCube = Min_CubeAlloc( p );
+    for ( i = 0; i < p->nWords; i++ )
+        pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
+    pCube->nLits = Min_CubeCountLits( pCube );
+    return pCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the produce of two cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    int i;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+        if ( pCube0->uData[i] != pCube1->uData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pCube1 is contained in pCube0, bitwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
+{
+    int i;
+    for ( i = 0; i < (int)pCube0->nWords; i++ )
+        if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the cube into the result of merging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
+{
+    int w;
+    for ( w = 0; w < (int)pCube->nWords; w++ )
+    {
+        pCube->uData[w]  =  pCube->uData[w] ^ pDist->uData[w];
+        pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2, * pThis;
+    if ( pCover == NULL )
+    {
+        Min_ManClean( p, p->nVars );
+        return;
+    }
+    Min_ManClean( p, pCover->nVars );
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        // go through the linked list
+        Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+            if ( Min_CubesAreEqual( pCube, pThis ) )
+            {
+                Min_CubeRecycle( p, pCube );
+                break;
+            }
+        if ( pThis != NULL )
+            continue;
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the cube is equal or dist1 or contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
+{
+    Min_Cube_t * pCube;
+    int i;
+    // check identity
+    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
+        if ( Min_CubesAreEqual( pCube, pNew ) )
+            return 1;
+    // check containment
+    for ( i = 0; i < (int)pNew->nLits; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+            if ( Min_CubeIsContained( pCube, pNew ) )
+                return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the cube is equal or dist1 or contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
+{
+    Min_Cube_t * pCube;
+    Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
+        if ( Min_CubesDistOne( pCube, pNew, NULL ) )
+            return pCube;
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMan.c b/src/opt/xyz/xyzMan.c
new file mode 100644
index 00000000..844e8c13
--- /dev/null
+++ b/src/opt/xyz/xyzMan.c
@@ -0,0 +1,144 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Decomposition manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
+{
+    Xyz_Man_t * pMan;
+    Xyz_Obj_t * pMem;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( pNtk->pManCut == NULL );
+
+    // start the manager
+    pMan = ALLOC( Xyz_Man_t, 1 );
+    memset( pMan, 0, sizeof(Xyz_Man_t) );
+    pMan->nFaninMax = nFaninMax;
+    pMan->nCubesMax = 2 * pMan->nFaninMax;
+    pMan->nWords    = Abc_BitWordNum( nFaninMax * 2 );
+
+    // get the cubes
+    pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
+    pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
+    pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
+    pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
+
+    // allocate memory for object structures
+    pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    // allocate storage for the pointers to the memory
+    pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
+    Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
+    // create the cube manager
+    pMan->pManMin = Min_ManAlloc( nFaninMax );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Xyz_ManFree( Xyz_Man_t * p )
+{
+    Vec_Int_t * vSupp;
+    int i;
+    for ( i = 0; i < p->vObjStrs->nSize; i++ )
+    {
+        vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
+        if ( vSupp ) Vec_IntFree( vSupp );
+    }
+
+    Min_ManFree( p->pManMin );
+    Vec_PtrFree( p->vObjStrs );
+    Vec_IntFree( p->vFanCounts );
+    Vec_IntFree( p->vTriv0 );
+    Vec_IntFree( p->vTriv1 );
+    Vec_IntFree( p->vComTo0 );
+    Vec_IntFree( p->vComTo1 );
+    Vec_IntFree( p->vPairs0 );
+    Vec_IntFree( p->vPairs1 );
+    free( p->pMemory );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drop the covers at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+    {
+        Vec_IntFree( Abc_ObjGetSupp(pObj) );
+        Abc_ObjSetSupp( pObj, NULL );
+        Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
+        Abc_ObjSetCover2( pObj, NULL );
+        p->nSupps--;
+    }
+    Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
new file mode 100644
index 00000000..114e28a6
--- /dev/null
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -0,0 +1,277 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinEsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [ESOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_EsopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_EsopRewrite( p );
+        nIter++;
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
+    int nPairs = 0;
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars - 1 )
+        Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        // Exorlink-2:
+        // A{v00}     B{v01}      +  A{v10}     B{v11}     =
+        // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} =
+        // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11}
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // derive the first pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= (v00 != 3);
+        pCube->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= (v11 != 3);
+        pThis->nLits += ((v01 ^ v11) != 3);
+
+        // add the cubes
+        nCubesOld = p->nCubes;
+        while ( Min_EsopAddCube( p, pCube ) );
+        while ( Min_EsopAddCube( p, pThis ) );
+        // check if the cubes were absorbed
+        if ( p->nCubes < nCubesOld + 2 )
+            continue;
+
+        // pull out both cubes
+        assert( pThis == p->ppStore[pThis->nLits] );
+        p->ppStore[pThis->nLits] = pThis->pNext;
+        assert( pCube == p->ppStore[pCube->nLits] );
+        p->ppStore[pCube->nLits] = pCube->pNext;
+        p->nCubes -= 2;
+
+        // derive the second pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= ((v00 ^ v10) != 3);
+        pCube->nLits += (v00 != 3);
+        Min_CubeXorVar( pCube, Var1, v11 );
+        pCube->nLits -= (v01 != 3);
+        pCube->nLits += ((v01 ^ v11) != 3);
+
+        Min_CubeXorVar( pThis, Var0, v00 );
+        pThis->nLits -= (v10 != 3);
+        pThis->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= ((v01 ^ v11) != 3);
+        pThis->nLits += (v11 != 3);
+
+        // add them anyhow
+        while ( Min_EsopAddCube( p, pCube ) );
+        while ( Min_EsopAddCube( p, pThis ) );
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description [If the distance one cube is found, returns the transformed
+  cube. If there is no distance one, adds the given cube to storage.
+  Do not forget to clean the storage!]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis, ** ppPrev;
+    // try to find the identical cube
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubeRecycle( p, pCube );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 0;
+        }
+    }
+    // find a distance-1 cube if it exists
+    if ( pCube->nLits < pCube->nVars )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits++;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    if ( pCube->nLits > 0 )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
new file mode 100644
index 00000000..423564c1
--- /dev/null
+++ b/src/opt/xyz/xyzMinMan.c
@@ -0,0 +1,112 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Man_t * Min_ManAlloc( int nVars )
+{
+    Min_Man_t * pMan;
+    // start the manager
+    pMan = ALLOC( Min_Man_t, 1 );
+    memset( pMan, 0, sizeof(Min_Man_t) );
+    pMan->nVars   = nVars;
+    pMan->nWords  = Abc_BitWordNum( nVars * 2 );
+    pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
+    // allocate storage for the temporary cover
+    pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 );
+    // create tautology cubes
+    Min_ManClean( pMan, nVars );
+    pMan->pOne0  = Min_CubeAlloc( pMan );
+    pMan->pOne1  = Min_CubeAlloc( pMan );
+    pMan->pTemp  = Min_CubeAlloc( pMan );
+    pMan->pBubble = Min_CubeAlloc( pMan );  pMan->pBubble->uData[0] = 0;
+    // create trivial cubes
+    Min_ManClean( pMan, 1 );
+    pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManClean( Min_Man_t * p, int nSupp )
+{
+    // set the size of the cube manager
+    p->nVars  = nSupp;
+    p->nWords = Abc_BitWordNum(2*nSupp);
+    // clean the storage
+    memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
+    p->nCubes = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManFree( Min_Man_t * p )
+{
+    Extra_MmFixedStop ( p->pMemMan, 0 );
+    free( p->ppStore );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
new file mode 100644
index 00000000..1c5951fe
--- /dev/null
+++ b/src/opt/xyz/xyzMinSop.c
@@ -0,0 +1,341 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinSop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_SopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_SopRewrite( p );
+        nIter++;
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    Min_Cube_t * pTemp;
+    int v00, v01, v10, v11, Var0, Var1, Index;
+    int nPairs = 0;
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+        assert( v00 != v10 && v01 != v11 );
+        assert( v00 != 3   || v01 != 3 );
+        assert( v10 != 3   || v11 != 3 );
+
+        // skip the case when rewriting is impossible
+        if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+            continue;
+
+        // if one of them does not have DC lit, move it
+        if ( v00 != 3 && v01 != 3 )
+        {
+            pTemp = pCube; pCube = pThis; pThis = pTemp;
+            Index = v00; v00 = v10; v10 = Index;
+            Index = v01; v01 = v11; v11 = Index;
+        }
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // make sure the first cube has first var DC
+        if ( v00 != 3 )
+        {
+            assert( v01 == 3 );
+            Index = Var0; Var0 = Var1; Var1 = Index;
+            Index = v00; v00 = v01; v01 = Index;
+            Index = v10; v10 = v11; v11 = Index;
+        }
+
+        // consider both cases: both have DC lit
+        if ( v00 == 3 && v11 == 3 )
+        {
+            assert( v01 != 3 && v10 != 3 );
+            // try two reduced cubes
+
+        }
+        else // the first cube has DC lit
+        {
+            assert( v01 != 3 && v10 != 3 && v11 != 3 );
+            // try reduced and expanded cube
+        }
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    return 1;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, * pCubeNew;
+    int i;
+    for ( i = p->nVars; i >= 0; i-- )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCube( pCube->pNext, pCube2 )
+        {
+            assert( pCube->nLits == pCube2->nLits );
+            if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+                continue;
+            pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+            assert( pCubeNew->nLits == pCube->nLits - 1 );
+            pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+            p->ppStore[pCubeNew->nLits] = pCubeNew;
+            p->nCubes++;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_SopContain( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, * pCube2, ** ppPrev;
+    int i, k;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
+        {
+            if ( !Min_CubesAreEqual( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+        for ( k = i + 1; k <= p->nVars; k++ )
+        Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
+        {
+            if ( !Min_CubeIsContained( pCube, pCube2 ) )
+                continue;
+            *ppPrev = pCube2->pNext;
+            Min_CubeRecycle( p, pCube2 );
+            p->nCubes--;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
+{
+     Vec_Int_t * vVars;
+     Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
+     int Num, Value, i;
+
+     // get the variables
+     vVars = Vec_IntAlloc( 100 );
+    // create the tautology cube
+     pCover = Min_CubeAlloc( p );
+     // sharp it with all cubes
+     Min_CoverForEachCube( pSharp, pCube )
+     Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
+     {
+        if ( Min_CubesDisjoint( pThis, pCube ) )
+            continue;
+        // remember the next pointer
+        pNext = pThis->pNext;
+        // get the variables, in which pThis is '-' while pCube is fixed
+        Min_CoverGetDisjVars( pThis, pCube, vVars );
+        // generate the disjoint cubes
+        pReady = pThis;
+        Vec_IntForEachEntryReverse( vVars, Num, i )
+        {
+            // correct the literal
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
+            if ( i == 0 )
+                break;
+            // create the new cube and clean this value
+            Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
+            pReady = Min_CubeDup( p, pReady );
+            Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
+            // add to the cover
+            *ppPrev = pReady;
+            ppPrev = &pReady->pNext;
+        }
+        pThis = pReady;
+        pThis->pNext = pNext;
+     }
+     Vec_IntFree( vVars );
+
+     // perform dist-1 merge and contain
+     Min_CoverExpandRemoveEqual( p, pCover );
+     Min_SopDist1Merge( p );
+     Min_SopContain( p );
+     return Min_CoverCollect( p, p->nVars );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
new file mode 100644
index 00000000..0aebb815
--- /dev/null
+++ b/src/opt/xyz/xyzMinUtil.c
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [xyzMinUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyzInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
+{
+    int i;
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeHasBit(pCube, i*2) )
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "-" );
+            else
+                fprintf( pFile, "0" );
+        }
+        else
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "1" );
+            else
+                fprintf( pFile, "?" );
+        }
+    fprintf( pFile, " 1\n" );
+//    fprintf( pFile, " %d\n", pCube->nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
+{
+    char Buffer[1000];
+    Min_Cube_t * pCube;
+    FILE * pFile;
+    int i;
+    sprintf( Buffer, "%s.esop", pName );
+    for ( i = strlen(Buffer) - 1; i >= 0; i-- )
+        if ( Buffer[i] == '<' || Buffer[i] == '>' )
+            Buffer[i] = '_';
+    pFile = fopen( Buffer, "w" );
+    fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
+    fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
+    fprintf( pFile, ".o %d\n", 1 );
+    fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
+    if ( fEsop ) fprintf( pFile, ".type esop\n" );
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    fprintf( pFile, ".e\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+            assert( i == (int)pCube->nLits );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the cover from the sorted structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
+{
+    Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
+    Min_Cube_t * pCube, * pCube2;
+    int i;
+    for ( i = 0; i <= nSuppSize; i++ )
+    {
+        Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
+        {
+            assert( i == (int)pCube->nLits );
+            *ppTail = pCube; 
+            ppTail = &pCube->pNext;
+        }
+    }
+    *ppTail = NULL;
+    return pCov;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2;
+    Min_ManClean( p, p->nVars );
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    int i, Counter;
+    if ( pCover == NULL )
+        return 0;
+    // clean the cube
+    for ( i = 0; i < (int)pCover->nWords; i++ )
+        p->pTemp->uData[i]  = ~((unsigned)0);
+    // add the bit data
+    Min_CoverForEachCube( pCover, pCube )
+        for ( i = 0; i < (int)pCover->nWords; i++ )
+            p->pTemp->uData[i] &= pCube->uData[i];
+    // count the vars
+    Counter = 0;
+    for ( i = 0; i < (int)pCover->nVars; i++ )
+        Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
new file mode 100644
index 00000000..6c0a63f3
--- /dev/null
+++ b/src/opt/xyz/xyzTest.c
@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+  FileName    [xyzTest.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Testing procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "xyz.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index 99f1fafe..497087fb 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -71,6 +71,11 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin
 
     // start the file
     pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        return;
+    }
     fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
     fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
 
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index efc183a3..74503a2b 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -188,7 +188,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
             case CSAT_BAND:
                 if ( nofi < 1 )
                     { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi );
+                pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
                 break;
             case CSAT_BNAND:
                 if ( nofi < 1 )
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 4801e340..673fcad7 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -104,7 +104,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     Fraig_Man_t * p;
 
     // set the random seed for simulation
-    srand( 0xFEEDDEAF );
+//    srand( 0xFEEDDEAF );
+    srand( 0xDEADCAFE );
 
     // set parameters for equivalence checking
     if ( pParams == NULL )
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index e585e8ab..bc60e4e9 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -1049,6 +1049,26 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
     assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    Msat_IntVecClear( p->vProj );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  0^fCompT) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  0^fCompE) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  1) );
+    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+    assert( RetValue );
+    Msat_IntVecClear( p->vProj );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT,  1^fCompT) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE,  1^fCompE) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF,  0) );
+    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+    assert( RetValue );
 }
 
 
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 92311e48..ed228b33 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         if ( nBackTrackLimit > 0 )
             break;
         // if the runtime limit is exceeded, quit the restart loop
-        if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
             break;
     }
     Msat_SolverCancelUntil( p, 0 );
author	Alan Mishchenko <alanmi@berkeley.edu>	2005-12-22 08:01:00 -0800
committer	Alan Mishchenko <alanmi@berkeley.edu>	2005-12-22 08:01:00 -0800
commit	457e243e588e7ed5f39251784335e254a0c9e711 (patch)
tree	751d7b416e66e416983760d0b95d79bb24371309 /src
parent	37f19d8dfb17605abab38110beec5fc17413e635 (diff)
download	abc-457e243e588e7ed5f39251784335e254a0c9e711.tar.gz abc-457e243e588e7ed5f39251784335e254a0c9e711.tar.bz2 abc-457e243e588e7ed5f39251784335e254a0c9e711.zip