Merge remote-tracking branch 'origin/master' into acd66

src/aig/gia/gia.h

@@ -1532,6 +1532,7 @@ extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
 extern void                Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb, int fAssign, int fReverse );
+extern void                Gia_ManDumpVerilogNand( Gia_Man_t * p, char * pFileName );
 /*=== giaMem.c ===========================================================*/
 extern Gia_MmFixed_t *     Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
 extern void                Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
@@ -1790,6 +1791,39 @@ extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
 extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
 
+/*=== giaBound.c ===========================================================*/
+typedef struct Bnd_Man_t_  Bnd_Man_t;
+
+extern Bnd_Man_t*           Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose );
+extern void                 Bnd_ManStop();
+
+// getter
+extern int                  Bnd_ManGetNInternal();
+extern int                  Bnd_ManGetNExtra();
+
+//for fraig
+extern void                 Bnd_ManMap( int iLit, int id, int spec );
+extern void                 Bnd_ManMerge( int id1, int id2, int phaseDiff );
+extern void                 Bnd_ManFinalizeMappings();
+extern void                 Bnd_ManPrintMappings();
+extern Gia_Man_t*           Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl );
+extern int                  Bnd_ManCheckCoMerged( Gia_Man_t *p );
+
+// for eco
+extern int                  Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose );
+extern void                 Bnd_ManFindBound( Gia_Man_t *p, Gia_Man_t *pImpl );
+extern Gia_Man_t*           Bnd_ManGenSpecOut( Gia_Man_t *p );
+extern Gia_Man_t*           Bnd_ManGenImplOut( Gia_Man_t *p );
+extern Gia_Man_t*           Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
+extern Gia_Man_t*           Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec );
+extern Gia_Man_t*           Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose );
+extern void                 Bnd_ManSetEqOut( int eq );
+extern void                 Bnd_ManSetEqRes( int eq );
+extern void                 Bnd_ManPrintStats();
+
+// util
+extern Gia_Man_t*           Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase );
+
 ABC_NAMESPACE_HEADER_END
 
 

src/aig/gia/giaDup.c

@@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+
+extern Bnd_Man_t* pBnd; 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -5674,7 +5677,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
 {
-    Vec_Int_t * vLits;
+    // Vec_Int_t * vLits;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i, iLit;
@@ -5692,7 +5695,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
     assert( Gia_ManRegNum(p2) == 0 );        
     assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
     assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
-    vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
+    // vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
     if ( fVerbose )
         printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n", 
             Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
@@ -5702,28 +5705,124 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
     Gia_ManHashStart( pNew );
     Gia_ManConst0(p1)->Value = 0;
     Gia_ManConst0(p2)->Value = 0;
-    Gia_ManForEachCi( p1, pObj, i )
+
-        pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
+
-    Gia_ManForEachAnd( p2, pObj, i )
+    for( int i = 0; i < Gia_ManCiNum(p1); i++ )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    {
-    Gia_ManForEachAnd( p1, pObj, i ) {
+        int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew);
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+
-        if ( Gia_ObjIsBuf(pObj) )
+        pObj = Gia_ManCi(p1, i);
-            Vec_IntPush( vLits, pObj->Value );
+        if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 );
+
+        pObj = Gia_ManCi(p2, i);
+        if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 );
+
     }
