llbInt.h File Reference

#include <stdio.h>
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extraBdd.h"
#include "llb.h"

Go to the source code of this file.

Data Structures
struct	Llb_Man_t_
struct	Llb_Mtr_t_
struct	Llb_Grp_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_	Llb_Man_t
	INCLUDES ///. More...
typedef struct Llb_Mtr_t_	Llb_Mtr_t
typedef struct Llb_Grp_t_	Llb_Grp_t

Functions
static int	Llb_ObjBddVar (Vec_Int_t *vOrder, Aig_Obj_t *pObj)
	MACRO DEFINITIONS ///. More...
Vec_Int_t *	Llb_ManDeriveConstraints (Aig_Man_t *p)
	FUNCTION DECLARATIONS ///. More...
void	Llb_ManPrintEntries (Aig_Man_t *p, Vec_Int_t *vCands)
int	Llb_ManModelCheckAig (Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars, Vec_Int_t *vHints, DdManager **pddGlo)
void	Llb_ManCluster (Llb_Mtr_t *p)
void	Llb_ManDumpReached (DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Vec_Ptr_t *	Llb_ManFlow (Aig_Man_t *p, Vec_Ptr_t *vSources, int *pnFlow)
int	Llb_ManReachabilityWithHints (Llb_Man_t *p)
int	Llb_ManModelCheckAigWithHints (Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars)
void	Llb_ManPrepareVarMap (Llb_Man_t *p)
	DECLARATIONS ///. More...
Llb_Man_t *	Llb_ManStart (Aig_Man_t *pAigGlo, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
void	Llb_ManStop (Llb_Man_t *p)
void	Llb_MtrVerifyMatrix (Llb_Mtr_t *p)
Llb_Mtr_t *	Llb_MtrCreate (Llb_Man_t *p)
void	Llb_MtrFree (Llb_Mtr_t *p)
void	Llb_MtrPrint (Llb_Mtr_t *p, int fOrder)
void	Llb_MtrPrintMatrixStats (Llb_Mtr_t *p)
Llb_Grp_t *	Llb_ManGroupAlloc (Llb_Man_t *pMan)
	DECLARATIONS ///. More...
void	Llb_ManGroupStop (Llb_Grp_t *p)
void	Llb_ManPrepareGroups (Llb_Man_t *pMan)
Llb_Grp_t *	Llb_ManGroupsCombine (Llb_Grp_t *p1, Llb_Grp_t *p2)
Llb_Grp_t *	Llb_ManGroupCreateFromCuts (Llb_Man_t *pMan, Vec_Int_t *vCut1, Vec_Int_t *vCut2)
void	Llb_ManPrepareVarLimits (Llb_Man_t *p)
int	Llb_ManTracePaths (Aig_Man_t *p, Aig_Obj_t *pPivot)
Vec_Int_t *	Llb_ManMarkPivotNodes (Aig_Man_t *p, int fUseInternal)
int	Llb_ManReachability (Llb_Man_t *p, Vec_Int_t *vHints, DdManager **pddGlo)
void	Llb_MtrSchedule (Llb_Mtr_t *p)
DdNode *	Llb_BddComputeBad (Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
	DECLARATIONS ///. More...
DdNode *	Llb_BddQuantifyPis (Aig_Man_t *pInit, DdManager *dd, DdNode *bFunc)
DdNode *	Llb_CoreComputeCube (DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
	FUNCTION DEFINITIONS ///. More...
int	Llb_CoreExperiment (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
Vec_Int_t *	Llb_DriverCountRefs (Aig_Man_t *p)
	DECLARATIONS ///. More...
Vec_Int_t *	Llb_DriverCollectNs (Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Vec_Int_t *	Llb_DriverCollectCs (Aig_Man_t *pAig)
DdNode *	Llb_DriverPhaseCube (Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
DdManager *	Llb_DriverLastPartition (Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)
Vec_Ptr_t *	Llb_ImgSupports (Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Llb_ImgSchedule (Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
DdManager *	Llb_ImgPartition (Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
void	Llb_ImgQuantifyFirst (Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
void	Llb_ImgQuantifyReset (Vec_Ptr_t *vDdMans)
DdNode *	Llb_ImgComputeImage (Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
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 ()
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)
DdNode *	Llb_NonlinComputeInitState (Aig_Man_t *pAig, DdManager *dd)
Abc_Cex_t *	Llb4_Nonlin4TransformCex (Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
	DECLARATIONS ///. More...
DdNode *	Llb_Nonlin4Image (DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Vec_Ptr_t *	Llb_Nonlin4Group (DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
void	Llb4_Nonlin4Sweep (Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)

Typedef Documentation

typedef struct Llb_Grp_t_ Llb_Grp_t

Definition at line 48 of file llbInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t

INCLUDES ///.

CFile****************************************************************

FileName [llbInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD-based reachability.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 8, 2010.]

Revision [

Id:

llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 46 of file llbInt.h.

typedef struct Llb_Mtr_t_ Llb_Mtr_t

Definition at line 47 of file llbInt.h.

Function Documentation

void Llb4_Nonlin4Sweep	(	Aig_Man_t *	pAig,
		int	nSweepMax,
		int	nClusterMax,
		DdManager **	pdd,
		Vec_Int_t **	pvOrder,
		Vec_Ptr_t **	pvGroups,
		int	fVerbose
	)

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

Synopsis [Performs BDD sweep on the netlist.]

Description [Returns BDD manager, ordering, clusters, and bad states inside dd->bFunc.]

SideEffects []

SeeAlso []

Definition at line 520 of file llb4Sweep.c.

{
    DdManager * ddBad, * ddWork;
    Vec_Ptr_t * vGroups;
    Vec_Int_t * vOrder;
    int Counter, nCutPoints;

    // get the original ordering
    Aig_ManCleanMarkA( pAig );
    vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 1 );
    assert( Counter == Aig_ManNodeNum(pAig) );
    // mark the nodes
    nCutPoints = Llb4_Nonlin4SweepCutpoints( pAig, vOrder, nSweepMax, fVerbose );
    Vec_IntFree( vOrder );
    // get better ordering
    vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 0 );
    assert( Counter == nCutPoints );
    Aig_ManCleanMarkA( pAig );
    // compute the BAD states
    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) );
    // compute the clusters
    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose );
    // transfer the result from the Bad manager
//printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
    ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc );   Cudd_Ref( ddWork->bFunc );
    Cudd_RecursiveDeref( ddBad, ddBad->bFunc );  ddBad->bFunc = NULL;
    Extra_StopManager( ddBad );
    // update ordering to exclude quantified variables
//printf( "Bad after = %d.\n", Cudd_DagSize(ddWork->bFunc) );

    Llb_Nonlin4SweepPrintSuppProfile( ddWork, pAig, vOrder, vGroups, fVerbose );

    // return the result
    *pdd = ddWork;
    *pvOrder = vOrder;
    *pvGroups = vGroups;
}

Abc_Cex_t* Llb4_Nonlin4TransformCex	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vStates,
		int	iCexPo,
		int	fVerbose
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [llb2Cex.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:

llb2Cex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Translates a sequence of states into a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file llb4Cex.c.

{
    Abc_Cex_t * pCex;
    Cnf_Dat_t * pCnf;
    Vec_Int_t * vAssumps;
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    unsigned * pNext, * pThis;
    int i, k, iBit, status, nRegs;//, clk = Abc_Clock();
/*
    Vec_PtrForEachEntry( unsigned *, vStates, pNext, i )
    {
        printf( "%4d : ", i );
        Extra_PrintBinary( stdout, pNext, Aig_ManRegNum(pAig) );
        printf( "\n" );
    }
*/
    // derive SAT solver
    nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0;
    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
    pAig->nRegs = nRegs;
//    Cnf_DataTranformPolarity( pCnf, 0 );
    // convert into SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat == NULL )
    {
        printf( "Llb4_Nonlin4TransformCex(): Counter-example generation has failed.\n" );
        Cnf_DataFree( pCnf );
        return NULL;
    }
    // simplify the problem
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        printf( "Llb4_Nonlin4TransformCex(): SAT solver is invalid.\n" );
        sat_solver_delete( pSat );
        Cnf_DataFree( pCnf );
        return NULL;
    }
    // start the counter-example
    pCex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), Vec_PtrSize(vStates) );
    pCex->iFrame = Vec_PtrSize(vStates)-1;
    pCex->iPo = -1;

    // solve each time frame
    iBit = Saig_ManRegNum(pAig);
    pThis = (unsigned *)Vec_PtrEntry( vStates, 0 );
    vAssumps = Vec_IntAlloc( 2 * Aig_ManRegNum(pAig) );
    Vec_PtrForEachEntryStart( unsigned *, vStates, pNext, i, 1 )
    {
        // create assumptions
        Vec_IntClear( vAssumps );
        Saig_ManForEachLo( pAig, pObj, k )
            Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pThis,k) ) );
        Saig_ManForEachLi( pAig, pObj, k )
            Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pNext,k) ) );
        // solve SAT problem
        status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
            (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        // if the problem is SAT, get the counterexample
        if ( status != l_True )
        {
            printf( "Llb4_Nonlin4TransformCex(): There is no transition between state %d and %d.\n", i-1, i );
            Vec_IntFree( vAssumps );
            sat_solver_delete( pSat );
            Cnf_DataFree( pCnf );
            ABC_FREE( pCex );
            return NULL;
        }
        // get the assignment of PIs
        Saig_ManForEachPi( pAig, pObj, k )
            if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
                Abc_InfoSetBit( pCex->pData, iBit + k );
        // update the counter
        iBit += Saig_ManPiNum(pAig);
        pThis = pNext;
    }

    // add the last frame when the property fails
    Vec_IntClear( vAssumps );
    if ( iCexPo >= 0 )
    {
        Saig_ManForEachPo( pAig, pObj, k )
            if ( k == iCexPo )
                Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
    }
    else
    {
        Saig_ManForEachPo( pAig, pObj, k )
            Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) );
    }

    // add clause
    status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) );
    if ( status == 0 )
    {
        printf( "Llb4_Nonlin4TransformCex(): The SAT solver is unsat after adding last clause.\n" );
        Vec_IntFree( vAssumps );
        sat_solver_delete( pSat );
        Cnf_DataFree( pCnf );
        ABC_FREE( pCex );
        return NULL;
    }
    // create assumptions
    Vec_IntClear( vAssumps );
    Saig_ManForEachLo( pAig, pObj, k )
        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !Abc_InfoHasBit(pThis,k) ) );
    // solve the last frame
    status = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
        (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status != l_True )
    {
        printf( "Llb4_Nonlin4TransformCex(): There is no last transition that makes the property fail.\n" );
        Vec_IntFree( vAssumps );
        sat_solver_delete( pSat );
        Cnf_DataFree( pCnf );
        ABC_FREE( pCex );
        return NULL;
    }
    // get the assignment of PIs
    Saig_ManForEachPi( pAig, pObj, k )
        if ( sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) )
            Abc_InfoSetBit( pCex->pData, iBit + k );
    iBit += Saig_ManPiNum(pAig);
    assert( iBit == pCex->nBits );

    // free the sat_solver
    Vec_IntFree( vAssumps );
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );

    // verify counter-example
    status = Saig_ManFindFailedPoCex( pAig, pCex );
    if ( status >= 0 && status < Saig_ManPoNum(pAig) )
        pCex->iPo = status;
    else
    {
        printf( "Llb4_Nonlin4TransformCex(): Counter-example verification has FAILED.\n" );
        ABC_FREE( pCex );
        return NULL;
    }
    // report the results
