/**CFile****************************************************************
FileName [llb3Image.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Computes image using partitioned structure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb3Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Var_t_ Llb_Var_t;
struct Llb_Var_t_
{
int iVar; // variable number
int nScore; // variable score
Vec_Int_t * vParts; // partitions
};
typedef struct Llb_Prt_t_ Llb_Prt_t;
struct Llb_Prt_t_
{
int iPart; // partition number
int nSize; // the number of BDD nodes
DdNode * bFunc; // the partition
Vec_Int_t * vVars; // support
};
typedef struct Llb_Mgr_t_ Llb_Mgr_t;
struct Llb_Mgr_t_
{
Aig_Man_t * pAig; // AIG manager
Vec_Ptr_t * vLeaves; // leaves in the AIG manager
Vec_Ptr_t * vRoots; // roots in the AIG manager
DdManager * dd; // working BDD manager
int * pVars2Q; // variables to quantify
// internal
Llb_Prt_t ** pParts; // partitions
Llb_Var_t ** pVars; // variables
int iPartFree; // next free partition
int nVars; // the number of BDD variables
int nSuppMax; // maximum support size
// temporary
int * pSupp; // temporary support storage
};
static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i ) { return p->pVars[i]; }
static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pParts[i]; }
// iterator over vars
#define Llb_MgrForEachVar( p, pVar, i ) \
for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
// iterator over parts
#define Llb_MgrForEachPart( p, pPart, i ) \
for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
// iterator over vars of one partition
#define Llb_PartForEachVar( p, pPart, pVar, i ) \
for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
// iterator over parts of one variable
#define Llb_VarForEachPart( p, pVar, pPart, i ) \
for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
// statistics
abctime timeBuild, timeAndEx, timeOther;
int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Removes one variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
{
assert( p->pVars[pVar->iVar] == pVar );
p->pVars[pVar->iVar] = NULL;
Vec_IntFree( pVar->vParts );
ABC_FREE( pVar );
}
/**Function*************************************************************
Synopsis [Removes one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
assert( p->pParts[pPart->iPart] == pPart );
p->pParts[pPart->iPart] = NULL;
Vec_IntFree( pPart->vVars );
Cudd_RecursiveDeref( p->dd, pPart->bFunc );
ABC_FREE( pPart );
}
/**Function*************************************************************
Synopsis [Create cube with singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
DdNode * bCube, * bTemp;
Llb_Var_t * pVar;
int i;
abctime TimeStop;
TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
Llb_PartForEachVar( p, pPart, pVar, i )
{
assert( Vec_IntSize(pVar->vParts) > 0 );
if ( Vec_IntSize(pVar->vParts) != 1 )
continue;
assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( p->dd, bTemp );
}
Cudd_Deref( bCube );
p->dd->TimeStop = TimeStop;
return bCube;
}
/**Function*************************************************************
Synopsis [Create cube of variables appearing only in two partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
{
DdNode * bCube, * bTemp;
Llb_Var_t * pVar;
int i;
abctime TimeStop;
TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube );
Llb_PartForEachVar( p, pPart1, pVar, i )
{
assert( Vec_IntSize(pVar->vParts) > 0 );
if ( Vec_IntSize(pVar->vParts) != 2 )
continue;
if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
(Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
{
bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( p->dd, bTemp );
}
}
Cudd_Deref( bCube );
p->dd->TimeStop = TimeStop;
return bCube;
}
/**Function*************************************************************
Synopsis [Returns 1 if partition has singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinHasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
{
Llb_Var_t * pVar;
int i;
Llb_PartForEachVar( p, pPart, pVar, i )
if ( Vec_IntSize(pVar->vParts) == 1 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Returns 1 if partition has singleton variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrint( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k;
printf( "\n" );
Llb_MgrForEachVar( p, pVar, i )
{
printf( "Var %3d : ", i );
Llb_VarForEachPart( p, pVar, pPart, k )
printf( "%d ", pPart->iPart );
printf( "\n" );
}
Llb_MgrForEachPart( p, pPart, i )
{
printf( "Part %3d : ", i );
Llb_PartForEachVar( p, pPart, pVar, k )
printf( "%d ", pVar->iVar );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Quantifies singles belonging to one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
{
Llb_Var_t * pVar;
Llb_Prt_t * pTemp;
Vec_Ptr_t * vSingles;
DdNode * bCube, * bTemp;
int i, RetValue, nSizeNew;
if ( fSubset )
{
int Length;
// int nSuppSize = Cudd_SupportSize( p->dd, pPart->bFunc );
// pPart->bFunc = Cudd_SubsetHeavyBranch( p->dd, bTemp = pPart->bFunc, nSuppSize, 3*pPart->nSize/4 ); Cudd_Ref( pPart->bFunc );
pPart->bFunc = Cudd_LargestCube( p->dd, bTemp = pPart->bFunc, &Length ); Cudd_Ref( pPart->bFunc );
printf( "Subsetting %3d : ", pPart->iPart );
printf( "(Supp =%3d Node =%5d) -> ", Cudd_SupportSize(p->dd, bTemp), Cudd_DagSize(bTemp) );
printf( "(Supp =%3d Node =%5d)\n", Cudd_SupportSize(p->dd, pPart->bFunc), Cudd_DagSize(pPart->bFunc) );
RetValue = (Cudd_DagSize(bTemp) == Cudd_DagSize(pPart->bFunc));
Cudd_RecursiveDeref( p->dd, bTemp );
if ( RetValue )
return 1;
}
else
{
// create cube to be quantified
bCube = Llb_NonlinCreateCube1( p, pPart ); Cudd_Ref( 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 );
Cudd_RecursiveDeref( p->dd, bCube );
}
// get support
vSingles = Vec_PtrAlloc( 0 );
nSizeNew = Cudd_DagSize(pPart->bFunc);
Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
Llb_PartForEachVar( p, pPart, pVar, i )
if ( p->pSupp[pVar->iVar] )
{
assert( Vec_IntSize(pVar->vParts) > 1 );
pVar->nScore -= pPart->nSize - nSizeNew;
}
else
{
RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
assert( RetValue );
pVar->nScore -= pPart->nSize;
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
// update partition
pPart->nSize = nSizeNew;
Vec_IntClear( pPart->vVars );
for ( i = 0; i < p->nVars; i++ )
if ( p->pSupp[i] && p->pVars2Q[i] )
Vec_IntPush( pPart->vVars, i );
// remove other variables
Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
Llb_NonlinQuantify1( p, pTemp, 0 );
Vec_PtrFree( vSingles );
return 0;
}
/**Function*************************************************************
Synopsis [Quantifies singles belonging to one partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
{
int fVerbose = 0;
Llb_Var_t * pVar;
Llb_Prt_t * pTemp;
Vec_Ptr_t * vSingles;
DdNode * bCube, * bFunc;
int i, RetValue, nSuppSize;
// int iPart1 = pPart1->iPart;
// int iPart2 = pPart2->iPart;
// create cube to be quantified
bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube );
if ( fVerbose )
{
printf( "\n" );
printf( "\n" );
Llb_NonlinPrint( p );
printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" );
}
// derive new function
// bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); Cudd_Ref( bFunc );
/*
bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );
if ( bFunc == NULL )
{
int RetValue;
Cudd_RecursiveDeref( p->dd, bCube );
if ( pPart1->nSize < pPart2->nSize )
RetValue = Llb_NonlinQuantify1( p, pPart1, 1 );
else
RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
if ( RetValue )
Limit = Limit + 1000;
Llb_NonlinQuantify2( p, pPart1, pPart2 );
return 0;
}
Cudd_Ref( bFunc );
*/
// bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut );
bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );
if ( bFunc == NULL )
{
Cudd_RecursiveDeref( p->dd, bCube );
return 0;
}
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bCube );
// create new partition
pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
pTemp->iPart = p->iPartFree++;
pTemp->nSize = Cudd_DagSize(bFunc);
pTemp->bFunc = bFunc;
pTemp->vVars = Vec_IntAlloc( 8 );
// update variables
Llb_PartForEachVar( p, pPart1, pVar, i )
{
RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
assert( RetValue );
pVar->nScore -= pPart1->nSize;
}
// update variables
Llb_PartForEachVar( p, pPart2, pVar, i )
{
RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
assert( RetValue );
pVar->nScore -= pPart2->nSize;
}
// add variables to the new partition
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( i = 0; i < p->nVars; i++ )
{
nSuppSize += p->pSupp[i];
if ( p->pSupp[i] && p->pVars2Q[i] )
{
pVar = Llb_MgrVar( p, i );
pVar->nScore += pTemp->nSize;
Vec_IntPush( pVar->vParts, pTemp->iPart );
Vec_IntPush( pTemp->vVars, i );
}
}
p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
// remove variables and collect partitions with singleton variables
vSingles = Vec_PtrAlloc( 0 );
Llb_PartForEachVar( p, pPart1, pVar, i )
{
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
{
if ( fVerbose )
printf( "Adding partition %d because of var %d.\n",
Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
}
Llb_PartForEachVar( p, pPart2, pVar, i )
{
if ( pVar == NULL )
continue;
if ( Vec_IntSize(pVar->vParts) == 0 )
Llb_NonlinRemoveVar( p, pVar );
else if ( Vec_IntSize(pVar->vParts) == 1 )
{
if ( fVerbose )
printf( "Adding partition %d because of var %d.\n",
Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
}
}
// remove partitions
Llb_NonlinRemovePart( p, pPart1 );
Llb_NonlinRemovePart( p, pPart2 );
// remove other variables
if ( fVerbose )
Llb_NonlinPrint( p );
Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
{
if ( fVerbose )
printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
Llb_NonlinQuantify1( p, pTemp, 0 );
}
if ( fVerbose )
Llb_NonlinPrint( p );
Vec_PtrFree( vSingles );
return 1;
}
/**Function*************************************************************
Synopsis [Computes volume of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinCutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Saig_ObjIsLi(p, pObj) )
{
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
return;
}
if ( Aig_ObjIsConst1(pObj) )
return;
assert( Aig_ObjIsNode(pObj) );
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
Llb_NonlinCutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Computes volume of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
// mark the lower cut with the traversal ID
Aig_ManIncrementTravId(p);
Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
// count the upper cut
vNodes = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
Llb_NonlinCutNodes_rec( p, pObj, vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis [Returns array of BDDs for the roots in terms of the leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
{
Vec_Ptr_t * vNodes, * vResult;
Aig_Obj_t * pObj;
DdNode * bBdd0, * bBdd1, * bProd;
int i, k;
Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
vNodes = Llb_NonlinCutNodes( p, vLower, vUpper );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
// pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
if ( pObj->pData == NULL )
{
Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
if ( pObj->pData )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return NULL;
}
Cudd_Ref( (DdNode *)pObj->pData );
}
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
{
bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
}
else
{
assert( Saig_ObjIsLi(p, pObj) );
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), bBdd0 ); Cudd_Ref( bProd );
}
Vec_PtrPush( vResult, bProd );
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return vResult;
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
{
if ( p->pVars[iVar] == NULL )
{
p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
p->pVars[iVar]->iVar = iVar;
p->pVars[iVar]->nScore = 0;
p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
}
Vec_IntPush( p->pVars[iVar]->vParts, iPart );
Vec_IntPush( p->pParts[iPart]->vVars, iVar );
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
{
int k, nSuppSize;
assert( !Cudd_IsConstant(bFunc) );
// create partition
p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
p->pParts[i]->iPart = i;
p->pParts[i]->bFunc = bFunc;
p->pParts[i]->vVars = Vec_IntAlloc( 8 );
// add support dependencies
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( k = 0; k < p->nVars; k++ )
{
nSuppSize += p->pSupp[k];
if ( p->pSupp[k] && p->pVars2Q[k] )
Llb_NonlinAddPair( p, bFunc, i, k );
}
p->nSuppMax = Abc_MaxInt( p->nSuppMax, nSuppSize );
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinStart( Llb_Mgr_t * p )
{
Vec_Ptr_t * vRootBdds;
DdNode * bFunc;
int i;
// create and collect BDDs
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
if ( vRootBdds == NULL )
return 0;
// add pairs (refs are consumed inside)
Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
Llb_NonlinAddPartition( p, i, bFunc );
Vec_PtrFree( vRootBdds );
return 1;
}
/**Function*************************************************************
Synopsis [Checks that each var appears in at least one partition.]
Description []
SideEffects []
SeeAlso []
**********************************************************************/
void Llb_NonlinCheckVars( Llb_Mgr_t * p )
{
Llb_Var_t * pVar;
int i;
Llb_MgrForEachVar( p, pVar, i )
assert( Vec_IntSize(pVar->vParts) > 1 );
}
/**Function*************************************************************
Synopsis [Find next partition to quantify]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
{
Llb_Var_t * pVar, * pVarBest = NULL;
Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
int i;
Llb_NonlinCheckVars( p );
// find variable with minimum score
Llb_MgrForEachVar( p, pVar, i )
if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
pVarBest = pVar;
if ( pVarBest == NULL )
return 0;
// find two partitions with minimum size
Llb_VarForEachPart( p, pVarBest, pPart, i )
{
if ( pPart1Best == NULL )
pPart1Best = pPart;
else if ( pPart2Best == NULL )
pPart2Best = pPart;
else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
{
if ( pPart1Best->nSize > pPart2Best->nSize )
pPart1Best = pPart;
else
pPart2Best = pPart;
}
}
*ppPart1 = pPart1Best;
*ppPart2 = pPart2Best;
return 1;
}
/**Function*************************************************************
Synopsis [Reorders BDDs in the working manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose )
{
abctime clk = Abc_Clock();
if ( fVerbose )
Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
if ( fTwice )
{
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
}
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis [Recomputes scores after variable reordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinRecomputeScores( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k;
Llb_MgrForEachPart( p, pPart, i )
pPart->nSize = Cudd_DagSize(pPart->bFunc);
Llb_MgrForEachVar( p, pVar, i )
{
pVar->nScore = 0;
Llb_VarForEachPart( p, pVar, pPart, k )
pVar->nScore += pPart->nSize;
}
}
/**Function*************************************************************
Synopsis [Recomputes scores after variable reordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i, k, nScore;
Llb_MgrForEachPart( p, pPart, i )
assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
Llb_MgrForEachVar( p, pVar, i )
{
nScore = 0;
Llb_VarForEachPart( p, pVar, pPart, k )
nScore += pPart->nSize;
assert( nScore == pVar->nScore );
}
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd )
{
Llb_Mgr_t * p;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
p->pAig = pAig;
p->vLeaves = vLeaves;
p->vRoots = vRoots;
p->dd = dd;
p->pVars2Q = pVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vRoots);
p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) );
return p;
}
/**Function*************************************************************
Synopsis [Stops non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinFree( Llb_Mgr_t * p )
{
Llb_Prt_t * pPart;
Llb_Var_t * pVar;
int i;
Llb_MgrForEachVar( p, pVar, i )
Llb_NonlinRemoveVar( p, pVar );
Llb_MgrForEachPart( p, pPart, i )
Llb_NonlinRemovePart( p, pPart );
ABC_FREE( p->pVars );
ABC_FREE( p->pParts );
ABC_FREE( p->pSupp );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Performs image computation.]
Description [Computes image of BDDs (vFuncs).]
SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
Llb_Mgr_t * p;
DdNode * bFunc, * bTemp;
int i, nReorders, timeInside;
abctime clk = Abc_Clock(), clk2;
// start the manager
clk2 = Abc_Clock();
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
if ( !Llb_NonlinStart( p ) )
{
Llb_NonlinFree( p );
return NULL;
}
// add partition
Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
timeBuild += Abc_Clock() - clk2;
timeInside = Abc_Clock() - clk2;
// compute scores
Llb_NonlinRecomputeScores( p );
// save permutation
if ( pOrder )
memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
{
clk2 = Abc_Clock();
nReorders = Cudd_ReadReorderings(dd);
if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeAndEx += Abc_Clock() - clk2;
timeInside += Abc_Clock() - clk2;
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
}
nSuppMax = p->nSuppMax;
Llb_NonlinFree( p );
// reorder variables
if ( fReorder )
Llb_NonlinReorder( dd, 0, fVerbose );
timeOther += Abc_Clock() - clk - timeInside;
// return
Cudd_Deref( bFunc );
return bFunc;
}
static Llb_Mgr_t * p = NULL;
/**Function*************************************************************
Synopsis [Starts image computation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, abctime TimeTarget )
{
DdManager * dd;
abctime clk = Abc_Clock();
assert( p == NULL );
// start a new manager (disable reordering)
dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
dd->TimeStop = TimeTarget;
Cudd_ShuffleHeap( dd, pOrder );
// if ( fFirst )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
// start the manager
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
if ( !Llb_NonlinStart( p ) )
{
Llb_NonlinFree( p );
p = NULL;
return NULL;
}
timeBuild += Abc_Clock() - clk;
// if ( !fFirst )
// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
return dd;
}
/**Function*************************************************************
Synopsis [Performs image computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
DdNode * bFunc, * bTemp;
int i, nReorders, timeInside = 0;
abctime clk = Abc_Clock(), clk2;
// add partition
Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
// reorder
if ( fReorder )
Llb_NonlinReorder( p->dd, 0, 0 );
// save permutation
memcpy( pOrder, p->dd->invperm, sizeof(int) * p->dd->size );
// compute scores
Llb_NonlinRecomputeScores( p );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
{
clk2 = Abc_Clock();
nReorders = Cudd_ReadReorderings(p->dd);
if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeAndEx += Abc_Clock() - clk2;
timeInside += Abc_Clock() - clk2;
if ( nReorders < Cudd_ReadReorderings(p->dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );
if ( bFunc == NULL )
{
Cudd_RecursiveDeref( p->dd, bTemp );
Llb_NonlinFree( p );
return NULL;
}
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
}
nSuppMax = p->nSuppMax;
// reorder variables
// if ( fReorder )
// Llb_NonlinReorder( p->dd, 0, fVerbose );
// save permutation
// memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) );
timeOther += Abc_Clock() - clk - timeInside;
// return
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Quits image computation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinImageQuit()
{
DdManager * dd;
if ( p == NULL )
return;
dd = p->dd;
Llb_NonlinFree( p );
if ( dd->bFunc )
Cudd_RecursiveDeref( dd, dd->bFunc );
Extra_StopManager( dd );
// Cudd_Quit ( dd );
p = NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END