+
+    // record the corresponding impl node of each lit
+    Gia_ManForEachAnd( p2, pObj, i )
+    {
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 );
+    }
+
+    // record hashed equivalent nodes
+    Gia_ManForEachAnd( p1, pObj, i ) 
+    {
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 );
+    }
+
     Gia_ManForEachCo( p2, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    {
-    //Gia_ManForEachCo( p1, pObj, i )
+        iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    //    Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
-    Vec_IntForEachEntry( vLits, iLit, i )
+    Gia_ManForEachCo( p1, pObj, i )
-        Gia_ManAppendCo( pNew, iLit );
+    {
-    Vec_IntFree( vLits );
+       iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+
+    // Vec_IntForEachEntry( vLits, iLit, i )
+        // Gia_ManAppendCo( pNew, iLit );
+    // Vec_IntFree( vLits );
     Gia_ManHashStop( pNew );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );    
     return pNew;
 }
 
+/**Function*************************************************************
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput )
+{
+    Gia_Man_t * pNew, *pTemp;
+    Gia_Obj_t * pObj, *pObj2;
+    int i;
+    int nBoundI = 0, nBoundO = 0;
+    int nExtra;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    // pNew->pName = Abc_UtilStrsav( p->pName );
+    // pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+
+    // add po of impl
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        if ( i < nPo )
+        {
+            Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+        }
+    }
+    nExtra = Gia_ManAndNum( pNew );
+
+    // add boundary as buf
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        if ( i >= 2 * nPo )
+        {
+            pObj2 = Gia_ObjFanin0(pObj);
+            if (~pObj2->Value)   // visited boundary
+            {
+                if ( i >=  2 * nPo + nBInput )
+                {
+                    nBoundO ++;
+                }
+                else nBoundI ++;
+            }
+
+            Gia_ManDupOrderDfs_rec( pNew, p, pObj2 );
+            Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        }
+    }
+    nExtra = Gia_ManAndNum( pNew ) - nExtra - Gia_ManBufNum( pNew );
+
+    Gia_ManForEachCi( p, pObj, i )
+        if ( !~pObj->Value )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+
+    Gia_ManDupRemapCis( pNew, p );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+
+
+    printf( "synthesized implementation:\n" );
+    printf( "\t%d / %d input boundary recovered.\n", nBoundI, nBInput );
+    printf( "\t%d / %d output boundary recovered.\n", nBoundO, Gia_ManCoNum(p)-2*nPo-nBInput );
+    printf( "\t%d / %d unused nodes in the box.\n", nExtra, Gia_ManAndNum(pNew) - Gia_ManBufNum( pNew ) );
+
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaFx.c

@@ -150,6 +150,13 @@ Vec_Wrd_t * Gia_ManComputeTruths( Gia_Man_t * p, int nCutSize, int nLutNum, int
         // collect and sort fanins
         vLeaves.nCap = vLeaves.nSize = Gia_ObjLutSize( p, i );
         vLeaves.pArray = Gia_ObjLutFanins( p, i );
+        if( !Vec_IntCheckUniqueSmall(&vLeaves) ) 
+        {
+            Vec_IntUniqify(&vLeaves);
+            Vec_IntWriteEntry(p->vMapping, Vec_IntEntry(p->vMapping, i), vLeaves.nSize);
+            for ( k = 0; k < vLeaves.nSize; k++ )
+                Vec_IntWriteEntry(p->vMapping, Vec_IntEntry(p->vMapping, i) + 1 + k, vLeaves.pArray[k]);
+        }
         assert( Vec_IntCheckUniqueSmall(&vLeaves) );
         Vec_IntSelectSort( Vec_IntArray(&vLeaves), Vec_IntSize(&vLeaves) );
         if ( !fReverse )

src/aig/gia/giaMan.c

@@ -1254,7 +1254,7 @@ void Gia_ManDfsSlacksPrint( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs )
+void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs, int fReverse )
 {
     int Length = Start, i, fFirst = 1; 
     char pName[100];
@@ -1318,9 +1318,9 @@ void Gia_ManDumpInterface2( Gia_Man_t * p, FILE * pFile )
     fprintf( pFile, "_inst" );
 
     fprintf( pFile, " (\n    " );
-    Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p) );
+    Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p), 0 );
     fprintf( pFile, ",\n    " );
-    Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p) );
+    Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p), 0 );
     fprintf( pFile, "\n  );\n\n" );
 
     fprintf( pFile, "endmodule\n\n" );
@@ -1387,16 +1387,17 @@ char * Gia_ObjGetDumpName( Vec_Ptr_t * vNames, char c, int i, int d )
         sprintf( pBuffer, "%c%0*d%c", c, d, i, c );
     return pBuffer;
 }
-void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Start, int Skip, Vec_Bit_t * vObjs )
+void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Start, int Skip, Vec_Bit_t * vObjs, int fReverse )
 {
     int Digits = Abc_Base10Log( n );
     int Length = Start, i, fFirst = 1; 
     char * pName;
     for ( i = 0; i < n; i++ )
     {
-        if ( vObjs && !Vec_BitEntry(vObjs, i) )
+        int k = fReverse ? n-1-i : i;
+        if ( vObjs && !Vec_BitEntry(vObjs, k) )
             continue;
-        pName = Gia_ObjGetDumpName( vNames, c, i, Digits );
+        pName = Gia_ObjGetDumpName( vNames, c, k, Digits );
         Length += strlen(pName) + 2;
         if ( Length > 60 )
         {
@@ -1413,12 +1414,12 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int
     if ( fInterComb ) 
     {
         if ( fAssign ) {
-            extern void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse );
+            extern void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName );
-            Gia_ManDumpInterfaceAssign( p, pFileName, fReverse );
+            Gia_ManDumpInterfaceAssign( p, pFileName );
         }
         else {
-            extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse );
+            extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName );
-            Gia_ManDumpInterface( p, pFileName, fReverse );
+            Gia_ManDumpInterface( p, pFileName );
         }
     }
     else
@@ -1464,26 +1465,26 @@ void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vOb
     if ( fVerBufs )
     {
         fprintf( pFile, " (\n    " );
-        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL, 0 );
         fprintf( pFile, ",\n    " );
 
-        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL, 0 );
         fprintf( pFile, "\n  );\n\n" );
 
         fprintf( pFile, "  input " );
-        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  output " );
-        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         Gia_ManForEachPi( p, pObj, i )
@@ -1503,32 +1504,32 @@ void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vOb
     else
     {
         fprintf( pFile, " (\n    " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL, 0 );
         fprintf( pFile, ",\n    " );
 
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL, 0 );
         fprintf( pFile, "\n  );\n\n" );
 
         fprintf( pFile, "  input " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  output " );
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vUsed) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vInvs) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
@@ -1644,26 +1645,26 @@ void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t
     if ( fVerBufs )
     {
         fprintf( pFile, " (\n    " );
-        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL, 0 );
         fprintf( pFile, ",\n    " );
 
-        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL, 0 );
         fprintf( pFile, "\n  );\n\n" );
 
         fprintf( pFile, "  input " );
-        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  output " );
-        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         Gia_ManForEachPi( p, pObj, i )
@@ -1683,32 +1684,32 @@ void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t
     else
     {
         fprintf( pFile, " (\n    " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL, 0 );
         fprintf( pFile, ",\n    " );
 
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL, 0 );
         fprintf( pFile, "\n  );\n\n" );
 
         fprintf( pFile, "  input " );
-        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
 
         fprintf( pFile, "  output " );
-        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vUsed) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vInvs) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
@@ -1838,7 +1839,7 @@ Vec_Int_t * Gia_ManCountSymbsAll( Vec_Ptr_t * vNames )
     }
     return vArray;
 }
-void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts )
+void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse )
 {
     Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
     if ( vNames == NULL )
@@ -1849,13 +1850,18 @@ void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts )
         int iName, Size, i;
         Vec_IntForEachEntryDouble( vArray, iName, Size, i )
         {
+            if ( fReverse )
+            {
+                iName = Vec_IntEntry(vArray, Vec_IntSize(vArray)-2-i);
+                Size  = Vec_IntEntry(vArray, Vec_IntSize(vArray)-1-i);
+            }
             if ( i ) fprintf( pFile, ", " );
             Gia_ManPrintOneName( pFile, (char *)Vec_PtrEntry(vNames, iName), Size );
         }
         Vec_IntFree( vArray );            
     }
 }
-void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse )
+void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts )
 {
     Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
     if ( p->vNamesOut == NULL )
@@ -1874,7 +1880,7 @@ void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse )
             int NumEnd = Gia_ManReadRangeNum( pNameLast, Size );
             fprintf( pFile, "  %s ", fOuts ? "output" : "input" );
             if ( NumBeg != -1 && iName < iNameNext-1 )
-                fprintf( pFile, "[%d:%d] ", fReverse ? NumBeg : NumEnd, fReverse ? NumEnd : NumBeg );
+                fprintf( pFile, "[%d:%d] ", NumEnd, NumBeg );
             Gia_ManPrintOneName( pFile, pName, Size );
             fprintf( pFile, ";\n" );                
         }
@@ -1893,7 +1899,7 @@ void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse )
+void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName )
 {
     Gia_Obj_t * pObj;
     Vec_Bit_t * vInvs, * vUsed;
@@ -1916,45 +1922,45 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse )
     Gia_ManDumpModuleName( pFile, p->pName );
     fprintf( pFile, "_wrapper" );
     fprintf( pFile, " ( " );
-    Gia_ManDumpIoList( p, pFile, 0 );
+    Gia_ManDumpIoList( p, pFile, 0, 0 );
     fprintf( pFile, ", " );
-    Gia_ManDumpIoList( p, pFile, 1 );    
+    Gia_ManDumpIoList( p, pFile, 1, 0 );    
     fprintf( pFile, " );\n\n" );
-    Gia_ManDumpIoRanges( p, pFile, 0, fReverse );
+    Gia_ManDumpIoRanges( p, pFile, 0 );
-    Gia_ManDumpIoRanges( p, pFile, 1, fReverse );
+    Gia_ManDumpIoRanges( p, pFile, 1 );
     fprintf( pFile, "\n" );
 
     fprintf( pFile, "  wire " );
-    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
     fprintf( pFile, ";\n\n" );
 
     fprintf( pFile, "  wire " );
-    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
     fprintf( pFile, ";\n\n" );
 
     fprintf( pFile, "  assign { " );
-    Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL, 1 );
     fprintf( pFile, " } = { " );
-    Gia_ManDumpIoList( p, pFile, 0 );    
+    Gia_ManDumpIoList( p, pFile, 0, 1 );    
     fprintf( pFile, " };\n\n" );    
 
     fprintf( pFile, "  assign { " );
-    Gia_ManDumpIoList( p, pFile, 1 );       
+    Gia_ManDumpIoList( p, pFile, 1, 1 );       
     fprintf( pFile, " } = { " );    
-    Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL, 1 );
     fprintf( pFile, " };\n\n" );
 
     if ( Vec_BitCount(vUsed) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vInvs) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
@@ -2004,7 +2010,7 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse )
     Vec_BitFree( vInvs );
     Vec_BitFree( vUsed );
 }
-void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse )
+void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName )
 {
     Gia_Obj_t * pObj;
     Vec_Bit_t * vInvs, * vUsed;
@@ -2027,45 +2033,45 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse )
     Gia_ManDumpModuleName( pFile, p->pName );
     fprintf( pFile, "_wrapper" );
     fprintf( pFile, " ( " );
-    Gia_ManDumpIoList( p, pFile, 0 );
+    Gia_ManDumpIoList( p, pFile, 0, 0 );
     fprintf( pFile, ", " );
-    Gia_ManDumpIoList( p, pFile, 1 );    
+    Gia_ManDumpIoList( p, pFile, 1, 0 );    
     fprintf( pFile, " );\n\n" );
-    Gia_ManDumpIoRanges( p, pFile, 0, fReverse );
+    Gia_ManDumpIoRanges( p, pFile, 0 );
-    Gia_ManDumpIoRanges( p, pFile, 1, fReverse );
+    Gia_ManDumpIoRanges( p, pFile, 1 );
     fprintf( pFile, "\n" );
 
     fprintf( pFile, "  wire " );
-    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 );
     fprintf( pFile, ";\n\n" );
 
     fprintf( pFile, "  wire " );
-    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 );
     fprintf( pFile, ";\n\n" );
 
     fprintf( pFile, "  assign { " );
-    Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL, 1 );
     fprintf( pFile, " } = { " );
-    Gia_ManDumpIoList( p, pFile, 0 );    
+    Gia_ManDumpIoList( p, pFile, 0, 1 );    
     fprintf( pFile, " };\n\n" );    
 
     fprintf( pFile, "  assign { " );
-    Gia_ManDumpIoList( p, pFile, 1 );       
+    Gia_ManDumpIoList( p, pFile, 1, 1 );       
     fprintf( pFile, " } = { " );    
-    Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL, 1 );
     fprintf( pFile, " };\n\n" );
 
     if ( Vec_BitCount(vUsed) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
     if ( Vec_BitCount(vInvs) )
     {
         fprintf( pFile, "  wire " );
-        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 );
         fprintf( pFile, ";\n\n" );
     }
 
@@ -2117,6 +2123,93 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDumpNandLit( FILE * pFile, int nIns, int Lit, int nDigits )
+{
+    if ( Lit == 0 )
+        fprintf( pFile, "1\'b0" );
+    else if ( Lit == 1 )
+        fprintf( pFile, "1\'b1" );
+    else if ( Abc_Lit2Var(Lit) <= nIns )
+        fprintf( pFile, "%cn%0*d", (char)(Abc_LitIsCompl(Lit)? '~':' '), nDigits, Abc_Lit2Var(Lit) );
+    else
+        fprintf( pFile, "%cn%0*d", (char)(Abc_LitIsCompl(Lit)? ' ':'~'), nDigits, Abc_Lit2Var(Lit) );
+}
+void Gia_ManDumpVerilogNand( Gia_Man_t * p, char * pFileName )
+{
+    Gia_Obj_t * pObj;  int i, nPis = Gia_ManPiNum(p);
+    int nDigits  = Abc_Base10Log( Gia_ManObjNum(p) );
+    int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
+    int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    assert( Gia_ManRegNum(p) == 0 );
+    fprintf( pFile, "module " );
+    Gia_ManDumpModuleName( pFile, p->pName );
+    fprintf( pFile, "_wrapper" );
+    fprintf( pFile, " ( " );
+    if ( p->vNamesIn ) {
+        Gia_ManDumpIoList( p, pFile, 0, 0 );
+        fprintf( pFile, ", " );
+        Gia_ManDumpIoList( p, pFile, 1, 0 );
+        fprintf( pFile, " );\n\n" );
+        Gia_ManDumpIoRanges( p, pFile, 0 );
+        Gia_ManDumpIoRanges( p, pFile, 1 );
+    }
+    else {
+        fprintf( pFile, "\n  " );        
+        Gia_ManForEachPi( p, pObj, i )
+            fprintf( pFile, "%s, ", Gia_ObjGetDumpName(NULL, 'x', i, nDigitsI) );
+        fprintf( pFile, "\n  " );        
+        Gia_ManForEachPo( p, pObj, i )
+            fprintf( pFile, "%s%s ", Gia_ObjGetDumpName(NULL, 'z', i, nDigitsO), i < Gia_ManPoNum(p)-1 ? ",":"" );
+        fprintf( pFile, "\n);\n\n" );
+        fprintf( pFile, "  input" );
+        Gia_ManForEachPi( p, pObj, i )
+            fprintf( pFile, " %s%s", Gia_ObjGetDumpName(NULL, 'x', i, nDigitsI), i < Gia_ManPiNum(p)-1 ? ",":"" );
+        fprintf( pFile, ";\n" );
+        fprintf( pFile, "  output" );
+        Gia_ManForEachPo( p, pObj, i )
+            fprintf( pFile, " %s%s", Gia_ObjGetDumpName(NULL, 'z', i, nDigitsO), i < Gia_ManPoNum(p)-1 ? ",":"" );
+        fprintf( pFile, ";\n" );
+    }
+    fprintf( pFile, "\n" );
+    Gia_ManForEachPi( p, pObj, i )
+        fprintf( pFile, "  wire n%0*d = %s;\n", nDigits, i+1, p->vNamesIn ? (char *)Vec_PtrEntry(p->vNamesIn, i) : Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+    fprintf( pFile, "\n" );    
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        fprintf( pFile, "  wire n%0*d = ~(", nDigits, i );
+        Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit0(pObj, i), nDigits );
+        fprintf( pFile, " & " );
+        Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit1(pObj, i), nDigits );
+        fprintf( pFile, ");\n" );
+    }
+    fprintf( pFile, "\n" );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        fprintf( pFile, "  assign %s = ", p->vNamesOut ? (char *)Vec_PtrEntry(p->vNamesOut, i) : Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
+        Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit0p(p, pObj), nDigits );
+        fprintf( pFile, ";\n" );
+    }   
+    fprintf( pFile, "\nendmodule\n\n" );
+    fclose( pFile );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Generate hierarchical design.]
@@ -2189,6 +2282,8 @@ void Gia_GenSandwich( char ** pFNames, int nFNames, char * pFileName )
     fprintf( pFile, "endmodule\n" );
     fclose( pFile );
     for ( i = 0; i < nFNames; i++ ) {
+        Vec_PtrFreeFree( pGias[i]->vNamesIn );  pGias[i]->vNamesIn = NULL;
+        Vec_PtrFreeFree( pGias[i]->vNamesOut ); pGias[i]->vNamesOut = NULL;
         Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1, 0, 0 );
         printf( "Dumped Verilog file \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") );        
     }

src/aig/gia/module.make

@@ -109,4 +109,5 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaTsim.c \
     src/aig/gia/giaTtopt.cpp \
     src/aig/gia/giaUnate.c \
-    src/aig/gia/giaUtil.c
+    src/aig/gia/giaUtil.c \
+    src/aig/gia/giaBound.c

src/base/abci/abc.c

@@ -219,6 +219,7 @@ static int Abc_CommandInter                  ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandBb2Wb                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOutdec                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandNodeDup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandWrap                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestColor              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -599,6 +600,8 @@ static int Abc_CommandAbc9ProdAdd            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9AddFlop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BMiter             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GenHie             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9BRecover           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9StrEco             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -996,6 +999,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "bb2wb",         Abc_CommandBb2Wb,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "outdec",        Abc_CommandOutdec,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "nodedup",       Abc_CommandNodeDup,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "wrap",          Abc_CommandWrap,             0 );
     Cmd_CommandAdd( pAbc, "Various",      "testcolor",     Abc_CommandTestColor,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 //    Cmd_CommandAdd( pAbc, "Various",      "qbf_solve",     Abc_CommandTest,               0 );
@@ -1380,6 +1384,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&addflop",      Abc_CommandAbc9AddFlop,                0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmiter",       Abc_CommandAbc9BMiter,                 0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&gen_hie",      Abc_CommandAbc9GenHie,                 0 );    
+    Cmd_CommandAdd( pAbc, "ABC9",         "&brecover",     Abc_CommandAbc9BRecover,               0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&str_eco",      Abc_CommandAbc9StrEco,                 0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
     {
@@ -14459,6 +14465,67 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandWrap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pFileName = NULL, * pFileName2 = NULL;
+    FILE * pFile = NULL, * pFile2 = NULL;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 2 )
+    {
+        Abc_Print( 1,"Two file names are expected on the command line.\n" );
+        return 0;
+    }
+    pFileName  = argv[globalUtilOptind];
+    pFileName2 = argv[globalUtilOptind+1];
+    pFile  = fopen( pFileName, "rb" );
+    pFile2 = fopen( pFileName2, "wb" );
+    if ( pFile && pFile2 )
+    {
+        char Buffer[1000];
+        while ( fgets( Buffer, 1000, pFile ) != NULL )
+        {
+            if ( Buffer[strlen(Buffer)-1] == '\n' )
+                Buffer[strlen(Buffer)-1] = 0;            
+            if ( Buffer[strlen(Buffer)-1] == '\r' )
+                Buffer[strlen(Buffer)-1] = 0;
+            fprintf( pFile2, "  printf(\"%s\\n\");\n", Buffer );
+        }
+    }
+    if ( pFile  ) fclose(pFile);   
+    if ( pFile2 ) fclose(pFile2);   
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: wrap [-h] <file> <file2>\n" );
+    Abc_Print( -2, "\t           wrapping lines\n" );
+    Abc_Print( -2, "\t<file>   : input text file\n");
+    Abc_Print( -2, "\t<file2>  : output text file\n");    
+    return 1;
+
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -32083,6 +32150,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nArgcNew;
     int fUnique  = 0;
     int fVerilog = 0;
+    int fVerNand = 0;
     int fInter   = 0;
     int fInterComb = 0;
     int fAssign  = 0;
@@ -32094,7 +32162,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSkipComment = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "upicabmlnrsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "upqicabmlnrsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32104,6 +32172,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fVerilog ^= 1;
             break;
+        case 'q':
+            fVerNand ^= 1;
+            break;
         case 'i':
             fInter ^= 1;
             break;
@@ -32159,6 +32230,8 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         Gia_AigerWriteSimple( pGia, pFileName );
         Gia_ManStop( pGia );
     }
+    else if ( fVerNand )
+        Gia_ManDumpVerilogNand( pAbc->pGia, pFileName );
     else if ( fVerilog )
         Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter, fInterComb, fAssign, fReverse );
     else if ( fMiniAig )
@@ -32170,10 +32243,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-upicabmlnrsvh] <file>\n" );
+    Abc_Print( -2, "usage: &w [-upqicabmlnsvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
     Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
     Abc_Print( -2, "\t-p     : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
+    Abc_Print( -2, "\t-q     : toggle writing Verilog with NAND-gates [default = %s]\n", fVerNand? "yes" : "no" );
     Abc_Print( -2, "\t-i     : toggle writing the interface module in Verilog [default = %s]\n", fInter? "yes" : "no" );
     Abc_Print( -2, "\t-c     : toggle writing the interface module in Verilog [default = %s]\n", fInterComb? "yes" : "no" );
     Abc_Print( -2, "\t-a     : toggle writing the interface module with assign-statements [default = %s]\n", fAssign? "yes" : "no" );
@@ -32181,7 +32255,7 @@ usage:
     Abc_Print( -2, "\t-m     : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
     Abc_Print( -2, "\t-l     : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
     Abc_Print( -2, "\t-n     : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggle reversing the order of input/output bits [default = %s]\n", fReverse? "yes": "no" );    
+    //Abc_Print( -2, "\t-r     : toggle reversing the order of input/output bits [default = %s]\n", fReverse? "yes": "no" );    
     Abc_Print( -2, "\t-s     : toggle skipping the timestamp in the output file [default = %s]\n", fSkipComment? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -34423,11 +34497,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, fOutputs = 0, nWords = 4, fTruth = 0, fVerbose = 0;
+    int c, fOutputs = 0, nWords = 4, fTruth = 0, fReverse = 0, fVerbose = 0;
     char ** pArgvNew;
     int nArgcNew;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Wtovh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wtrovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -34445,6 +34519,9 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             fTruth ^= 1;
             break;
+        case 'r':
+            fReverse ^= 1;
+            break;            
         case 'o':
             fOutputs ^= 1;
             break;
@@ -34475,7 +34552,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
-        pAbc->pGia->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pAbc->pGia) );
+        pAbc->pGia->vSimsPi = fReverse ? Vec_WrdStartTruthTablesRev( Gia_ManCiNum(pAbc->pGia) ) : Vec_WrdStartTruthTables( Gia_ManCiNum(pAbc->pGia) );
         Vec_WrdFreeP( &pAbc->pGia->vSimsPo );
         pAbc->pGia->vSimsPo = Gia_ManSimPatSimOut( pAbc->pGia, pAbc->pGia->vSimsPi, 1 );
         return 0;
@@ -34518,10 +34595,11 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sim_read [-W num] [-tovh] <file>\n" );
+    Abc_Print( -2, "usage: &sim_read [-W num] [-trovh] <file>\n" );
     Abc_Print( -2, "\t         reads simulation patterns from file\n" );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
     Abc_Print( -2, "\t-t     : toggle creating exhaustive simulation info [default = %s]\n", fTruth? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle reversing MSB and LSB input variables [default = %s]\n", fReverse? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle reading output information [default = %s]\n", fOutputs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -38081,7 +38159,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
     Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -38234,6 +38312,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
+        case 'q':
+            pPars->fBMiterInfo ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -38298,6 +38379,7 @@ usage:
     Abc_Print( -2, "\t-o     : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-q     : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -51961,11 +52043,21 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * FileName = NULL;
     FILE * pFile = NULL;
     int c, fVerbose = 0;
+    int bi  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    // TODO: use a flag to block Bnd_Man
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            bi = atoi(argv[globalUtilOptind++]);
+            break;    
         case 'v':
             fVerbose ^= 1;
             break;
@@ -52010,8 +52102,9 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmiter [-vh] <file>\n" );
+    Abc_Print( -2, "usage: &bmiter -I <biNum> [-vh] <file>\n" );
     Abc_Print( -2, "\t         creates the boundary miter\n" );
+    Abc_Print( -2, "\t-I <biNum>:   number of boundary inputs\n" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the implementation file\n");    
@@ -52078,6 +52171,360 @@ usage:
     Abc_Print( -2, "\t            (the PO count of <file[i]> should not be less than the PI count of <file[i+1]>)\n");    
     return 1;}
 
+extern Bnd_Man_t* pBnd;
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
+    extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
+    extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
+    Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter;
+    char * FileName = NULL;
+    FILE * pFile = NULL;
+    int c, fVerbose = 0, success = 1, fEq = 1, fEqOut = 1;
+
+    // params
+    Gps_Par_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Gps_Par_t) );
+    Cec_ParCec_t ParsCec, *pParsCec = &ParsCec;
+    Cec_ManCecSetDefaultParams( pParsCec );
+    Cec_ParFra_t ParsFra, *pParsFra = &ParsFra;
+    Cec4_ManSetParams( pParsFra );
+    pParsFra -> fBMiterInfo = 1;
+
+    // parse options
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vhCkeo" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            pParsFra->fVerbose ^= 1;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParsFra->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pParsFra->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'k':
+            pParsFra ->fUseCones ^= 1;
+            break;
+        case 'e':
+            fEq ^= 1;
+            break;
+        case 'o':
+            fEqOut ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf("%d\n", argc-globalUtilOptind);
+        Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" );
+        return 0;
+    }
+
+    // read spec
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+        Abc_Print( 1, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+    pSpec = Gia_AigerRead( FileName, 0, 1, 0 );
+    if ( pSpec == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" );
+        return 0;
+    }    
+    if ( Gia_ManBufNum(pSpec) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" );
+        Gia_ManStop(pSpec);
+        return 0;
+    }    
+
+    // start boundary manager
+    pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose );
+
+    // check boundary
+    if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" );
+        success = 0;
+    }
+
+    if ( success )
+    {
+        // create bmiter, run fraig, record mapping
+        pBmiter = Bnd_ManStackGias( pSpec, pAbc->pGia );
+        pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
+
+        // every output should be equivalent
+        // else, terminate the command (TODO?)
+        if ( !Bnd_ManCheckCoMerged( pTemp ) )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec and impl cannot be proved equivalent.\n" );
+            success = 0;
+        }
+
+        Gia_ManStop(pBmiter);
+        Gia_ManStop(pTemp);
+    }
+
+    if ( success )
+    {
+        // find 
+        Bnd_ManFindBound( pSpec, pAbc->pGia );
+
+        // create spec_out and 
+        pSpec_out = Bnd_ManGenSpecOut( pSpec );
+        if ( !pSpec_out ) success = 0;
+        pImpl_out = Bnd_ManGenImplOut( pAbc->pGia );
+        if ( !pImpl_out ) success = 0;
+
+        // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
+        // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
+        // Gia_ManPrintStats( pSpec_out, pPars );
+        // Gia_ManPrintStats( pImpl_out, pPars );
+
+        if ( !success )
+        {
+            printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n");
+        }
+    }
+
+    if ( success )
+    {
+
+        // check if spec_out and imnpl_out are equivalent
+        if ( fVerbose ) 
+        {
+            if ( fEqOut )
+            {
+                printf("Checking the equivalence of spec_out and impl_out\n");
+                pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
+                Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
+                Gia_ManStop( pMiter );
+            }
+            else
+            {
+                printf("Skip checking the equivalence of spec_out and impl_out\n");
+            }
+        }
+
+        // generate patched impl
+        if ( fVerbose ) printf("Generating patched impl\n");
+        pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec );
+
+        // // generate patched spec just for debugging
+        // printf("Generating patched spec\n");
+        // pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch );
+        // printf("Checking the equivalence of patched spec and patched impl\n");
+        // pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 );
+        // Cec_ManVerify( pMiter, pParsCec );
+        // Gia_ManStop( pMiter );
+        // printf("Checking the equivalence of patched spec and patch\n");
+        // pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 );
+        // Cec_ManVerify( pMiter, pParsCec );
+        // Gia_ManStop( pMiter );
+
+        // Gia_ManStop( pTemp );
+
+        // check if patched is equiv to spec
+        if ( fVerbose ) 
+        {
+            if ( fEq ) printf("Checking the equivalence of patched impl and spec\n");
+            else printf("Skip checking the equivalence of patched impl and spec\n");
+        }
+        if ( fEq )
+        {
+            pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 );
+            success = Cec_ManVerify( pMiter, pParsCec );
+            Bnd_ManSetEqRes( success );
+            if ( !success )
+            {
+                printf("Failed. The generated AIG is not equivalent.\n");
+            }
+            Gia_ManStop( pMiter );
+        }
+
+    }
+
+    if ( fVerbose ) Bnd_ManPrintStats();
+
+    Gia_ManStop( pSpec );
+    if ( pSpec_out ) Gia_ManStop( pSpec_out );
+    if ( pImpl_out ) Gia_ManStop( pImpl_out );
+    if ( success )
+    {
+        if ( fEq ) printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() );
+        else printf("Success. But the equivalence in unknown (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() );
+    }
+    if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched );
+    Bnd_ManStop();
+
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &brecover -I <biNum> [-vh] <impl> <patch>\n" );
+    Abc_Print( -2, "\t         recover boundary using SAT-Sweeping\n" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t-k     : toggle using logic cones in the SAT solver [default = %s]\n", pParsFra->fUseCones? "yes": "no" );
+    Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pParsFra->nBTLimit );
+    Abc_Print( -2, "\t-e     : toggle checking the equivalence of the result [default = %s]\n", fEq? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle checking the equivalence of the outsides in verbose [default = %s]\n", fEqOut? "yes": "no" );
+    Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");    
+    Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");    
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
+    extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
+    Gia_Man_t *pMiter, *pPatch, *pPatched;
+    char * FileName = NULL;
+    FILE * pFile = NULL;
+    int c, success = 1;
+    int fVerbose = 0, fSkipStrash = 0;
+
+    // params
+    Gps_Par_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Gps_Par_t) );
+    Cec_ParCec_t ParsCec, *pParsCec = &ParsCec;
+    Cec_ManCecSetDefaultParams( pParsCec );
+    Cec_ParFra_t ParsFra, *pParsFra = &ParsFra;
+    Cec4_ManSetParams( pParsFra );
+    pParsFra -> fBMiterInfo = 1;
+
+    // parse options
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vsh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 's':
+            fSkipStrash ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf("%d\n", argc-globalUtilOptind);
+        Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
+        return 0;
+    }
+
+    // read patch
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
+        Abc_Print( 1, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+    pPatch = Gia_AigerRead( FileName, 0, 1, 0 );
+    if ( pPatch == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
+        return 0;
+    }    
+
+    // generate patched impl
+    if ( fVerbose ) printf("Generating patched impl\n");
+    pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose );
+
+    if ( pPatched )
+    {
+        // check if patched is equiv to patch
+        if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n");
+        pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
+        success = Cec_ManVerify( pMiter, pParsCec );
+        if( !success ) 
+        {
+            printf("Failed. The patched circuit is not equivalent.\n");
+        }
+        Gia_ManStop( pMiter );
+        Abc_FrameUpdateGia( pAbc, pPatched );
+    }
+
+    Gia_ManStop( pPatch );
+    if ( success )
+    {
+        printf("Success. The patched circuit is equivalent.\n");
+    }
+
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
+    Abc_Print( -2, "\t         SAT-sweeping-based ECO\n" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggles skipping structural hash [default = %s]\n",  fSkipStrash? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");    
+    Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");    
+    return 1;
+}
 
 /**Function*************************************************************
 

src/base/abci/abcMiter.c

@@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer
     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
     // map the constant nodes
     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames);
+    
     // create new latches (or their initial values) and remember them in the new latches
     if ( !fInitial )
     {

src/base/wlc/wlc.c

@@ -677,7 +677,7 @@ Gia_Man_t * Wlc_ManGenTree( int nInputs, int Value, int nBits, int fVerbose )
 ***********************************************************************/
 Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose )
 {
-    extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
+    extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose );
     extern void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
     Vec_Int_t * vIns = Vec_IntAlloc( 2*nInputs );
     Gia_Man_t * pTemp, * pNew; 