//    if ( fVerbose )
//       Abc_PrintTime( 1, "SAT-based cex generation time", Abc_Clock() - clk );
    return pCex;
}

DdNode* Llb_BddComputeBad	(	Aig_Man_t *	pInit,
		DdManager *	dd,
		abctime	TimeOut
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [llb2Bad.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Computing bad states.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

llb2Bad.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Computes bad in working manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb2Bad.c.

{
    Vec_Ptr_t * vNodes;
    DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
    Aig_Obj_t * pObj;
    int i, k;
    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
    // initialize elementary variables
    Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
    Saig_ManForEachLo( pInit, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, i );
    Saig_ManForEachPi( pInit, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
    // compute internal nodes
    vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vCos), Saig_ManPoNum(pInit) );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) )
            continue;
        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 );
    }
    // quantify PIs of each PO
    bResult = Cudd_ReadLogicZero( dd );  Cudd_Ref( bResult );
    Saig_ManForEachPo( pInit, pObj, i )
    {
        bBdd0   = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
        bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 );     Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    // deref
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) )
            continue;
        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
    }
    Vec_PtrFree( vNodes );
    Cudd_Deref( bResult );
    return bResult;
}

DdNode* Llb_BddQuantifyPis	(	Aig_Man_t *	pInit,
		DdManager *	dd,
		DdNode *	bFunc
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file llb2Bad.c.

{
    DdNode * bVar, * bCube, * bTemp;
    Aig_Obj_t * pObj;
    int i;
    abctime TimeStop;
    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
    TimeStop = dd->TimeStop; dd->TimeStop = 0;
    // create PI cube
    bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
    Saig_ManForEachPi( pInit, pObj, i )    {
        bVar  = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    // quantify PI cube
    bFunc = Cudd_bddExistAbstract( dd, bFunc, bCube );  Cudd_Ref( bFunc );
    Cudd_RecursiveDeref( dd, bCube );
    Cudd_Deref( bFunc );
    dd->TimeStop = TimeStop;
    return bFunc;
}

DdNode* Llb_CoreComputeCube	(	DdManager *	dd,
		Vec_Int_t *	vVars,
		int	fUseVarIndex,
		char *	pValues
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes cube composed of given variables with given values.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file llb2Core.c.

{
    DdNode * bRes, * bVar, * bTemp;
    int i, iVar, Index;
    abctime TimeStop;
    TimeStop = dd->TimeStop; dd->TimeStop = 0;
    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
    Vec_IntForEachEntry( vVars, Index, i )
    {
        iVar  = fUseVarIndex ? Index : i;
        bVar  = Cudd_NotCond( Cudd_bddIthVar(dd, iVar), (int)(pValues == NULL || pValues[i] != 1) );
        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bRes );
    dd->TimeStop = TimeStop;
    return bRes;
}

int Llb_CoreExperiment	(	Aig_Man_t *	pInit,
		Aig_Man_t *	pAig,
		Gia_ParLlb_t *	pPars,
		Vec_Ptr_t *	vResult,
		abctime	TimeTarget
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 694 of file llb2Core.c.

{
    int RetValue;
    Llb_Img_t * p;
//    printf( "\n" );
//    pPars->fVerbose = 1;
    p = Llb_CoreStart( pInit, pAig, pPars );
    p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget );
    if ( p->vDdMans == NULL )
    {
        if ( !pPars->fSilent )
            printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit );
        Llb_CoreStop( p );
        return -1;
    }
    RetValue = Llb_CoreReachability( p );
    Llb_CoreStop( p );
    return RetValue;
}

Vec_Int_t* Llb_DriverCollectCs

(

Aig_Man_t *

pAig

)

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

Synopsis [Returns array of CS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file llb2Driver.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj;
    int i;
    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLo( pAig, pObj, i )
        Vec_IntPush( vVars, Aig_ObjId(pObj) );
    return vVars;
}

Vec_Int_t* Llb_DriverCollectNs	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vDriRefs
	)

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

Synopsis [Returns array of NS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file llb2Driver.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj, * pDri;
    int i;
    vVars = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        pDri = Aig_ObjFanin0(pObj);
        if ( Vec_IntEntry( vDriRefs, Aig_ObjId(pDri) ) != 1 || Saig_ObjIsPi(pAig, pDri) || Aig_ObjIsConst1(pDri) )
            Vec_IntPush( vVars, Aig_ObjId(pObj) );
        else
            Vec_IntPush( vVars, Aig_ObjId(pDri) );
    }
    return vVars;
}

Vec_Int_t* Llb_DriverCountRefs

(

Aig_Man_t *

p

)

DECLARATIONS ///.

CFile****************************************************************

