Version abc80705

23 files changed, 520 insertions, 54 deletions

diff --git a/abc.rc b/abc.rc
index 526a08de..e0304667 100644
--- a/abc.rc
+++ b/abc.rc
@@ -2,7 +2,7 @@
 #set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
 #set checkread     # checks new networks after reading from file
-set backup        # saves backup networks retrived by "undo" and "recall"
+#set backup        # saves backup networks retrived by "undo" and "recall"
 set savesteps 1   # sets the maximum number of backup networks to save 
 set progressbar   # display the progress bar
 
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index bf109b17..5c742f5d 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -140,6 +140,8 @@ extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
+extern int             Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
+extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index fc71f936..e3e6bfe1 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -20,6 +20,7 @@
 
 #include "cnf.h"
 #include "satSolver.h"
+#include "zlib.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -237,7 +238,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
+void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
     FILE * pFile;
     int * pLit, * pStop, i;
@@ -270,6 +271,39 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
+{
+    gzFile pFile;
+    int * pLit, * pStop, i;
+    pFile = gzopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
+        return;
+    }
+    gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
+    gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
+            gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
+        gzprintf( pFile, "0\n" );
+    }
+    gzprintf( pFile, "\n" );
+    gzclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
 {
     sat_solver * pSat;
@@ -379,6 +413,63 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver * pSat = p;
+    Aig_Obj_t * pObj;
+    int i, Lit;
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+    {
+        Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms polarity of the internal veriables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf )
+{
+    Aig_Obj_t * pObj;
+    int * pVarToPol;
+    int i, iVar;
+    // create map from the variable number to its polarity
+    pVarToPol = CALLOC( int, pCnf->nVars );
+    Aig_ManForEachObj( pCnf->pMan, pObj, i )
+        if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 )
+            pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
+    // transform literals
+    for ( i = 0; i < pCnf->nLiterals; i++ )
+    {
+        iVar = lit_var(pCnf->pClauses[0][i]);
+        assert( iVar < pCnf->nVars );
+        if ( pVarToPol[iVar] )
+            pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] );
+    }
+    free( pVarToPol );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index cd47cb58..3738fee5 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -140,6 +140,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     else
     {
         pCutBest = pObj->pData;
+//        assert( pCutBest->nFanins > 0 );
         assert( pCutBest->Cost < 127 );
         aArea = pCutBest->Cost;
         Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index e9e7ad9c..6721634e 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -282,7 +282,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraCec.c ========================================================*/
-extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
 extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index d67839a4..e5940992 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
 {
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -53,6 +53,10 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     // derive CNF
     pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
 //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+
+    if ( fFlipBits ) 
+        Cnf_DataTranformPolarity( pCnf );
+
     // convert into SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     if ( pSat == NULL )
@@ -60,12 +64,27 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
         Cnf_DataFree( pCnf );
         return 1;
     }
-    // add the OR clause for the outputs
-    if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+
+
+    if ( fAndOuts )
     {
-        sat_solver_delete( pSat );
-        Cnf_DataFree( pCnf );
-        return 1;
+        // assert each output independently
+        if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+        {
+            sat_solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+    }
+    else
+    {
+        // add the OR clause for the outputs
+        if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+        {
+            sat_solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
     }
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
     Cnf_DataFree( pCnf );
@@ -160,7 +179,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
 
     // if SAT only, solve without iteration
 clk = clock();
-    RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 0 );
+    RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 );
     if ( fVerbose )
     {
         printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
@@ -228,7 +247,7 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     {
 clk = clock();
-        RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 0 );
+        RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 );
         if ( fVerbose )
         {
             printf( "Final SAT:            Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ab076472..1935bb7f 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -437,6 +437,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
  
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
+    p->pPars->nBTLimitNode = 0;
     // derive and refine e-classes using K initialized frames
     if ( fUseOldSimulation )
     {
@@ -529,6 +530,7 @@ p->timeTrav += clock() - clk2;
             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
         else
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//        Cnf_DataTranformPolarity( pCnf );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index e1d3edd1..b0f3b1fb 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -377,6 +377,7 @@ extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
 extern ABC_DLL Vec_Vec_t *     Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose );
+extern ABC_DLL void            Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose );
 extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ManIsComb( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ModelCombLeafNum( Ntl_Mod_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index f6f1ebb2..f4d33cf1 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -649,9 +649,9 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
     if ( pAig->vClockDoms )
     {
         if ( Vec_VecSize(pAig->vClockDoms) == 0 )
-            printf( "Clock domains are small. Seq synthesis is not performed.\n" );
+            printf( "Register classes are small. Seq synthesis is not performed.\n" );
         else
-            printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) );
+            printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
         printf( "\n" );
     }
     return pAig;
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 6449cc33..bd39956e 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -320,6 +320,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     // perform SCL for the given design
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
+    if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -353,6 +355,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // perform SCL for the given design
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
+    if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 4fd1762c..51f3b818 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -403,7 +403,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         printf( "The number of register clases = %d.\n", nClasses );
         for ( i = 0; i <= ClassMax; i++ )
             if ( pClassNums[i] )
-                printf( "%d:%d  ", i, pClassNums[i] );
+                printf( "(%d, %d)  ", i, pClassNums[i] );
         printf( "\n" );
     }
     // skip if there is only one class
@@ -416,7 +416,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
             vPart = Vec_IntStartNatural( Vec_IntSize(pMan->vRegClasses) );
             Vec_PtrPush( vParts, vPart );
         }