@@ -693,7 +693,7 @@ Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose )
     //    Vec_IntPush( vIns, Vec_IntEntry(vIns, i) );
 
     Gia_ManHashAlloc( pNew );
-    Wlc_BlastBooth( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds );
+    Wlc_BlastBooth( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds, 0 );
     //Wlc_BlastMultiplier3( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds );
     //Vec_WecPrint( vProds, 0 );
     Wlc_ManGenTreeOne( pNew, vProds, 1, fVerbose );

src/base/wlc/wlcBlast.c

@@ -1050,7 +1050,7 @@ void Wlc_BlastReduceMatrix2( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Int_t * v
 }
 
 
-void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds )
+void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose )
 {
     Vec_Wec_t * vProds  = Vec_WecStart( nArgA + nArgB );
     Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB );
@@ -1064,13 +1064,17 @@ void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA
         }
     if ( fSigned )
     {
-        Vec_WecPush( vProds,  nArgA, 1 );
+        Vec_WecPush( vProds,  nArgB-1, 1 );
-        Vec_WecPush( vLevels, nArgA, 0 );
+        Vec_WecPush( vLevels, nArgB-1, 0 );
+
+        Vec_WecPush( vProds,  nArgA-1, 1 );
+        Vec_WecPush( vLevels, nArgA-1, 0 );
 
         Vec_WecPush( vProds,  nArgA+nArgB-1, 1 );
         Vec_WecPush( vLevels, nArgA+nArgB-1, 0 );
     }
