abcExact.c File Reference

#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecInt.h"
#include "misc/vec/vecPtr.h"
#include "proof/cec/cec.h"
#include "sat/bsat/satSolver.h"

Include dependency graph for abcExact.c:

Go to the source code of this file.

Classes
struct	Ses_Man_t_
struct	Ses_TimesEntry_t_
struct	Ses_TruthEntry_t_
struct	Ses_Store_t_

Macros
#define	ABC_EXACT_SOL_NVARS   0
#define	ABC_EXACT_SOL_NFUNC   1
#define	ABC_EXACT_SOL_NGATES   2
#define	ANSI_COLOR_RED   "\x1b[31m"
#define	ANSI_COLOR_GREEN   "\x1b[32m"
#define	ANSI_COLOR_YELLOW   "\x1b[33m"
#define	ANSI_COLOR_BLUE   "\x1b[34m"
#define	ANSI_COLOR_MAGENTA   "\x1b[35m"
#define	ANSI_COLOR_CYAN   "\x1b[36m"
#define	ANSI_COLOR_RESET   "\x1b[0m"
#define	SES_STORE_TABLE_SIZE   1024

Typedefs
typedef struct Ses_Man_t_	Ses_Man_t
typedef struct Ses_TimesEntry_t_	Ses_TimesEntry_t
typedef struct Ses_TruthEntry_t_	Ses_TruthEntry_t
typedef struct Ses_Store_t_	Ses_Store_t

Functions
int	Ses_StoreAddEntry (Ses_Store_t *pStore, word *pTruth, int nVars, int *pArrTimeProfile, char *pSol, int fResLimit)
int	Ses_StoreGetEntrySimple (Ses_Store_t *pStore, word *pTruth, int nVars, int *pArrTimeProfile, char **pSol)
int	Ses_StoreGetEntry (Ses_Store_t *pStore, word *pTruth, int nVars, int *pArrTimeProfile, char **pSol)
Abc_Ntk_t *	Abc_NtkFindExact (word *pTruth, int nVars, int nFunc, int nMaxDepth, int *pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose)
Gia_Man_t *	Gia_ManFindExact (word *pTruth, int nVars, int nFunc, int nMaxDepth, int *pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose)
Abc_Ntk_t *	Abc_NtkFromTruthTable (word *pTruth, int nVars)
void	Abc_ExactTestSingleOutput (int fVerbose)
void	Abc_ExactTestSingleOutputAIG (int fVerbose)
void	Abc_ExactTest (int fVerbose)
int	Abc_ExactIsRunning ()
int	Abc_ExactInputNum ()
void	Abc_ExactStart (int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char *pFilename)
void	Abc_ExactStop (const char *pFilename)
void	Abc_ExactStats ()
int	Abc_ExactDelayCost (word *pTruth, int nVars, int *pArrTimeProfile, char *pPerm, int *Cost, int AigLevel)
Abc_Obj_t *	Abc_ExactBuildNode (word *pTruth, int nVars, int *pArrTimeProfile, Abc_Obj_t **pFanins, Abc_Ntk_t *pNtk)
void	Abc_ExactStoreTest (int fVerbose)

Macro Definition Documentation

ABC_EXACT_SOL_NFUNC

#define ABC_EXACT_SOL_NFUNC   1

Definition at line 204 of file abcExact.c.

ABC_EXACT_SOL_NGATES

#define ABC_EXACT_SOL_NGATES   2

Definition at line 205 of file abcExact.c.

ABC_EXACT_SOL_NVARS

#define ABC_EXACT_SOL_NVARS   0

Definition at line 203 of file abcExact.c.

ANSI_COLOR_BLUE

#define ANSI_COLOR_BLUE   "\x1b[34m"

Definition at line 210 of file abcExact.c.

ANSI_COLOR_CYAN

#define ANSI_COLOR_CYAN   "\x1b[36m"

Definition at line 212 of file abcExact.c.

ANSI_COLOR_GREEN

#define ANSI_COLOR_GREEN   "\x1b[32m"

Definition at line 208 of file abcExact.c.

