resInt.h File Reference

#include "res.h"

Go to the source code of this file.

Data Structures
struct	Res_Win_t_
struct	Res_Sim_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Res_Win_t_	Res_Win_t
	INCLUDES ///. More...
typedef struct Res_Sim_t_	Res_Sim_t

Functions
void	Res_WinDivisors (Res_Win_t *p, int nLevDivMax)
	MACRO DEFINITIONS ///. More...
void	Res_WinSweepLeafTfo_rec (Abc_Obj_t *pObj, int nLevelLimit)
int	Res_WinVisitMffc (Abc_Obj_t *pNode)
int	Res_FilterCandidates (Res_Win_t *pWin, Abc_Ntk_t *pAig, Res_Sim_t *pSim, Vec_Vec_t *vResubs, Vec_Vec_t *vResubsW, int nFaninsMax, int fArea)
	FUNCTION DEFINITIONS ///. More...
int	Res_FilterCandidatesArea (Res_Win_t *pWin, Abc_Ntk_t *pAig, Res_Sim_t *pSim, Vec_Vec_t *vResubs, Vec_Vec_t *vResubsW, int nFaninsMax)
void *	Res_SatProveUnsat (Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
	FUNCTION DEFINITIONS ///. More...
int	Res_SatSimulate (Res_Sim_t *p, int nPats, int fOnSet)
Res_Sim_t *	Res_SimAlloc (int nWords)
	DECLARATIONS ///. More...
void	Res_SimFree (Res_Sim_t *p)
int	Res_SimPrepare (Res_Sim_t *p, Abc_Ntk_t *pAig, int nTruePis, int fVerbose)
Abc_Ntk_t *	Res_WndStrash (Res_Win_t *p)
	FUNCTION DEFINITIONS ///. More...
void	Res_UpdateNetwork (Abc_Obj_t *pObj, Vec_Ptr_t *vFanins, Hop_Obj_t *pFunc, Vec_Vec_t *vLevels)
Res_Win_t *	Res_WinAlloc ()
	DECLARATIONS ///. More...
void	Res_WinFree (Res_Win_t *p)
int	Res_WinIsTrivial (Res_Win_t *p)
int	Res_WinCompute (Abc_Obj_t *pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t *p)

Typedef Documentation

typedef struct Res_Sim_t_ Res_Sim_t

Definition at line 69 of file resInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Res_Win_t_ Res_Win_t

INCLUDES ///.

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

FileName [resInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:

resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 44 of file resInt.h.

Function Documentation

int Res_FilterCandidates	(	Res_Win_t *	pWin,
		Abc_Ntk_t *	pAig,
		Res_Sim_t *	pSim,
		Vec_Vec_t *	vResubs,
		Vec_Vec_t *	vResubsW,
		int	nFaninsMax,
		int	fArea
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Finds sets of feasible candidates.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file resFilter.c.

{
    Abc_Obj_t * pFanin, * pFanin2, * pFaninTemp;
    unsigned * pInfo, * pInfoDiv, * pInfoDiv2;
    int Counter, RetValue, i, i2, d, d2, iDiv, iDiv2, k;

    // check that the info the node is one
    pInfo = (unsigned *)Vec_PtrEntry( pSim->vOuts, 1 );
    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
    if ( RetValue == 0 )
    {
//        printf( "Failed 1!\n" );
        return 0;
    }

    // collect the fanin info
    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
    if ( RetValue == 0 )
    {
//        printf( "Failed 2!\n" );
        return 0;
    }

    // try removing each fanin
//    printf( "Fanins: " );
    Counter = 0;
    Vec_VecClear( vResubs );
    Vec_VecClear( vResubsW );
    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
    {
        if ( fArea && Abc_ObjFanoutNum(pFanin) > 1 )
            continue;
        // get simulation info without this fanin
        pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
        RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
        if ( RetValue )
        {
//            printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id );
            // collect the nodes
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
            Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
            {
                if ( k != i )
                {
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                    Vec_VecPush( vResubsW, Counter, pFaninTemp );
                }
            }
            Counter++;
            if ( Counter == Vec_VecSize(vResubs) )
                return Counter;    
        }
    }

    // try replacing each critical fanin by a non-critical fanin
    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
    {
        if ( Abc_ObjFanoutNum(pFanin) > 1 )
            continue;
        // get simulation info without this fanin
        pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
        // go over the set of divisors
        for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
        {
            pInfoDiv = (unsigned *)Vec_PtrEntry( pSim->vOuts, d );
            iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
            if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
                continue;
            // collect the nodes
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
            // collect the remaning fanins and the divisor
            Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
            {
                if ( k != i )
                {
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                    Vec_VecPush( vResubsW, Counter, pFaninTemp );
                }
            }
            // collect the divisor
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
            Counter++;
            if ( Counter == Vec_VecSize(vResubs) )
                return Counter;           
        }
    }

    // consider the case when two fanins can be added instead of one
    if ( Abc_ObjFaninNum(pWin->pNode) < nFaninsMax )
    {
        // try to replace each critical fanin by two non-critical fanins
        Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
        {
            if ( Abc_ObjFanoutNum(pFanin) > 1 )
                continue;
            // get simulation info without this fanin
            pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
            // go over the set of divisors
            for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
            {
                pInfoDiv = (unsigned *)Vec_PtrEntry( pSim->vOuts, d );
                iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
                // go through the second divisor
                for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ )
                {
                    pInfoDiv2 = (unsigned *)Vec_PtrEntry( pSim->vOuts, d2 );
                    iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2);
                    if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) )
                        continue;
                    // collect the nodes
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
                    // collect the remaning fanins and the divisor
                    Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
                    {
                        if ( k != i )
                        {
                            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                            Vec_VecPush( vResubsW, Counter, pFaninTemp );
                        }
                    }
                    // collect the divisor
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) );
                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) );
                    Counter++;
                    if ( Counter == Vec_VecSize(vResubs) )
                        return Counter;           
                }
            }
        }
    }

    // try to replace two nets by one
    if ( !fArea )
    {
        Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
        {
            for ( i2 = i + 1; i2 < Abc_ObjFaninNum(pWin->pNode); i2++ )
            {
                pFanin2 = Abc_ObjFanin(pWin->pNode, i2);
                // get simulation info without these fanins
                pInfo = Res_FilterCollectFaninInfo( pWin, pSim, (~(1 << i)) & (~(1 << i2)) );
                // go over the set of divisors
                for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
                {
                    pInfoDiv = (unsigned *)Vec_PtrEntry( pSim->vOuts, d );
                    iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
                    if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
                        continue;
                    // collect the nodes
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
                    // collect the remaning fanins and the divisor
                    Abc_ObjForEachFanin( pWin->pNode, pFaninTemp, k )
                    {
                        if ( k != i && k != i2 )
                        {
                            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                            Vec_VecPush( vResubsW, Counter, pFaninTemp );
                        }
                    }
                    // collect the divisor
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
                    Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
                    Counter++;
                    if ( Counter == Vec_VecSize(vResubs) )
                        return Counter;           
                }
            }
        }
    }
    return Counter;
}

