llb3Image.c File Reference

#include "llbInt.h"

Go to the source code of this file.

Data Structures
struct	Llb_Var_t_
struct	Llb_Prt_t_
struct	Llb_Mgr_t_

Macros
#define	Llb_MgrForEachVar(p, pVar, i)   for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
#define	Llb_MgrForEachPart(p, pPart, i)   for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
#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++ )
#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++ )

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Var_t_	Llb_Var_t
	DECLARATIONS ///. More...
typedef struct Llb_Prt_t_	Llb_Prt_t
typedef struct Llb_Mgr_t_	Llb_Mgr_t

Functions
static Llb_Var_t *	Llb_MgrVar (Llb_Mgr_t *p, int i)
static Llb_Prt_t *	Llb_MgrPart (Llb_Mgr_t *p, int i)
void	Llb_NonlinRemoveVar (Llb_Mgr_t *p, Llb_Var_t *pVar)
	FUNCTION DEFINITIONS ///. More...
void	Llb_NonlinRemovePart (Llb_Mgr_t *p, Llb_Prt_t *pPart)
DdNode *	Llb_NonlinCreateCube1 (Llb_Mgr_t *p, Llb_Prt_t *pPart)
DdNode *	Llb_NonlinCreateCube2 (Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
int	Llb_NonlinHasSingletonVars (Llb_Mgr_t *p, Llb_Prt_t *pPart)
void	Llb_NonlinPrint (Llb_Mgr_t *p)
int	Llb_NonlinQuantify1 (Llb_Mgr_t *p, Llb_Prt_t *pPart, int fSubset)
int	Llb_NonlinQuantify2 (Llb_Mgr_t *p, Llb_Prt_t *pPart1, Llb_Prt_t *pPart2)
void	Llb_NonlinCutNodes_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Llb_NonlinCutNodes (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
Vec_Ptr_t *	Llb_NonlinBuildBdds (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, DdManager *dd)
void	Llb_NonlinAddPair (Llb_Mgr_t *p, DdNode *bFunc, int iPart, int iVar)
void	Llb_NonlinAddPartition (Llb_Mgr_t *p, int i, DdNode *bFunc)
int	Llb_NonlinStart (Llb_Mgr_t *p)
void	Llb_NonlinCheckVars (Llb_Mgr_t *p)
int	Llb_NonlinNextPartitions (Llb_Mgr_t *p, Llb_Prt_t **ppPart1, Llb_Prt_t **ppPart2)
void	Llb_NonlinReorder (DdManager *dd, int fTwice, int fVerbose)
void	Llb_NonlinRecomputeScores (Llb_Mgr_t *p)
void	Llb_NonlinVerifyScores (Llb_Mgr_t *p)
Llb_Mgr_t *	Llb_NonlinAlloc (Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd)
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)
DdManager *	Llb_NonlinImageStart (Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, int *pOrder, int fFirst, abctime TimeTarget)
DdNode *	Llb_NonlinImageCompute (DdNode *bCurrent, int fReorder, int fDrop, int fVerbose, int *pOrder)
void	Llb_NonlinImageQuit ()

Variables
abctime	timeBuild
abctime	timeAndEx
abctime	timeOther
int	nSuppMax
static Llb_Mgr_t *	p = NULL

Macro Definition Documentation

#define Llb_MgrForEachPart	(		p,
			pPart,
			i
	)		for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else

Definition at line 71 of file llb3Image.c.

#define Llb_MgrForEachVar	(		p,
			pVar,
			i
	)		for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else

Definition at line 68 of file llb3Image.c.

#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++ )

Definition at line 75 of file llb3Image.c.

#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++ )

Definition at line 78 of file llb3Image.c.

Typedef Documentation

typedef struct Llb_Mgr_t_ Llb_Mgr_t

Definition at line 46 of file llb3Image.c.

typedef struct Llb_Prt_t_ Llb_Prt_t

Definition at line 37 of file llb3Image.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Var_t_ Llb_Var_t

DECLARATIONS ///.

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

]

Definition at line 29 of file llb3Image.c.

Function Documentation

static Llb_Prt_t* Llb_MgrPart ( Llb_Mgr_t *  p, int  i  )

inlinestatic

Definition at line 65 of file llb3Image.c.

{ return p->pParts[i]; }

static Llb_Var_t* Llb_MgrVar ( Llb_Mgr_t *  p, int  i  )

inlinestatic

Definition at line 64 of file llb3Image.c.

{ return p->pVars[i];  }

void Llb_NonlinAddPair	(	Llb_Mgr_t *	p,
		DdNode *	bFunc,
		int	iPart,
		int	iVar
	)

Function*************************************************************

Synopsis [Starts non-linear quantification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 604 of file llb3Image.c.

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

void Llb_NonlinAddPartition	(	Llb_Mgr_t *	p,
		int	i,
		DdNode *	bFunc
	)

Function*************************************************************

Synopsis [Starts non-linear quantification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 628 of file llb3Image.c.

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

Llb_Mgr_t* Llb_NonlinAlloc	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vRoots,
		int *	pVars2Q,
		DdManager *	dd
	)

Function*************************************************************

Synopsis [Starts non-linear quantification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 830 of file llb3Image.c.

{
    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;
}

Vec_Ptr_t* Llb_NonlinBuildBdds	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vLower,
		Vec_Ptr_t *	vUpper,
		DdManager *	dd
	)

Function*************************************************************

Synopsis [Returns array of BDDs for the roots in terms of the leaves.]

Description []

SideEffects []

SeeAlso []

Definition at line 542 of file llb3Image.c.

{
    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;
}

void Llb_NonlinCheckVars

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Checks that each var appears in at least one partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 686 of file llb3Image.c.

{
    Llb_Var_t * pVar;
    int i;
    Llb_MgrForEachVar( p, pVar, i )
        assert( Vec_IntSize(pVar->vParts) > 1 );
}

DdNode* Llb_NonlinCreateCube1	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart
	)