FileName [llb2Driver.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Procedures working with flop drivers.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

llb2Driver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Returns the array of times each flop driver is referenced.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file llb2Driver.c.

{
    Vec_Int_t * vCounts;
    Aig_Obj_t * pObj;
    int i;
    vCounts = Vec_IntStart( Aig_ManObjNumMax(p) );
    Saig_ManForEachLi( p, pObj, i )
        Vec_IntAddToEntry( vCounts, Aig_ObjFaninId0(pObj), 1 );
    return vCounts;
}

DdManager* Llb_DriverLastPartition	(	Aig_Man_t *	p,
		Vec_Int_t *	vVarsNs,
		abctime	TimeTarget
	)

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

Synopsis [Compute the last partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file llb2Driver.c.

{
//    int fVerbose = 1;
    DdManager * dd;
    DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp;
    Aig_Obj_t * pObj;
    int i;
    dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
    dd->TimeStop = TimeTarget;
    bRes = Cudd_ReadOne(dd);                                   Cudd_Ref( bRes );

    // mark the duplicated flop inputs
    Aig_ManForEachObjVec( vVarsNs, p, pObj, i )
    {
        if ( !Saig_ObjIsLi(p, pObj) )
            continue;
        bVar1 = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
        bVar2 = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            bVar2 = Cudd_ReadOne(dd);
        bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
        bProd = Cudd_bddXnor( dd, bVar1, bVar2 );              Cudd_Ref( bProd );
//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
        if ( bRes == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bProd );
            return NULL;
        }        
        Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }

/*
    Saig_ManForEachLi( p, pObj, i )
        printf( "%d ", Aig_ObjId(pObj) );
    printf( "\n" );
    Saig_ManForEachLi( p, pObj, i )
        printf( "%c%d ", Aig_ObjFaninC0(pObj)? '-':'+', Aig_ObjFaninId0(pObj) );
    printf( "\n" );
*/
    Cudd_AutodynDisable( dd );
//    Cudd_RecursiveDeref( dd, bRes );
//    Extra_StopManager( dd );
    dd->bFunc = bRes;
    dd->TimeStop = 0;
    return dd;
}

DdNode* Llb_DriverPhaseCube	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vDriRefs,
		DdManager *	dd
	)

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

Synopsis [Create cube for phase swapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file llb2Driver.c.

{
    DdNode * bCube, * bVar, * bTemp;
    Aig_Obj_t * pObj;
    int i;
    abctime TimeStop;
    TimeStop = dd->TimeStop; dd->TimeStop = 0;
    bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
    Saig_ManForEachLi( pAig, pObj, i )
    {
        assert( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) >= 1 );
        if ( Vec_IntEntry( vDriRefs, Aig_ObjFaninId0(pObj) ) != 1 )
            continue;
        if ( !Aig_ObjFaninC0(pObj) )
            continue;
        bVar  = Cudd_bddIthVar( dd, Aig_ObjFaninId0(pObj) );
        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bCube );
    dd->TimeStop = TimeStop;
    return bCube;
}

DdNode* Llb_ImgComputeImage	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vDdMans,
		DdManager *	dd,
		DdNode *	bInit,
		Vec_Ptr_t *	vQuant0,
		Vec_Ptr_t *	vQuant1,
		Vec_Int_t *	vDriRefs,
		abctime	TimeTarget,
		int	fBackward,
		int	fReorder,
		int	fVerbose
	)

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

Synopsis [Computes image of the initial set of states.]

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file llb2Image.c.

{
//    int fCheckSupport = 0;
    DdManager * ddPart;
    DdNode * bImage, * bGroup, * bCube, * bTemp;
    int i;
    abctime clk, clk0 = Abc_Clock();

    bImage = bInit;  Cudd_Ref( bImage );
    if ( fBackward )
    {
        // change polarity
        bCube  = Llb_DriverPhaseCube( pAig, vDriRefs, dd );                Cudd_Ref( bCube );
        bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube );     Cudd_Ref( bImage );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
    }
    else
    {
        // quantify unique vriables
        bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
        bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );                    
        if ( bImage == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bCube );
            return NULL;
        }
        Cudd_Ref( bImage );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
    }
    // perform image computation
    Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i )
    {
        clk = Abc_Clock();
if ( fVerbose )
printf( "   %2d : ", i );
        // transfer the BDD from the group manager to the main manager
        bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc );                           
        if ( bGroup == NULL )
            return NULL;
        Cudd_Ref( bGroup );
if ( fVerbose )
printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
        // perform partial product
        bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
//        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );                
//        bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );  
        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );  
        if ( bImage == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bCube );
            Cudd_RecursiveDeref( dd, bGroup );
            return NULL;
        }
        Cudd_Ref( bImage );

if ( fVerbose )
printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
//printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n");
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
        Cudd_RecursiveDeref( dd, bGroup );

//        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
//        Abc_Print( 1, "Reo =%6d.  ", Cudd_DagSize(bImage) );

if ( fVerbose )
printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
if ( fVerbose )
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
    }

    if ( !fBackward )
    {
        // change polarity
        bCube  = Llb_DriverPhaseCube( pAig, vDriRefs, dd );                Cudd_Ref( bCube );
        bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube );     Cudd_Ref( bImage );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
    }
    else
    {
        // quantify unique vriables
        bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
        bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );                    Cudd_Ref( bImage );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
    }

    if ( fReorder )
    {
    if ( fVerbose )
    Abc_Print( 1, "        Reordering... Before =%5d. ", Cudd_DagSize(bImage) );
    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
    if ( fVerbose )
    Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
//    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
//    Abc_Print( 1, "After =%5d.  ", Cudd_DagSize(bImage) );
    if ( fVerbose )
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk0 );
//    Abc_Print( 1, "\n" );
    }

    Cudd_Deref( bImage );
    return bImage;
}

DdManager* Llb_ImgPartition	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vLower,
		Vec_Ptr_t *	vUpper,
		abctime	TimeTarget
	)

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

Synopsis [Computes one partition in a separate BDD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file llb2Image.c.

{
    Vec_Ptr_t * vNodes, * vRange;
    Aig_Obj_t * pObj;
    DdManager * dd;
    DdNode * bBdd0, * bBdd1, * bProd, * bRes, * bTemp;
    int i;

    dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
    dd->TimeStop = TimeTarget;

    Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
        pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );

    vNodes = Llb_ManCutNodes( 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 );
//        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );  
        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );  
        if ( pObj->pData == NULL )
        {
            Cudd_Quit( dd );
            Vec_PtrFree( vNodes );
            return NULL;
        }
        Cudd_Ref( (DdNode *)pObj->pData );
    }

    vRange = Llb_ManCutRange( p, vLower, vUpper );
    bRes   = Cudd_ReadOne(dd);   Cudd_Ref( bRes );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRange, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData );   Cudd_Ref( bProd );
//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
//        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );  
        if ( bRes == NULL )
        {
            Cudd_Quit( dd );
            Vec_PtrFree( vRange );
            Vec_PtrFree( vNodes );
            return NULL;
        }        
        Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );

    Vec_PtrFree( vRange );
    Vec_PtrFree( vNodes );
    Cudd_AutodynDisable( dd );
//    Cudd_RecursiveDeref( dd, bRes );
//    Extra_StopManager( dd );
    dd->bFunc = bRes;
    dd->TimeStop = 0;
    return dd;
}

void Llb_ImgQuantifyFirst	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vDdMans,
		Vec_Ptr_t *	vQuant0,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file llb2Image.c.

{
    DdManager * dd;
    DdNode * bProd, * bRes, * bTemp;
    int i;
    abctime clk = Abc_Clock();
    Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
    {
        // remember unquantified ones
        assert( dd->bFunc2 == NULL );
        dd->bFunc2 = dd->bFunc;   Cudd_Ref( dd->bFunc2 );

        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );

        bRes = dd->bFunc;
        if ( fVerbose )
            Abc_Print( 1, "Part %2d : Init =%5d. ", i, Cudd_DagSize(bRes) );
        bProd = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, i+1), dd );   Cudd_Ref( bProd );
        bRes  = Cudd_bddExistAbstract( dd, bTemp = bRes, bProd );                          Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
        dd->bFunc = bRes;

        Cudd_AutodynDisable( dd );

        if ( fVerbose )
            Abc_Print( 1, "Quant =%5d. ", Cudd_DagSize(bRes) );
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
        if ( fVerbose ) 
            Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
        if ( fVerbose ) 
            Abc_Print( 1, "Reo = %5d.  ", Cudd_DagSize(bRes) );
        if ( fVerbose ) 
            Abc_Print( 1, "Supp = %3d.  ", Cudd_SupportSize(dd, bRes) );
        if ( fVerbose ) 
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    }
}