ANSI_COLOR_MAGENTA

#define ANSI_COLOR_MAGENTA   "\x1b[35m"

Definition at line 211 of file abcExact.c.

ANSI_COLOR_RED

#define ANSI_COLOR_RED   "\x1b[31m"

Definition at line 207 of file abcExact.c.

ANSI_COLOR_RESET

#define ANSI_COLOR_RESET   "\x1b[0m"

Definition at line 213 of file abcExact.c.

ANSI_COLOR_YELLOW

#define ANSI_COLOR_YELLOW   "\x1b[33m"

Definition at line 209 of file abcExact.c.

SES_STORE_TABLE_SIZE

#define SES_STORE_TABLE_SIZE   1024

Definition at line 311 of file abcExact.c.

Typedef Documentation

Ses_Man_t

typedef struct Ses_Man_t_ Ses_Man_t

Definition at line 215 of file abcExact.c.

Ses_Store_t

typedef struct Ses_Store_t_ Ses_Store_t

Definition at line 312 of file abcExact.c.

Ses_TimesEntry_t

typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t

Definition at line 293 of file abcExact.c.

Ses_TruthEntry_t

typedef struct Ses_TruthEntry_t_ Ses_TruthEntry_t

Definition at line 302 of file abcExact.c.

Function Documentation

Abc_ExactBuildNode()

Abc_Obj_t * Abc_ExactBuildNode	(	word *	pTruth,
		int	nVars,
		int *	pArrTimeProfile,
		Abc_Obj_t **	pFanins,
		Abc_Ntk_t *	pNtk )

Definition at line 2894 of file abcExact.c.

{
    char * pSol = NULL;
    int i, j, nMaxArrival;
    int pNormalArrTime[8];
    char const * p;
    Abc_Obj_t * pObj;
    Vec_Ptr_t * pGates;
    char pGateTruth[5];
    char * pSopCover;
    abctime timeStart = Abc_Clock();
 
    if ( nVars == 0 )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
    }
    if ( nVars == 1 )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
    }
 
    for ( i = 0; i < nVars; ++i )
        pNormalArrTime[i] = pArrTimeProfile[i];
    Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
    assert( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) );
    if ( !pSol )
    {
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return NULL;
    }
 
    assert( pSol[ABC_EXACT_SOL_NVARS] == nVars );
    assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );
 
    pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] );
    pGateTruth[3] = '0';
    pGateTruth[4] = '\0';
 
    /* primary inputs */
    for ( i = 0; i < nVars; ++i )
    {
        assert( pFanins[i] );
        Vec_PtrPush( pGates, pFanins[i] );
    }
 
    /* gates */
    p = pSol + 3;
    for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
    {
        pGateTruth[2] = '0' + ( *p & 1 );
        pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
        pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
        ++p;
 
        assert( *p == 2 ); /* binary gate */
        ++p;
 
        /* invert truth table if we are last gate and inverted */
        if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
            for ( j = 0; j < 4; ++j )
                pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
 
        pSopCover = Abc_SopFromTruthBin( pGateTruth );
        pObj = Abc_NtkCreateNode( pNtk );
        assert( pObj );
        pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
        Vec_PtrPush( pGates, pObj );
        ABC_FREE( pSopCover );
 
        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
        Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
    }
 
    /* output */
    pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
 
    Vec_PtrFree( pGates );
 
    s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
    return pObj;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_ExactDelayCost()

int Abc_ExactDelayCost	(	word *	pTruth,
		int	nVars,
		int *	pArrTimeProfile,
		char *	pPerm,
		int *	Cost,
		int	AigLevel )

Definition at line 2716 of file abcExact.c.