int Res_FilterCandidatesArea	(	Res_Win_t *	pWin,
		Abc_Ntk_t *	pAig,
		Res_Sim_t *	pSim,
		Vec_Vec_t *	vResubs,
		Vec_Vec_t *	vResubsW,
		int	nFaninsMax
	)

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

Synopsis [Finds sets of feasible candidates.]

Description [This procedure is a special case of the above.]

SideEffects []

SeeAlso []

Definition at line 241 of file resFilter.c.

{
    Abc_Obj_t * pFanin;
    unsigned * pInfo, * pInfoDiv, * pInfoDiv2;
    int Counter, RetValue, d, d2, k, iDiv, iDiv2, iBest;

    // check that the info the node is one
    pInfo = (unsigned *)Vec_PtrEntry( pSim->vOuts, 1 );
    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
    if ( RetValue == 0 )
    {
//        printf( "Failed 1!\n" );
        return 0;
    }

    // collect the fanin info
    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
    if ( RetValue == 0 )
    {
//        printf( "Failed 2!\n" );
        return 0;
    }

    // try removing fanins
//    printf( "Fanins: " );
    Counter = 0;
    Vec_VecClear( vResubs );
    Vec_VecClear( vResubsW );
    // get the best fanins
    iBest = Res_FilterCriticalFanin( pWin->pNode );
    if ( iBest == -1 )
        return 0;

    // get the info without the critical fanin
    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) );
    RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
    if ( RetValue )
    {
//        printf( "Can be done without one!\n" );
        // collect the nodes
        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
        Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
        {
            if ( k != iBest )
            {
                Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                Vec_VecPush( vResubsW, Counter, pFanin );
            }
        }
        Counter++;
//        printf( "*" );
        return Counter;
    }

    // go through the divisors
    for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
    {
        pInfoDiv = (unsigned *)Vec_PtrEntry( pSim->vOuts, d );
        iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
        if ( !Abc_InfoIsOrOne( pInfo, pInfoDiv, pSim->nWordsOut ) )
            continue;
//if ( Abc_ObjLevel(pWin->pNode) <= Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) )
//    printf( "Node level = %d. Divisor level = %d.\n", Abc_ObjLevel(pWin->pNode), Abc_ObjLevel( Vec_PtrEntry(pWin->vDivs, iDiv) ) );
        // collect the nodes
        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
        // collect the remaning fanins and the divisor
        Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
        {
            if ( k != iBest )
            {
                Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                Vec_VecPush( vResubsW, Counter, pFanin );
            }
        }
        // collect the divisor
        Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
        Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
        Counter++;

        if ( Counter == Vec_VecSize(vResubs) )
            break;            
    }

    if ( Counter > 0 || Abc_ObjFaninNum(pWin->pNode) >= nFaninsMax )
        return Counter;

    // try to find the node pairs
    for ( d = Abc_ObjFaninNum(pWin->pNode) + 2; d < Abc_NtkPoNum(pAig); d++ )
    {
        pInfoDiv = (unsigned *)Vec_PtrEntry( pSim->vOuts, d );
        iDiv = d - (Abc_ObjFaninNum(pWin->pNode) + 2);
        // go through the second divisor
        for ( d2 = d + 1; d2 < Abc_NtkPoNum(pAig); d2++ )
        {
            pInfoDiv2 = (unsigned *)Vec_PtrEntry( pSim->vOuts, d2 );
            iDiv2 = d2 - (Abc_ObjFaninNum(pWin->pNode) + 2);

            if ( !Abc_InfoIsOrOne3( pInfo, pInfoDiv, pInfoDiv2, pSim->nWordsOut ) )
                continue;
            // collect the nodes
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
            // collect the remaning fanins and the divisor
            Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
            {
                if ( k != iBest )
                {
                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
                    Vec_VecPush( vResubsW, Counter, pFanin );
                }
            }
            // collect the divisor
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d) );
            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,d2) );
            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv) );
            Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, iDiv2) );
            Counter++;

            if ( Counter == Vec_VecSize(vResubs) )
                break;            
        }
        if ( Counter == Vec_VecSize(vResubs) )
            break;            
    }
    return Counter;
}

