summaryrefslogtreecommitdiffstats
path: root/src/aig/bbr
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/bbr')
-rw-r--r--src/aig/bbr/bbr.h4
-rw-r--r--src/aig/bbr/bbrCex.c2
-rw-r--r--src/aig/bbr/bbrImage.c18
-rw-r--r--src/aig/bbr/bbrReach.c24
4 files changed, 30 insertions, 18 deletions
diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
index ee91fe8b..e5d585ce 100644
--- a/src/aig/bbr/bbr.h
+++ b/src/aig/bbr/bbr.h
@@ -57,7 +57,7 @@ typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t;
extern Bbr_ImageTree_t * Bbr_bddImageStart(
DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
- int nVars, DdNode ** pbVars, int fVerbose );
+ int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
extern DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
extern void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
extern DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
@@ -74,7 +74,7 @@ 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 fVerbose, int fSilent );
+extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
#ifdef __cplusplus
}
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index 41253dbc..4555570a 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -63,7 +63,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
// create the cube of NS variables
bCubeNs = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) ); Cudd_Ref( bCubeNs );
- pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
+ pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose );
Cudd_RecursiveDeref( dd, bCubeNs );
if ( pTree == NULL )
{
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index edd344bf..aed302eb 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -27,7 +27,7 @@
Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
Image Computation. ICCAD, 2001.
*/
-
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -49,6 +49,7 @@ struct Bbr_ImageTree_t_
int nNodesMax; // the max number of nodes in one iter
int nNodesMaxT; // the overall max number of nodes
int nIter; // the number of iterations with this tree
+ int nBddMax; // the number of node to stop
};
struct Bbr_ImageNode_t_
@@ -89,8 +90,6 @@ struct Bbr_ImageVar_t_
/* Macro declarations */
/*---------------------------------------------------------------------------*/
-#define BDD_BLOW_UP 2000000
-
#define b0 Cudd_Not((dd)->one)
#define b1 (dd)->one
@@ -116,7 +115,7 @@ static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
static int Bbr_BuildTreeNode( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes,
- int nVars, Bbr_ImageVar_t ** pVars, int * pfStop );
+ int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes );
static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
@@ -166,7 +165,7 @@ static void Bbr_bddPrint( DdManager * dd, DdNode * F );
Bbr_ImageTree_t * Bbr_bddImageStart(
DdManager * dd, DdNode * bCare, // the care set
int nParts, DdNode ** pbParts, // the partitions for image computation
- int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
+ int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not quantified!)
{
Bbr_ImageTree_t * pTree;
Bbr_ImagePart_t ** pParts;
@@ -184,7 +183,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
pCare = pNodes[nParts];
// process the nodes
- while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) );
+ while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
// consider the case of BDD node blowup
if ( fStop )
@@ -213,6 +212,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
pTree->pCare = pCare;
+ pTree->nBddMax = nBddMax;
pTree->fVerbose = fVerbose;
// merge the topmost nodes
@@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
if ( pTree->nNodesMax < nNodes )
pTree->nNodesMax = nNodes;
}
- if ( dd->keys-dd->dead > BDD_BLOW_UP )
+ if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
return 0;
return 1;
}
@@ -716,7 +716,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
***********************************************************************/
int Bbr_BuildTreeNode( DdManager * dd,
int nNodes, Bbr_ImageNode_t ** pNodes,
- int nVars, Bbr_ImageVar_t ** pVars, int * pfStop )
+ int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax )
{
Bbr_ImageNode_t * pNode1, * pNode2;
Bbr_ImageVar_t * pVar;
@@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
}
*pfStop = 0;
- if ( dd->keys-dd->dead > BDD_BLOW_UP )
+ if ( dd->keys-dd->dead > (unsigned)nBddMax )
{
*pfStop = 1;
return 0;
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-06 01:55:29 +0000