void Llb_ImgQuantifyReset

(

Vec_Ptr_t *

vDdMans

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file llb2Image.c.

{
    DdManager * dd;
    int i;
    Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
    {
        assert( dd->bFunc2 != NULL );
        Cudd_RecursiveDeref( dd, dd->bFunc );
        dd->bFunc = dd->bFunc2;
        dd->bFunc2 = NULL;
    }
}

void Llb_ImgSchedule	(	Vec_Ptr_t *	vSupps,
		Vec_Ptr_t **	pvQuant0,
		Vec_Ptr_t **	pvQuant1,
		int	fVerbose
	)

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

Synopsis [Computes quantification schedule.]

Description [Input array contains supports: 0=starting, ... intermediate... N-1=final. Output arrays contain immediately quantifiable vars (vQuant0) and vars that should be quantified after conjunction (vQuant1).]

SideEffects []

SeeAlso []

Definition at line 122 of file llb2Image.c.

{
    Vec_Int_t * vOne;
    int nVarsAll, Counter, iSupp = -1, Entry, i, k;
    // start quantification arrays
    *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
    *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
    Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
    {
        Vec_PtrPush( *pvQuant0, Vec_IntAlloc(16) );
        Vec_PtrPush( *pvQuant1, Vec_IntAlloc(16) );
    }
    // count how many times each var appears
    nVarsAll = Vec_IntSize( (Vec_Int_t *)Vec_PtrEntry(vSupps, 0) );
    for ( i = 0; i < nVarsAll; i++ )
    {
        Counter = 0;
        Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
            if ( Vec_IntEntry(vOne, i) )
            {
                iSupp = k;
                Counter++;
            }
        if ( Counter == 0 )
            continue;
        if ( Counter == 1 )
            Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, iSupp), i );
        else // if ( Counter > 1 )
            Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, iSupp), i );
    }

    if ( fVerbose )
    for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
    {
        printf( "%2d : Quant0 = ", i );
        Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, i), Entry, k )
            printf( "%d ", Entry );
        printf( "\n" );
    }

    if ( fVerbose )
    for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
    {
        printf( "%2d : Quant1 = ", i );
        Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, i), Entry, k )
            printf( "%d ", Entry );
        printf( "\n" );
    }
}

Vec_Ptr_t* Llb_ImgSupports	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vDdMans,
		Vec_Int_t *	vStart,
		Vec_Int_t *	vStop,
		int	fAddPis,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes supports of the partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file llb2Image.c.

{
    Vec_Ptr_t * vSupps;
    Vec_Int_t * vOne;
    Aig_Obj_t * pObj;
    DdManager * dd;
    DdNode * bSupp, * bTemp;
    int i, Entry, nSize;
    nSize  = Cudd_ReadSize( (DdManager *)Vec_PtrEntry( vDdMans, 0 ) );
    vSupps = Vec_PtrAlloc( 100 );
    // create initial
    vOne = Vec_IntStart( nSize );
    Vec_IntForEachEntry( vStart, Entry, i )
        Vec_IntWriteEntry( vOne, Entry, 1 );
    Vec_PtrPush( vSupps, vOne );
    // create intermediate 
    Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
    {
        vOne  = Vec_IntStart( nSize );
        bSupp = Cudd_Support( dd, dd->bFunc );  Cudd_Ref( bSupp );
        for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
            Vec_IntWriteEntry( vOne, bTemp->index, 1 );
        Cudd_RecursiveDeref( dd, bSupp );
        Vec_PtrPush( vSupps, vOne );
    }
    // create final
    vOne = Vec_IntStart( nSize );
    Vec_IntForEachEntry( vStop, Entry, i )
        Vec_IntWriteEntry( vOne, Entry, 1 );
    if ( fAddPis )
        Saig_ManForEachPi( p, pObj, i )
            Vec_IntWriteEntry( vOne, Aig_ObjId(pObj), 1 );
    Vec_PtrPush( vSupps, vOne );

    // print supports
    assert( nSize == Aig_ManObjNumMax(p) );
    if ( !fVerbose )
        return vSupps;
    Aig_ManForEachObj( p, pObj, i )
    {
        int k, Counter = 0;
        Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
            Counter += Vec_IntEntry(vOne, i);
        if ( Counter == 0 ) 
            continue;
        printf( "Obj = %4d : ", i );
        if ( Saig_ObjIsPi(p,pObj) )
            printf( "pi  " );
        else if ( Saig_ObjIsLo(p,pObj) )
            printf( "lo  " );
        else if ( Saig_ObjIsLi(p,pObj) )
            printf( "li  " );
        else if ( Aig_ObjIsNode(pObj) )
            printf( "and " );
        Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
            printf( "%d", Vec_IntEntry(vOne, i) );
        printf( "\n" );
    }
    return vSupps;
}

void Llb_ManCluster

(

Llb_Mtr_t *

p

)

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

Synopsis [Combines one pair of columns.]

Description []

SideEffects []

SeeAlso []

Definition at line 324 of file llb1Cluster.c.

{
    int RetValue;
    do
    {
        do {
            RetValue = Llb_ManComputeBestQuant( p );
            if ( RetValue > 0 )
                Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff );
        }
        while ( RetValue > 0 );

        RetValue = Llb_ManComputeBestAttr( p );
        if ( RetValue > 0 )
            Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff );

        Llb_MtrVerifyMatrix( p );
    }
    while ( RetValue > 0 );

    Llb_ManClusterCompress( p );

    Llb_MtrVerifyMatrix( p );
}

Vec_Int_t* Llb_ManDeriveConstraints

(

Aig_Man_t *

p

)

FUNCTION DECLARATIONS ///.

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

Synopsis [Derives inductive constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file llb1Constr.c.

{
    DdManager * dd;
    Vec_Int_t * vNodes;
    if ( Saig_ManPoNum(p) != 1 )
    {
        printf( "The AIG has %d property outputs.\n", Saig_ManPoNum(p) );
        return NULL;
    }
    assert( Saig_ManPoNum(p) == 1 );
    dd = Llb_ManConstructGlobalBdds( p );
    vNodes = Llb_ManComputeBaseCase( p, dd );
    if ( Llb_ManCountEntries(vNodes) > 0 )
        Llb_ManComputeIndCase( p, dd, vNodes );
    if ( Llb_ManCountEntries(vNodes) == 0 )
        Vec_IntFreeP( &vNodes );
    Llb_ManDerefenceBdds( p, dd );
    Extra_StopManager( dd );
    return vNodes;
}

void Llb_ManDumpReached	(	DdManager *	ddG,
		DdNode *	bReached,
		char *	pModel,
		char *	pFileName
	)

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

Synopsis [Writes reached state BDD into a BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file llb2Dump.c.

{
    FILE * pFile;
    Vec_Ptr_t * vNamesIn, * vNamesOut;
    char * pName;
    int i, nDigits;
    // reorder the BDD
    Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );

    // create input names
    nDigits = Abc_Base10Log( Cudd_ReadSize(ddG) );
    vNamesIn = Vec_PtrAlloc( Cudd_ReadSize(ddG) );
    for ( i = 0; i < Cudd_ReadSize(ddG); i++ )
    {
        pName = Llb_ManGetDummyName( "ff", i, nDigits );
        Vec_PtrPush( vNamesIn, Extra_UtilStrsav(pName) );
    }
    // create output names
    vNamesOut = Vec_PtrAlloc( 1 );
    Vec_PtrPush( vNamesOut, Extra_UtilStrsav("Reached") );

    // write the file
    pFile = fopen( pFileName, "wb" );
    Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 );
    fclose( pFile );

    // cleanup
    Vec_PtrForEachEntry( char *, vNamesIn, pName, i )
        ABC_FREE( pName );
    Vec_PtrForEachEntry( char *, vNamesOut, pName, i )
        ABC_FREE( pName );
    Vec_PtrFree( vNamesIn );
    Vec_PtrFree( vNamesOut );
}

Vec_Ptr_t* Llb_ManFlow	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vSources,
		int *	pnFlow
	)

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