void* Res_SatProveUnsat	(	Abc_Ntk_t *	pAig,
		Vec_Ptr_t *	vFanins
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Loads AIG into the SAT solver for checking resubstitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file resSat.c.

{
    void * pCnf = NULL;
    sat_solver * pSat;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pObj;
    int i, nNodes, status;

    // make sure fanins contain POs of the AIG
    pObj = (Abc_Obj_t *)Vec_PtrEntry( vFanins, 0 );
    assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );

    // collect reachable nodes
    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );

    // assign unique numbers to each node
    nNodes = 0;
    Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Abc_NtkForEachPi( pAig, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;

    // start the solver
    pSat = sat_solver_new();
    sat_solver_store_alloc( pSat );

    // add clause for the constant node
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
    // add clauses for AND gates
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
    Vec_PtrFree( vNodes );
    // add clauses for POs
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
    // add trivial clauses
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 0);
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set

    // bookmark the clauses of A
    sat_solver_store_mark_clauses_a( pSat );

    // duplicate the clauses
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
    Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
    // add the equality constraints
    Vec_PtrForEachEntryStart( Abc_Obj_t *, vFanins, pObj, i, 2 )
        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );

    // bookmark the roots
    sat_solver_store_mark_roots( pSat );

    // solve the problem
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status == l_False )
    {
        pCnf = sat_solver_store_release( pSat );
//        printf( "unsat\n" );
    }
    else if ( status == l_True )
    {
//        printf( "sat\n" );
    }
    else
    {
//        printf( "undef\n" );
    }
    sat_solver_delete( pSat );
    return pCnf;
}