{
    int i, nMaxArrival, nDelta, l;
    Ses_Man_t * pSes = NULL;
    char * pSol = NULL, * pSol2 = NULL, * p;
    int pNormalArrTime[8];
    int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
    abctime timeStart = Abc_Clock(), timeStartExact;
 
    /* some checks */
    if ( nVars < 0 || nVars > 8 )
    {
        printf( "invalid truth table size %d\n", nVars );
        assert( 0 );
    }
 
    /* statistics */
    s_pSesStore->nCutCount++;
    s_pSesStore->pCutCount[nVars]++;
 
    if ( nVars == 0 )
    {
        s_pSesStore->nSynthesizedTrivial++;
        s_pSesStore->pSynthesizedTrivial[0]++;
 
        *Cost = 0;
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return 0;
    }
 
    if ( nVars == 1 )
    {
        s_pSesStore->nSynthesizedTrivial++;
        s_pSesStore->pSynthesizedTrivial[1]++;
 
        *Cost = 0;
        pPerm[0] = (char)0;
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return pArrTimeProfile[0];
    }
 
    for ( l = 0; l < nVars; ++l )
        pNormalArrTime[l] = pArrTimeProfile[l];
 
    nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
 
    *Cost = ABC_INFINITY;
 
    if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
    {
        s_pSesStore->nCacheHits++;
        s_pSesStore->pCacheHits[nVars]++;
    }
    else
    {
        if ( s_pSesStore->fVeryVerbose )
        {
            printf( ANSI_COLOR_CYAN );
            Abc_TtPrintHexRev( stdout, pTruth, nVars );
            printf( ANSI_COLOR_RESET );
            printf( " [%d", pNormalArrTime[0] );
            for ( l = 1; l < nVars; ++l )
                printf( " %d", pNormalArrTime[l] );
            printf( "]@%d:", AigLevel );
            fflush( stdout );
        }
 
        nMaxDepth = pNormalArrTime[0];
        for ( i = 1; i < nVars; ++i )
            nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] );
        nMaxDepth += nVars + 1;
        if ( AigLevel != -1 )
            nMaxDepth = Abc_MinInt( AigLevel - nDelta, nMaxDepth + nVars + 1 );
 
        timeStartExact = Abc_Clock();
 
        pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose );
        pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
        pSes->pSat = s_pSesStore->pSat;
        pSes->nStartGates = nVars - 2;
 
        while ( pSes->nMaxDepth ) /* there is improvement */
        {
            if ( s_pSesStore->fVeryVerbose )
            {
                printf( " %d", pSes->nMaxDepth );
                fflush( stdout );
            }
 
            if ( ( pSol2 = Ses_ManFindMinimumSize( pSes ) ) != NULL )
            {
                if ( s_pSesStore->fVeryVerbose )
                {
                    if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
                    printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth );
                }
                if ( pSol )
                    ABC_FREE( pSol );
                pSol = pSol2;
                pSes->nMaxDepth--;
            }
            else
            {
                if ( s_pSesStore->fVeryVerbose )
                {
                    if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
                    printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth );
                }
                break;
            }
        }
 
        if ( s_pSesStore->fVeryVerbose )
            printf( "        \n" );
 
        /* log unsuccessful case for debugging */
        if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit )
            Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth, pSol, nVars - 2 );
 
        pSes->timeTotal = Abc_Clock() - timeStartExact;
 
        /* statistics */
        s_pSesStore->nSatCalls += pSes->nSatCalls;
        s_pSesStore->nUnsatCalls += pSes->nUnsatCalls;
        s_pSesStore->nUndefCalls += pSes->nUndefCalls;
 
        s_pSesStore->timeSat += pSes->timeSat;
        s_pSesStore->timeSatSat += pSes->timeSatSat;
        s_pSesStore->timeSatUnsat += pSes->timeSatUnsat;
        s_pSesStore->timeSatUndef += pSes->timeSatUndef;
        s_pSesStore->timeInstance += pSes->timeInstance;
        s_pSesStore->timeExact += pSes->timeTotal;
 
        /* cleanup (we need to clean before adding since pTruth may have been modified by pSes) */
        fResLimit = pSes->fHitResLimit;
        Ses_ManCleanLight( pSes );
 
        /* store solution */
        Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol, fResLimit );
    }
 
    if ( pSol )
    {
        *Cost = pSol[ABC_EXACT_SOL_NGATES];
        p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1;
        Delay = *p++;
        for ( l = 0; l < nVars; ++l )
            pPerm[l] = *p++;
    }
 
    if ( pSol )
    {
        int Delay2 = 0;
        for ( l = 0; l < nVars; ++l )
        {
            //printf( "%d ", pPerm[l] );
            Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] );
        }
        //printf( "  output arrival = %d    recomputed = %d\n", Delay, Delay2 );
        //if ( Delay != Delay2 )
        //{
        //    printf( "^--- BUG!\n" );
        //    assert( 0 );
        //}
 
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return Delay2;
    }
    else
    {
        assert( *Cost == ABC_INFINITY );
 
        s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
        return ABC_INFINITY;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_ExactInputNum()

int Abc_ExactInputNum

(

)

Definition at line 2611 of file abcExact.c.

{
    return 8;
}

Abc_ExactIsRunning()

int Abc_ExactIsRunning

(

)

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

Synopsis [APIs for integraging with the mapper.]

Definition at line 2605 of file abcExact.c.

{
    return s_pSesStore != NULL;
}

Abc_ExactStart()

void Abc_ExactStart	(	int	nBTLimit,
		int	fMakeAIG,
		int	fVerbose,
		int	fVeryVerbose,
		const char *	pFilename )

Definition at line 2616 of file abcExact.c.

{
    if ( !s_pSesStore )
    {
        s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
        s_pSesStore->fVeryVerbose = fVeryVerbose;
        if ( pFilename )
        {
            Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );
 
            s_pSesStore->szDBName = ABC_CALLOC( char, strlen( pFilename ) + 1 );
            strcpy( s_pSesStore->szDBName, pFilename );
        }
        if ( s_pSesStore->fVeryVerbose )
        {
            s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
        }
    }
    else
        printf( "BMS manager already started\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_ExactStats()

void Abc_ExactStats

(

)

Definition at line 2652 of file abcExact.c.

{
    int i;
 
    if ( !s_pSesStore )
    {
        printf( "BMS manager has not been started\n" );
        return;
    }
 
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "                                    0         1         2         3         4         5         6         7         8     total\n" );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of considered cuts :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pCutCount[i] );
    printf( "%10lu\n", s_pSesStore->nCutCount );
    printf( " - trivial                :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedTrivial[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedTrivial );
    printf( " - synth (imp)            :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedImp[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedImp );
    printf( " - synth (res)            :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pSynthesizedRL[i] );
    printf( "%10lu\n", s_pSesStore->nSynthesizedRL );
    printf( " - not synth (imp)        :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pUnsynthesizedImp[i] );
    printf( "%10lu\n", s_pSesStore->nUnsynthesizedImp );
    printf( " - not synth (res)        :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pUnsynthesizedRL[i] );
    printf( "%10lu\n", s_pSesStore->nUnsynthesizedRL );
    printf( " - cache hits             :" );
    for ( i = 0; i < 9; ++i )
        printf( "%10lu", s_pSesStore->pCacheHits[i] );
    printf( "%10lu\n", s_pSesStore->nCacheHits );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of entries         : %d\n", s_pSesStore->nEntriesCount );
    printf( "number of valid entries   : %d\n", s_pSesStore->nValidEntriesCount );
    printf( "number of invalid entries : %d\n", s_pSesStore->nEntriesCount - s_pSesStore->nValidEntriesCount );
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "number of SAT calls       : %lu\n", s_pSesStore->nSatCalls );
    printf( "number of UNSAT calls     : %lu\n", s_pSesStore->nUnsatCalls );
    printf( "number of UNDEF calls     : %lu\n", s_pSesStore->nUndefCalls );
 
    printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
    printf( "Runtime breakdown:\n" );
    ABC_PRTP( "Exact    ", s_pSesStore->timeExact,                          s_pSesStore->timeTotal );
    ABC_PRTP( " Sat     ", s_pSesStore->timeSat,                            s_pSesStore->timeTotal );
    ABC_PRTP( "  Sat    ", s_pSesStore->timeSatSat,                         s_pSesStore->timeTotal );
    ABC_PRTP( "  Unsat  ", s_pSesStore->timeSatUnsat,                       s_pSesStore->timeTotal );
    ABC_PRTP( "  Undef  ", s_pSesStore->timeSatUndef,                       s_pSesStore->timeTotal );
    ABC_PRTP( " Instance", s_pSesStore->timeInstance,                       s_pSesStore->timeTotal );
    ABC_PRTP( "Other    ", s_pSesStore->timeTotal - s_pSesStore->timeExact, s_pSesStore->timeTotal );
    ABC_PRTP( "ALL      ", s_pSesStore->timeTotal,                          s_pSesStore->timeTotal );
}

Abc_ExactStop()

void Abc_ExactStop

(

const char *

pFilename

)

Definition at line 2638 of file abcExact.c.

{
    if ( s_pSesStore )
    {
        if ( pFilename )
            Ses_StoreWrite( s_pSesStore, pFilename, 1, 0, 0, 0 );
        if ( s_pSesStore->pDebugEntries )
            fclose( s_pSesStore->pDebugEntries );
        Ses_StoreClean( s_pSesStore );
    }
    else
        printf( "BMS manager has not been started\n" );
}

Here is the caller graph for this function:

Abc_ExactStoreTest()

void Abc_ExactStoreTest

(

int

fVerbose

)

Definition at line 2978 of file abcExact.c.

{
    int i;
    word pTruth[4] = {0xcafe, 0, 0, 0};
    int pArrTimeProfile[4] = {6, 2, 8, 5};
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pFanins[4];
    Vec_Ptr_t * vNames;
    char pPerm[4] = {0};
    int Cost = 0;
 
    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
    pNtk->pName = Extra_UtilStrsav( "exact" );
    vNames = Abc_NodeGetFakeNames( 4u );
 
    /* primary inputs */
    Vec_PtrPush( pNtk->vObjs, NULL );
    for ( i = 0; i < 4; ++i )
    {
        pFanins[i] = Abc_NtkCreatePi( pNtk );
        Abc_ObjAssignName( pFanins[i], (char*)Vec_PtrEntry( vNames, i ), NULL );
    }
    Abc_NodeFreeNames( vNames );
 
    Abc_ExactStart( 10000, 1, fVerbose, 0, NULL );
 
    assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
 
    assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 );
 
    assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
 
    (*pArrTimeProfile)++;
    assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
    (*pArrTimeProfile)--;
 
    Abc_ExactStop( NULL );
 
    Abc_NtkDelete( pNtk );
}

Here is the call graph for this function:

Abc_ExactTest()

void Abc_ExactTest

(

int

fVerbose

)

Definition at line 2589 of file abcExact.c.

{
    Abc_ExactTestSingleOutput( fVerbose );
    Abc_ExactTestSingleOutputAIG( fVerbose );
 
    printf( "\n" );
}

Here is the call graph for this function:

Abc_ExactTestSingleOutput()

void Abc_ExactTestSingleOutput

(

int

fVerbose

)

Definition at line 2509 of file abcExact.c.

{
    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
 
    word pTruth[4] = {0xcafe, 0, 0, 0};
    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
    int pArrTimeProfile[4] = {6, 2, 8, 5};
 
    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
 
    pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
    Abc_NtkShortNames( pNtk2 );
    Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
    assert( pNtk2 );
    assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
    Abc_NtkDelete( pNtk2 );
 
    pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
    Abc_NtkShortNames( pNtk3 );
    Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
    assert( pNtk3 );
    assert( Abc_NtkLevel( pNtk3 ) <= 3 );
    Abc_NtkDelete( pNtk3 );
 
    pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
    Abc_NtkShortNames( pNtk4 );
    Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
    assert( pNtk4 );
    assert( Abc_NtkLevel( pNtk4 ) <= 9 );
    Abc_NtkDelete( pNtk4 );
 
    assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
 
    assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
 
    Abc_NtkDelete( pNtk );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_ExactTestSingleOutputAIG()

void Abc_ExactTestSingleOutputAIG

(

int

fVerbose

)

Definition at line 2547 of file abcExact.c.

{
    word pTruth[4] = {0xcafe, 0, 0, 0};
    Abc_Ntk_t * pNtk;
    Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
    int pArrTimeProfile[4] = {6, 2, 8, 5};
 
    Cec_ManCecSetDefaultParams( pPars );
 
    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
    Abc_NtkToAig( pNtk );
    pGia = Abc_NtkAigToGia( pNtk, 1 );
 
    pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );
 
    pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );
 
    pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
    pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
    assert( pMiter );
    Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );
 
    assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
 
    assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
 
    Gia_ManStop( pGia );
    Gia_ManStop( pGia2 );
    Gia_ManStop( pGia3 );
    Gia_ManStop( pGia4 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkFindExact()

Abc_Ntk_t * Abc_NtkFindExact	(	word *	pTruth,
		int	nVars,
		int	nFunc,
		int	nMaxDepth,
		int *	pArrTimeProfile,
		int	nBTLimit,
		int	nStartGates,
		int	fVerbose )

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

Synopsis [Find minimum size networks with a SAT solver.]

Description [If nMaxDepth is -1, then depth constraints are ignored. If nMaxDepth is not -1, one can set pArrTimeProfile which should have the length of nVars. One can ignore pArrTimeProfile by setting it to NULL.]

SideEffects []

SeeAlso []

Definition at line 2414 of file abcExact.c.

{
    Ses_Man_t * pSes;
    char * pSol;
    Abc_Ntk_t * pNtk = NULL;
    abctime timeStart;
 
    /* some checks */
    assert( nVars >= 2 && nVars <= 8 );
 
    timeStart = Abc_Clock();
 
    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
    pSes->nStartGates = nStartGates;
    pSes->fReasonVerbose = 0;
    pSes->fSatVerbose = 0;
    if ( fVerbose )
        Ses_ManPrintFuncs( pSes );
 
    if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
    {
        pNtk = Ses_ManExtractNtk( pSol );
        ABC_FREE( pSol );
    }
 
    pSes->timeTotal = Abc_Clock() - timeStart;
 
    if ( fVerbose )
        Ses_ManPrintRuntime( pSes );
 
    /* cleanup */
    Ses_ManClean( pSes );
 
    return pNtk;
}

Here is the caller graph for this function:

Abc_NtkFromTruthTable()

Abc_Ntk_t * Abc_NtkFromTruthTable	(	word *	pTruth,
		int	nVars )

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

Synopsis [Some test cases.]

Definition at line 2494 of file abcExact.c.

{
    Abc_Ntk_t * pNtk;
    Mem_Flex_t * pMan;
    char * pSopCover;
 
    pMan = Mem_FlexStart();
    pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
    pNtk = Abc_NtkCreateWithNode( pSopCover );
    Abc_NtkShortNames( pNtk );
    Mem_FlexStop( pMan, 0 );
 
    return pNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFindExact()

Gia_Man_t * Gia_ManFindExact	(	word *	pTruth,
		int	nVars,
		int	nFunc,
		int	nMaxDepth,
		int *	pArrTimeProfile,
		int	nBTLimit,
		int	nStartGates,
		int	fVerbose )

Definition at line 2450 of file abcExact.c.

{
    Ses_Man_t * pSes;
    char * pSol;
    Gia_Man_t * pGia = NULL;
    abctime timeStart;
 
    /* some checks */
    assert( nVars >= 2 && nVars <= 8 );
 
    timeStart = Abc_Clock();
 
    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
    pSes->nStartGates = nStartGates;
    pSes->fVeryVerbose = 1;
    pSes->fExtractVerbose = 0;
    pSes->fSatVerbose = 0;
    pSes->fReasonVerbose = 1;
    if ( fVerbose )
        Ses_ManPrintFuncs( pSes );
 
    if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
    {
        pGia = Ses_ManExtractGia( pSol );
        ABC_FREE( pSol );
    }
 
    pSes->timeTotal = Abc_Clock() - timeStart;
 
    if ( fVerbose )
        Ses_ManPrintRuntime( pSes );
 
    /* cleanup */
    Ses_ManClean( pSes );
 
    return pGia;
}

Here is the caller graph for this function:

Ses_StoreAddEntry()

int Ses_StoreAddEntry	(	Ses_Store_t *	pStore,
		word *	pTruth,
		int	nVars,
		int *	pArrTimeProfile,
		char *	pSol,
		int	fResLimit )

Definition at line 629 of file abcExact.c.

{
    int key, fAdded;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
 
    if ( pSol )
        Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pArrTimeProfile, pSol );
 
    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];
 
    /* does truth table already exist? */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }
 
    /* entry does not yet exist, so create new one and enqueue */
    if ( !pTEntry )
    {
        pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 );
        Ses_StoreTruthCopy( pTEntry, pTruth, nVars );
        pTEntry->next = pStore->pEntries[key];
        pStore->pEntries[key] = pTEntry;
    }
 
    /* does arrival time already exist? */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }
 
    /* entry does not yet exist, so create new one and enqueue */
    if ( !pTiEntry )
    {
        pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
        Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
        pTiEntry->pNetwork = pSol;
        pTiEntry->fResLimit = fResLimit;
        pTiEntry->next = pTEntry->head;
        pTEntry->head = pTiEntry;
 
        /* item has been added */
        fAdded = 1;
        pStore->nEntriesCount++;
        if ( pSol )
            pStore->nValidEntriesCount++;
    }
    else
    {
        //assert( 0 );
        /* item was already present */
        fAdded = 0;
    }
 
    /* statistics */
    if ( pSol )
    {
        if ( fResLimit )
        {
            pStore->nSynthesizedRL++;
            pStore->pSynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nSynthesizedImp++;
            pStore->pSynthesizedImp[nVars]++;
        }
    }
    else
    {
        if ( fResLimit )
        {
            pStore->nUnsynthesizedRL++;
            pStore->pUnsynthesizedRL[nVars]++;
        }
        else
        {
            pStore->nUnsynthesizedImp++;
            pStore->pUnsynthesizedImp[nVars]++;
        }
    }
 
    if ( fAdded && pStore->szDBName )
        Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 );
 
    return fAdded;
}