Synopsis [Implementation of max-flow/min-cut computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 762 of file llb2Flow.c.

{
    Vec_Ptr_t * vMinCut;
    Aig_Obj_t * pObj;
    int Flow, FlowCur, RetValue, i;
    // find the max-flow
    Flow = 0;
    Aig_ManCleanData( p );
    Aig_ManIncrementTravId(p);
    Vec_PtrForEachEntry( Aig_Obj_t *, vSources, pObj, i )
    {
        assert( !pObj->fMarkA && pObj->fMarkB );
        if ( !Aig_ObjFanin0(pObj)->fMarkB )
        {
            FlowCur  = Llb_ManFlowBwdPath2_rec( p, Aig_ObjFanin0(pObj) );
            Flow    += FlowCur;
            if ( FlowCur )
                Aig_ManIncrementTravId(p);
        }
        if ( Aig_ObjIsNode(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
        {
            FlowCur  = Llb_ManFlowBwdPath2_rec( p, Aig_ObjFanin1(pObj) );
            Flow    += FlowCur;
            if ( FlowCur )
                Aig_ManIncrementTravId(p);
        }
    }
    if ( pnFlow )
        *pnFlow = Flow;

    // mark the nodes reachable from the latches
    Aig_ManIncrementTravId(p);
    Vec_PtrForEachEntry( Aig_Obj_t *, vSources, pObj, i )
    {
        assert( !pObj->fMarkA && pObj->fMarkB );
        if ( !Aig_ObjFanin0(pObj)->fMarkB )
        {
            RetValue = Llb_ManFlowBwdPath2_rec( p, Aig_ObjFanin0(pObj) );
            assert( RetValue == 0 );
        }
        if ( Aig_ObjIsNode(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
        {
            RetValue = Llb_ManFlowBwdPath2_rec( p, Aig_ObjFanin1(pObj) );
            assert( RetValue == 0 );
        }
    }

    // find the min-cut with the smallest volume
    vMinCut = Llb_ManFlowMinCut( p );
    assert( Vec_PtrSize(vMinCut) == Flow );
    // verify the cut
    if ( !Llb_ManFlowVerifyCut(p, vMinCut) )
        printf( "Llb_ManFlow() error! The computed min-cut is not a cut!\n" );
//    Llb_ManFlowPrintCut( p, vMinCut );
    return vMinCut;
}

Llb_Grp_t* Llb_ManGroupAlloc

(

Llb_Man_t *

pMan

)

DECLARATIONS ///.

CFile****************************************************************

FileName [llb1Group.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Initial partition computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

llb1Group.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb1Group.c.

{
    Llb_Grp_t * p;
    p = ABC_CALLOC( Llb_Grp_t, 1 );
    p->pMan   = pMan;
    p->vIns   = Vec_PtrAlloc( 8 );
    p->vOuts  = Vec_PtrAlloc( 8 );
    p->Id     = Vec_PtrSize( pMan->vGroups );
    Vec_PtrPush( pMan->vGroups, p );
    return p;
}

Llb_Grp_t* Llb_ManGroupCreateFromCuts	(	Llb_Man_t *	pMan,
		Vec_Int_t *	vCut1,
		Vec_Int_t *	vCut2
	)

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

Synopsis [Creates group from two cuts derived by the flow computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file llb1Group.c.

{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( pMan );

    // mark Cut1
    Aig_ManIncrementTravId( pMan->pAig );
    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
        Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
    // collect unmarked Cut2
    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
        if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
            Vec_PtrPush( p->vOuts, pObj );

    // mark nodes reachable from Cut2
    Aig_ManIncrementTravId( pMan->pAig );
    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
        Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
    // collect marked Cut1
    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
        if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
            Vec_PtrPush( p->vIns, pObj );

    // derive internal objects
    assert( p->vNodes == NULL );
    p->vNodes = Llb_ManGroupCollect( p );
    return p;
}

Llb_Grp_t* Llb_ManGroupsCombine	(	Llb_Grp_t *	p1,
		Llb_Grp_t *	p2
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file llb1Group.c.

{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( p1->pMan );
    // create inputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
        Vec_PtrPush( p->vIns, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
        Vec_PtrPushUnique( p->vIns, pObj );
    // create outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
        Vec_PtrPush( p->vOuts, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
        Vec_PtrPushUnique( p->vOuts, pObj );

    // derive internal objects
    assert( p->vNodes == NULL );
    p->vNodes = Llb_ManGroupCollect( p );
    return p;
}

void Llb_ManGroupStop

(

Llb_Grp_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file llb1Group.c.

{
    if ( p == NULL )
        return;
    Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
    Vec_PtrFreeP( &p->vIns );
    Vec_PtrFreeP( &p->vOuts );
    Vec_PtrFreeP( &p->vNodes );
    ABC_FREE( p );
}

Vec_Int_t* Llb_ManMarkPivotNodes	(	Aig_Man_t *	p,
		int	fUseInternal
	)

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

Synopsis [Determine starting cut-points.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file llb1Pivot.c.

{
    Vec_Int_t * vVar2Obj;
    Aig_Obj_t * pObj;
    int i;
    // mark inputs/outputs
    Aig_ManForEachCi( p, pObj, i )
        pObj->fMarkA = 1;
    Saig_ManForEachLi( p, pObj, i )
        pObj->fMarkA = 1;

    // mark internal pivot nodes
    if ( fUseInternal )
        Llb_ManMarkInternalPivots( p );

    // assign variable numbers
    Aig_ManConst1(p)->fMarkA = 0;
    vVar2Obj = Vec_IntAlloc( 100 );
    Aig_ManForEachCi( p, pObj, i )
        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    Aig_ManForEachNode( p, pObj, i )
        if ( pObj->fMarkA )
            Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    Saig_ManForEachLi( p, pObj, i )
        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    return vVar2Obj;
}

int Llb_ManModelCheckAig	(	Aig_Man_t *	pAigGlo,
		Gia_ParLlb_t *	pPars,
		Vec_Int_t *	vHints,
		DdManager **	pddGlo
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file llb1Core.c.

{
    Llb_Man_t * p = NULL; 
    Aig_Man_t * pAig;
    int RetValue = -1;
    abctime clk = Abc_Clock();

    if ( pPars->fIndConstr )
    {
        assert( vHints == NULL );
        vHints = Llb_ManDeriveConstraints( pAigGlo );
    }

    // derive AIG for hints
    if ( vHints == NULL )
        pAig = Aig_ManDupSimple( pAigGlo );
    else
    {
        if ( pPars->fVerbose )
            Llb_ManPrintEntries( pAigGlo, vHints );
        pAig = Aig_ManDupSimpleWithHints( pAigGlo, vHints );
    }


    if ( pPars->fUseFlow )
    {
//        p = Llb_ManStartFlow( pAigGlo, pAig, pPars );
    }
    else
    {
        p = Llb_ManStart( pAigGlo, pAig, pPars );
        if ( pPars->fVerbose )
        {
            Llb_ManPrintAig( p );
            printf( "Original matrix:          " );
            Llb_MtrPrintMatrixStats( p->pMatrix );
            if ( pPars->fVeryVerbose )
                Llb_MtrPrint( p->pMatrix, 1 );
        }
        if ( pPars->fCluster )
        {
            Llb_ManCluster( p->pMatrix );
            if ( pPars->fVerbose )
            {
                printf( "Matrix after clustering:  " );
                Llb_MtrPrintMatrixStats( p->pMatrix );
                if ( pPars->fVeryVerbose )
                    Llb_MtrPrint( p->pMatrix, 1 );
            }
        }
        if ( pPars->fSchedule )
        {
            Llb_MtrSchedule( p->pMatrix );
            if ( pPars->fVerbose )
            {
                printf( "Matrix after scheduling:  " );
                Llb_MtrPrintMatrixStats( p->pMatrix );
                if ( pPars->fVeryVerbose )
                    Llb_MtrPrint( p->pMatrix, 1 );
            }
        }
    }
    
    if ( !p->pPars->fSkipReach ) 
        RetValue = Llb_ManReachability( p, vHints, pddGlo );
    Llb_ManStop( p );

    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    if ( pPars->fIndConstr )
        Vec_IntFreeP( &vHints );
    return RetValue;
}

int Llb_ManModelCheckAigWithHints	(	Aig_Man_t *	pAigGlo,
		Gia_ParLlb_t *	pPars
	)

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

Synopsis [Derives AIG whose PI is substituted by a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file llb1Hint.c.

{
    DdManager * ddGlo = NULL;
    Vec_Int_t * vHints;
    Vec_Int_t * vHFCands;
    int i, Entry, RetValue = -1;
    abctime clk = Abc_Clock();
    assert( pPars->nHintDepth > 0 );
/*
    // perform reachability without hints
    RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL );
    if ( RetValue >= 0 )
        return RetValue;
*/
    // create hints representation
    vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 );
    vHints   = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) );
    // add one hint at a time till the problem is solved
    Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst )
    {
        Vec_IntWriteEntry( vHints, Entry, 1 );   // change to 1 to start from zero cof!!!
        // solve under hints
        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
        if ( RetValue == 0 )
            goto Finish;
        if ( RetValue == 1 )
            break;
    }
    if ( RetValue == -1 )
        goto Finish;
    // undo the hints one at a time
    for ( ; i >= pPars->HintFirst; i-- )
    {
        Entry = Vec_IntEntry( vHFCands, i );
        Vec_IntWriteEntry( vHints, Entry, -1 );        
        // solve under relaxed hints
        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
        if ( RetValue == 0 )
            goto Finish;
        if ( RetValue == 1 )
            continue;
        break;
    }
Finish:
    if ( ddGlo )
    {
        if ( ddGlo->bFunc )
            Cudd_RecursiveDeref( ddGlo, ddGlo->bFunc ); 
        Extra_StopManager( ddGlo );
    }
    Vec_IntFreeP( &vHFCands );
    Vec_IntFreeP( &vHints );
    if ( pPars->fVerbose )
        Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk );
    return RetValue;
}

void Llb_ManPrepareGroups

(

Llb_Man_t *

pMan

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 356 of file llb1Group.c.

{
    Aig_Obj_t * pObj;
    int i;
    assert( pMan->vGroups == NULL );
    pMan->vGroups = Vec_PtrAlloc( 1000 );
    Llb_ManGroupCreateFirst( pMan );
    Aig_ManForEachNode( pMan->pAig, pObj, i )
    {
        if ( pObj->fMarkA )
            Llb_ManGroupCreate( pMan, pObj );
    }
    Saig_ManForEachLi( pMan->pAig, pObj, i )
    {
        if ( pObj->fMarkA )
            Llb_ManGroupCreate( pMan, pObj );
    }
    Llb_ManGroupCreateLast( pMan );
}

void Llb_ManPrepareVarLimits

(

Llb_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file llb1Man.c.

{
    Llb_Grp_t * pGroup;
    Aig_Obj_t * pVar;
    int i, k;
    assert( p->vVarBegs == NULL );
    assert( p->vVarEnds == NULL );
    p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
    p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
    Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols );

    for ( i = 0; i < p->pMatrix->nCols; i++ )
    {
        pGroup = p->pMatrix->pColGrps[i];

        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );

        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
    }
}

void Llb_ManPrepareVarMap

(

Llb_Man_t *

p

)

DECLARATIONS ///.

CFile****************************************************************

FileName [llb1Man.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Reachability manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

llb1Man.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb1Man.c.

{
    Aig_Obj_t * pObjLi, * pObjLo;
    int i, iVarLi, iVarLo;
    assert( p->vNs2Glo == NULL );
    assert( p->vCs2Glo == NULL );
    assert( p->vGlo2Cs == NULL );
    assert( p->vGlo2Ns == NULL );
    p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
    p->vCs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
    p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
    {
        iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
        iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
        assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
        assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
        Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
        Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
        Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
        Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
    }
    // add mapping of the PIs
    Saig_ManForEachPi( p->pAig, pObjLo, i )
    {
        iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
        Vec_IntWriteEntry( p->vCs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
        Vec_IntWriteEntry( p->vNs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
    }
}

void Llb_ManPrintEntries	(	Aig_Man_t *	p,
		Vec_Int_t *	vCands
	)

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

Synopsis [Returns the array of constraint candidates.]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file llb1Constr.c.

{
    int i, Entry;
    if ( vCands == NULL )
    {
        printf( "There is no hints.\n" );
        return;
    }
    Entry = Llb_ManCountEntries(vCands);
    printf( "\n*** Using %d hint%s:\n", Entry, (Entry != 1 ? "s":"") );
    Vec_IntForEachEntry( vCands, Entry, i )
    {
        if ( Entry != 0 && Entry != 1 )
            continue;
        printf( "%c", Entry ? '+' : '-' );
        printf( "%-6d : ", i );
        Aig_ObjPrint( p, Aig_ManObj(p, i) );
        printf( "\n" );
    }
}

int Llb_ManReachability	(	Llb_Man_t *	p,
		Vec_Int_t *	vHints,
		DdManager **	pddGlo
	)

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

Synopsis [Perform reachability with hints and returns reached states in ppGlo.]

Description []

SideEffects []

SeeAlso []

Definition at line 582 of file llb1Reach.c.

{
    int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
    int * pCs2Glo = Vec_IntArray( p->vCs2Glo );
    int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
    DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
    DdNode * bConstrCs, * bConstrNs;
    abctime clk2, clk = Abc_Clock();
    int nIters, nBddSize = 0;
//    int nThreshold = 10000;

    // compute time to stop
    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;

    // define variable limits
    Llb_ManPrepareVarLimits( p );

    // start the managers
    assert( p->dd == NULL );
    assert( p->ddG == NULL );
    assert( p->ddR == NULL );
    p->dd  = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    if ( pddGlo && *pddGlo )
        p->ddG = *pddGlo, *pddGlo = NULL; 
    else
        p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig),   0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );

    if ( p->pPars->fReorder )
    {
        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
        Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
        Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
    }
    else
    {
        Cudd_AutodynDisable( p->dd );
        Cudd_AutodynDisable( p->ddG );
        Cudd_AutodynDisable( p->ddR );
    }

    // set the stop time parameter
    p->dd->TimeStop  = p->pPars->TimeTarget;
    p->ddG->TimeStop = p->pPars->TimeTarget;
    p->ddR->TimeStop = p->pPars->TimeTarget;

    // create bad state in the ring manager
    p->ddR->bFunc  = Llb_BddComputeBad( p->pAigGlo, 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 );
        p->pPars->iFrame = -1;
        return -1;
    }
    Cudd_Ref( p->ddR->bFunc );

    // derive constraints
    bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 );   Cudd_Ref( bConstrCs );
    bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 );   Cudd_Ref( bConstrNs );
//Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" );
//Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" );

    // perform reachability analysis
    // compute the starting set of states
    if ( p->ddG->bFunc )
    {
        bReached = p->ddG->bFunc; p->ddG->bFunc = NULL;
        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs );    Cudd_Ref( bCurrent );
    }
    else
    {
        bReached = Llb_ManComputeInitState( p, p->ddG );                         Cudd_Ref( bReached );
        bCurrent = Llb_ManComputeInitState( p, p->dd  );                         Cudd_Ref( bCurrent );
    }
//Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" );
//Extra_bddPrintSupport( p->dd,  bCurrent ); printf( "\n" );

//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
    { 
        clk2 = Abc_Clock();
        // check the runtime limit
        if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
        {
            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;
            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
            return -1;
        }

        // save the onion ring
        bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo );
        if ( bTemp == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during ring transfer.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
            return -1;
        }
        Cudd_Ref( bTemp );
        Vec_PtrPush( p->vRings, bTemp );

        // check it for bad states
        if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) ) 
        {
            assert( p->pAigGlo->pSeqModel == NULL );
            if ( !p->pPars->fBackward )
                p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p ); 
            if ( !p->pPars->fSilent )
            {
                if ( !p->pPars->fBackward )
                    Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters );
                else
                    Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced).  ", p->pAigGlo->pName, nIters );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
            return 0; 
        }

        // restrict reachable states using constraints
        if ( vHints )
        {
            bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs );                                Cudd_Ref( bCurrent );
            Cudd_RecursiveDeref( p->dd, bTemp );
        }

        // quantify variables appearing only in the init state
        bCube    = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 );  Cudd_Ref( bCube );
        bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube );                              Cudd_Ref( bCurrent );
        Cudd_RecursiveDeref( p->dd, bTemp );
        Cudd_RecursiveDeref( p->dd, bCube );

        // compute the next states
        bNext = Llb_ManComputeImage( p, bCurrent, 0 );
        if ( bNext == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->dd,  bCurrent );   bCurrent = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
            return -1;
        }
        Cudd_Ref( bNext );
        Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;

        // restrict reachable states using constraints
        if ( vHints )
        {
            bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs );                Cudd_Ref( bNext );
            Cudd_RecursiveDeref( p->dd, bTemp );
        }