int Res_SatSimulate	(	Res_Sim_t *	p,
		int	nPatsLimit,
		int	fOnSet
	)

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

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description [Returns 1 if the required number of patterns are found. Returns 0 if the solver ran out of time or proved a constant. In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]

SideEffects []

SeeAlso []

Definition at line 212 of file resSat.c.

{
    Vec_Int_t * vLits;
    Vec_Ptr_t * vPats;
    sat_solver * pSat;
    int RetValue = -1; // Suppress "might be used uninitialized"
    int i, k, value, status, Lit, Var, iPat;
    abctime clk = Abc_Clock();

//printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );

    // decide what problem should be solved
    Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
    if ( fOnSet )
    {
        iPat = p->nPats1;
        vPats = p->vPats1;
    }
    else
    {
        iPat = p->nPats0;
        vPats = p->vPats0;
    }
    assert( iPat < nPatsLimit );

    // derive the SAT solver
    pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet );
    pSat->fSkipSimplify = 1;
    status = sat_solver_simplify( pSat );
    if ( status == 0 )
    {
        if ( iPat == 0 )
        {
//            if ( fOnSet )
//                p->fConst0 = 1;
//            else
//                p->fConst1 = 1;
            RetValue = 0;
        }
        goto finish;
    }
 
    // enumerate through the SAT assignments
    RetValue = 1;
    vLits = Vec_IntAlloc( 32 );
    for ( k = iPat; k < nPatsLimit; k++ )
    {
        // solve with the assumption
//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_False )
        {
//printf( "Const %d\n", !fOnSet );
            if ( k == 0 )
            {
                if ( fOnSet )
                    p->fConst0 = 1;
                else
                    p->fConst1 = 1;
                RetValue = 0;
            }
            break;
        }
        else if ( status == l_True )
        {
            // save the pattern
            Vec_IntClear( vLits );
            for ( i = 0; i < p->nTruePis; i++ )
            {
                Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
//                value = (int)(pSat->model.ptr[Var] == l_True);
                value = sat_solver_var_value(pSat, Var);
                if ( value )
                    Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
                Lit = toLitCond( Var, value );
                Vec_IntPush( vLits, Lit );
//                printf( "%d", value );
            }
//            printf( "\n" );

            status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
            if ( status == 0 )
            {
                k++;
                RetValue = 1; 
                break;
            }
        }
        else
        {
//printf( "Undecided\n" );
            if ( k == 0 )
                RetValue = 0;
            else
                RetValue = 1; 
            break;
        }
    }
    Vec_IntFree( vLits );
//printf( "Found %d patterns\n", k - iPat );

    // set the new number of patterns
    if ( fOnSet )
        p->nPats1 = k;
    else
        p->nPats0 = k;

finish:

    sat_solver_delete( pSat );
p->timeSat += Abc_Clock() - clk;
    return RetValue;
}

Res_Sim_t* Res_SimAlloc

(

int

nWords

)

DECLARATIONS ///.

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

