cecInt.h File Reference

#include "sat/bsat/satSolver.h"
#include "misc/bar/bar.h"
#include "aig/gia/gia.h"
#include "cec.h"

Go to the source code of this file.

Data Structures
struct	Cec_ManPat_t_
struct	Cec_ManSat_t_
struct	Cec_ManSim_t_
struct	Cec_ManFra_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Cec_ManPat_t_	Cec_ManPat_t
	INCLUDES ///. More...
typedef struct Cec_ManSat_t_	Cec_ManSat_t
typedef struct Cec_ManSim_t_	Cec_ManSim_t
typedef struct Cec_ManFra_t_	Cec_ManFra_t

Functions
void	Cec_ManRefinedClassPrintStats (Gia_Man_t *p, Vec_Str_t *vStatus, int iIter, abctime Time)
	MACRO DEFINITIONS ///. More...
int	Cec_ManSimClassRemoveOne (Cec_ManSim_t *p, int i)
int	Cec_ManSimClassesPrepare (Cec_ManSim_t *p, int LevelMax)
int	Cec_ManSimClassesRefine (Cec_ManSim_t *p)
int	Cec_ManSimSimulateRound (Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
int *	Cec_ManDetectIsomorphism (Gia_Man_t *p)
Cec_ManSat_t *	Cec_ManSatCreate (Gia_Man_t *pAig, Cec_ParSat_t *pPars)
	DECLARATIONS ///. More...
void	Cec_ManSatPrintStats (Cec_ManSat_t *p)
void	Cec_ManSatStop (Cec_ManSat_t *p)
Cec_ManPat_t *	Cec_ManPatStart ()
void	Cec_ManPatPrintStats (Cec_ManPat_t *p)
void	Cec_ManPatStop (Cec_ManPat_t *p)
Cec_ManSim_t *	Cec_ManSimStart (Gia_Man_t *pAig, Cec_ParSim_t *pPars)
void	Cec_ManSimStop (Cec_ManSim_t *p)
Cec_ManFra_t *	Cec_ManFraStart (Gia_Man_t *pAig, Cec_ParFra_t *pPars)
void	Cec_ManFraStop (Cec_ManFra_t *p)
void	Cec_ManPatSavePattern (Cec_ManPat_t *pPat, Cec_ManSat_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatSavePatternCSat (Cec_ManPat_t *pMan, Vec_Int_t *vPat)
Vec_Ptr_t *	Cec_ManPatCollectPatterns (Cec_ManPat_t *pMan, int nInputs, int nWords)
Vec_Ptr_t *	Cec_ManPatPackPatterns (Vec_Int_t *vCexStore, int nInputs, int nRegs, int nWordsInit)
int	Cec_ManSeqResimulate (Cec_ManSim_t *p, Vec_Ptr_t *vInfo)
int	Cec_ManSeqResimulateInfo (Gia_Man_t *pAig, Vec_Ptr_t *vSimInfo, Abc_Cex_t *pBestState, int fCheckMiter)
void	Cec_ManSeqDeriveInfoInitRandom (Vec_Ptr_t *vInfo, Gia_Man_t *pAig, Abc_Cex_t *pCex)
int	Cec_ManCountNonConstOutputs (Gia_Man_t *pAig)
int	Cec_ManCheckNonTrivialCands (Gia_Man_t *pAig)
int	Cec_ObjSatVarValue (Cec_ManSat_t *p, Gia_Obj_t *pObj)
	FUNCTION DEFINITIONS ///. More...
void	Cec_ManSatSolve (Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
void	Cec_ManSatSolveCSat (Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Vec_Str_t *	Cec_ManSatSolveSeq (Vec_Ptr_t *vPatts, Gia_Man_t *pAig, Cec_ParSat_t *pPars, int nRegs, int *pnPats)
Vec_Int_t *	Cec_ManSatSolveMiter (Gia_Man_t *pAig, Cec_ParSat_t *pPars, Vec_Str_t **pvStatus)
int	Cec_ManSatCheckNode (Cec_ManSat_t *p, Gia_Obj_t *pObj)
int	Cec_ManSatCheckNodeTwo (Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
void	Cec_ManSavePattern (Cec_ManSat_t *p, Gia_Obj_t *pObj1, Gia_Obj_t *pObj2)
Vec_Int_t *	Cec_ManSatReadCex (Cec_ManSat_t *p)
Gia_Man_t *	Cec_ManFraSpecReduction (Cec_ManFra_t *p)
	DECLARATIONS ///. More...
int	Cec_ManFraClassesUpdate (Cec_ManFra_t *p, Cec_ManSim_t *pSim, Cec_ManPat_t *pPat, Gia_Man_t *pNew)

Typedef Documentation

typedef struct Cec_ManFra_t_ Cec_ManFra_t

Definition at line 145 of file cecInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Cec_ManPat_t_ Cec_ManPat_t

INCLUDES ///.

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

FileName [cecInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 48 of file cecInt.h.

typedef struct Cec_ManSat_t_ Cec_ManSat_t

Definition at line 74 of file cecInt.h.

typedef struct Cec_ManSim_t_ Cec_ManSim_t

Definition at line 111 of file cecInt.h.

Function Documentation

int Cec_ManCheckNonTrivialCands

(

Gia_Man_t *

pAig

)

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

Synopsis [Returns the number of POs that are not const0 cands.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file cecSeq.c.

{
    Gia_Obj_t * pObj;
    int i, RetValue = 0;
    if ( pAig->pReprs == NULL )
        return 0;
    // label internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 1;
    // check if there are non-labled equivs
    Gia_ManForEachObj( pAig, pObj, i )
        if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
        {
            RetValue = 1;
            break;
        }
    // clean internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 0;
    return RetValue;
}

int Cec_ManCountNonConstOutputs

(

Gia_Man_t *

pAig

)

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

Synopsis [Returns the number of POs that are not const0 cands.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file cecSeq.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    if ( pAig->pReprs == NULL )
        return -1;
    Gia_ManForEachPo( pAig, pObj, i )
        if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
            Counter++;
    return Counter;
}

int* Cec_ManDetectIsomorphism

(

Gia_Man_t *

p

)

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

Synopsis [Finds node correspondences in the miter.]

Description [Assumes that the colors are assigned.]

SideEffects []

SeeAlso []

Definition at line 297 of file cecIso.c.

{
    int nWords = 2;
    Gia_Obj_t * pObj;
    Vec_Int_t * vNodesA, * vNodesB;
    unsigned * pStore, Counter;
    int i, * pIso, * pTable, nTableSize;
    // start equivalence classes
    pIso = ABC_CALLOC( int, Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsCo(pObj) )
        {
            assert( Gia_ObjColors(p, i) == 0 );
            continue;
        }
        assert( Gia_ObjColors(p, i) );
        if ( Gia_ObjColors(p, i) == 3 )
            pIso[i] = i;
    }
    // start simulation info
    pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
    // simulate and create table
    nTableSize = Abc_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
    pTable = ABC_CALLOC( int, nTableSize );
    Gia_ManCleanValue( p );
    Gia_ManForEachObj1( p, pObj, i )
    {
        if ( Gia_ObjIsCo(pObj) )
            continue;
        if ( pIso[i] == 0 ) // simulate
            Gia_ManIsoSimulate( pObj, i, pStore, nWords );
        else if ( pIso[i] < i ) // copy
            Gia_ManIsoCopy( i, pIso[i], pStore, nWords );
        else // generate
            Gia_ManIsoRandom( i, pStore, nWords );
        if ( pIso[i] == 0 )
            Gia_ManIsoTableAdd( p, i, pStore, nWords, pTable, nTableSize );
    }
    // create equivalence classes
    vNodesA = Vec_IntAlloc( 100 );
    vNodesB = Vec_IntAlloc( 100 );
    for ( i = 0; i < nTableSize; i++ )
        if ( Gia_ManIsoExtractClasses( p, pTable[i], pStore, nWords, vNodesA, vNodesB ) )
            Gia_ManIsoMatchNodes( pIso, pStore, nWords, vNodesA, vNodesB );
    Vec_IntFree( vNodesA );
    Vec_IntFree( vNodesB );
    // collect info
    Counter = 0;
    Gia_ManForEachObj1( p, pObj, i )
    {
        Counter += (pIso[i] && pIso[i] < i);
/*
        if ( pIso[i] && pIso[i] < i )
        {
            if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) || 
                 (Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) )
                 Abc_Print( 1, "1" );
            else
                Abc_Print( 1, "0" );
        }
*/
    }
    Abc_Print( 1, "Computed %d pairs of structurally equivalent nodes.\n", Counter );
//    p->pIso = pIso;
//    Cec_ManTransformClasses( p );

    ABC_FREE( pTable );
    ABC_FREE( pStore );
    return pIso;
}

int Cec_ManFraClassesUpdate	(	Cec_ManFra_t *	p,
		Cec_ManSim_t *	pSim,
		Cec_ManPat_t *	pPat,
		Gia_Man_t *	pNew
	)

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

Synopsis [Updates equivalence classes using the patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file cecSweep.c.

{
    Vec_Ptr_t * vInfo;
    Gia_Obj_t * pObj, * pObjOld, * pReprOld;
    int i, k, iRepr, iNode;
    abctime clk;
clk = Abc_Clock();
    vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
p->timePat += Abc_Clock() - clk;
clk = Abc_Clock();
    if ( vInfo != NULL )
    {
        Gia_ManCreateValueRefs( p->pAig );
        for ( i = 0; i < pPat->nSeries; i++ )
        {
            Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i );
            if ( Cec_ManSimSimulateRound( pSim, pSim->vCiSimInfo, pSim->vCoSimInfo ) )
            {
                Vec_PtrFree( vInfo );
                return 1;
            }
        }
        Vec_PtrFree( vInfo );
    }
p->timeSim += Abc_Clock() - clk;
    assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
    // mark the transitive fanout of failed nodes
    if ( p->pPars->nDepthMax != 1 )
    {
        Gia_ManCleanMark0( p->pAig );
        Gia_ManCleanMark1( p->pAig );
        Gia_ManForEachCo( pNew, pObj, k )
        {
            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
                continue;
//            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
            Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
        }
        // mark the nodes reachable through the failed nodes
        Gia_ManForEachAnd( p->pAig, pObjOld, k )
            pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
        // unmark the disproved nodes
        Gia_ManForEachCo( pNew, pObj, k )
        {
            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
                continue; 
            pObjOld = Gia_ManObj(p->pAig, iNode);
            assert( pObjOld->fMark0 == 1 );
            if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
                pObjOld->fMark1 = 1;
        }
        // clean marks
        Gia_ManForEachAnd( p->pAig, pObjOld, k )
            if ( pObjOld->fMark1 )
            {
                pObjOld->fMark0 = 0;
                pObjOld->fMark1 = 0;
            }
    }
    // set the results
    p->nAllProved = p->nAllDisproved = p->nAllFailed = 0;
    Gia_ManForEachCo( pNew, pObj, k )
    {
        iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
        iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
        pReprOld = Gia_ManObj(p->pAig, iRepr);
        pObjOld = Gia_ManObj(p->pAig, iNode);
        if ( pObj->fMark1 )
        { // proved
            assert( pObj->fMark0 == 0 );
            assert( !Gia_ObjProved(p->pAig, iNode) );
            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
//            if ( pObjOld->fMark0 == 0 )
            {
                assert( iRepr == Gia_ObjRepr(p->pAig, iNode) );
                Gia_ObjSetProved( p->pAig, iNode );
                p->nAllProved++;
            }
        }
        else if ( pObj->fMark0 )
        { // disproved
            assert( pObj->fMark1 == 0 );
            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
//            if ( pObjOld->fMark0 == 0 )
            {
                if ( iRepr == Gia_ObjRepr(p->pAig, iNode) )
                    Abc_Print( 1, "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" );
                p->nAllDisproved++;
            }
        }
        else
        { // failed
            assert( pObj->fMark0 == 0 );
            assert( pObj->fMark1 == 0 );
            assert( !Gia_ObjFailed(p->pAig, iNode) );
            assert( !Gia_ObjProved(p->pAig, iNode) );
            Gia_ObjSetFailed( p->pAig, iNode );
            p->nAllFailed++;
        }
    } 
    return 0;
}

Gia_Man_t* Cec_ManFraSpecReduction

(

Cec_ManFra_t *

p

)

DECLARATIONS ///.

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

FileName [cecSweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [SAT sweeping manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Performs limited speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cecSweep.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr = NULL;
    int iRes0, iRes1, iRepr, iNode, iMiter;
    int i, fCompl, * piCopies, * pDepths;
    Gia_ManSetPhase( p->pAig );
    Vec_IntClear( p->vXorNodes );
    if ( p->pPars->nLevelMax )
        Gia_ManLevelNum( p->pAig );
    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
    pNew->pName = Abc_UtilStrsav( p->pAig->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pAig->pName );
    Gia_ManHashAlloc( pNew );
    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
    pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
    piCopies[0] = 0;
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            piCopies[i] = Gia_ManAppendCi( pNew );
            continue;
        }
        if ( Gia_ObjIsCo(pObj) ) 
            continue;
        if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
             piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
             continue;
        iRes0 = Abc_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
        iRes1 = Abc_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
        pDepths[i] = Abc_MaxInt( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
        if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
            continue;
        assert( Gia_ObjRepr(p->pAig, i) < i );
        iRepr = piCopies[Gia_ObjRepr(p->pAig, i)];
        if ( iRepr == -1 )
            continue;
        if ( Abc_LitRegular(iNode) == Abc_LitRegular(iRepr) )
            continue;
        if ( p->pPars->nLevelMax && 
            (Gia_ObjLevelId(p->pAig, i)  > p->pPars->nLevelMax || 
             Gia_ObjLevelId(p->pAig, Abc_Lit2Var(iRepr)) > p->pPars->nLevelMax) )
            continue;
        if ( p->pPars->fDualOut )
        {
//            if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) )
//                Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 );
            if ( p->pPars->fColorDiff )
            {
                if ( !Gia_ObjDiffColors( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
                    continue;
            }
            else
            {
                if ( !Gia_ObjDiffColors2( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
                    continue;
            }
        }
        pRepr = Gia_ManObj( p->pAig, Gia_ObjRepr(p->pAig, i) );
        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
        piCopies[i] = Abc_LitNotCond( iRepr, fCompl );
        if ( Gia_ObjProved(p->pAig, i) )
            continue;
        // produce speculative miter
        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
        Gia_ManAppendCo( pNew, iMiter );
        Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
        Vec_IntPush( p->vXorNodes, i );
        // add to the depth of this node
        pDepths[i] = 1 + Abc_MaxInt( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
        if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
            piCopies[i] = -1;
    }
    ABC_FREE( piCopies );
    ABC_FREE( pDepths );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, 0 );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

Cec_ManFra_t* Cec_ManFraStart	(	Gia_Man_t *	pAig,
		Cec_ParFra_t *	pPars
	)

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

Synopsis [Creates AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file cecMan.c.

{ 
    Cec_ManFra_t * p;
    p = ABC_ALLOC( Cec_ManFra_t, 1 );
    memset( p, 0, sizeof(Cec_ManFra_t) );
    p->pAig  = pAig;
    p->pPars = pPars;
    p->vXorNodes  = Vec_IntAlloc( 1000 );
    return p;
}

void Cec_ManFraStop

(

Cec_ManFra_t *

p

)

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

Synopsis [Deletes AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 284 of file cecMan.c.

{
    Vec_IntFree( p->vXorNodes );
    ABC_FREE( p );
}

Vec_Ptr_t* Cec_ManPatCollectPatterns	(	Cec_ManPat_t *	pMan,
		int	nInputs,
		int	nWordsInit
	)

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file cecPat.c.

{
    Vec_Int_t * vPat = pMan->vPattern1;
    Vec_Ptr_t * vInfo, * vPres;
    int k, kMax = -1, nPatterns = 0;
    int iStartOld = pMan->iStart;
    int nWords = nWordsInit;
    int nBits = 32 * nWords;
    abctime clk = Abc_Clock();
    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
    Gia_ManRandomInfo( vInfo, 0, 0, nWords );
    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vPres, 0, nWords );
    while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
    {
        nPatterns++;
        Cec_ManPatRestore( pMan, vPat );
        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
                break;
        kMax = Abc_MaxInt( kMax, k );
        if ( k == nBits-1 )
        {
            Vec_PtrReallocSimInfo( vInfo );
            Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
            Vec_PtrReallocSimInfo( vPres );
            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
            nWords *= 2;
            nBits *= 2;
        }
    }
    Vec_PtrFree( vPres );
    pMan->nSeries = Vec_PtrReadWordsSimInfo(vInfo) / nWordsInit;
    pMan->timePack += Abc_Clock() - clk;
    pMan->timeTotal += Abc_Clock() - clk;
    pMan->iStart = iStartOld;
    if ( pMan->fVerbose )
    {
        Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", 
            nPatterns, kMax, nWordsInit*32, pMan->nSeries );
        ABC_PRT( "Time", Abc_Clock() - clk );
        Cec_ManPatPrintStats( pMan );
    }
    return vInfo;
}

Vec_Ptr_t* Cec_ManPatPackPatterns	(	Vec_Int_t *	vCexStore,
		int	nInputs,
		int	nRegs,
		int	nWordsInit
	)

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file cecPat.c.

{
    Vec_Int_t * vPat;
    Vec_Ptr_t * vInfo, * vPres;
    int k, nSize, iStart, kMax = 0, nPatterns = 0;
    int nWords = nWordsInit;
    int nBits = 32 * nWords;
//    int RetValue;
    assert( nRegs <= nInputs );
    vPat  = Vec_IntAlloc( 100 );

    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vInfo, 0, nWords );
    Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );

    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vPres, 0, nWords );
    iStart = 0;
    while ( iStart < Vec_IntSize(vCexStore) )
    {
        nPatterns++;
        // skip the output number
        iStart++;
        // get the number of items
        nSize = Vec_IntEntry( vCexStore, iStart++ );
        if ( nSize <= 0 )
            continue;
        // extract pattern
        Vec_IntClear( vPat );
        for ( k = 0; k < nSize; k++ )
            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
        // add pattern to storage
        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
                break;

//        k = kMax + 1;
//        RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
//        assert( RetValue == 1 );

        kMax = Abc_MaxInt( kMax, k );
        if ( k == nBits-1 )
        {
            Vec_PtrReallocSimInfo( vInfo );
            Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
            Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );

            Vec_PtrReallocSimInfo( vPres );
            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
            nWords *= 2;
            nBits *= 2;
        }
    }
//    Abc_Print( 1, "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
    Vec_PtrFree( vPres );
    Vec_IntFree( vPat );
    return vInfo;
}

void Cec_ManPatPrintStats

(

Cec_ManPat_t *

p

)

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

Synopsis [Creates AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file cecMan.c.

{ 
    Abc_Print( 1, "Latest: P = %8d.  L = %10d.  Lm = %10d. Ave = %6.1f. MEM =%6.2f MB\n", 
        p->nPats, p->nPatLits, p->nPatLitsMin, 1.0 * p->nPatLitsMin/p->nPats, 
        1.0*(Vec_StrSize(p->vStorage)-p->iStart)/(1<<20) );
    Abc_Print( 1, "Total:  P = %8d.  L = %10d.  Lm = %10d. Ave = %6.1f. MEM =%6.2f MB\n", 
        p->nPatsAll, p->nPatLitsAll, p->nPatLitsMinAll, 1.0 * p->nPatLitsMinAll/p->nPatsAll, 
        1.0*Vec_StrSize(p->vStorage)/(1<<20) );
    Abc_PrintTimeP( 1, "Finding  ", p->timeFind,   p->timeTotal );
    Abc_PrintTimeP( 1, "Shrinking", p->timeShrink, p->timeTotal );
    Abc_PrintTimeP( 1, "Verifying", p->timeVerify, p->timeTotal );
    Abc_PrintTimeP( 1, "Sorting  ", p->timeSort,   p->timeTotal );
    Abc_PrintTimeP( 1, "Packing  ", p->timePack,   p->timeTotal );
    Abc_PrintTime( 1, "TOTAL    ",  p->timeTotal );
}

void Cec_ManPatSavePattern	(	Cec_ManPat_t *	pMan,
		Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file cecPat.c.

{
    Vec_Int_t * vPat;
    int nPatLits;
    abctime clkTotal = Abc_Clock();
//    abctime clk;
    assert( Gia_ObjIsCo(pObj) );
    pMan->nPats++;
    pMan->nPatsAll++;
    // compute values in the cone of influence
//clk = Abc_Clock();
    Gia_ManIncrementTravId( p->pAig );
    nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
    assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
    pMan->nPatLits += nPatLits;
    pMan->nPatLitsAll += nPatLits;
//pMan->timeFind += Abc_Clock() - clk;
    // compute sensitizing path
//clk = Abc_Clock();
    Vec_IntClear( pMan->vPattern1 );
    Gia_ManIncrementTravId( p->pAig );
    Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
    // compute sensitizing path
    Vec_IntClear( pMan->vPattern2 );
    Gia_ManIncrementTravId( p->pAig );
    Cec_ManPatComputePattern2_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern2 );
    // compare patterns
    vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
    pMan->nPatLitsMin += Vec_IntSize(vPat);
    pMan->nPatLitsMinAll += Vec_IntSize(vPat);
//pMan->timeShrink += Abc_Clock() - clk;
    // verify pattern using ternary simulation
//clk = Abc_Clock();
//    Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
//pMan->timeVerify += Abc_Clock() - clk;
    // sort pattern
//clk = Abc_Clock();
    Vec_IntSort( vPat, 0 );
//pMan->timeSort += Abc_Clock() - clk;
    // save pattern
    Cec_ManPatStore( pMan, vPat );
    pMan->timeTotal += Abc_Clock() - clkTotal;
}

void Cec_ManPatSavePatternCSat	(	Cec_ManPat_t *	pMan,
		Vec_Int_t *	vPat
	)

Definition at line 402 of file cecPat.c.

{
    // sort pattern
    Vec_IntSort( vPat, 0 );
    // save pattern
    Cec_ManPatStore( pMan, vPat );
}

Cec_ManPat_t* Cec_ManPatStart

(

)

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

Synopsis [Creates AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file cecMan.c.

{ 
    Cec_ManPat_t * p;
    p = ABC_CALLOC( Cec_ManPat_t, 1 );
    p->vStorage  = Vec_StrAlloc( 1<<20 );
    p->vPattern1 = Vec_IntAlloc( 1000 );
    p->vPattern2 = Vec_IntAlloc( 1000 );
    return p;
}

void Cec_ManPatStop

(

Cec_ManPat_t *

p

)

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

Synopsis [Deletes AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file cecMan.c.

{
    Vec_StrFree( p->vStorage );
    Vec_IntFree( p->vPattern1 );
    Vec_IntFree( p->vPattern2 );
    ABC_FREE( p );
}

void Cec_ManRefinedClassPrintStats	(	Gia_Man_t *	p,
		Vec_Str_t *	vStatus,
		int	iIter,
		abctime	Time
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Prints statistics during solving.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file cecCorr.c.

{ 
    int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
    int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
    for ( i = 1; i < Gia_ManObjNum(p); i++ )
    {
        if ( Gia_ObjIsNone(p, i) )
            CounterX++;
        else if ( Gia_ObjIsConst(p, i) )
            Counter0++;
        else if ( Gia_ObjIsHead(p, i) )
            Counter++;
    }
    CounterX -= Gia_ManCoNum(p);
    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
    if ( iIter == -1 )
        Abc_Print( 1, "BMC : " );
    else
        Abc_Print( 1, "%3d : ", iIter );
    Abc_Print( 1, "c =%8d  cl =%7d  lit =%8d  ", Counter0, Counter, nLits );
    if ( vStatus )
    Vec_StrForEachEntry( vStatus, Entry, i )
    {
        if ( Entry == 1 )
            nProve++;
        else if ( Entry == 0 )
            nDispr++;
        else if ( Entry == -1 )
            nFail++;
    }
    Abc_Print( 1, "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
    Abc_Print( 1, "%c  ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
    Abc_PrintTime( 1, "T", Time );
}

int Cec_ManSatCheckNode	(	Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file cecSolve.c.

{
    Gia_Obj_t * pObjR = Gia_Regular(pObj);
    int nBTLimit = p->pPars->nBTLimit;
    int Lit, RetValue, status, nConflicts;
    abctime clk, clk2;

    if ( pObj == Gia_ManConst0(p->pAig) )
        return 1;
    if ( pObj == Gia_ManConst1(p->pAig) )
    {
        assert( 0 );
        return 0;
    }

    p->nCallsSince++;  // experiment with this!!!
    p->nSatTotal++;
    
    // check if SAT solver needs recycling
    if ( p->pSat == NULL || 
        (p->pPars->nSatVarMax && 
         p->nSatVars > p->pPars->nSatVarMax && 
         p->nCallsSince > p->pPars->nCallsRecycle) )
        Cec_ManSatSolverRecycle( p );

    // if the nodes do not have SAT variables, allocate them
clk2 = Abc_Clock();
    Cec_CnfNodeAddToSolver( p, pObjR );
//ABC_PRT( "cnf", Abc_Clock() - clk2 );
//Abc_Print( 1, "%d \n", p->pSat->size );

clk2 = Abc_Clock();
//    Cec_SetActivityFactors( p, pObjR ); 
//ABC_PRT( "act", Abc_Clock() - clk2 );

    // propage unit clauses
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
    if ( p->pPars->fPolarFlip )
    {
        if ( pObjR->fPhase )  Lit = lit_neg( Lit );
    }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = Abc_Clock();
    nConflicts = p->pSat->stats.conflicts;

clk2 = Abc_Clock();
    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
//ABC_PRT( "sat", Abc_Clock() - clk2 );

    if ( RetValue == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        Lit = lit_neg( Lit );
        RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
        assert( RetValue );
        p->nSatUnsat++;
        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;       
//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return 1;
    }
    else if ( RetValue == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatSat++;
        p->nConfSat += p->pSat->stats.conflicts - nConflicts;
//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return 0;
    }
    else // if ( RetValue == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatUndec++;
        p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return -1;
    }
}

int Cec_ManSatCheckNodeTwo	(	Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj1,
		Gia_Obj_t *	pObj2
	)

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 569 of file cecSolve.c.

{
    Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
    Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
    int nBTLimit = p->pPars->nBTLimit;
    int Lits[2], RetValue, status, nConflicts;
    abctime clk, clk2;

    if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
        return 1;
    if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
    {
        assert( 0 );
        return 0;
    }

    p->nCallsSince++;  // experiment with this!!!
    p->nSatTotal++;
    
    // check if SAT solver needs recycling
    if ( p->pSat == NULL || 
        (p->pPars->nSatVarMax && 
         p->nSatVars > p->pPars->nSatVarMax && 
         p->nCallsSince > p->pPars->nCallsRecycle) )
        Cec_ManSatSolverRecycle( p );

    // if the nodes do not have SAT variables, allocate them
clk2 = Abc_Clock();
    Cec_CnfNodeAddToSolver( p, pObjR1 );
    Cec_CnfNodeAddToSolver( p, pObjR2 );
//ABC_PRT( "cnf", Abc_Clock() - clk2 );
//Abc_Print( 1, "%d \n", p->pSat->size );

clk2 = Abc_Clock();
//    Cec_SetActivityFactors( p, pObjR1 ); 
//    Cec_SetActivityFactors( p, pObjR2 ); 
//ABC_PRT( "act", Abc_Clock() - clk2 );

    // propage unit clauses
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) );
    Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) );
    if ( p->pPars->fPolarFlip )
    {
        if ( pObjR1->fPhase )  Lits[0] = lit_neg( Lits[0] );
        if ( pObjR2->fPhase )  Lits[1] = lit_neg( Lits[1] );
    }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = Abc_Clock();
    nConflicts = p->pSat->stats.conflicts;

clk2 = Abc_Clock();
    RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
//ABC_PRT( "sat", Abc_Clock() - clk2 );

    if ( RetValue == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        Lits[0] = lit_neg( Lits[0] );
        Lits[1] = lit_neg( Lits[1] );
        RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
        assert( RetValue );
        p->nSatUnsat++;
        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;       
//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return 1;
    }
    else if ( RetValue == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatSat++;
        p->nConfSat += p->pSat->stats.conflicts - nConflicts;
//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return 0;
    }
    else // if ( RetValue == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatUndec++;
        p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
        return -1;
    }
}

Cec_ManSat_t* Cec_ManSatCreate	(	Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars
	)

DECLARATIONS ///.

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

FileName [cecMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Manager procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Creates the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cecMan.c.

{
    Cec_ManSat_t * p;
    // create interpolation manager
    p = ABC_ALLOC( Cec_ManSat_t, 1 );
    memset( p, 0, sizeof(Cec_ManSat_t) );
    p->pPars        = pPars;
    p->pAig         = pAig;
    // SAT solving
    p->nSatVars     = 1;
    p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
    p->vFanins      = Vec_PtrAlloc( 100 );
    p->vCex         = Vec_IntAlloc( 100 );
    p->vVisits      = Vec_IntAlloc( 100 );
    return p;
}

void Cec_ManSatPrintStats

(

Cec_ManSat_t *

p

)

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

Synopsis [Prints statistics of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file cecMan.c.

{
    Abc_Print( 1, "CO = %8d  ", Gia_ManCoNum(p->pAig) );
    Abc_Print( 1, "AND = %8d  ", Gia_ManAndNum(p->pAig) );
    Abc_Print( 1, "Conf = %5d  ", p->pPars->nBTLimit );
    Abc_Print( 1, "MinVar = %5d  ", p->pPars->nSatVarMax );
    Abc_Print( 1, "MinCalls = %5d\n", p->pPars->nCallsRecycle );
    Abc_Print( 1, "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
    Abc_PrintTimeP( 1, "Time", p->timeSatUnsat, p->timeTotal );
    Abc_Print( 1, "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0,   p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
    Abc_PrintTimeP( 1, "Time", p->timeSatSat,   p->timeTotal );
    Abc_Print( 1, "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
    Abc_PrintTimeP( 1, "Time", p->timeSatUndec, p->timeTotal );
    Abc_PrintTime( 1, "Total time", p->timeTotal );
}

Vec_Int_t* Cec_ManSatReadCex

(

Cec_ManSat_t *

pSat

)

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

Synopsis [Returns the pattern stored.]

Description []

SideEffects []

SeeAlso []

Definition at line 820 of file cecSolve.c.

{
    return pSat->vCex;
}

void Cec_ManSatSolve	(	Cec_ManPat_t *	pPat,
		Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars
	)

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

Synopsis [Performs one round of solving for the POs of the AIG.]

Description [Labels the nodes that have been proved (pObj->fMark1) and returns the set of satisfying assignments.]

SideEffects []

SeeAlso []

Definition at line 676 of file cecSolve.c.

{
    Bar_Progress_t * pProgress = NULL;
    Cec_ManSat_t * p;
    Gia_Obj_t * pObj;
    int i, status;
    abctime clk = Abc_Clock(), clk2;
    // reset the manager
    if ( pPat )
    {
        pPat->iStart = Vec_StrSize(pPat->vStorage);
        pPat->nPats = 0;
        pPat->nPatLits = 0;
        pPat->nPatLitsMin = 0;
    } 
    Gia_ManSetPhase( pAig );
    Gia_ManLevelNum( pAig );
    Gia_ManIncrementTravId( pAig );
    p = Cec_ManSatCreate( pAig, pPars );
    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
    Gia_ManForEachCo( pAig, pObj, i )
    {
        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
        {
            pObj->fMark0 = 0;
            pObj->fMark1 = 1;
            continue;
        }
        Bar_ProgressUpdate( pProgress, i, "SAT..." );
clk2 = Abc_Clock();
        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
        pObj->fMark0 = (status == 0);
        pObj->fMark1 = (status == 1);
/*
        if ( status == -1 )
        {
            Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
            Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
            Gia_ManStop( pTemp );
            Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
        }
*/
        if ( status != 0 )
            continue;
        // save the pattern
        if ( pPat )
        {
            abctime clk3 = Abc_Clock();
            Cec_ManPatSavePattern( pPat, p, pObj );
            pPat->timeTotalSave += Abc_Clock() - clk3;
        }
        // quit if one of them is solved
        if ( pPars->fCheckMiter )
            break;
    }
    p->timeTotal = Abc_Clock() - clk;
    Bar_ProgressStop( pProgress );
    if ( pPars->fVerbose )
        Cec_ManSatPrintStats( p );
    Cec_ManSatStop( p );
}

void Cec_ManSatSolveCSat	(	Cec_ManPat_t *	pPat,
		Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars
	)

Definition at line 765 of file cecSolve.c.

{
    Vec_Str_t * vStatus;
    Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
    Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
    Gia_Obj_t * pObj;
    int i, status, iStart = 0;
    assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
    // reset the manager
    if ( pPat )
    {
        pPat->iStart = Vec_StrSize(pPat->vStorage);
        pPat->nPats = 0;
        pPat->nPatLits = 0;
        pPat->nPatLitsMin = 0;
    } 
    Gia_ManForEachCo( pAig, pObj, i )
    {
        status = (int)Vec_StrEntry(vStatus, i);
        pObj->fMark0 = (status == 0);
        pObj->fMark1 = (status == 1);
        if ( Vec_IntSize(vCexStore) > 0 && status != 1 )
            iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat );
        if ( status != 0 )
            continue;
        // save the pattern
        if ( pPat && Vec_IntSize(vPat) > 0 )
        {
            abctime clk3 = Abc_Clock();
            Cec_ManPatSavePatternCSat( pPat, vPat );
            pPat->timeTotalSave += Abc_Clock() - clk3;
        }
        // quit if one of them is solved
        if ( pPars->fCheckMiter )
            break;
    }
    assert( iStart == Vec_IntSize(vCexStore) );
    Vec_IntFree( vPat );
    Vec_StrFree( vStatus );
    Vec_IntFree( vCexStore );
}

Vec_Int_t* Cec_ManSatSolveMiter	(	Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars,
		Vec_Str_t **	pvStatus
	)

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

Synopsis [Performs one round of solving for the POs of the AIG.]

Description [Labels the nodes that have been proved (pObj->fMark1) and returns the set of satisfying assignments.]

SideEffects []

SeeAlso []

Definition at line 1026 of file cecSolve.c.

{
    Bar_Progress_t * pProgress = NULL;
    Vec_Int_t * vCexStore;
    Vec_Str_t * vStatus;
    Cec_ManSat_t * p;
    Gia_Obj_t * pObj;
    int i, status;
    abctime clk = Abc_Clock();
    // prepare AIG
    Gia_ManSetPhase( pAig );
    Gia_ManLevelNum( pAig );
    Gia_ManIncrementTravId( pAig );
    // create resulting data-structures
    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
    vCexStore = Vec_IntAlloc( 10000 );
    // perform solving
    p = Cec_ManSatCreate( pAig, pPars );
    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
    Gia_ManForEachCo( pAig, pObj, i )
    {
        Vec_IntClear( p->vCex );
        Bar_ProgressUpdate( pProgress, i, "SAT..." );
        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
        {
            if ( Gia_ObjFaninC0(pObj) )
            {
//                Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
                Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
                Vec_StrPush( vStatus, 0 );
            }
            else
            {
//                Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
                Vec_StrPush( vStatus, 1 );
            }
            continue;
        }
        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
        Vec_StrPush( vStatus, (char)status );
        if ( status == -1 )
        {
            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
            continue;
        }
        if ( status == 1 )
            continue;
        assert( status == 0 );
        // save the pattern
//        Gia_ManIncrementTravId( pAig );
//        Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
        Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
        Cec_ManSatAddToStore( vCexStore, p->vCex, i );
    }
    p->timeTotal = Abc_Clock() - clk;
    Bar_ProgressStop( pProgress );
//    if ( pPars->fVerbose )
//        Cec_ManSatPrintStats( p );
    Cec_ManSatStop( p );
    *pvStatus = vStatus;
    return vCexStore;
}

Vec_Str_t* Cec_ManSatSolveSeq	(	Vec_Ptr_t *	vPatts,
		Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars,
		int	nRegs,
		int *	pnPats
	)

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

Synopsis [Performs one round of solving for the POs of the AIG.]

Description [Labels the nodes that have been proved (pObj->fMark1) and returns the set of satisfying assignments.]

SideEffects []

SeeAlso []

Definition at line 867 of file cecSolve.c.

{
    Bar_Progress_t * pProgress = NULL;
    Vec_Str_t * vStatus;
    Cec_ManSat_t * p;
    Gia_Obj_t * pObj;
    int iPat = 0, nPatsInit, nPats;
    int i, status;
    abctime clk = Abc_Clock();
    nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
    Gia_ManSetPhase( pAig );
    Gia_ManLevelNum( pAig );
    Gia_ManIncrementTravId( pAig );
    p = Cec_ManSatCreate( pAig, pPars );
    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
    Gia_ManForEachCo( pAig, pObj, i )
    {
        Bar_ProgressUpdate( pProgress, i, "SAT..." );
        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
        {
            if ( Gia_ObjFaninC0(pObj) )
            {
//                Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
                Vec_StrPush( vStatus, 0 );
            }
            else
            {
//                Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
                Vec_StrPush( vStatus, 1 );
            }
            continue;
        }
        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
//Abc_Print( 1, "output %d   status = %d\n", i, status );
        Vec_StrPush( vStatus, (char)status );
        if ( status != 0 )
            continue;
        // resize storage
        if ( iPat == nPats )
        {
            int nWords = Vec_PtrReadWordsSimInfo(vPatts);
            Vec_PtrReallocSimInfo( vPatts );
            Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords );
            nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
        }
        if ( iPat % nPatsInit == 0 )
            iPat++;
        // save the pattern
        Gia_ManIncrementTravId( pAig );
//        Vec_IntClear( p->vCex );
        Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
//        Cec_ManSatAddToStore( p->vCexStore, p->vCex );
//        if ( iPat == nPats )
//            break;
        // quit if one of them is solved
//        if ( pPars->fFirstStop )
//            break;
//        if ( iPat == 32 * 15 * 16 - 1 )
//            break;
    }
    p->timeTotal = Abc_Clock() - clk;
    Bar_ProgressStop( pProgress );
    if ( pPars->fVerbose )
        Cec_ManSatPrintStats( p );
//    Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
    Cec_ManSatStop( p );
    if ( pnPats )
        *pnPats = iPat-1;
    return vStatus;
}

void Cec_ManSatStop

(

Cec_ManSat_t *

p

)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cecMan.c.

{
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    Vec_IntFree( p->vCex );
    Vec_IntFree( p->vVisits );
    Vec_PtrFree( p->vUsedNodes );
    Vec_PtrFree( p->vFanins );
    ABC_FREE( p->pSatVars );
    ABC_FREE( p );
}

void Cec_ManSavePattern	(	Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj1,
		Gia_Obj_t *	pObj2
	)

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

Synopsis [Save patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 1005 of file cecSolve.c.

{
    Vec_IntClear( p->vCex );
    Gia_ManIncrementTravId( p->pAig );
    Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
    if ( pObj2 )
    Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
}

void Cec_ManSeqDeriveInfoInitRandom	(	Vec_Ptr_t *	vInfo,
		Gia_Man_t *	pAig,
		Abc_Cex_t *	pCex
	)

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

Synopsis [Sets register values from the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cecSeq.c.

{
    unsigned * pInfo;
    int k, w, nWords;
    nWords = Vec_PtrReadWordsSimInfo( vInfo );
    assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs );
    assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
        for ( w = 0; w < nWords; w++ )
            pInfo[w] = (pCex && Abc_InfoHasBit(pCex->pData, k))? ~0 : 0;
    }

    for ( ; k < Vec_PtrSize(vInfo); k++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
        for ( w = 0; w < nWords; w++ )
            pInfo[w] = Gia_ManRandom( 0 );
    }
}

int Cec_ManSeqResimulate	(	Cec_ManSim_t *	p,
		Vec_Ptr_t *	vInfo
	)

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

Synopsis [Resimulates the classes using sequential simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file cecSeq.c.

{
    unsigned * pInfo0, * pInfo1;
    int f, i, k, w;
//    assert( Gia_ManRegNum(p->pAig) > 0 );
    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
    for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
    {
        pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k );
        pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
        for ( w = 0; w < p->nWords; w++ )
            pInfo1[w] = pInfo0[w];
    }
    for ( f = 0; f < p->pPars->nFrames; f++ )
    {
        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
        {
            pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ );
            pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
            for ( w = 0; w < p->nWords; w++ )
                pInfo1[w] = pInfo0[w];
        }
        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
        {
            pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
            pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
            for ( w = 0; w < p->nWords; w++ )
                pInfo1[w] = pInfo0[w];
        }
        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
            return 1;
    }
    assert( k == Vec_PtrSize(vInfo) );
    return 0;
}

int Cec_ManSeqResimulateInfo	(	Gia_Man_t *	pAig,
		Vec_Ptr_t *	vSimInfo,
		Abc_Cex_t *	pBestState,
		int	fCheckMiter
	)

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

Synopsis [Resimulates information to refine equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file cecSeq.c.

{
    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
    Cec_ManSim_t * pSim;
    int RetValue;//, clkTotal = Abc_Clock();
    assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
    Cec_ManSimSetDefaultParams( pParsSim );
    pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
    pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
    pParsSim->fCheckMiter = fCheckMiter;
    Gia_ManCreateValueRefs( pAig );
    pSim = Cec_ManSimStart( pAig, pParsSim );
    if ( pBestState )
        pSim->pBestState = pBestState;
    RetValue = Cec_ManSeqResimulate( pSim, vSimInfo );
    pSim->pBestState = NULL;
    Cec_ManSimStop( pSim );
    return RetValue;
}

int Cec_ManSimClassesPrepare	(	Cec_ManSim_t *	p,
		int	LevelMax
	)

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

Synopsis [Returns 1 if the bug is found.]

Description []

SideEffects []

SeeAlso []

Definition at line 851 of file cecClass.c.

{
    Gia_Obj_t * pObj;
    int i;
    assert( p->pAig->pReprs == NULL );
    // allocate representation
    p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
    p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
    // create references
    Gia_ManCreateValueRefs( p->pAig );
    // set starting representative of internal nodes to be constant 0
    if ( p->pPars->fLatchCorr )
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
    else if ( LevelMax == -1 )
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
    else
    {
        Gia_ManLevelNum( p->pAig );
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID );
        Vec_IntFreeP( &p->pAig->vLevels );
    }
    // if sequential simulation, set starting representative of ROs to be constant 0
    if ( p->pPars->fSeqSimulate )
        Gia_ManForEachRo( p->pAig, pObj, i )
            if ( pObj->Value )
                Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
    // perform simulation
    p->nWords = 1;
    do {
        if ( p->pPars->fVerbose )
            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
        for ( i = 0; i < 4; i++ )
        {
            Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
            if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
                return 1;
        }
        p->nWords = 2 * p->nWords + 1;
    }
    while ( p->nWords <= p->pPars->nWords );
    return 0;
}

int Cec_ManSimClassesRefine

(

Cec_ManSim_t *

p

)

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

Synopsis [Returns 1 if the bug is found.]

Description []

SideEffects []

SeeAlso []

Definition at line 908 of file cecClass.c.

{
    int i;
    Gia_ManCreateValueRefs( p->pAig );
    p->nWords = p->pPars->nWords;
    for ( i = 0; i < p->pPars->nRounds; i++ )
    {
        if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
        Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
            return 1;
    }
    if ( p->pPars->fVerbose )
        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
    return 0;
}

int Cec_ManSimClassRemoveOne	(	Cec_ManSim_t *	p,
		int	i
	)

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

Synopsis [Refines one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file cecClass.c.

{
    int iRepr, Ent;
    if ( Gia_ObjIsConst(p->pAig, i) )
    {
        Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
        return 1;
    }
    if ( !Gia_ObjIsClass(p->pAig, i) )
        return 0;
    assert( Gia_ObjIsClass(p->pAig, i) );
    iRepr = Gia_ObjRepr( p->pAig, i );
    if ( iRepr == GIA_VOID )
        iRepr = i;
    // collect nodes
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
    {
        if ( Ent == i )
            Vec_IntPush( p->vClassNew, Ent );
        else
            Vec_IntPush( p->vClassOld, Ent );
    }
    assert( Vec_IntSize( p->vClassNew ) == 1 );
    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
    assert( !Gia_ObjIsClass(p->pAig, i) );
    return 1;
}

int Cec_ManSimSimulateRound	(	Cec_ManSim_t *	p,
		Vec_Ptr_t *	vInfoCis,
		Vec_Ptr_t *	vInfoCos
	)

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

Synopsis [Simulates one round.]

Description [Returns the number of PO entry if failed; 0 otherwise.]

SideEffects []

SeeAlso []

Definition at line 652 of file cecClass.c.

{
    Gia_Obj_t * pObj;
    unsigned * pRes0, * pRes1, * pRes;
    int i, k, w, Ent, iCiId = 0, iCoId = 0;
    // prepare internal storage
    if ( p->nWordsOld != p->nWords )
        Cec_ManSimMemRelink( p );
    p->nMemsMax = 0;
    // allocate score counters
    ABC_FREE( p->pScores );
    if ( p->pBestState )
        p->pScores = ABC_CALLOC( int, 32 * p->nWords );
    // simulate nodes
    Vec_IntClear( p->vRefinedC );
    if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
    {
        pRes = Cec_ManSimSimRef( p, 0 );
        for ( w = 1; w <= p->nWords; w++ )
            pRes[w] = 0;
    }
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            if ( Gia_ObjValue(pObj) == 0 )
            {
                iCiId++;
                continue;
            }
            pRes = Cec_ManSimSimRef( p, i );
            if ( vInfoCis ) 
            {
                pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ );
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w-1];
            }
            else
            {
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = Gia_ManRandom( 0 );
            }
            // make sure the first pattern is always zero
            pRes[1] ^= (pRes[1] & 1);
            goto references;
        }
        if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
        {
            pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
            if ( vInfoCos )
            {
                pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ );
                if ( Gia_ObjFaninC0(pObj) )
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w-1] = ~pRes0[w];
                else 
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w-1] = pRes0[w];
            }
            continue;
        }
        assert( Gia_ObjValue(pObj) );
        pRes  = Cec_ManSimSimRef( p, i );
        pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
        pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );

//        Abc_Print( 1, "%d,%d  ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );

        if ( Gia_ObjFaninC0(pObj) )
        {
            if ( Gia_ObjFaninC1(pObj) )
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = ~(pRes0[w] | pRes1[w]);
            else
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = ~pRes0[w] & pRes1[w];
        }
        else
        {
            if ( Gia_ObjFaninC1(pObj) )
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w] & ~pRes1[w];
            else
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w] & pRes1[w];
        }

references:
        // if this node is candidate constant, collect it
        if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
        {
            pRes[0]++;
            Vec_IntPush( p->vRefinedC, i );
            if ( p->pBestState )
                Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
        }
        // if the node belongs to a class, save it
        if ( Gia_ObjIsClass(p->pAig, i) )
            pRes[0]++;
        // if this is the last node of the class, process it
        if ( Gia_ObjIsTail(p->pAig, i) )
        {
            Vec_IntClear( p->vClassTemp );
            Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
                Vec_IntPush( p->vClassTemp, Ent );
            Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
            Vec_IntForEachEntry( p->vClassTemp, Ent, k )
                Cec_ManSimSimDeref( p, Ent );
        }
    }

    if ( p->pPars->fConstCorr )
    {
        Vec_IntForEachEntry( p->vRefinedC, i, k )
        {
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
            Cec_ManSimSimDeref( p, i );
        }
        Vec_IntClear( p->vRefinedC );
    }

    if ( Vec_IntSize(p->vRefinedC) > 0 )
        Cec_ManSimProcessRefined( p, p->vRefinedC );
    assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
    assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
    assert( p->nMems == 1 );
    if ( p->nMems != 1 )
        Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" );
    if ( p->pPars->fVeryVerbose )
        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
    if ( p->pBestState )
        Cec_ManSimFindBestPattern( p );
/*
    if ( p->nMems > 1 ) {
        for ( i = 1; i < p->nObjs; i++ )
        if ( p->pSims[i] ) {
            int x = 0;
        }
    }
*/
    return Cec_ManSimAnalyzeOutputs( p );
}

Cec_ManSim_t* Cec_ManSimStart	(	Gia_Man_t *	pAig,
		Cec_ParSim_t *	pPars
	)

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

Synopsis [Creates AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file cecMan.c.

{ 
    Cec_ManSim_t * p;
    p = ABC_ALLOC( Cec_ManSim_t, 1 );
    memset( p, 0, sizeof(Cec_ManSim_t) );
    p->pAig  = pAig;
    p->pPars = pPars;
    p->nWords = pPars->nWords;
    p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
    p->vClassOld  = Vec_IntAlloc( 1000 );
    p->vClassNew  = Vec_IntAlloc( 1000 );
    p->vClassTemp = Vec_IntAlloc( 1000 );
    p->vRefinedC  = Vec_IntAlloc( 10000 );
    p->vCiSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(p->pAig), pPars->nWords );
    if ( pPars->fCheckMiter || Gia_ManRegNum(p->pAig) )
    {
        p->vCoSimInfo = Vec_PtrAllocSimInfo( Gia_ManCoNum(p->pAig), pPars->nWords );
        Vec_PtrCleanSimInfo( p->vCoSimInfo, 0, pPars->nWords );
    }
    p->iOut = -1;
    return p;
}

void Cec_ManSimStop

(

Cec_ManSim_t *

p

)

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

Synopsis [Deletes AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file cecMan.c.

{
    Vec_IntFree( p->vClassOld );
    Vec_IntFree( p->vClassNew );
    Vec_IntFree( p->vClassTemp );
    Vec_IntFree( p->vRefinedC );
    if ( p->vCiSimInfo ) 
        Vec_PtrFree( p->vCiSimInfo );
    if ( p->vCoSimInfo ) 
        Vec_PtrFree( p->vCoSimInfo );
    ABC_FREE( p->pScores );
    ABC_FREE( p->pCexComb );
    ABC_FREE( p->pCexes );
    ABC_FREE( p->pMems );
    ABC_FREE( p->pSimInfo );
    ABC_FREE( p );
}

int Cec_ObjSatVarValue	(	Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns value of the SAT variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file cecSolve.c.

{ 
    return sat_solver_var_value( p->pSat, Cec_ObjSatNum(p, pObj) );
}