summaryrefslogtreecommitdiffstats
path: root/src/aig/llb
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/llb')
-rw-r--r--src/aig/llb/llb4Cluster.c339
-rw-r--r--src/aig/llb/llb4Image.c101
-rw-r--r--src/aig/llb/llb4Nonlin.c22
-rw-r--r--src/aig/llb/llbInt.h1
4 files changed, 450 insertions, 13 deletions
diff --git a/src/aig/llb/llb4Cluster.c b/src/aig/llb/llb4Cluster.c
new file mode 100644
index 00000000..71e044be
--- /dev/null
+++ b/src/aig/llb/llb4Cluster.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+ FileName [llb2Cluster.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [BDD based reachability.]
+
+ Synopsis [Non-linear quantification scheduling.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Find good static variable ordering.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
+{
+ Aig_Obj_t * pFanin0, * pFanin1;
+ if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent( pAig, pObj );
+ assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+ return;
+ }
+ // try fanins with higher level first
+ pFanin0 = Aig_ObjFanin0(pObj);
+ pFanin1 = Aig_ObjFanin1(pObj);
+// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
+ if ( pFanin0->Level > pFanin1->Level )
+ {
+ Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
+ Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
+ }
+ else
+ {
+ Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
+ Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
+ }
+ Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find good static variable ordering.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig )
+{
+ Vec_Int_t * vNodes = NULL;
+ Vec_Int_t * vOrder;
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ // collect nodes in the order
+ vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
+ Aig_ManIncrementTravId( pAig );
+ Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+ Aig_ManForEachPo( pAig, pObj, i )
+ {
+printf( "PO %d Var %d\n", i, Counter );
+ Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+ Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
+ }
+ Aig_ManForEachPi( pAig, pObj, i )
+ if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+ Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+ Aig_ManCleanMarkA( pAig );
+ Vec_IntFreeP( &vNodes );
+ assert( Counter == Aig_ManObjNum(pAig) - 1 );
+ return vOrder;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives BDDs for the partitions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+ Vec_Ptr_t * vRoots;
+ Aig_Obj_t * pObj;
+ DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
+ int i;
+ Aig_ManCleanData( pAig );
+ // assign elementary variables
+ Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+ {
+ pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+ Cudd_Ref( (DdNode *)pObj->pData );
+ }
+ Aig_ManForEachPo( pAig, pObj, i )
+ pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+ // compute intermediate BDDs
+ vRoots = Vec_PtrAlloc( 100 );
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+ bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+ bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
+ Cudd_Ref( bBdd );
+ if ( pObj->pData == NULL )
+ {
+ pObj->pData = bBdd;
+ continue;
+ }
+ // create new partition
+ bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );
+ if ( bPart == NULL )
+ goto finish;
+ Cudd_Ref( bPart );
+ Cudd_RecursiveDeref( dd, bBdd );
+ Vec_PtrPush( vRoots, bPart );
+ }
+ // compute register output BDDs
+ Aig_ManForEachPo( pAig, pObj, i )
+ {
+ bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+ bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );
+ if ( bPart == NULL )
+ goto finish;
+ Cudd_Ref( bPart );
+ Vec_PtrPush( vRoots, bPart );
+//printf( "%d ", Cudd_DagSize(bPart) );
+ }
+//printf( "\n" );
+ Aig_ManForEachNode( pAig, pObj, i )
+ Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+ return vRoots;
+ // early termination
+finish:
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( pObj->pData )
+ Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+ Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
+ Cudd_RecursiveDeref( dd, bPart );
+ Vec_PtrFree( vRoots );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates quantifiable varaibles for both types of traversal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+ Vec_Int_t * vVars2Q;
+ Aig_Obj_t * pObj;
+ int i;
+ vVars2Q = Vec_IntAlloc( 0 );
+ Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
+ Saig_ManForEachLo( pAig, pObj, i )
+ Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+ Aig_ManForEachPo( pAig, pObj, i )
+ Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+ return vVars2Q;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates quantifiable varaibles for both types of traversal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
+{
+ DdNode * bSupp;
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bFunc );
+ if ( !fCo && !fFlop )
+ {
+ Saig_ManForEachPi( pAig, pObj, i )
+ Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+ }
+ else if ( fCo && !fFlop )
+ {
+ Saig_ManForEachPo( pAig, pObj, i )
+ Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+ }
+ else if ( !fCo && fFlop )
+ {
+ Saig_ManForEachLo( pAig, pObj, i )
+ Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+ }
+ else if ( fCo && fFlop )
+ {
+ Saig_ManForEachLi( pAig, pObj, i )
+ Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+ }
+ Cudd_RecursiveDeref( dd, bFunc );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates quantifiable varaibles for both types of traversal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
+{
+ DdNode * bTemp;
+ int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
+ Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
+ {
+ nSuppAll = Cudd_SupportSize(dd,bTemp);
+ nSuppPi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
+ nSuppPo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
+ nSuppLi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
+ nSuppLo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
+ nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
+
+ printf( "%4d : bdd =%6d supp =%3d ", i, Cudd_DagSize(bTemp), nSuppAll );
+ printf( "pi =%3d ", nSuppPi );
+ printf( "po =%3d ", nSuppPo );
+ printf( "lo =%3d ", nSuppLo );
+ printf( "li =%3d ", nSuppLi );
+ printf( "and =%3d", nSuppAnd );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Llb_Nonlin4Cluster( Aig_Man_t * pAig )
+{
+ DdManager * dd;
+ Vec_Int_t * vOrder, * vVars2Q;
+ Vec_Ptr_t * vParts, * vGroups;
+ DdNode * bTemp;
+ int i;
+
+ // create the BDD manager
+ dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
+ vOrder = Llb_Nonlin4FindOrder( pAig );
+ vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
+ vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder );
+
+ vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, 500 );
+
+ Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
+
+ Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
+ Cudd_RecursiveDeref( dd, bTemp );
+
+ Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
+ Cudd_RecursiveDeref( dd, bTemp );
+ Extra_StopManager( dd );
+// Cudd_Quit( dd );
+
+ Vec_IntFree( vOrder );
+ Vec_IntFree( vVars2Q );
+ Vec_PtrFree( vParts );
+ Vec_PtrFree( vGroups );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c
index b882ac65..45efaead 100644
--- a/src/aig/llb/llb4Image.c
+++ b/src/aig/llb/llb4Image.c
@@ -48,6 +48,7 @@ struct Llb_Mgr_t_
{
DdManager * dd; // working BDD manager
Vec_Int_t * vVars2Q; // variables to quantify
+ int nSizeMax; // maximum size of the cluster
// internal
Llb_Prt_t ** pParts; // partitions
Llb_Var_t ** pVars; // variables
@@ -263,7 +264,7 @@ int Llb_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
int i, RetValue, nSizeNew;
// create cube to be quantified
bCube = Llb_Nonlin4CreateCube1( p, pPart ); Cudd_Ref( bCube );
- assert( !Cudd_IsConstant(bCube) );
+// assert( !Cudd_IsConstant(bCube) );
// derive new function
pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
@@ -323,9 +324,13 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
int i, RetValue, nSuppSize;
int iPart1 = pPart1->iPart;
int iPart2 = pPart2->iPart;
+ int liveBeg, liveEnd;
// create cube to be quantified
bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
+
+printf( "Quantifying " ); Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
+
if ( fVerbose )
{
printf( "\n" );
@@ -334,7 +339,11 @@ Llb_Nonlin4Print( p );
printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
}
+liveBeg = p->dd->keys - p->dd->dead;
bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );
+liveEnd = p->dd->keys - p->dd->dead;
+//printf( "%d ", liveEnd-liveBeg );
+
if ( bFunc == NULL )
{
Cudd_RecursiveDeref( p->dd, bCube );
@@ -343,6 +352,8 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bCube );
+printf( "Createing part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc ); printf( "\n" );
+
// create new partition
pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
pTemp->iPart = p->iPartFree++;
@@ -573,8 +584,15 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
Llb_Nonlin4CheckVars( p );
// find variable with minimum score
Llb_MgrForEachVar( p, pVar, i )
+ {
+ if ( p->nSizeMax && pVar->nScore > p->nSizeMax )
+ continue;
+// if ( pVarBest == NULL || Vec_IntSize(pVarBest->vParts) * pVarBest->nScore > Vec_IntSize(pVar->vParts) * pVar->nScore )
if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
pVarBest = pVar;
+// printf( "%d ", pVar->nScore );
+ }
+//printf( "\n" );
if ( pVarBest == NULL )
return 0;
// find two partitions with minimum size
@@ -592,6 +610,10 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
pPart2Best = pPart;
}
}
+printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
+Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
+Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
+
*ppPart1 = pPart1Best;
*ppPart2 = pPart2Best;
return 1;
@@ -661,13 +683,14 @@ void Llb_Nonlin4VerifyScores( Llb_Mgr_t * p )
SeeAlso []
***********************************************************************/
-Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
+Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q, int nSizeMax )
{
Llb_Mgr_t * p;
DdNode * bFunc;
int i;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
p->dd = dd;
+ p->nSizeMax = nSizeMax;
p->vVars2Q = vVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vParts);
@@ -678,7 +701,8 @@ Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurr
Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
Llb_Nonlin4AddPartition( p, i, bFunc );
// add partition
- Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
+ if ( bCurrent )
+ Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
return p;
}
@@ -710,11 +734,11 @@ void Llb_Nonlin4Free( Llb_Mgr_t * p )
/**Function*************************************************************
- Synopsis [Performs image computation.]
+ Synopsis []
- Description [Computes image of BDDs (vFuncs).]
+ Description []
- SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
+ SideEffects []
SeeAlso []
@@ -726,7 +750,7 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
DdNode * bFunc, * bTemp;
int i, nReorders;
// start the manager
- p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q );
+ p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q, 0 );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
@@ -744,8 +768,8 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
}
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_Nonlin4RecomputeScores( p );
- else
- Llb_Nonlin4VerifyScores( p );
+// else
+// Llb_Nonlin4VerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
@@ -756,11 +780,70 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
}
// nSuppMax = p->nSuppMax;
Llb_Nonlin4Free( p );
+//printf( "\n" );
// return
Cudd_Deref( bFunc );
return bFunc;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax )
+{
+ Vec_Ptr_t * vGroups;
+ Llb_Prt_t * pPart, * pPart1, * pPart2;
+ Llb_Mgr_t * p;
+ int i, nReorders;
+ // start the manager
+ p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
+ // remove singles
+ Llb_MgrForEachPart( p, pPart, i )
+ if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
+ Llb_Nonlin4Quantify1( p, pPart );
+ // compute scores
+ Llb_Nonlin4RecomputeScores( p );
+ // iteratively quantify variables
+ while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
+ {
+ nReorders = Cudd_ReadReorderings(dd);
+ if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
+ {
+ Llb_Nonlin4Free( p );
+ return NULL;
+ }
+ if ( nReorders < Cudd_ReadReorderings(dd) )
+ Llb_Nonlin4RecomputeScores( p );
+ else
+ Llb_Nonlin4VerifyScores( p );
+ }
+ // load partitions
+ vGroups = Vec_PtrAlloc( 1000 );
+ Llb_MgrForEachPart( p, pPart, i )
+ {
+ if ( Cudd_IsConstant(pPart->bFunc) )
+ {
+ assert( !Cudd_IsComplement(pPart->bFunc) );
+ continue;
+ }
+ Vec_PtrPush( vGroups, pPart->bFunc );
+ Cudd_Ref( pPart->bFunc );
+printf( "Part %d ", pPart->iPart );
+Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
+ }
+ Llb_Nonlin4Free( p );
+ return vGroups;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 11f5ba3e..d7b3c6c3 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -255,6 +255,8 @@ void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_In
assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
if ( Aig_ObjIsPi(pObj) )
{
+// if ( Saig_ObjIsLo(pAig, pObj) )
+// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
return;
}
@@ -345,7 +347,11 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
}
Aig_ManForEachPi( pAig, pObj, i )
if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+ {
+// if ( Saig_ObjIsLo(pAig, pObj) )
+// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+ }
assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
Aig_ManCleanMarkA( pAig );
Vec_IntFreeP( &vNodes );
@@ -701,6 +707,13 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
if ( Cudd_IsConstant(p->bCurrent) )
break;
+/*
+ // reduce BDD size using constrain // Cudd_bddRestrict
+ p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );
+ Cudd_Ref( p->bCurrent );
+printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
+ Cudd_RecursiveDeref( p->dd, bAux );
+*/
// add to the reached set
p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );
@@ -715,14 +728,15 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
Cudd_Ref( p->bReached );
Cudd_RecursiveDeref( p->dd, bAux );
+
// report the results
if ( p->pPars->fVerbose )
{
printf( "I =%5d : ", nIters );
- printf( "Fr =%7d ", nBddSizeFr );
- printf( "ImNs =%7d ", nBddSizeTo );
- printf( "ImCs =%7d ", nBddSizeTo2 );
- printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
+ printf( "Fr =%7d ", nBddSizeFr );
+ printf( "ImNs =%7d ", nBddSizeTo );
+ printf( "ImCs =%7d ", nBddSizeTo2 );
+ printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
Abc_PrintTime( 1, "T", clock() - clkIter );
}
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 357ddb5c..5d145831 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -184,6 +184,7 @@ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager *
/*=== llb4Image.c =======================================================*/
extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
+extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
/*=== llb4Map.c =========================================================*/
//extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
/*=== llb4Nonlin.c ======================================================*/
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 13:31:45 +0000