Skip to content

A
abc
Commit 3e92b873 by Alan Mishchenko
Options

Added timeout to &reachn.

parent 82e9de90
Showing with 114 additions and 1505 deletions
src/aig/llb/llb2Bad.c
......@@ -42,12 +42,12 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd )
DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
{
Vec_Ptr_t * vNodes;
DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
Aig_Obj_t * pObj;
int i;
int i, k;
assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
// initialize elementary variables
Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
......@@ -64,6 +64,14 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd )
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
{
Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i+1 )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return NULL;
}
}
// quantify PIs of each PO
bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult );
......
src/aig/llb/llb2Core.c
......@@ -217,10 +217,17 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
// compute initial states
if ( p->pPars->fBackward )
{
// create init state in the global manager
bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );
if ( bTemp == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
return -1;
}
Cudd_Ref( bTemp );
// create bad state in the ring manager
p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL ); Cudd_Ref( p->ddR->bFunc );
// create init state in the global manager
bTemp = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( bTemp );
bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->ddR, bTemp );
bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached );
......@@ -231,7 +238,16 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
else
{
// create bad state in the ring manager
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( p->ddR->bFunc );
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );
if ( p->ddR->bFunc == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
return -1;
}
if ( p->ddR->bFunc == NULL )
return -1;
Cudd_Ref( p->ddR->bFunc );
// create init state in the working and global manager
bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent );
bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL ); Cudd_Ref( bReached );
......
src/aig/llb/llb3Image.c
......@@ -524,7 +524,7 @@ Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * v
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd, int TimeOut )
{
Vec_Ptr_t * vNodes, * vResult;
Aig_Obj_t * pObj;
......@@ -541,6 +541,15 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t *
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
if ( i % 10 == 0 && TimeOut && clock() >= TimeOut )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( pObj->pData )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return NULL;
}
}
vResult = Vec_PtrAlloc( 100 );
......@@ -600,14 +609,16 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
SeeAlso []
***********************************************************************/
void Llb_NonlinStart( Llb_Mgr_t * p )
int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
{
Vec_Ptr_t * vRootBdds;
Llb_Prt_t * pPart;
DdNode * bFunc;
int i, k, nSuppSize;
// create and collect BDDs
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced
if ( vRootBdds == NULL )
return 0;
Vec_PtrPush( vRootBdds, p->bCurrent );
// add pairs (refs are consumed inside)
Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
......@@ -634,6 +645,7 @@ void Llb_NonlinStart( Llb_Mgr_t * p )
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
return 1;
}
/**Function*************************************************************
......@@ -844,7 +856,7 @@ void Llb_NonlinFree( Llb_Mgr_t * p )
***********************************************************************/
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, int Limit )
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeOut )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
Llb_Mgr_t * p;
......@@ -854,7 +866,11 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
// start the manager
clk2 = clock();
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
Llb_NonlinStart( p );
if ( !Llb_NonlinStart( p, TimeOut ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeBuild += clock() - clk2;
timeInside = clock() - clk2;
// compute scores
......
src/aig/llb/llb3Nonlin.c
......@@ -294,7 +294,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
//Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
// compute the next states
bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState,
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY ); // consumed reference
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, ABC_INFINITY ); // consumed reference
assert( bImage != NULL );
Cudd_Ref( bImage );
//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
......@@ -340,6 +340,44 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
return pCex;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
{
Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
Aig_Obj_t * pObj;
int i;
printf( "Order: " );
for ( i = 0; i < Cudd_ReadSize(dd); i++ )
{
pObj = Aig_ManObj( pAig, i );
if ( pObj == NULL )
continue;
if ( Saig_ObjIsPi(pAig, pObj) )
printf( "pi" );
else if ( Saig_ObjIsLo(pAig, pObj) )
printf( "lo" );
else if ( Saig_ObjIsPo(pAig, pObj) )
printf( "po" );
else if ( Saig_ObjIsLi(pAig, pObj) )
printf( "li" );
else continue;
printf( "%d=%d ", i, dd->perm[i] );
}
printf( "\n" );
return 1;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
......@@ -364,8 +402,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
else
p->pPars->TimeTarget = 0;
// set reordering hooks
assert( p->dd->bFunc == NULL );
// p->dd->bFunc = (DdNode *)p->pAig;
// Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );
// create bad state in the ring manager
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR ); Cudd_Ref( p->ddR->bFunc );
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
if ( p->ddR->bFunc == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
return -1;
}
Cudd_Ref( p->ddR->bFunc );
// compute the starting set of states
bCurrent = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( bCurrent );
p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached
......@@ -429,8 +479,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
nBddSize0 = Cudd_DagSize( bCurrent );
bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
// p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, nIters ? p->pPars->nBddMax : ABC_INFINITY );
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY );
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, p->pPars->TimeTarget );
// Abc_PrintTime( 1, "Image time", clock() - clk3 );
if ( bNext == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
return -1;
}
if ( bNext == NULL ) // Llb_NonlimImage() consumes reference of bCurrent!!!
{
DdNode * bVar, * bVarG;
......@@ -632,6 +690,7 @@ void Llb_MnnStop( Llb_Mnn_t * p )
ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
}
p->dd->bFunc = NULL;
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
......
src/aig/llb/llb3Nonlin_multi.c deleted 100644 → 0
/**CFile****************************************************************
FileName [llb2Nonlin.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: llb2Nonlin.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
Vec_Ptr_t * vFuncs; // current state functions in terms of vLeaves
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++ )
static int timeBuild, timeAndEx, timeOther;
static int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Vec_Int_t * vVars )
{
DdNode * bCof, * bVar;
int i, iVar, iVarBest = -1;
int Size, Size0, Size1;
if ( vVars == NULL )
vVars = Vec_IntStartNatural( Cudd_ReadSize(dd) );
printf( "\nOriginal = %6d. SuppSize = %3d. Vars = %3d.\n",
Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Vec_IntSize(vVars) );
Vec_IntForEachEntry( vVars, iVar, i )
{
printf( "Var =%3d : ", iVar );
bVar = Cudd_bddIthVar(dd, iVar);
bCof = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
printf( "Size0 =%6d ", Size0 = Cudd_DagSize(bCof) );
Cudd_RecursiveDeref( dd, bCof );
bCof = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof );
printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
printf( "Size1 =%6d ", Size1 = Cudd_DagSize(bCof) );
Cudd_RecursiveDeref( dd, bCof );
printf( "D =%6d ", Size0 + Size1 - Size );
printf( "B =%6d\n", ABC_MAX(Size0, Size1) - ABC_MIN(Size0, Size1) );
}
return iVarBest;
}
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
{
DdNode * bNew;
printf( "Original = %6d. SuppSize = %3d. ",
Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 ); Cudd_Ref( bNew );
printf( "Result = %6d. SuppSize = %3d.\n",
Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
Cudd_RecursiveDeref( dd, bNew );
}
/**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;
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 );
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;
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 );
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 Limit )
{
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;
/*
if ( iPart1 == 91 && iPart2 == 134 )
{
fVerbose = 1;
}
*/
// 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, Limit );
return 1;
}
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_MAX( 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 0;
}
/**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;
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 = Cudd_bddAnd( dd, bBdd0, bBdd1 ); 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_NonlinStart( Llb_Mgr_t * p )
{
Vec_Ptr_t * vRootBdds;
Llb_Prt_t * pPart;
DdNode * bFunc;
int i, k, nSuppSize;
// create and collect BDDs
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
Vec_PtrForEachEntry( DdNode *, p->vFuncs, bFunc, i )
Vec_PtrPush( vRootBdds, bFunc );
// add pairs (refs are consumed inside)
Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
{
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_MAX( p->nSuppMax, nSuppSize );
}
Vec_PtrFree( vRootBdds );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
}
/**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, Vec_Ptr_t * vFuncs )
{
Llb_Mgr_t * p;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
p->pAig = pAig;
p->vLeaves = vLeaves;
p->vRoots = vRoots;
p->dd = dd;
p->vFuncs = vFuncs;
p->pVars2Q = pVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vRoots) + Vec_PtrSize(vFuncs);
p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
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 [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 fVerbose )
{
int clk = 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) );
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", 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 [Performs image computation.]
Description [Computes image of BDDs (vFuncs).]
SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
SeeAlso []
***********************************************************************/
int Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, Vec_Ptr_t * vFuncs, int fReorder, int fVerbose, int * pOrder, int * pfSubset, int Limit )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
Llb_Mgr_t * p;
int i, nReorders, timeInside, fSubset = 0;
int clk = clock(), clk2;
// start the manager
clk2 = clock();
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, vFuncs );
Llb_NonlinStart( p );
timeBuild += clock() - clk2;
timeInside = clock() - clk2;
// reorder variables
// if ( fReorder )
// Llb_NonlinReorder( dd, fVerbose );
// compute scores
Llb_NonlinRecomputeScores( p );
// save permutation
memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
{
nReorders = Cudd_ReadReorderings(dd);
clk2 = clock();
fSubset |= Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
timeAndEx += clock() - clk2;
timeInside += clock() - clk2;
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
Vec_PtrClear( vFuncs );
Llb_MgrForEachPart( p, pPart, i )
{
Vec_PtrPush( vFuncs, pPart->bFunc );
Cudd_Ref( pPart->bFunc );
}
nSuppMax = p->nSuppMax;
Llb_NonlinFree( p );
// reorder variables
if ( fReorder )
Llb_NonlinReorder( dd, fVerbose );
timeOther += clock() - clk - timeInside;
if ( pfSubset )
*pfSubset |= fSubset;
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrepareVarMap( Aig_Man_t * pAig, Vec_Int_t ** pvNs2Glo, Vec_Int_t ** pvGlo2Cs )
{
Aig_Obj_t * pObjLi, * pObjLo;
int i, iVarLi, iVarLo;
*pvNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
*pvGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(pAig) );
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
{
iVarLi = Aig_ObjId(pObjLi);
iVarLo = Aig_ObjId(pObjLo);
assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(pAig) );
assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(pAig) );
Vec_IntWriteEntry( *pvNs2Glo, iVarLi, i );
Vec_IntWriteEntry( *pvGlo2Cs, i, iVarLo );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
{
Aig_Obj_t * pObj;
DdNode * bRes, * bVar, * bTemp;
int i, iVar;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
bVar = Cudd_bddIthVar( dd, iVar );
bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
return bRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinComputeInitStateVec( Aig_Man_t * pAig, DdManager * dd )
{
Vec_Ptr_t * vFuncs;
Aig_Obj_t * pObj;
DdNode * bVar;
int i;
vFuncs = Vec_PtrAlloc( Aig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
bVar = Cudd_bddIthVar( dd, Aig_ObjId(pObj) ); Cudd_Ref( bVar );
Vec_PtrPush( vFuncs, Cudd_Not(bVar) );
}
return vFuncs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinDerefVec( DdManager * dd, Vec_Ptr_t * vFuncs )
{
DdNode * bFunc;
int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrFree( vFuncs );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinTransferVec( DdManager * dd, DdManager * ddG, Vec_Ptr_t * vFuncs, Vec_Int_t * vNs2Glo )
{
DdNode * bFunc, * bTemp;
int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
{
bFunc = Extra_TransferPermute( dd, ddG, bTemp = bFunc, Vec_IntArray(vNs2Glo) ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrWriteEntry( vFuncs, i, bFunc );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinSharpVec( DdManager * ddG, DdNode * bReached, Vec_Ptr_t * vFuncs )
{
DdNode * bFunc, * bTemp;
int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
{
bFunc = Cudd_bddAnd( ddG, bTemp = bFunc, Cudd_Not(bReached) ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( ddG, bTemp );
Vec_PtrWriteEntry( vFuncs, i, bFunc );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinAddToReachVec( DdManager * ddG, DdNode * bReached, Vec_Ptr_t * vFuncs )
{
DdNode * bFunc, * bProd, * bTemp;
int i;
bProd = Cudd_ReadOne( ddG ); Cudd_Ref( bProd );
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
{
bProd = Cudd_bddAnd( ddG, bTemp = bProd, bFunc ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( ddG, bTemp );
}
if ( Cudd_IsConstant(bProd) )
{
Cudd_RecursiveDeref( ddG, bProd );
return NULL;
}
bTemp = Cudd_bddOr( ddG, bReached, bProd ); Cudd_Ref( bTemp );
Cudd_RecursiveDeref( ddG, bProd );
Cudd_Deref( bTemp );
return bTemp;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_NonlinCreateReachVec( DdManager * dd, DdManager * ddG, DdNode * bReachG, Vec_Int_t * vGlo2Cs )
{
Vec_Ptr_t * vFuncs;
DdNode * bFunc;
vFuncs = Vec_PtrAlloc( 1 );
bFunc = Extra_TransferPermute( ddG, dd, bReachG, Vec_IntArray(vGlo2Cs) ); Cudd_Ref( bFunc );
Vec_PtrPush( vFuncs, bFunc );
// Llb_NonlinReorder( dd, 1 );
return vFuncs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrintVec( DdManager * dd, Vec_Ptr_t * vFuncs )
{
DdNode * bFunc;
int i;
Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
{
printf( "%2d : ", i );
printf( "Support =%5d ", Cudd_SupportSize(dd, bFunc) );
printf( "DagSize =%7d\n", Cudd_DagSize(bFunc) );
}
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinReachability( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Aig_Obj_t * pObj;
Vec_Ptr_t * vLeaves, * vRoots, * vParts;
Vec_Int_t * vNs2Glo, * vGlo2Cs;
DdManager * dd, * ddG;
DdNode * bReached, * bTemp;
int i, nIters, nBddSize0, nBddSize, Limit, fSubset, * pVars2Q, * pOrder;
int clk2, clk3, clk = clock();
// int RetValue;
int timeImage = 0;
int timeTran1 = 0;
int timeTran2 = 0;
int timeGloba = 0;
int timeOther = 0;
int timeTotal = 0;
int timeReo = 0;
int timeReoG = 0;
assert( Aig_ManRegNum(pAig) > 0 );
timeBuild = timeAndEx = timeOther = 0;
// compute time to stop
if ( pPars->TimeLimit )
pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
else
pPars->TimeTarget = 0;
// create leaves
vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
Vec_PtrPush( vLeaves, pObj );
// create roots
vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
Vec_PtrPush( vRoots, pObj );
// variables to quantify
pOrder = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
pVars2Q[Aig_ObjId(pObj)] = 1;
// start the managers
Llb_NonlinPrepareVarMap( pAig, &vNs2Glo, &vGlo2Cs );
dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( ddG, CUDD_REORDER_SYMM_SIFT );
// compute the starting set of states
vParts = Llb_NonlinComputeInitStateVec( pAig, dd );
bReached = Llb_NonlinComputeInitState( pAig, ddG ); Cudd_Ref( bReached );
fSubset = 1;
for ( Limit = pPars->nBddMax; fSubset; Limit *= 2 )
{
if ( pPars->fVerbose )
printf( "*********** LIMIT %d ************\n", Limit );
fSubset = 0;
for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
{
clk2 = clock();
// check the runtime limit
if ( pPars->TimeLimit && clock() >= pPars->TimeTarget )
{
if ( !pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", pPars->TimeLimit );
pPars->iFrame = nIters - 1;
Llb_NonlinDerefVec( dd, vParts ); vParts = NULL;
Cudd_RecursiveDeref( ddG, bReached ); bReached = NULL;
return -1;
}
// Llb_NonlinReorder( dd, 1 );
// compute the next states
clk3 = clock();
nBddSize0 = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vParts), Vec_PtrSize(vParts) );
if ( !Llb_NonlinImage( pAig, vLeaves, vRoots, pVars2Q, dd, vParts, pPars->fReorder, pPars->fVeryVerbose, pOrder, &fSubset, Limit ) )
{
if ( !pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", pPars->TimeLimit );
pPars->iFrame = nIters - 1;
Llb_NonlinDerefVec( dd, vParts ); vParts = NULL;
Cudd_RecursiveDeref( ddG, bReached ); bReached = NULL;
return -1;
}
timeImage += clock() - clk3;
nBddSize = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vParts), Vec_PtrSize(vParts) );
// Llb_NonlinPrintVec( dd, vParts );
// check containment in reached and derive new frontier
clk3 = clock();
Llb_NonlinTransferVec( dd, ddG, vParts, vNs2Glo );
timeTran1 += clock() - clk3;
clk3 = clock();
Llb_NonlinSharpVec( ddG, bReached, vParts );
bReached = Llb_NonlinAddToReachVec( ddG, bTemp = bReached, vParts );
if ( bReached == NULL )
{
bReached = bTemp;
Llb_NonlinDerefVec( ddG, vParts ); vParts = NULL;
if ( fSubset )
vParts = Llb_NonlinCreateReachVec( dd, ddG, bReached, vGlo2Cs );
break;
}
Cudd_Ref( bReached );
Cudd_RecursiveDeref( ddG, bTemp );
timeGloba += clock() - clk3;
// reset permutation
// RetValue = Cudd_CheckZeroRef( dd );
// assert( RetValue == 0 );
// Cudd_ShuffleHeap( dd, pOrder );
clk3 = clock();
Llb_NonlinTransferVec( ddG, dd, vParts, vGlo2Cs );
// Llb_NonlinDerefVec( ddG, vParts ); vParts = NULL;
// vParts = Llb_NonlinCreateReachVec( dd, ddG, bReached, vGlo2Cs );
timeTran2 += clock() - clk3;
// report the results
if ( pPars->fVerbose )
{
printf( "I =%3d : ", nIters );
printf( "Fr =%6d ", nBddSize0 );
printf( "Im =%6d ", nBddSize );
printf( "(%4d %3d) ", Cudd_ReadReorderings(dd), Cudd_ReadGarbageCollections(dd) );
printf( "Rea =%6d ", Cudd_DagSize(bReached) );
printf( "(%4d %3d) ", Cudd_ReadReorderings(ddG), Cudd_ReadGarbageCollections(ddG) );
printf( "S =%4d ", nSuppMax );
printf( "P =%2d ", Vec_PtrSize(vParts) );
Abc_PrintTime( 1, "T", clock() - clk2 );
}
/*
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
// Extra_bddPrint( ddG, bReached );printf( "\n" );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
fflush( stdout );
}
*/
if ( nIters == pPars->nIterMax - 1 )
{
if ( !pPars->fSilent )
printf( "Reached limit on the number of timeframes (%d).\n", pPars->nIterMax );
pPars->iFrame = nIters;
Llb_NonlinDerefVec( dd, vParts ); vParts = NULL;
Cudd_RecursiveDeref( ddG, bReached ); bReached = NULL;
return -1;
}
// Llb_NonlinReorder( ddG, 1 );
// Llb_NonlinFindBestVar( ddG, bReached, NULL );
}
}
if ( bReached == NULL )
return 0; // reachable
// report the stats
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
if ( nIters >= pPars->nIterMax || nBddSize > pPars->nBddMax )
printf( "Reachability analysis is stopped after %d frames.\n", nIters );
else
printf( "Reachability analysis completed after %d frames.\n", nIters );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
fflush( stdout );
}
if ( nIters >= pPars->nIterMax || nBddSize > pPars->nBddMax )
{
if ( !pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
Cudd_RecursiveDeref( ddG, bReached );
return -1; // undecided
}
// cleanup
Cudd_RecursiveDeref( ddG, bReached );
timeReo = Cudd_ReadReorderingTime(dd);
timeReoG = Cudd_ReadReorderingTime(ddG);
Extra_StopManager( dd );
Extra_StopManager( ddG );
// cleanup
Vec_IntFree( vNs2Glo );
Vec_IntFree( vGlo2Cs );
Vec_PtrFree( vLeaves );
Vec_PtrFree( vRoots );
ABC_FREE( pVars2Q );
ABC_FREE( pOrder );
// report
if ( !pPars->fSilent )
printf( "The miter is proved unreachable after %d iterations. ", nIters );
pPars->iFrame = nIters - 1;
Abc_PrintTime( 1, "Time", clock() - clk );
if ( pPars->fVerbose )
{
timeTotal = clock() - clk;
timeOther = timeTotal - timeImage - timeTran1 - timeTran2 - timeGloba;
ABC_PRTP( "Image ", timeImage, timeTotal );
ABC_PRTP( " build ", timeBuild, timeTotal );
ABC_PRTP( " and-ex ", timeAndEx, timeTotal );
ABC_PRTP( " other ", timeOther, timeTotal );
ABC_PRTP( "Transfer1", timeTran1, timeTotal );
ABC_PRTP( "Transfer2", timeTran2, timeTotal );
ABC_PRTP( "Global ", timeGloba, timeTotal );
ABC_PRTP( "Other ", timeOther, timeTotal );
ABC_PRTP( "TOTAL ", timeTotal, timeTotal );
ABC_PRTP( " reo ", timeReo, timeTotal );
ABC_PRTP( " reoG ", timeReoG, timeTotal );
}
return 1; // unreachable
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
{
Gia_ParLlb_t Pars, * pPars = &Pars;
Aig_Man_t * p;
Llb_ManSetDefaultParams( pPars );
pPars->fVerbose = 1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
Aig_ManPrintStats( pAig );
Aig_ManPrintStats( p );
Llb_NonlinReachability( p, pPars );
Aig_ManStop( p );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Aig_Man_t * p;
int RetValue = -1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
if ( pPars->fVerbose )
Aig_ManPrintStats( pAig );
if ( pPars->fVerbose )
Aig_ManPrintStats( p );
if ( !pPars->fSkipReach )
RetValue = Llb_NonlinReachability( p, pPars );
Aig_ManStop( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/aig/llb/llbInt.h
......@@ -146,7 +146,7 @@ extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, D
extern void Llb_MtrSchedule( Llb_Mtr_t * p );
/*=== llb2Bad.c ======================================================*/
extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd );
extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut );
extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
/*=== llb2Core.c ======================================================*/
extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
......@@ -168,7 +168,7 @@ extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
/*=== llb3Image.c ======================================================*/
extern 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, int Limit );
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeLimit );
ABC_NAMESPACE_HEADER_END
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment