initial commit of public abc

6 files changed, 151 insertions, 67 deletions

diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
index e5d585ce..bb83ac95 100644
--- a/src/aig/bbr/bbr.h
+++ b/src/aig/bbr/bbr.h
@@ -21,22 +21,24 @@
 #ifndef __BBR_H__
 #define __BBR_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
-#include "cuddInt.h"
 #include "aig.h"
 #include "saig.h"
+#include "cuddInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -46,7 +48,7 @@ extern "C" {
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj )  { return pObj->pData; }
+static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj )  { return (DdNode *)pObj->pData; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -74,11 +76,14 @@ extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
 extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
 extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
 /*=== bbrReach.c ==========================================================*/
-extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
+extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, Saig_ParBbr_t * pPars );
+extern void        Bbr_ManSetDefaultParams( Saig_ParBbr_t * p );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
 
-#ifdef __cplusplus
-}
-#endif
 
 #endif
 
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index 947c393c..8f99ea3c 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -21,6 +21,9 @@
 #include "bbr.h"
 #include "ssw.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,11 +45,11 @@ extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
     DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
     int iOutput, int fVerbose, int fSilent )
 {
-    Ssw_Cex_t * pCex;
+    Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Bbr_ImageTree_t * pTree;
     DdNode * bCubeNs, * bState, * bImage;
@@ -96,7 +99,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
     }
 
     // perform backward analysis