Here is the caller graph for this function:

Ses_StoreGetEntry()

int Ses_StoreGetEntry	(	Ses_Store_t *	pStore,
		word *	pTruth,
		int	nVars,
		int *	pArrTimeProfile,
		char **	pSol )

Definition at line 768 of file abcExact.c.

{
    int key;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
    int pTimes[8];
 
    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];
 
    /* find truth table entry */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }
 
    /* no entry found? */
    if ( !pTEntry )
        return 0;
 
    /* find times entry */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        /* found after normalization wrt. to network */
        if ( pTiEntry->pNetwork )
        {
            memcpy( pTimes, pArrTimeProfile, sizeof(int) * nVars );
            Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pTimes, pTiEntry->pNetwork );
 
            if ( Ses_StoreTimesEqual( pTimes, pTiEntry->pArrTimeProfile, nVars ) )
                break;
        }
        /* found for non synthesized network */
        else if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }
 
    /* no entry found? */
    if ( !pTiEntry )
        return 0;
 
    *pSol = pTiEntry->pNetwork;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ses_StoreGetEntrySimple()

int Ses_StoreGetEntrySimple	(	Ses_Store_t *	pStore,
		word *	pTruth,
		int	nVars,
		int *	pArrTimeProfile,
		char **	pSol )

Definition at line 728 of file abcExact.c.

{
    int key;
    Ses_TruthEntry_t * pTEntry;
    Ses_TimesEntry_t * pTiEntry;
 
    key = Ses_StoreTableHash( pTruth, nVars );
    pTEntry = pStore->pEntries[key];
 
    /* find truth table entry */
    while ( pTEntry )
    {
        if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
            break;
        else
            pTEntry = pTEntry->next;
    }
 
    /* no entry found? */
    if ( !pTEntry )
        return 0;
 
    /* find times entry */
    pTiEntry = pTEntry->head;
    while ( pTiEntry )
    {
        if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
            break;
        else
            pTiEntry = pTiEntry->next;
    }
 
    /* no entry found? */
    if ( !pTiEntry )
        return 0;
 
    *pSol = pTiEntry->pNetwork;
    return 1;
}