cecMan.c File Reference

#include "cecInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START 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)

Function Documentation

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

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

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

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

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

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