-    Vec_PtrForEachEntryReverse( vOnionRings, bRing, v )
+    Vec_PtrForEachEntryReverse( DdNode *, vOnionRings, bRing, v )
     { 
         // compute the next states
         bImage = Bbr_bddImageCompute( pTree, bState );           
@@ -166,3 +169,5 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index c16a8ff4..8b18d84d 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "bbr.h"
-#include "mtr.h" 
+#include "mtr.h"
+
+ABC_NAMESPACE_IMPL_START
+ 
 
 /* 
     The ideas implemented in this file are inspired by the paper:
@@ -1320,3 +1323,5 @@ DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/bbr/bbrNtbdd.c b/src/aig/bbr/bbrNtbdd.c
index 05c98fe1..09456df0 100644
--- a/src/aig/bbr/bbrNtbdd.c
+++ b/src/aig/bbr/bbrNtbdd.c
@@ -21,6 +21,9 @@
 #include "bbr.h"
 //#include "bar.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 typedef char ProgressBar;
 
 ////////////////////////////////////////////////////////////////////////
@@ -28,7 +31,7 @@ typedef char ProgressBar;
 ////////////////////////////////////////////////////////////////////////
 
 static inline void     Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc )   { pObj->pData = bFunc; }
-static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, pObj->pData ); pObj->pData = NULL; }
+static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); pObj->pData = NULL; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -211,3 +214,5 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index 7d0e4bc0..f76c9671 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -21,11 +21,14 @@
 #include "bbr.h"
 #include "ssw.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern void * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
+extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
     DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, 
     int iOutput, int fVerbose, int fSilent );
 
@@ -33,6 +36,31 @@ extern void * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default resynthesis parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p )
+{
+    memset( p, 0, sizeof(Saig_ParBbr_t) );
+    p->TimeLimit     =     0;
+    p->nBddMax       = 50000;
+    p->nIterMax      =  1000;
+    p->fPartition    =     1;
+    p->fReorder      =     1;
+    p->fReorderImage =     1;
+    p->fVerbose      =     0;
+    p->fSilent       =     0;
+    p->iFrame        =    -1;
+}
+
 /**Function********************************************************************
 
   Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
@@ -208,7 +236,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder,
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
+int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs )
 {
     int fInternalReorder = 0;
     Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
@@ -217,10 +245,10 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     DdNode * bCurrent;
     DdNode * bNext = NULL; // Suppress "might be used uninitialized"
     DdNode * bTemp;
-    int i, nIters, nBddSize;
-    int nThreshold = 10000;
+    Cudd_ReorderingType method;
+    int i, nIters, nBddSize, status;
+    int nThreshold = 10000, clk = clock();
     Vec_Ptr_t * vOnionRings;
-    int status, method;
 
     status = Cudd_ReorderingStatus( dd, &method );
     if ( status )
@@ -228,14 +256,14 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
 
     // start the image computation
     bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
-    if ( fPartition )
-        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), nBddMax, fVerbose );
+    if ( pPars->fPartition )
+        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose );
     else
-        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
+        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose );
     Cudd_RecursiveDeref( dd, bCubeCs );
     if ( pTree == NULL )
     {
-        if ( !fSilent )
+        if ( !pPars->fSilent )
             printf( "BDDs blew up during qualitification scheduling.  " );
         return -1;
     }
@@ -246,30 +274,46 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     // start the onion rings
     vOnionRings = Vec_PtrAlloc( 1000 );
 
-    // perform reachability analisys
+    // perform reachability analysis
     bCurrent = bInitial;   Cudd_Ref( bCurrent );
     bReached = bInitial;   Cudd_Ref( bReached );
     Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
-    for ( nIters = 1; nIters <= nIterMax; nIters++ )
+    for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
     { 
+        // check the runtime limit
+        if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
+        {
+            printf( "Reached timeout after image computation (%d seconds).\n",  pPars->TimeLimit );
+            Vec_PtrFree( vOnionRings );
+            // undo the image tree
+            if ( pPars->fPartition )
+                Bbr_bddImageTreeDelete( pTree );
+            else
+                Bbr_bddImageTreeDelete2( pTree2 );
+            pPars->iFrame = nIters - 1;
+            return -1;
+        }
+
         // compute the next states
-        if ( fPartition )
+        if ( pPars->fPartition )
             bNext = Bbr_bddImageCompute( pTree, bCurrent );           
         else
             bNext = Bbr_bddImageCompute2( pTree2, bCurrent );  
         if ( bNext == NULL )
         {
-            if ( !fSilent )
+            if ( !pPars->fSilent )
                 printf( "BDDs blew up during image computation.  " );
-            if ( fPartition )
+            if ( pPars->fPartition )
                 Bbr_bddImageTreeDelete( pTree );
             else
                 Bbr_bddImageTreeDelete2( pTree2 );
             Vec_PtrFree( vOnionRings );
+            pPars->iFrame = nIters - 1;
             return -1;
         }
         Cudd_Ref( bNext );
         Cudd_RecursiveDeref( dd, bCurrent );
+
         // remap these states into the current state vars
         bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
         Cudd_RecursiveDeref( dd, bTemp );
@@ -278,23 +322,24 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             break;
         // check the BDD size
         nBddSize = Cudd_DagSize(bNext);
-        if ( nBddSize > nBddMax )
+        if ( nBddSize > pPars->nBddMax )
             break;
         // check the result
         for ( i = 0; i < Saig_ManPoNum(p); i++ )
         {
-            if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
+            if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
             {
                 DdNode * bIntersect;
                 bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] );  Cudd_Ref( bIntersect );
                 assert( p->pSeqModel == NULL );
                 p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
-                    vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+                    vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
                 Cudd_RecursiveDeref( dd, bIntersect );
-                if ( !fSilent )
+                if ( !pPars->fSilent )
                     printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) );
                 Cudd_RecursiveDeref( dd, bReached );
                 bReached = NULL;
+                pPars->iFrame = nIters;
                 break;
             }
         }
@@ -310,38 +355,39 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
         bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
         Cudd_RecursiveDeref( dd, bTemp );
         Cudd_RecursiveDeref( dd, bNext );
-        if ( fVerbose )
+        if ( pPars->fVerbose )
             fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
-        if ( fInternalReorder && fReorder && nBddSize > nThreshold )
+        if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold )
         {
-            if ( fVerbose )
+            if ( pPars->fVerbose )
                 fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
             Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
             Cudd_AutodynDisable( dd );
-            if ( fVerbose )
+            if ( pPars->fVerbose )
                 fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
             nThreshold *= 2;
         }
-        if ( fVerbose )
-            fprintf( stdout, "\r" );
+        if ( pPars->fVerbose )
+//            fprintf( stdout, "\r" );
+            fprintf( stdout, "\n" );
     }
     Cudd_RecursiveDeref( dd, bNext );
     // free the onion rings
-    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
         Cudd_RecursiveDeref( dd, bTemp );
     Vec_PtrFree( vOnionRings );
     // undo the image tree
-    if ( fPartition )
+    if ( pPars->fPartition )
         Bbr_bddImageTreeDelete( pTree );
     else
         Bbr_bddImageTreeDelete2( pTree2 );
     if ( bReached == NULL )
         return 0; // proved reachable
     // report the stats
-    if ( fVerbose )
+    if ( pPars->fVerbose )
     {
         double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
-        if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+        if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
             fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
         else
             fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
@@ -350,14 +396,15 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     }
 //ABC_PRB( dd, bReached );
     Cudd_RecursiveDeref( dd, bReached );
-    if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+    if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
     {
-        if ( !fSilent )
+        if ( !pPars->fSilent )
             printf( "Verified only for states reachable in %d frames.  ", nIters );
         return -1; // undecided
     }
-    if ( !fSilent )
+    if ( !pPars->fSilent )
         printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    pPars->iFrame = nIters - 1;
     return 1; // unreachable
 }
 
@@ -372,8 +419,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
+int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
 {
+    int fCheckOutputs = !pPars->fSkipOutCheck;
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
     DdNode * bInitial, * bTemp;
@@ -383,16 +431,24 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
     assert( Saig_ManRegNum(p) > 0 );
 
     // compute the global BDDs of the latches
-    dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );    
+    dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose );    
     if ( dd == NULL )
     {
-        if ( !fSilent )
-            printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+        if ( !pPars->fSilent )
+            printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax );
         return -1;
     }
-    if ( fVerbose )
+    if ( pPars->fVerbose )
         printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
+    // check the runtime limit
+    if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
+    {
+        printf( "Reached timeout after constructing global BDDs (%d seconds).\n",  pPars->TimeLimit );
+        Cudd_Quit( dd );
+        return -1;
+    }
+
     // start the onion rings
     vOnionRings = Vec_PtrAlloc( 1000 );
 
@@ -400,40 +456,40 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
     pbOutputs = Aig_ManCreateOutputs( dd, p );
 
     // create partitions
-    pbParts = Aig_ManCreatePartitions( dd, p, fReorder, fVerbose );
+    pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose );
 
     // create the initial state and the variable map
-    bInitial  = Aig_ManInitStateVarMap( dd, p, fVerbose );  Cudd_Ref( bInitial );
+    bInitial  = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose );  Cudd_Ref( bInitial );
 
     // set reordering
-    if ( fReorderImage )
+    if ( pPars->fReorderImage )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
     // check the result
     RetValue = -1;
     for ( i = 0; i < Saig_ManPoNum(p); i++ )
     {
-        if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
+        if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
         {
             DdNode * bIntersect;
             bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] );  Cudd_Ref( bIntersect );
             assert( p->pSeqModel == NULL );
             p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
-                vOnionRings, bIntersect, i, fVerbose, fSilent ); 
+                vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
             Cudd_RecursiveDeref( dd, bIntersect );
-            if ( !fSilent )
+            if ( !pPars->fSilent )
                 printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i );
             RetValue = 0;
             break;
         }
     }
     // free the onion rings
-    Vec_PtrForEachEntry( vOnionRings, bTemp, i )
+    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
         Cudd_RecursiveDeref( dd, bTemp );
     Vec_PtrFree( vOnionRings );
     // explore reachable states
     if ( RetValue == -1 )
-        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); 
+        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs ); 
 
     // cleanup
     Cudd_RecursiveDeref( dd, bInitial );
@@ -443,13 +499,13 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
     for ( i = 0; i < Saig_ManPoNum(p); i++ )
         Cudd_RecursiveDeref( dd, pbOutputs[i] );
     ABC_FREE( pbOutputs );
-    if ( RetValue == -1 )
+//    if ( RetValue == -1 )
         Cudd_Quit( dd );
-    else
-        Bbr_StopManager( dd );
+//    else
+//        Bbr_StopManager( dd );
 
     // report the runtime
-    if ( !fSilent )
+    if ( !pPars->fSilent )
     {
     ABC_PRT( "Time", clock() - clk );
     fflush( stdout );
@@ -468,24 +524,25 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
+int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
 {
-    Ssw_Cex_t * pCexOld, * pCexNew;
+    Abc_Cex_t * pCexOld, * pCexNew;
     Aig_Man_t * p;
     Aig_Obj_t * pObj;
     Vec_Int_t * vInputMap;
     int i, k, Entry, iBitOld, iBitNew, RetValue;
+//    pPars->fVerbose = 1;
     // check if there are PIs without fanout
     Saig_ManForEachPi( pInit, pObj, i )
         if ( Aig_ObjRefs(pObj) == 0 )
             break;
     if ( i == Saig_ManPiNum(pInit) )
-        return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
+        return Aig_ManVerifyUsingBdds_int( pInit, pPars );
     // create new AIG
     p = Aig_ManDupTrim( pInit );
     assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
     assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
-    RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
+    RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
     if ( RetValue != 0 )
     {
         Aig_ManStop( p );
@@ -498,7 +555,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP
     vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
     Saig_ManForEachPi( pInit, pObj, i )
         if ( pObj->pData != NULL )
-            Vec_IntPush( vInputMap, Aig_ObjPioNum(pObj->pData) );
+            Vec_IntPush( vInputMap, Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) );
         else
             Vec_IntPush( vInputMap, -1 );
     // create new pattern
@@ -537,3 +594,5 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/bbr/bbr_.c b/src/aig/bbr/bbr_.c
index f94c50e6..df934f7d 100644
--- a/src/aig/bbr/bbr_.c
+++ b/src/aig/bbr/bbr_.c
@@ -20,6 +20,9 @@
 
 #include "__Int.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,3 +48,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+