FileName [resSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Simulation engine.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:

resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

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

Synopsis [Allocate simulation engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file resSim.c.

{
    Res_Sim_t * p;
    p = ABC_ALLOC( Res_Sim_t, 1 );
    memset( p, 0, sizeof(Res_Sim_t) );
    // simulation parameters
    p->nWords    = nWords;
    p->nPats     = p->nWords * 8 * sizeof(unsigned);
    p->nWordsIn  = p->nPats;
    p->nBytesIn  = p->nPats * sizeof(unsigned);
    p->nPatsIn   = p->nPats * 8 * sizeof(unsigned);
    p->nWordsOut = p->nPats * p->nWords;
    p->nPatsOut  = p->nPats * p->nPats;
    // simulation info
    p->vPats     = Vec_PtrAllocSimInfo( 1024, p->nWordsIn );
    p->vPats0    = Vec_PtrAllocSimInfo( 128, p->nWords );
    p->vPats1    = Vec_PtrAllocSimInfo( 128, p->nWords );
    p->vOuts     = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
    // resub candidates
    p->vCands    = Vec_VecStart( 16 );
    return p;
}

void Res_SimFree

(

Res_Sim_t *

p

)

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

Synopsis [Free simulation engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file resSim.c.

{
    Vec_PtrFree( p->vPats );
    Vec_PtrFree( p->vPats0 );
    Vec_PtrFree( p->vPats1 );
    Vec_PtrFree( p->vOuts );
    Vec_VecFree( p->vCands );
    ABC_FREE( p );
}

int Res_SimPrepare	(	Res_Sim_t *	p,
		Abc_Ntk_t *	pAig,
		int	nTruePis,
		int	fVerbose
	)

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

Synopsis [Prepares simulation info for candidate filtering.]

Description []

SideEffects []

SeeAlso []

Definition at line 731 of file resSim.c.

{
    int i, nOnes = 0, nZeros = 0, nDcs = 0;
    if ( fVerbose )
        printf( "\n" );
    // prepare the manager
    Res_SimAdjust( p, pAig, nTruePis );
    // estimate the number of patterns
    Res_SimSetRandomBytes( p );
    Res_SimPerformRound( p, p->nWordsIn );
    Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
    // collect the patterns
    Res_SimCollectPatterns( p, fVerbose );
    // add more patterns using constraint simulation
    if ( p->nPats0 < 8 )
    {
        if ( !Res_SatSimulate( p, 16, 0 ) )
            return p->fConst0 || p->fConst1;
//            return 0;
//        printf( "Value0 = %d\n", Res_SimVerifyValue( p, 0 ) );
    }
    if ( p->nPats1 < 8 )
    {
        if ( !Res_SatSimulate( p, 16, 1 ) )
            return p->fConst0 || p->fConst1;
//            return 0;
//        printf( "Value1 = %d\n", Res_SimVerifyValue( p, 1 ) );
    }
    // generate additional patterns
    for ( i = 0; i < 2; i++ )
    {
        if ( p->nPats0 > p->nPats*7/8 && p->nPats1 > p->nPats*7/8 )
            break;
        Res_SimSetDerivedBytes( p, i==0 );
        Res_SimPerformRound( p, p->nWordsIn );
        Res_SimCountResults( p, &nDcs, &nOnes, &nZeros, fVerbose );
        Res_SimCollectPatterns( p, fVerbose );
    }
    // create bit-matrix info
    if ( p->nPats0 < p->nPats )
        Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
    if ( p->nPats1 < p->nPats )
        Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
    // resimulate 0-patterns
    Res_SimSetGiven( p, p->vPats0 );
    Res_SimPerformRound( p, p->nWords );
//Res_SimPrintNodePatterns( p, pAig );
    Res_SimDeriveInfoReplicate( p );
    // resimulate 1-patterns
    Res_SimSetGiven( p, p->vPats1 );
    Res_SimPerformRound( p, p->nWords );
//Res_SimPrintNodePatterns( p, pAig );
    Res_SimDeriveInfoComplement( p );
    // print output patterns
//    Res_SimPrintOutPatterns( p, pAig );
    return 1;
}

void Res_UpdateNetwork	(	Abc_Obj_t *	pObj,
		Vec_Ptr_t *	vFanins,
		Hop_Obj_t *	pFunc,
		Vec_Vec_t *	vLevels
	)

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

Synopsis [Incrementally updates level of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file resCore.c.

{
    Abc_Obj_t * pObjNew, * pFanin;
    int k;

    // create the new node
    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
    pObjNew->pData = pFunc;
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k )
        Abc_ObjAddFanin( pObjNew, pFanin );
    // replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
    // update the level of the node
    Abc_NtkUpdate( pObj, pObjNew, vLevels );
}

Res_Win_t* Res_WinAlloc

(

)

DECLARATIONS ///.

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

FileName [resWin.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Windowing algorithm.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:

resWin.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

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

Synopsis [Allocates the window.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file resWin.c.

{
    Res_Win_t * p;
    // start the manager
    p = ABC_ALLOC( Res_Win_t, 1 );
    memset( p, 0, sizeof(Res_Win_t) );
    // set internal parameters
    p->nFanoutLimit = 10;
    p->nLevTfiMinus =  3;
    // allocate storage
    p->vRoots    = Vec_PtrAlloc( 256 );
    p->vLeaves   = Vec_PtrAlloc( 256 );
    p->vBranches = Vec_PtrAlloc( 256 );
    p->vNodes    = Vec_PtrAlloc( 256 );
    p->vDivs     = Vec_PtrAlloc( 256 );
    p->vMatrix   = Vec_VecStart( 128 );
    return p;
}

int Res_WinCompute	(	Abc_Obj_t *	pNode,
		int	nWinTfiMax,
		int	nWinTfoMax,
		Res_Win_t *	p
	)

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

Synopsis [Computes the window.]

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file resWin.c.

{
    assert( Abc_ObjIsNode(pNode) );
    assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
    assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );

    // initialize the window
    p->pNode      = pNode;
    p->nWinTfiMax = nWinTfiMax;
    p->nWinTfoMax = nWinTfoMax;

    Vec_PtrClear( p->vBranches );
    Vec_PtrClear( p->vDivs );
    Vec_PtrClear( p->vRoots );
    Vec_PtrPush( p->vRoots, pNode );

    // compute the leaves
    if ( !Res_WinCollectLeavesAndNodes( p ) )
        return 0;

    // compute the candidate roots
    if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
    {
        // mark the paths from the roots to the leaves
        Res_WinMarkPaths( p );
        // refine the roots and add branches and missing nodes
        if ( Res_WinFinalizeRoots( p ) )
            Res_WinAddMissing( p );
    }

    return 1;
}

void Res_WinDivisors	(	Res_Win_t *	p,
		int	nLevDivMax
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

Synopsis [Adds candidate divisors of the node to its window.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file resDivs.c.

{
    Abc_Obj_t * pObj, * pFanout, * pFanin;
    int k, f, m;

    // set the maximum level of the divisors
    p->nLevDivMax = nLevDivMax;

    // mark the TFI with the current trav ID
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Res_WinMarkTfi( p );

    // mark with the current trav ID those nodes that should not be divisors:
    // (1) the node and its TFO
    // (2) the MFFC of the node
    // (3) the node's fanins (these are treated as a special case)
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
    Res_WinVisitMffc( p->pNode );
    Abc_ObjForEachFanin( p->pNode, pObj, k )
        Abc_NodeSetTravIdCurrent( pObj );

    // at this point the nodes are marked with two trav IDs:
    // nodes to be collected as divisors are marked with previous trav ID
    // nodes to be avoided as divisors are marked with current trav ID

    // start collecting the divisors
    Vec_PtrClear( p->vDivs );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, k )
    {
        assert( (int)pObj->Level >= p->nLevLeafMin ); 
        if ( !Abc_NodeIsTravIdPrevious(pObj) )
            continue;
        if ( (int)pObj->Level > p->nLevDivMax )
            continue;
        Vec_PtrPush( p->vDivs, pObj );
    }
    // add the internal nodes to the data structure
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, k )
    {
        if ( !Abc_NodeIsTravIdPrevious(pObj) )
            continue;
        if ( (int)pObj->Level > p->nLevDivMax )
            continue;
        Vec_PtrPush( p->vDivs, pObj );
    }

    // explore the fanouts of already collected divisors
    p->nDivsPlus = 0;
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pObj, k )
    {
        // consider fanouts of this node
        Abc_ObjForEachFanout( pObj, pFanout, f )
        {
            // stop if there are too many fanouts
            if ( f > 20 )
                break;
            // skip nodes that are already added
            if ( Abc_NodeIsTravIdPrevious(pFanout) )
                continue;
            // skip nodes in the TFO or in the MFFC of node
            if ( Abc_NodeIsTravIdCurrent(pFanout) )
                continue;
            // skip COs
            if ( !Abc_ObjIsNode(pFanout) ) 
                continue;
            // skip nodes with large level
            if ( (int)pFanout->Level > p->nLevDivMax )
                continue;
            // skip nodes whose fanins are not divisors
            Abc_ObjForEachFanin( pFanout, pFanin, m )
                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
                    break;
            if ( m < Abc_ObjFaninNum(pFanout) )
                continue;
            // add the node to the divisors
            Vec_PtrPush( p->vDivs, pFanout );
            Vec_PtrPush( p->vNodes, pFanout );
            Abc_NodeSetTravIdPrevious( pFanout );
            p->nDivsPlus++;
        }
    }
/*
    printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
    Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs, pObj, k, Vec_PtrSize(p->vDivs)-p->nDivsPlus )
        printf( "%d ", Abc_ObjLevel(pObj) );
    printf( "\n" );
*/
//printf( "%d ", p->nDivsPlus );
}

void Res_WinFree

(

Res_Win_t *

p

)

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

Synopsis [Frees the window.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file resWin.c.

{
    Vec_PtrFree( p->vRoots  );
    Vec_PtrFree( p->vLeaves );
    Vec_PtrFree( p->vBranches );
    Vec_PtrFree( p->vNodes  );
    Vec_PtrFree( p->vDivs   );
    Vec_VecFree( p->vMatrix );
    ABC_FREE( p );
}

int Res_WinIsTrivial

(

Res_Win_t *

p

)

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

Synopsis [Returns 1 if the window is trivial (without TFO).]

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file resWin.c.

{
    return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
}

void Res_WinSweepLeafTfo_rec	(	Abc_Obj_t *	pObj,
		int	nLevelLimit
	)

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

Synopsis [Marks the TFO of the collected nodes up to the given level.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file resDivs.c.

{
    Abc_Obj_t * pFanout;
    int i;
    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
        return;
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return;
    Abc_NodeSetTravIdCurrent( pObj );
    Abc_ObjForEachFanout( pObj, pFanout, i )
        Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit );
}

int Res_WinVisitMffc

(

Abc_Obj_t *

pNode

)

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

Synopsis [Labels MFFC of the node with the current trav ID.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file resDivs.c.

{
    int Count1, Count2;
    assert( Abc_ObjIsNode(pNode) );
    // dereference the node (mark with the current trav ID)
    Count1 = Res_NodeDeref_rec( pNode );
    // reference it back
    Count2 = Res_NodeRef_rec( pNode );
    assert( Count1 == Count2 );
    return Count1;
}

Abc_Ntk_t* Res_WndStrash

(

Res_Win_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Structurally hashes the given window.]

Description [The first PO is the observability condition. The second is the node's function. The remaining POs are the candidate divisors.]

SideEffects []

SeeAlso []

Definition at line 49 of file resStrash.c.

{
    Vec_Ptr_t * vPairs;
    Abc_Ntk_t * pAig;
    Abc_Obj_t * pObj, * pMiter;
    int i;
    assert( Abc_NtkHasAig(p->pNode->pNtk) );
//    Abc_NtkCleanCopy( p->pNode->pNtk );
    // create the network
    pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pAig->pName = Extra_UtilStrsav( "window" );
    // create the inputs
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
        pObj->pCopy = Abc_NtkCreatePi( pAig );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vBranches, pObj, i )
        pObj->pCopy = Abc_NtkCreatePi( pAig );
    // go through the nodes in the topological order
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
    {
        pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
        if ( pObj == p->pNode )
            pObj->pCopy = Abc_ObjNot( pObj->pCopy );
    }
    // collect the POs
    vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
    {
        Vec_PtrPush( vPairs, pObj->pCopy );
        Vec_PtrPush( vPairs, NULL );
    }
    // mark the TFO of the node
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax );
    // update strashing of the node
    p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
    Abc_NodeSetTravIdPrevious( p->pNode );
    // redo strashing in the TFO
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
    {
        if ( Abc_NodeIsTravIdCurrent(pObj) )
            pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
    }
    // collect the POs
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
    // add the miter
    pMiter = Abc_AigMiter( (Abc_Aig_t *)pAig->pManFunc, vPairs, 0 );
    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter );
    Vec_PtrFree( vPairs );
    // add the node
    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
    // add the fanins
    Abc_ObjForEachFanin( p->pNode, pObj, i )
        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
    // add the divisors
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pObj, i )
        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
    // add the names
    Abc_NtkAddDummyPiNames( pAig );
    Abc_NtkAddDummyPoNames( pAig );
    // check the resulting network
    if ( !Abc_NtkCheck( pAig ) )
        fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" );
    return pAig;
}