-
+    if ( fVerbose )
+        Vec_WecPrint( vProds, 0 );
     if ( pvProds )
         *pvProds = Vec_WecDup(vProds);
     else
@@ -1117,7 +1121,7 @@ void Wlc_BlastDecoder( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
         Vec_IntPush( vRes, iMint );
     }
 }
-void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds )
+void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose )
 {
     Vec_Wec_t * vProds  = Vec_WecStart( nArgA + nArgB + 3 );
     Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB + 3 );
@@ -1194,7 +1198,10 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
         Vec_WecPush( vProds,  k, Neg );
         Vec_WecPush( vLevels, k, 0 );
     }
-    //Vec_WecPrint( vProds, 0 );
+    //Vec_WecShrink( vProds,  nArgA + nArgB );
+    //Vec_WecShrink( vLevels, nArgA + nArgB );   
+    if ( fVerbose )
+        Vec_WecPrint( vProds, 0 );
     //Wlc_BlastPrintMatrix( pNew, vProds, 1 );
     //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
     if ( pvProds )
@@ -1832,9 +1839,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                 if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
                     ABC_SWAP( int *, pArg0, pArg1 );
                 if ( pPar->fBooth )
-                    Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL );
+                    Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL, pParIn->fVerbose );
                 else if ( pPar->fCla )
