diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:53 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:53 -0700 |
commit | 0398ced8243806439b814f21ca7d6e584cea13a1 (patch) | |
tree | 8812787fdd028d6fa04b1206c628a1b0c4743417 /src/aig/bbr/bbrReach.c | |
parent | 70697f868a263930e971c062e5b46e64fbb1ee18 (diff) | |
download | abc-0398ced8243806439b814f21ca7d6e584cea13a1.tar.gz abc-0398ced8243806439b814f21ca7d6e584cea13a1.tar.bz2 abc-0398ced8243806439b814f21ca7d6e584cea13a1.zip |
Version abc90714
committer: Baruch Sterin <baruchs@gmail.com>
Diffstat (limited to 'src/aig/bbr/bbrReach.c')
-rw-r--r-- | src/aig/bbr/bbrReach.c | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index 1d43f6fb..7d0e4bc0 100644 --- a/src/aig/bbr/bbrReach.c +++ b/src/aig/bbr/bbrReach.c @@ -220,11 +220,16 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D int i, nIters, nBddSize; int nThreshold = 10000; Vec_Ptr_t * vOnionRings; + int status, method; + + status = Cudd_ReorderingStatus( dd, &method ); + if ( status ) + Cudd_AutodynDisable( dd ); // 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), fVerbose ); + pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), nBddMax, fVerbose ); else pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose ); Cudd_RecursiveDeref( dd, bCubeCs ); @@ -235,6 +240,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D return -1; } + if ( status ) + Cudd_AutodynEnable( dd, method ); + // start the onion rings vOnionRings = Vec_PtrAlloc( 1000 ); @@ -360,11 +368,11 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D Description [] SideEffects [] - + SeeAlso [] ***********************************************************************/ -int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) +int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ) { DdManager * dd; DdNode ** pbParts, ** pbOutputs; @@ -397,6 +405,10 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP // create the initial state and the variable map bInitial = Aig_ManInitStateVarMap( dd, p, fVerbose ); Cudd_Ref( bInitial ); + // set reordering + if ( fReorderImage ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + // check the result RetValue = -1; for ( i = 0; i < Saig_ManPoNum(p); i++ ) @@ -456,7 +468,7 @@ 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 fVerbose, int fSilent ) +int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ) { Ssw_Cex_t * pCexOld, * pCexNew; Aig_Man_t * p; @@ -468,12 +480,12 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP if ( Aig_ObjRefs(pObj) == 0 ) break; if ( i == Saig_ManPiNum(pInit) ) - return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); + return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent ); // 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, fVerbose, fSilent ); + RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent ); if ( RetValue != 0 ) { Aig_ManStop( p ); |