//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );

        // remap these states into the current state vars
//        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    Cudd_Ref( bNext );
//        Cudd_RecursiveDeref( p->dd, bTemp );
//        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );    
        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    
        if ( bNext == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->dd,  bTemp );  
            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
            return -1;
        }
        Cudd_Ref( bNext );
        Cudd_RecursiveDeref( p->dd, bTemp );  


        // check if there are any new states
        if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
        {
            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
            break;
        }

        // check the BDD size
        nBddSize = Cudd_DagSize(bNext);
        if ( nBddSize > p->pPars->nBddMax )
        {
            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
            break;
        }

        // get the new states
        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
        if ( bCurrent == NULL )
        {
            Cudd_RecursiveDeref( p->ddG,  bNext );        bNext = NULL;
            Cudd_RecursiveDeref( p->ddG,  bReached );     bReached = NULL;
            break;
        }
        Cudd_Ref( bCurrent );
        // minimize the new states with the reached states
//        bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
//        bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) );  Cudd_Ref( bCurrent );
//        Cudd_RecursiveDeref( p->ddG, bTemp );
//printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) );

        // remap these states into the current state vars
//        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );   Cudd_Ref( bCurrent );
//        Cudd_RecursiveDeref( p->ddG, bTemp );
//        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );    
        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );    
        if ( bCurrent == NULL )
        {
            if ( !p->pPars->fSilent )
                printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
            p->pPars->iFrame = nIters - 1;
            Cudd_RecursiveDeref( p->ddG, bTemp );  
            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
            return -1;
        }
        Cudd_Ref( bCurrent );
        Cudd_RecursiveDeref( p->ddG, bTemp ); 
        

        // add to the reached states
        bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );                       
        if ( bReached == NULL )
        {
            Cudd_RecursiveDeref( p->ddG,  bTemp );     bTemp = NULL;
            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
            break;
        }
        Cudd_Ref( bReached );
        Cudd_RecursiveDeref( p->ddG, bTemp );
        Cudd_RecursiveDeref( p->ddG, bNext );
        bNext = NULL;

        if ( p->pPars->fVerbose )
        {
            fprintf( stdout, "F =%5d : ",    nIters );
            fprintf( stdout, "Im =%6d  ",    nBddSize );
            fprintf( stdout, "(%4d %3d)   ", Cudd_ReadReorderings(p->dd),  Cudd_ReadGarbageCollections(p->dd) );
            fprintf( stdout, "Rea =%6d  ",   Cudd_DagSize(bReached) );
            fprintf( stdout, "(%4d%4d)   ",  Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
        }
/*
        if ( p->pPars->fVerbose )
        {
            double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
//            Extra_bddPrint( p->ddG, bReached );printf( "\n" );
            fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
            fflush( stdout ); 
        }
*/
    }
    Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
    Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
    if ( bReached == NULL )
    {
        p->pPars->iFrame = nIters - 1;
        return 0; // reachable
    }