-        printf( "There is only one clock domain with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
+        printf( "There is only one class with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
         free( pClassNums );
         return (Vec_Vec_t *)vParts;
     }
@@ -434,12 +434,13 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         Vec_PtrPush( vParts, vPart );
     }
     free( pClassNums );
+    Vec_VecSort( (Vec_Vec_t *)vParts, 1 );
     // report the selected classes
     if ( fVerbose )
     {
         printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) );
         Vec_PtrForEachEntry( vParts, vPart, i )
-            printf( "%d:%d  ", i, Vec_IntSize(vPart) );
+            printf( "(%d, %d)  ", i, Vec_IntSize(vPart) );
         printf( "\n" );
     }
     return (Vec_Vec_t *)vParts;
@@ -447,6 +448,57 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
 
 /**Function*************************************************************
 
+  Synopsis    [Filter register clases using clock-domain information.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, k, nOmitted, nTotal;
+    if ( pAig->pReprs == NULL )
+        return;
+    assert( pAig->nRegs > 0 );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    k = 0;
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        pObj->PioNum = k++;
+    // consider equivalences
+    nOmitted = nTotal = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pRepr = pAig->pReprs[pObj->Id];
+        if ( pRepr == NULL )
+            continue;
+        nTotal++;
+        assert( Aig_ObjIsPi(pObj) );
+        assert( Aig_ObjIsPi(pRepr) || Aig_ObjIsConst1(pRepr) );
+        if ( Aig_ObjIsConst1(pRepr) )
+            continue;
+        assert( pObj->PioNum >= 0 && pRepr->PioNum >= 0 );
+        // remove equivalence if they belong to different classes
+        if ( Vec_IntEntry( vRegClasses, pObj->PioNum ) == 
+             Vec_IntEntry( vRegClasses, pRepr->PioNum ) )
+             continue;
+         pAig->pReprs[pObj->Id] = NULL;
+         nOmitted++;
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    if ( fVerbose )
+        printf( "Omitted %d (out of %d) equivs due to register class mismatch.\n", 
+            nOmitted, nTotal );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of CIs in the model.]
 
   Description []
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 64508474..fc56b387 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -589,14 +589,14 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                // it may happen that a box-input (CO) was already marked as visited
-                // when some other box-input of the same box was visited - here we undo this
                 iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId );
-                if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) )
-                    Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox );
-                Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival );
                 if ( iBox >= 0 ) // this CO is an input of the box
                 {
+                    // it may happen that a box-input (CO) was already marked as visited
+                    // when some other box-input of the same box was visited - here we undo this
+                    if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) )
+                        Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox );
+                    Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival );
                     Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
@@ -673,14 +673,14 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                // it may happen that a box-output (CI) was already marked as visited
-                // when some other box-output of the same box was visited - here we undo this
                 iBox = Tim_ManBoxForCi( pManTime, pTemp->PioId );
-                if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) )
-                    Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox );
-                Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired );
                 if ( iBox >= 0 ) // this CI is an output of the box
                 {
+                    // it may happen that a box-output (CI) was already marked as visited
+                    // when some other box-output of the same box was visited - here we undo this
+                    if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) )
+                        Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox );
+                    Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired );
                     Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( pManTime, iBox );
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index afc4a34a..ae8d02ec 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -412,7 +412,7 @@ int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 9cb7a855..09ea8b16 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -589,6 +589,7 @@ extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * p
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsIterNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
 extern ABC_DLL bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 8759500b..e83bd132 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -558,6 +558,33 @@ Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll )
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of logic nodes.]
+
+  Description [Collects only the internal nodes, leaving CIs and CO.
+  However it marks with the current TravId both CIs and COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsIterNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots )
+{
+    Vec_Ptr_t * vNodes, * vStack;
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 1000 );
+    vStack = Vec_PtrAlloc( 1000 );
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pObj)) )
+            Abc_NtkDfs_iter( vStack, Abc_ObjRegular(pObj), vNodes );
+    Vec_PtrFree( vStack );
+    return vNodes;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ae1c110f..2c34ed67 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -105,6 +105,7 @@ static int Abc_CommandReach          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCone           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandNode           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTopmost        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTopAnd         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -361,6 +362,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "topand",        Abc_CommandTopAnd,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "trim",          Abc_CommandTrim,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
@@ -6277,6 +6279,91 @@ usage:
   Description []
                
   SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( stdout, "Currently can only works for combinational circuits.\n" );
+        return 0;
+    } 
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "Currently expects a single-output miter.\n" );
+        return 0;
+    } 
+    if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) )
+    {
+        fprintf( stdout, "The PO driver is complemented. AND-decomposition is impossible.\n" );
+        return 0;
+    } 
+    if ( !Abc_ObjIsNode(Abc_ObjChild0(Abc_NtkPo(pNtk, 0))) )
+    {
+        fprintf( stdout, "The PO driver is not a node. AND-decomposition is impossible.\n" );
+        return 0;
+    } 
+    pNtkRes = Abc_NtkTopAnd( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "The command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: topand [-h]\n" );
+    fprintf( pErr, "\t         AND-decomposition of single-output combinational miter\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tname   : the node name\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
  
   SeeAlso     []
 
@@ -13997,7 +14084,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14097,7 +14184,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat && fMiter )
-        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, fVerbose );
+        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
     else
         Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
 
@@ -14651,12 +14738,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
+    int fFlipBits;
+    int fAndOuts;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14664,11 +14753,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fFlipBits  = 0;
+    fAndOuts   = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14694,6 +14785,12 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
+        case 'f':
+            fFlipBits ^= 1;
+            break;
+        case 'a':
+            fAndOuts ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -14714,12 +14811,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     } 
+/*
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
         fprintf( stdout, "Currently expects a single-output miter.\n" );
         return 0;
     } 
- 
+*/
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
@@ -14727,7 +14825,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -14760,11 +14858,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" );
+    fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
+    fprintf( pErr, "\t-f     : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" );  
+    fprintf( pErr, "\t-a     : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d89ee618..2a234b68 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -932,9 +932,9 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 {
-    Vec_Ptr_t * vMapped;
+    Vec_Ptr_t * vMapped = NULL;
     Aig_Man_t * pMan;
-    Cnf_Man_t * pManCnf;
+    Cnf_Man_t * pManCnf = NULL;
     Cnf_Dat_t * pCnf;
     Abc_Ntk_t * pNtkNew = NULL;
     assert( Abc_NtkIsStrash(pNtk) );
@@ -954,13 +954,14 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 
     // derive CNF
     pCnf = Cnf_Derive( pMan, 0 );
-    pManCnf = Cnf_ManRead();
-
+    Cnf_DataTranformPolarity( pCnf );
+/*
     // write the network for verification
+    pManCnf = Cnf_ManRead();
     vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
     pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
     Vec_PtrFree( vMapped );
-
+*/
     // write CNF into a file
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
     Cnf_DataFree( pCnf );
@@ -982,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -990,7 +991,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     assert( Abc_NtkLatchNum(pNtk) == 0 );
     assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fFlipBits, fAndOuts, fVerbose ); 
     pNtk->pModel = pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 084f6a6c..ad09f084 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -443,7 +443,7 @@ Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int Leve
 Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
 {
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObjNew, * pPoNew;
+    Abc_Obj_t * pObjNew, * pObjPo;
     int LevelCut;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCoNum(pNtk) == 1 );
@@ -458,10 +458,10 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut );
     pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) );
     // add the PO node and name
-    pPoNew = Abc_NtkCreatePo(pNtkNew);
-    Abc_ObjAddFanin( pPoNew, pObjNew );
+    pObjPo = Abc_NtkCreatePo(pNtkNew);
+    Abc_ObjAddFanin( pObjPo, pObjNew );
     Abc_NtkAddDummyPiNames( pNtkNew );
-    Abc_ObjAssignName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL );
+    Abc_ObjAssignName( pObjPo, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -473,6 +473,131 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Vec_CompareNodeIds( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    if ( Abc_ObjRegular(*pp1)->Id < Abc_ObjRegular(*pp2)->Id )
+        return -1;
+    if ( Abc_ObjRegular(*pp1)->Id > Abc_ObjRegular(*pp2)->Id ) //
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the large supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetSuper( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vSuper, * vFront;
+    Abc_Obj_t * pAnd, * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pNode) && !Abc_ObjIsComplement(pNode) );
+    vSuper = Vec_PtrAlloc( 100 ); 
+    // explore the frontier
+    vFront = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vFront, pNode );
+    Vec_PtrForEachEntry( vFront, pAnd, i )
+    {
+        pFanin = Abc_ObjChild0(pAnd);
+        if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            Vec_PtrPush( vFront, pFanin );
+        else
+            Vec_PtrPush( vSuper, pFanin );
+
+        pFanin = Abc_ObjChild1(pAnd);
+        if ( Abc_ObjIsNode(pFanin) && !Abc_ObjIsComplement(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+            Vec_PtrPush( vFront, pFanin );
+        else
+            Vec_PtrPush( vSuper, pFanin );
+    }
+    Vec_PtrFree( vFront );
+    // reverse the array of pointers to start with lower IDs
+    vFront = Vec_PtrAlloc( Vec_PtrSize(vSuper) );
+    Vec_PtrForEachEntryReverse( vSuper, pNode, i )
+        Vec_PtrPush( vFront, pNode );
+    Vec_PtrFree( vSuper );
+    vSuper = vFront;
+    // uniquify and return the frontier
+    Vec_PtrUniqify( vSuper, Vec_CompareNodeIds );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copies the topmost levels of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkTopAnd( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes, * vOrder;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj, * pDriver, * pObjPo;
+    int i, nNodes;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // get the first PO
+    pObjPo = Abc_NtkPo(pNtk, 0);
+    vNodes = Abc_NodeGetSuper( Abc_ObjChild0(pObjPo) );
+    assert( Vec_PtrSize(vNodes) >= 2 );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    Abc_NtkCleanCopy( pNtk );
+    pNtkAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkAig);
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkAig, pObj, 1 );
+    // restrash the nodes reachable from the roots
+    vOrder = Abc_NtkDfsIterNodes( pNtk, vNodes );
+    Vec_PtrForEachEntry( vOrder, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vOrder );
+    // finalize the network
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pObjPo = Abc_NtkCreatePo(pNtkAig);
+        pDriver = Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj));
+        Abc_ObjAddFanin( pObjPo, pDriver );
+        Abc_ObjAssignName( pObjPo, Abc_ObjName(pObjPo), NULL );
+    }
+    Vec_PtrFree( vNodes );
+    // perform cleanup if requested
+    if ( (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 
+        printf( "Abc_NtkTopAnd(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cmd/cmdApi.c b/src/base/cmd/cmdApi.c
index 7167e22b..71db1846 100644
--- a/src/base/cmd/cmdApi.c
+++ b/src/base/cmd/cmdApi.c
@@ -90,7 +90,7 @@ int Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand )
         loop = 0;
         fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop );
         if ( fStatus == 0 ) 
-            fStatus = CmdCommandDispatch( pAbc, argc, argv );
+            fStatus = CmdCommandDispatch( pAbc, &argc, &argv );
            CmdFreeArgv( argc, argv );
     } 
     while ( fStatus == 0 && *sCommandNext != '\0' );
diff --git a/src/base/cmd/cmdInt.h b/src/base/cmd/cmdInt.h
index c082bd94..3a6a2803 100644
--- a/src/base/cmd/cmdInt.h
+++ b/src/base/cmd/cmdInt.h
@@ -65,12 +65,13 @@ extern void       CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias )
 extern char *     CmdCommandAliasLookup( Abc_Frame_t * pAbc, char * sCommand );
 extern void       CmdCommandAliasFree( Abc_Alias * p );
 /*=== cmdUtils.c =======================================================*/
-extern int        CmdCommandDispatch( Abc_Frame_t * pAbc, int  argc, char ** argv );
+extern int        CmdCommandDispatch( Abc_Frame_t * pAbc, int * argc, char *** argv );
 extern char *     CmdSplitLine( Abc_Frame_t * pAbc, char * sCommand, int * argc, char *** argv );
 extern int        CmdApplyAlias( Abc_Frame_t * pAbc, int * argc, char *** argv, int * loop );
 extern char *     CmdHistorySubstitution( Abc_Frame_t * pAbc, char * line, int * changed );
 extern FILE *     CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMode, char ** pFileNameReal, int silent );
 extern void       CmdFreeArgv( int argc, char ** argv );
+extern char **    CmdAddToArgv( int argc, char ** argv );
 extern void       CmdCommandFree( Abc_Command * pCommand );
 extern void       CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll );
 extern void       CmdPrintTable( st_table * tTable, int fAliases );
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 6b4bdcbe..8c3fd38c 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -85,8 +85,12 @@ int cmdCheckShellEscape( Abc_Frame_t * pAbc, int argc, char ** argv)
   SeeAlso     []
 
 ***********************************************************************/
-int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
+int CmdCommandDispatch( Abc_Frame_t * pAbc, int * pargc, char *** pargv )
 {
+    int argc = *pargc;
+    char ** argv = *pargv;
+    char ** argv2;
+
     Abc_Ntk_t * pNetCopy;
     int (*pFunc) ( Abc_Frame_t *, int, char ** );
     Abc_Command * pCommand;
@@ -103,8 +107,17 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the command
     if ( !st_lookup( pAbc->tCommands, argv[0], (char **)&pCommand ) )
     {   // the command is not in the table
-        fprintf( pAbc->Err, "** cmd error: unknown command '%s'\n", argv[0] );
-        return 1;
+//        fprintf( pAbc->Err, "** cmd error: unknown command '%s'\n", argv[0] );
+//        return 1;
+        // add command 'read' assuming that this is the file name
+        argv2 = CmdAddToArgv( argc, argv );
+        CmdFreeArgv( argc, argv );
+        argc = argc+1;
+        argv = argv2;
+        *pargc = argc;
+        *pargv = argv;
+        if ( !st_lookup( pAbc->tCommands, argv[0], (char **)&pCommand ) )
+            assert( 0 );
     }
 
     // get the backup network if the command is going to change the network
@@ -303,7 +316,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop )
                 fError = CmdApplyAlias( pAbc, &newc, &newv, loop );
                 if ( fError == 0 )
                 {
-                       fError = CmdCommandDispatch( pAbc, newc, newv );
+                       fError = CmdCommandDispatch( pAbc, &newc, &newv );
                 }
                 CmdFreeArgv( newc, newv );
             }
@@ -455,6 +468,28 @@ void CmdFreeArgv( int argc, char **argv )
 
 /**Function*************************************************************
 
+  Synopsis    [Frees the previously allocated argv array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char ** CmdAddToArgv( int argc, char ** argv )
+{
+    char ** argv2;
+    int i;
+    argv2 = ALLOC( char *, argc + 1 ); 
+    argv2[0] = Extra_UtilStrsav( "read" ); 
+    for ( i = 0; i < argc; i++ )
+        argv2[i+1] = Extra_UtilStrsav( argv[i] ); 
+    return argv2;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Frees the previously allocated command.]
 
   Description []
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1695942e..371adfc9 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -144,7 +144,7 @@ void Io_End()
 int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
-    char * pFileName;
+    char * pFileName, * pTemp;
     int fCheck;
     int c;
 
@@ -171,6 +171,10 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         goto usage;
     // get the input file name
     pFileName = argv[globalUtilOptind];
+    // fix the wrong symbol
+    for ( pTemp = pFileName; *pTemp; pTemp++ )
+        if ( *pTemp == '>' )
+            *pTemp = '\\';
     // read the file using the corresponding file reader
     pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck );
     if ( pNtk == NULL )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 7ecbe48e..1f1f19ba 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -221,8 +221,8 @@ int main( int argc, char * argv[] )
     // if the memory should be freed, quit packages
     if ( fStatus < 0 ) 
     {
-        Abc_Stop();
-    } 
+        Abc_Stop(); 
+    }  
     return 0; 
 
 usage: