From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/aig/bbr/bbr.h | 23 ++++--- src/aig/bbr/bbrCex.c | 11 +++- src/aig/bbr/bbrImage.c | 7 ++- src/aig/bbr/bbrNtbdd.c | 7 ++- src/aig/bbr/bbrReach.c | 165 +++++++++++++++++++++++++++++++++---------------- src/aig/bbr/bbr_.c | 5 ++ 6 files changed, 151 insertions(+), 67 deletions(-) (limited to 'src/aig/bbr') 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 -#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 + -- cgit v1.2.3