//    assert( bCurrent == NULL );
    if ( bCurrent )
        Cudd_RecursiveDeref( p->dd, bCurrent );
    // report the stats
    if ( p->pPars->fVerbose )
    {
        double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
        if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
        else
            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
        fflush( stdout ); 
    }
    if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
    {
        if ( !p->pPars->fSilent )
            printf( "Verified only for states reachable in %d frames.  ", nIters );
        p->pPars->iFrame = p->pPars->nIterMax;
        Cudd_RecursiveDeref( p->ddG, bReached );
        return -1; // undecided
    }
    if ( pddGlo ) 
    {
        assert( p->ddG->bFunc == NULL );
        p->ddG->bFunc = bReached; bReached = NULL;
        assert( *pddGlo == NULL );
        *pddGlo = p->ddG;  p->ddG = NULL;
    }
    else
        Cudd_RecursiveDeref( p->ddG, bReached );
    if ( !p->pPars->fSilent )
        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
    p->pPars->iFrame = nIters - 1;
    return 1; // unreachable
}

int Llb_ManReachabilityWithHints

(

Llb_Man_t *

p

)

Llb_Man_t* Llb_ManStart	(	Aig_Man_t *	pAigGlo,
		Aig_Man_t *	pAig,
		Gia_ParLlb_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file llb1Man.c.

{
    Llb_Man_t * p;
    Aig_ManCleanMarkA( pAig );
    p = ABC_CALLOC( Llb_Man_t, 1 );
    p->pAigGlo  = pAigGlo;
    p->pPars    = pPars;
    p->pAig     = pAig;
    p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
    p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
    p->vRings   = Vec_PtrAlloc( 100 );
    Llb_ManPrepareVarMap( p );
    Llb_ManPrepareGroups( p );
    Aig_ManCleanMarkA( pAig );
    p->pMatrix = Llb_MtrCreate( p );
    p->pMatrix->pMan = p;
    return p;
}

void Llb_ManStop

(

Llb_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file llb1Man.c.

{
    Llb_Grp_t * pGrp;
    DdNode * bTemp;
    int i;

//    Vec_IntFreeP( &p->vMem );
//    Vec_PtrFreeP( &p->vTops );
//    Vec_PtrFreeP( &p->vBots );
//    Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts );

    if ( p->pMatrix )
        Llb_MtrFree( p->pMatrix );
    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
        Llb_ManGroupStop( pGrp );
    if ( p->dd )
    {
//        printf( "Manager dd\n" );
        Extra_StopManager( p->dd );
    }
    if ( p->ddG )
    {
//        printf( "Manager ddG\n" );
        if ( p->ddG->bFunc )
            Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc ); 
        Extra_StopManager( p->ddG );
    }
    if ( p->ddR )
    {
//        printf( "Manager ddR\n" );
        if ( p->ddR->bFunc )
            Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc ); 
        Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
            Cudd_RecursiveDeref( p->ddR, bTemp );
        Extra_StopManager( p->ddR );
    }
    Aig_ManStop( p->pAig );
    Vec_PtrFreeP( &p->vGroups );
    Vec_IntFreeP( &p->vVar2Obj );
    Vec_IntFreeP( &p->vObj2Var );
    Vec_IntFreeP( &p->vVarBegs );
    Vec_IntFreeP( &p->vVarEnds );
    Vec_PtrFreeP( &p->vRings  );
    Vec_IntFreeP( &p->vNs2Glo );
    Vec_IntFreeP( &p->vCs2Glo );
    Vec_IntFreeP( &p->vGlo2Cs );
    Vec_IntFreeP( &p->vGlo2Ns );
//    Vec_IntFreeP( &p->vHints );
    ABC_FREE( p );
}

int Llb_ManTracePaths	(	Aig_Man_t *	p,
		Aig_Obj_t *	pPivot
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file llb1Pivot.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManIncrementTravId( p ); // prev = visited with path to LI  (value 0)
    Aig_ManIncrementTravId( p ); // cur  = visited w/o  path to LI  (value 1)
    Saig_ManForEachLo( p, pObj, i )
        Counter += Llb_ManTracePaths_rec( p, pObj, pPivot );
    return Counter;
}

Llb_Mtr_t* Llb_MtrCreate

(

Llb_Man_t *

p

)

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

Synopsis [Matrix reduce.]

Description []

SideEffects []

SeeAlso []

Definition at line 410 of file llb1Matrix.c.

{
    Llb_Mtr_t * pMatrix;
    Llb_Grp_t * pGroup;
    int i;
    pMatrix = Llb_MtrAlloc( Saig_ManPiNum(p->pAig), Saig_ManRegNum(p->pAig), 
        Vec_PtrSize(p->vGroups), Vec_IntSize(p->vVar2Obj) );
    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
        Llb_MtrAddColumn( pMatrix, pGroup );
//    Llb_MtrRemoveSingletonRows( pMatrix );
    return pMatrix;
}

void Llb_MtrFree

(

Llb_Mtr_t *

p

)

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

