Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

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 );