-                    Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL );
+                    Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL, pParIn->fVerbose );
                 else
                     Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
                     //Wlc_BlastMultiplierC( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );

src/base/wln/wlnBlast.c

@@ -69,7 +69,7 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
     extern int  Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits, int Carry ); // result is in pAdd0
     extern void Wlc_BlastSubtract( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits, int Carry ); // result is in pAdd0
     extern int  Wlc_NtkCountConstBits( int * pArray, int nSize );
-    extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
+    extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose );
     extern void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds );
     extern void Wlc_BlastZeroCondition( Gia_Man_t * pNew, int * pDiv, int nDiv, Vec_Int_t * vRes );
     extern void Wlc_BlastDividerTop( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest );
@@ -303,7 +303,7 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
             if ( Wlc_NtkCountConstBits(Vec_IntArray(vArg0), Vec_IntSize(vArg0)) < Wlc_NtkCountConstBits(Vec_IntArray(vArg1), Vec_IntSize(vArg1)) )
                 ABC_SWAP( Vec_Int_t, *vArg0, *vArg1 )
             if ( fBooth )
-                Wlc_BlastBooth( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL );
+                Wlc_BlastBooth( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL, 0 );
             else
                 Wlc_BlastMultiplier3( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL );
             if ( nRange > Vec_IntSize(vRes) )

src/misc/vec/vecBit.h

@@ -626,6 +626,27 @@ static inline void Vec_BitReset( Vec_Bit_t * p )
         p->pArray[i] = 0;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_BitPrint( Vec_Bit_t * p )
+{
+    int i, Entry;
+    printf( "Vector has %d entries: {", Vec_BitSize(p) );
+    Vec_BitForEachEntry( p, Entry, i )
+        printf( " %d", Entry );
+    printf( " }\n" );
+}
+
 ABC_NAMESPACE_HEADER_END
 
 #endif

src/misc/vec/vecWrd.h

@@ -195,6 +195,32 @@ static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars )
     }
     return p;
 }
+static inline Vec_Wrd_t * Vec_WrdStartTruthTablesRev( int nVars )
+{
+    Vec_Wrd_t * p;
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    int i, k, nWords;
+    nWords = nVars <= 6 ? 1 : (1 << (nVars - 6));
+    p = Vec_WrdStart( nWords * nVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        unsigned * pTruth = (unsigned *)(p->pArray + nWords * (nVars-1-i));
+        if ( i < 5 )
+        {
+            for ( k = 0; k < 2*nWords; k++ )
+                pTruth[k] = Masks[i];
+        }
+        else
+        {
+            for ( k = 0; k < 2*nWords; k++ )
+                if ( k & (1 << (i-5)) )
+                    pTruth[k] = ~(unsigned)0;
+                else
+                    pTruth[k] = 0;
+        }
+    }
+    return p;
+}
 static inline int Vec_WrdShiftOne( Vec_Wrd_t * p, int nWords )
 {
     int i, nObjs = p->nSize/nWords;

src/proof/cec/cec.h

@@ -120,6 +120,8 @@ struct Cec_ParFra_t_
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
     int              iOutFail;      // the failed output
+    int              fBMiterInfo;   // printing BMiter information
+    int              nPO;           // number of po in original design given a bmiter
 };
 
 // combinational equivalence checking parameters

src/proof/cec/cecSatG2.c

@@ -219,6 +219,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars )
     pPars->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
     pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
     pPars->nGenIters      =     100;    // pattern generation iterations
+    pPars->fBMiterInfo    =       0;    // printing BMiter information
 }
 
 /**Function*************************************************************
@@ -1781,8 +1782,10 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
     }
     //Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
 }
+
 int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
 {
+
     Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); 
     Gia_Obj_t * pObj, * pRepr; 
     int i, fSimulate = 1;
@@ -1878,8 +1881,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
             if ( pRepr == NULL )
                 continue;
         }
+        int id_obj = Gia_ObjId( p, pObj );
+        int id_repr = Gia_ObjId( p, pRepr );
+
         if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
         {
+            if ( pPars->fBMiterInfo ) 
+            {
+                Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
+            }
+
             assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
             Gia_ObjSetProved( p, i );
             if ( Gia_ObjId(p, pRepr) == 0 )
@@ -1887,8 +1898,26 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
             continue;
         }
         if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
-            pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
+        {
+            if (pPars->fBMiterInfo){
+
+                Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
+                // printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase );
+
             }
+            pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
+
+
+        }
+    }
+    
+    if ( pPars->fBMiterInfo )
+    {
+        // print
+        Bnd_ManFinalizeMappings();
+        // Bnd_ManPrintMappings();
+    }
+
     if ( p->iPatsPi > 0 )
     {
         abctime clk2 = Abc_Clock();
@@ -1937,6 +1966,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
 {
     Gia_Man_t * pNew = NULL;
     Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
+
     return pNew;
 }
 void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )

src/sat/bsat2/Alg.h

@@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alg_h
 #define Minisat_Alg_h
 
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -81,4 +83,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true);
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Alloc.h

@@ -21,8 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Alloc_h
 #define Minisat_Alloc_h
 
-#include "XAlloc.h"
+#include "sat/bsat2/XAlloc.h"
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -128,4 +130,6 @@ RegionAllocator<T>::alloc(int size)
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Dimacs.h

@@ -23,8 +23,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <stdio.h>
 
-#include "ParseUtils.h"
+#include "sat/bsat2/ParseUtils.h"
-#include "SolverTypes.h"
+#include "sat/bsat2/SolverTypes.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -86,4 +88,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Heap.h

@@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Heap_h
 #define Minisat_Heap_h
 
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -146,4 +148,6 @@ class Heap {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/IntTypes.h

@@ -44,4 +44,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //=================================================================================================
 
+#include <misc/util/abc_namespaces.h>
+
 #endif

src/sat/bsat2/MainSat.cpp

@@ -23,11 +23,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <signal.h>
 #include "misc/zlib/zlib.h"
 
-#include "System.h"
+#include "sat/bsat2/System.h"
-#include "ParseUtils.h"
+#include "sat/bsat2/ParseUtils.h"
-#include "Options.h"
+#include "sat/bsat2/Options.h"
-#include "Dimacs.h"
+#include "sat/bsat2/Dimacs.h"
-#include "Solver.h"
+#include "sat/bsat2/Solver.h"
+
+ABC_NAMESPACE_IMPL_START
 
 using namespace Minisat;
 
@@ -195,3 +197,6 @@ extern "C" int MainSat(int argc, char** argv)
         exit(0);
     }
 }
+
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/MainSimp.cpp

@@ -27,11 +27,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <sys/resource.h>
 #endif
 
-#include "System.h"
+#include "sat/bsat2/System.h"
-#include "ParseUtils.h"
+#include "sat/bsat2/ParseUtils.h"
-#include "Options.h"
+#include "sat/bsat2/Options.h"
-#include "Dimacs.h"
+#include "sat/bsat2/Dimacs.h"
-#include "SimpSolver.h"
+#include "sat/bsat2/SimpSolver.h"
+
+ABC_NAMESPACE_IMPL_START
 
 using namespace Minisat;
 
@@ -204,3 +206,6 @@ extern "C" int MainSimp(int argc, char** argv)
         exit(0);
     }
 }
+
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/Map.h

@@ -20,8 +20,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
-#include "IntTypes.h"
+#include "sat/bsat2/IntTypes.h"
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -190,4 +192,6 @@ class Map {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Options.cpp

@@ -17,9 +17,11 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "Sort.h"
+#include "sat/bsat2/Sort.h"
-#include "Options.h"
+#include "sat/bsat2/Options.h"
-#include "ParseUtils.h"
+#include "sat/bsat2/ParseUtils.h"
+
+ABC_NAMESPACE_IMPL_START
 
 using namespace Minisat;
 
@@ -43,12 +45,14 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict)
             }
 
             if (!parsed_ok)
+            {
                 if (strict && match(argv[i], "-"))
                     { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } //  exit(0);
                 else
                     argv[j++] = argv[i];
             }
         }
+    }
 
     argc -= (i - j);
     return 1;
@@ -91,3 +95,5 @@ int Minisat::printUsageAndExit (int argc, char** argv, bool verbose)
     return 0;
 }
 
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/Options.h

@@ -25,9 +25,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 #include <string.h>
 
-#include "IntTypes.h"
+#include "sat/bsat2/IntTypes.h"
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
-#include "ParseUtils.h"
+#include "sat/bsat2/ParseUtils.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -60,7 +62,7 @@ class Option
     struct OptionLt {
         bool operator()(const Option* x, const Option* y) {
             int test1 = strcmp(x->category, y->category);
-            return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+            return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 );
         }
     };
 
@@ -384,4 +386,6 @@ class BoolOption : public Option
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/ParseUtils.h

@@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "misc/zlib/zlib.h"
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 namespace Minisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -119,4 +121,6 @@ static bool eagerMatch(B& in, const char* str) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Queue.h

@@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Queue_h
 #define Minisat_Queue_h
 
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -66,4 +68,6 @@ public:
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/SimpSolver.cpp

@@ -18,9 +18,11 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "Sort.h"
+#include "sat/bsat2/Sort.h"
-#include "SimpSolver.h"
+#include "sat/bsat2/SimpSolver.h"
-#include "System.h"
+#include "sat/bsat2/System.h"
+
+ABC_NAMESPACE_IMPL_START
 
 using namespace Minisat;
 
@@ -228,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
         if (var(qs[i]) != v){
             for (j = 0; j < ps.size(); j++)
                 if (var(ps[j]) == var(qs[i]))
+                {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+                }
             out_clause.push(qs[i]);
         }
         next:;
@@ -262,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
                 if (var(__ps[j]) == var(__qs[i]))
+                {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+                }
             size++;
         }
         next:;
@@ -718,3 +724,5 @@ void SimpSolver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/SimpSolver.h

@@ -21,9 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SimpSolver_h
 #define Minisat_SimpSolver_h
 
-#include "Queue.h"
+#include "sat/bsat2/Queue.h"
-#include "Solver.h"
+#include "sat/bsat2/Solver.h"
 
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -194,4 +195,6 @@ inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bo
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Solver.cpp

@@ -20,8 +20,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <math.h>
 
-#include "Sort.h"
+#include "sat/bsat2/Sort.h"
-#include "Solver.h"
+#include "sat/bsat2/Solver.h"
+
+ABC_NAMESPACE_IMPL_START
 
 using namespace Minisat;
 
@@ -209,7 +211,7 @@ void Solver::cancelUntil(int level) {
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+            if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
                 polarity[x] = sign(trail[c]);
             insertVarOrder(x); }
         qhead = trail_lim[level];
@@ -657,7 +659,7 @@ lbool Solver::search(int nof_conflicts)
 
         }else{
             // NO CONFLICT
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
@@ -922,3 +924,5 @@ void Solver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+ABC_NAMESPACE_IMPL_END

src/sat/bsat2/Solver.h

@@ -21,12 +21,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Solver_h
 #define Minisat_Solver_h
 
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
-#include "Heap.h"
+#include "sat/bsat2/Heap.h"
-#include "Alg.h"
+#include "sat/bsat2/Alg.h"
-#include "Options.h"
+#include "sat/bsat2/Options.h"
-#include "SolverTypes.h"
+#include "sat/bsat2/SolverTypes.h"
 
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -370,4 +371,6 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/SolverTypes.h

@@ -24,11 +24,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <assert.h>
 
-#include "IntTypes.h"
+#include "sat/bsat2/IntTypes.h"
-#include "Alg.h"
+#include "sat/bsat2/Alg.h"
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
-#include "Map.h"
+#include "sat/bsat2/Map.h"
-#include "Alloc.h"
+#include "sat/bsat2/Alloc.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -404,4 +406,6 @@ inline void Clause::strengthen(Lit p)
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/Sort.h

@@ -21,11 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Sort_h
 #define Minisat_Sort_h
 
-#include "Vec.h"
+#include "sat/bsat2/Vec.h"
 
 //=================================================================================================
 // Some sorting algorithms for vec's
 
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -95,4 +96,6 @@ template <class T> void sort(vec<T>& v) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/System.cpp

@@ -18,13 +18,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "System.h"
+#include "sat/bsat2/System.h"
 
 #if defined(__linux__)
 
 #include <stdio.h>
 #include <stdlib.h>
 
+ABC_NAMESPACE_IMPL_START
+
 using namespace Minisat;
 
 // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
@@ -72,24 +74,40 @@ double Minisat::memUsedPeak() {
     double peak = memReadPeak() / 1024;
     return peak == 0 ? memUsed() : peak; }
 
+ABC_NAMESPACE_IMPL_END
+
 #elif defined(__FreeBSD__)
 
+ABC_NAMESPACE_IMPL_START
+
 double Minisat::memUsed(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_maxrss / 1024; }
 double MiniSat::memUsedPeak(void) { return memUsed(); }
 
+ABC_NAMESPACE_IMPL_END
 
 #elif defined(__APPLE__)
 #include <malloc/malloc.h>
 
+ABC_NAMESPACE_IMPL_START
+
 double Minisat::memUsed(void) {
     malloc_statistics_t t;
     malloc_zone_statistics(NULL, &t);
     return (double)t.max_size_in_use / (1024*1024); }
 
+ABC_NAMESPACE_IMPL_END
+
 #else
+
+ABC_NAMESPACE_IMPL_START
+
 double Minisat::memUsed()     { return 0; }
 double Minisat::memUsedPeak() { return 0; }
+
+ABC_NAMESPACE_IMPL_END
+
 #endif
+

src/sat/bsat2/System.h

@@ -22,13 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_System_h
 
 #if defined(__linux__)
-#include <fpu_control.h>
+//#include <fpu_control.h>
 #endif
 
-#include "IntTypes.h"
+#include "sat/bsat2/IntTypes.h"
 
 //-------------------------------------------------------------------------------------------------
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 namespace Minisat {
 
 static inline double cpuTime(void); // CPU-time in seconds.
@@ -37,24 +39,35 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
 
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 static inline double Minisat::cpuTime(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
 
-#endif
+ABC_NAMESPACE_CXX_HEADER_END
+
+#endif
+
 
 #endif

src/sat/bsat2/Vec.h

@@ -24,8 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 #include <new>
 
-#include "IntTypes.h"
+#include "sat/bsat2/IntTypes.h"
-#include "XAlloc.h"
+#include "sat/bsat2/XAlloc.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Minisat {
 
@@ -91,7 +93,6 @@ public:
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };
 
-
 template<class T>
 void vec<T>::capacity(int min_cap) {
     if (cap >= min_cap) return;
@@ -127,4 +128,6 @@ void vec<T>::clear(bool dealloc) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/XAlloc.h

@@ -24,6 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <errno.h>
 #include <stdlib.h>
 
+#include <misc/util/abc_namespaces.h>
+
+ABC_NAMESPACE_CXX_HEADER_START
+
 namespace Minisat {
 
 //=================================================================================================
@@ -42,4 +46,6 @@ static inline void* xrealloc(void *ptr, size_t size)
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

src/sat/bsat2/module.make

@@ -1,6 +1,4 @@
 SRC +=  src/sat/bsat2/AbcApi.cpp \
-    src/sat/bsat2/MainSat.cpp \
-    src/sat/bsat2/MainSimp.cpp \
     src/sat/bsat2/Options.cpp \
     src/sat/bsat2/SimpSolver.cpp \
     src/sat/bsat2/Solver.cpp \