Synopsis [Stops the matrix representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file llb1Matrix.c.

{
    int i;
    ABC_FREE( p->pProdVars );
    ABC_FREE( p->pProdNums );
    for ( i = 0; i < p->nCols; i++ )
        ABC_FREE( p->pMatrix[i] );
    ABC_FREE( p->pRowSums );
    ABC_FREE( p->pColSums );
    ABC_FREE( p->pMatrix );
    ABC_FREE( p->pColGrps );
    ABC_FREE( p );
}

void Llb_MtrPrint	(	Llb_Mtr_t *	p,
		int	fOrder
	)

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

Synopsis [Creates one column with vars in the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file llb1Matrix.c.

{
    int * pOrder = NULL;
    int i, iRow, iCol;
    if ( fOrder )
        pOrder = Llb_MtrFindVarOrder( p );
    for ( i = 0; i < p->nRows; i++ )
    {
        iRow = pOrder ? pOrder[i] : i;
        printf( "%3d : ", iRow );
        printf( "%3d ", p->pRowSums[iRow] );
        printf( "%3s ", Llb_MtrVarName(p, iRow) );
        for ( iCol = 0; iCol < p->nCols; iCol++ )
            printf( "%c", p->pMatrix[iCol][iRow] ? '*' : ' ' );
        printf( "\n" );
    }
    ABC_FREE( pOrder );
}

void Llb_MtrPrintMatrixStats

(

Llb_Mtr_t *

p

)

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

Synopsis [Verify columns.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file llb1Matrix.c.

{
    int iVar, iGrp, iGrp1, iGrp2, Span = 0, nCutSize = 0, nCutSizeMax = 0;
    int * pGrp1 = ABC_CALLOC( int, p->nRows ); 
    int * pGrp2 = ABC_CALLOC( int, p->nRows ); 
    for ( iVar = 0; iVar < p->nRows; iVar++ )
    {
        if ( p->pRowSums[iVar] == 0 )
            continue;
        for ( iGrp1 = 0; iGrp1 < p->nCols; iGrp1++ )
            if ( p->pMatrix[iGrp1][iVar] == 1 )
                break;
        for ( iGrp2 = p->nCols - 1; iGrp2 >= 0; iGrp2-- )
            if ( p->pMatrix[iGrp2][iVar] == 1 )
                break;
        assert( iGrp1 <= iGrp2 );
        pGrp1[iVar] = iGrp1;
        pGrp2[iVar] = iGrp2;
        Span += iGrp2 - iGrp1;
    }
    // compute span
    for ( iGrp = 0; iGrp < p->nCols; iGrp++ )
    {
        for ( iVar = 0; iVar < p->nRows; iVar++ )
            if ( pGrp1[iVar] == iGrp )
                nCutSize++;
        if ( nCutSizeMax < nCutSize )
            nCutSizeMax = nCutSize;
        for ( iVar = 0; iVar < p->nRows; iVar++ )
            if ( pGrp2[iVar] == iGrp )
                nCutSize--;
    }
    ABC_FREE( pGrp1 );
    ABC_FREE( pGrp2 );
    printf( "[%4d x %4d]  Life-span =%6.2f  Max-cut =%5d\n", 
        p->nCols, p->nRows, 1.0*Span/p->nRows, nCutSizeMax );
    if ( nCutSize )
        Abc_Print( -1, "Cut size is not zero (%d).\n", nCutSize );
}

void Llb_MtrSchedule

(

Llb_Mtr_t *

p

)

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

Synopsis [Matrix reduce.]

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file llb1Sched.c.

{
    int iGrp, iGrpBest, i;
    // start partial product
    for ( i = 0; i < p->nRows; i++ )
    {
        if ( i >= p->nPis && i < p->nPis + p->nFfs )
        {
            p->pProdVars[i] = 1;
            p->pProdNums[i] = p->pRowSums[i] - 1;
        }
        else 
        {
            p->pProdVars[i] = 0;
            p->pProdNums[i] = p->pRowSums[i];
        }
    }
    // order the partitions
    Llb_MtrVerifyMatrix( p );
    for ( iGrp = 1; iGrp < p->nCols-1; iGrp++ )
    {
        Llb_MtrVerifyColumns( p, iGrp );
        iGrpBest = Llb_MtrFindBestColumn( p, iGrp );
        Llb_MtrUseSelectedColumn( p, iGrpBest );
        Llb_MtrSwapColumns( p, iGrp, iGrpBest );
    }
    Llb_MtrVerifyMatrix( p );
}

void Llb_MtrVerifyMatrix

(

Llb_Mtr_t *

p

)

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

Synopsis [Verify columns.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file llb1Matrix.c.

{
    Llb_MtrVerifyRowsAll( p );
    Llb_MtrVerifyColumnsAll( p );
}

Vec_Ptr_t* Llb_Nonlin4Group	(	DdManager *	dd,
		Vec_Ptr_t *	vParts,
		Vec_Int_t *	vVars2Q,
		int	nSizeMax
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 806 of file llb4Image.c.

{
    Vec_Ptr_t * vGroups;
    Llb_Prt_t * pPart, * pPart1, * pPart2;
    Llb_Mgr_t * p;
    int i, nReorders;//, clk = Abc_Clock();
    // start the manager
    p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
    // remove singles
    Llb_MgrForEachPart( p, pPart, i )
        if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
            Llb_Nonlin4Quantify1( p, pPart );
    // compute scores
    Llb_Nonlin4RecomputeScores( p );
    // iteratively quantify variables
    while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
    {
        nReorders = Cudd_ReadReorderings(dd);
        if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
        {
            Llb_Nonlin4Free( p );
            return NULL;
        }
        if ( nReorders < Cudd_ReadReorderings(dd) )
            Llb_Nonlin4RecomputeScores( p );
//        else
//            Llb_Nonlin4VerifyScores( p );
    }
    // load partitions
    vGroups = Vec_PtrAlloc( 1000 );
    Llb_MgrForEachPart( p, pPart, i )
    {
//printf( "Iteration %d ", pPart->iPart );
        if ( Cudd_IsConstant(pPart->bFunc) )
        {
//printf( "Constant\n" );
            assert( !Cudd_IsComplement(pPart->bFunc) );
            continue;
        }
//printf( "\n" );
        Vec_PtrPush( vGroups, pPart->bFunc );
        Cudd_Ref( pPart->bFunc );
//printf( "Part %d  ", pPart->iPart );
//Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
    }
    Llb_Nonlin4Free( p );
//Abc_PrintTime( 1, "Reparametrization time", Abc_Clock() - clk );
    return vGroups;
}

DdNode* Llb_Nonlin4Image	(	DdManager *	dd,
		Vec_Ptr_t *	vParts,
		DdNode *	bCurrent,
		Vec_Int_t *	vVars2Q
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 752 of file llb4Image.c.

{
    Llb_Prt_t * pPart, * pPart1, * pPart2;
    Llb_Mgr_t * p;
    DdNode * bFunc, * bTemp;
    int i, nReorders;
    // start the manager
    p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q, 0 );
    // remove singles
    Llb_MgrForEachPart( p, pPart, i )
        if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
            Llb_Nonlin4Quantify1( p, pPart );
    // compute scores
    Llb_Nonlin4RecomputeScores( p );
    // iteratively quantify variables
    while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
    {
        nReorders = Cudd_ReadReorderings(dd);
        if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
        {
            Llb_Nonlin4Free( p );
            return NULL;
        }
        if ( nReorders < Cudd_ReadReorderings(dd) )
            Llb_Nonlin4RecomputeScores( p );
//        else
//            Llb_Nonlin4VerifyScores( p );
    }
    // load partitions
    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_Nonlin4Free( p );
//printf( "\n" );
    // return
    Cudd_Deref( bFunc );
    return bFunc;
}

DdNode* Llb_NonlinComputeInitState	(	Aig_Man_t *	pAig,
		DdManager *	dd
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file llb3Nonlin.c.

{
    Aig_Obj_t * pObj;
    DdNode * bRes, * bVar, * bTemp;
    int i, iVar;
    abctime TimeStop;
    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
    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 );
    dd->TimeStop = TimeStop;
    return bRes;
}

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

static int Llb_ObjBddVar ( Vec_Int_t *  vOrder, Aig_Obj_t *  pObj  )

inlinestatic

MACRO DEFINITIONS ///.

Definition at line 109 of file llbInt.h.

{ return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }