#include "llbInt.h"

Include dependency graph for llb3Image.c:

Classes
struct	Llb_Var_t_

struct	Llb_Prt_t_

struct	Llb_Mgr_t_

Macros
#define	Llb_MgrForEachVar(p, pVar, i)

#define	Llb_MgrForEachPart(p, pPart, i)

#define	Llb_PartForEachVar(p, pPart, pVar, i)

#define	Llb_VarForEachPart(p, pVar, pPart, i)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Var_t_	Llb_Var_t
	DECLARATIONS ///.

typedef struct Llb_Prt_t_	Llb_Prt_t

typedef struct Llb_Mgr_t_	Llb_Mgr_t

Functions
void	Llb_NonlinRemoveVar (Llb_Mgr_t p, Llb_Var_t pVar)
	FUNCTION DEFINITIONS ///.

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

Macro Definition Documentation

◆ Llb_MgrForEachPart

#define Llb_MgrForEachPart	(	p,
		pPart,
		i )

Value:

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

p

Cube * p

Definition exorList.c:222

Definition at line 71 of file llb3Image.c.

71#define Llb_MgrForEachPart( p, pPart, i ) \

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

◆ Llb_MgrForEachVar

#define Llb_MgrForEachVar	(	p,
		pVar,
		i )

Value:

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.

68#define Llb_MgrForEachVar( p, pVar, i ) \

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

◆ Llb_PartForEachVar

#define Llb_PartForEachVar	(	p,
		pPart,
		pVar,
		i )

Value:

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.

75#define Llb_PartForEachVar( p, pPart, pVar, i ) \

76 for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )

◆ Llb_VarForEachPart

#define Llb_VarForEachPart	(	p,
		pVar,
		pPart,
		i )

Value:

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.

78#define Llb_VarForEachPart( p, pVar, pPart, i ) \

79 for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )

Typedef Documentation

◆ Llb_Mgr_t

typedef struct Llb_Mgr_t_ Llb_Mgr_t

Definition at line 46 of file llb3Image.c.

◆ Llb_Prt_t

typedef struct Llb_Prt_t_ Llb_Prt_t

Definition at line 37 of file llb3Image.c.

◆ Llb_Var_t

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

◆ Llb_NonlinAddPair()

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

Here is the caller graph for this function:

◆ Llb_NonlinAddPartition()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinAlloc()

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

Here is the caller graph for this function:

◆ Llb_NonlinBuildBdds()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinCheckVars()

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

Here is the caller graph for this function:

◆ Llb_NonlinCreateCube1()

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

Here is the caller graph for this function:

◆ Llb_NonlinCreateCube2()

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

Here is the caller graph for this function:

◆ Llb_NonlinCutNodes()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinCutNodes_rec()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinFree()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinHasSingletonVars()

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

Here is the caller graph for this function:

◆ Llb_NonlinImage()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinImageCompute()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinImageQuit()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinImageStart()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinNextPartitions()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinPrint()

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

Here is the caller graph for this function:

◆ Llb_NonlinQuantify1()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinQuantify2()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinRecomputeScores()

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

Here is the caller graph for this function:

◆ Llb_NonlinRemovePart()

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

Here is the caller graph for this function:

◆ Llb_NonlinRemoveVar()

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

Here is the caller graph for this function:

◆ Llb_NonlinReorder()

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

Here is the caller graph for this function:

◆ Llb_NonlinStart()

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_NonlinVerifyScores()

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

◆ nSuppMax

int nSuppMax

Definition at line 83 of file llb3Image.c.

◆ timeAndEx

abctime timeAndEx

Definition at line 82 of file llb3Image.c.

◆ timeBuild

abctime timeBuild

Definition at line 82 of file llb3Image.c.

◆ timeOther

abctime timeOther

Definition at line 82 of file llb3Image.c.

Classes

Macros

Typedefs

Functions

Variables

Macro Definition Documentation

◆ Llb_MgrForEachPart

◆ Llb_MgrForEachVar

◆ Llb_PartForEachVar

◆ Llb_VarForEachPart

Typedef Documentation

◆ Llb_Mgr_t

◆ Llb_Prt_t

◆ Llb_Var_t

Function Documentation

◆ Llb_NonlinAddPair()

◆ Llb_NonlinAddPartition()

◆ Llb_NonlinAlloc()

◆ Llb_NonlinBuildBdds()

◆ Llb_NonlinCheckVars()

◆ Llb_NonlinCreateCube1()

◆ Llb_NonlinCreateCube2()

◆ Llb_NonlinCutNodes()

◆ Llb_NonlinCutNodes_rec()

◆ Llb_NonlinFree()

◆ Llb_NonlinHasSingletonVars()

◆ Llb_NonlinImage()

◆ Llb_NonlinImageCompute()

◆ Llb_NonlinImageQuit()

◆ Llb_NonlinImageStart()

◆ Llb_NonlinNextPartitions()

◆ Llb_NonlinPrint()

◆ Llb_NonlinQuantify1()

◆ Llb_NonlinQuantify2()

◆ Llb_NonlinRecomputeScores()

◆ Llb_NonlinRemovePart()

◆ Llb_NonlinRemoveVar()

◆ Llb_NonlinReorder()

◆ Llb_NonlinStart()

◆ Llb_NonlinVerifyScores()

Variable Documentation

◆ nSuppMax

◆ timeAndEx

◆ timeBuild

◆ timeOther