Function*************************************************************

Synopsis [Create cube with singleton variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 139 of file llb3Image.c.

{
    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;
}

DdNode* Llb_NonlinCreateCube2	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart1,
		Llb_Prt_t *	pPart2
	)

Function*************************************************************

Synopsis [Create cube of variables appearing only in two partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 172 of file llb3Image.c.

{
    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;
}

Vec_Ptr_t* Llb_NonlinCutNodes	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vLower,
		Vec_Ptr_t *	vUpper
	)

Function*************************************************************

Synopsis [Computes volume of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 515 of file llb3Image.c.

{
    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;
}

void Llb_NonlinCutNodes_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

Function*************************************************************

Synopsis [Computes volume of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 486 of file llb3Image.c.

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

void Llb_NonlinFree

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Stops non-linear quantification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 858 of file llb3Image.c.

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

int Llb_NonlinHasSingletonVars	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart
	)

Function*************************************************************

Synopsis [Returns 1 if partition has singleton variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file llb3Image.c.

{
    Llb_Var_t * pVar;
    int i;
    Llb_PartForEachVar( p, pPart, pVar, i )
        if ( Vec_IntSize(pVar->vParts) == 1 )
            return 1;
    return 0;
}

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
	)

Function*************************************************************

Synopsis [Performs image computation.]

Description [Computes image of BDDs (vFuncs).]

SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]

SeeAlso []

Definition at line 884 of file llb3Image.c.

{
    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;
}

DdNode* Llb_NonlinImageCompute	(	DdNode *	bCurrent,
		int	fReorder,
		int	fDrop,
		int	fVerbose,
		int *	pOrder
	)

Function*************************************************************

Synopsis [Performs image computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 999 of file llb3Image.c.

{
    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;
}

void Llb_NonlinImageQuit

(

)

Function*************************************************************

Synopsis [Quits image computation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1075 of file llb3Image.c.

{
    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;
}

DdManager* Llb_NonlinImageStart	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vRoots,
		int *	pVars2Q,
		int *	pOrder,
		int	fFirst,
		abctime	TimeTarget
	)

Function*************************************************************

Synopsis [Starts image computation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 963 of file llb3Image.c.

{
    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;
}

int Llb_NonlinNextPartitions	(	Llb_Mgr_t *	p,
		Llb_Prt_t **	ppPart1,
		Llb_Prt_t **	ppPart2
	)

Function*************************************************************

Synopsis [Find next partition to quantify]

Description []

SideEffects []

SeeAlso []

Definition at line 705 of file llb3Image.c.

{
    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; 
}

void Llb_NonlinPrint

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Returns 1 if partition has singleton variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file llb3Image.c.

{
    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" );
    }
}

int Llb_NonlinQuantify1	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart,
		int	fSubset
	)

Function*************************************************************

Synopsis [Quantifies singles belonging to one partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file llb3Image.c.

{
    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;
}

int Llb_NonlinQuantify2	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart1,
		Llb_Prt_t *	pPart2
	)

Function*************************************************************

Synopsis [Quantifies singles belonging to one partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file llb3Image.c.

{
    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;
}

void Llb_NonlinRecomputeScores

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Recomputes scores after variable reordering.]

Description []

SideEffects []

SeeAlso []

Definition at line 777 of file llb3Image.c.

{
    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;
    }
}

void Llb_NonlinRemovePart	(	Llb_Mgr_t *	p,
		Llb_Prt_t *	pPart
	)

Function*************************************************************

Synopsis [Removes one partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file llb3Image.c.

{
    assert( p->pParts[pPart->iPart] == pPart );
    p->pParts[pPart->iPart] = NULL;
    Vec_IntFree( pPart->vVars );
    Cudd_RecursiveDeref( p->dd, pPart->bFunc );
    ABC_FREE( pPart );
}

void Llb_NonlinRemoveVar	(	Llb_Mgr_t *	p,
		Llb_Var_t *	pVar
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Removes one variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file llb3Image.c.

{
    assert( p->pVars[pVar->iVar] == pVar );
    p->pVars[pVar->iVar] = NULL;
    Vec_IntFree( pVar->vParts );
    ABC_FREE( pVar );
}

void Llb_NonlinReorder	(	DdManager *	dd,
		int	fTwice,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Reorders BDDs in the working manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 748 of file llb3Image.c.

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

int Llb_NonlinStart

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Starts non-linear quantification scheduling.]

Description []

SideEffects []

SeeAlso []

Definition at line 660 of file llb3Image.c.

{
    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;
}

void Llb_NonlinVerifyScores

(

Llb_Mgr_t *

p

)

Function*************************************************************

Synopsis [Recomputes scores after variable reordering.]

Description []

SideEffects []

SeeAlso []

Definition at line 803 of file llb3Image.c.

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

Variable Documentation

int nSuppMax

Definition at line 83 of file llb3Image.c.

Llb_Mgr_t* p = NULL

static

Definition at line 950 of file llb3Image.c.

abctime timeAndEx

Definition at line 82 of file llb3Image.c.

abctime timeBuild

Definition at line 82 of file llb3Image.c.

abctime timeOther

Definition at line 82 of file llb3Image.c.