abcLog.c File Reference

#include "base/abc/abc.h"
#include "aig/gia/gia.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Abc_NtkWriteLogFile (char *pFileName, Abc_Cex_t *pCex, int Status, int nFrames, char *pCommand)
	DECLARATIONS ///. More...
int	Abc_NtkReadLogFile (char *pFileName, Abc_Cex_t **ppCex, int *pnFrames)

Function Documentation

int Abc_NtkReadLogFile	(	char *	pFileName,
		Abc_Cex_t **	ppCex,
		int *	pnFrames
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file abcLog.c.

{
    FILE * pFile;
    Abc_Cex_t * pCex;
    Vec_Int_t * vNums;
    char Buffer[1000], * pToken, * RetValue;
    int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1, nFrames2 = -1;
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
        return -1;
    }
    RetValue = fgets( Buffer, 1000, pFile );
    if ( !strncmp( Buffer, "snl_UNSAT", strlen("snl_UNSAT") ) )
    {
        Status = 1;
        nFrames = atoi( Buffer + strlen("snl_UNSAT") ); 
    }
    else if ( !strncmp( Buffer, "snl_SAT", strlen("snl_SAT") ) )
    {
        Status = 0;
//        nFrames = atoi( Buffer + strlen("snl_SAT") ); 
        pToken  = strtok( Buffer + strlen("snl_SAT"), " \t\n" );
        nFrames = atoi( pToken ); 
        pToken  = strtok( NULL, " \t\n" );
        pToken  = strtok( NULL, " \t\n" );
        if ( pToken != NULL )
        {
            iPo     = atoi( pToken ); 
            pToken  = strtok( NULL, " \t\n" );
            if ( pToken )
                nFrames2 = atoi( pToken ); 
        }
//        else
//            printf( "Warning! The current status is SAT but the current CEX is not given.\n"  );
    }
    else if ( !strncmp( Buffer, "snl_UNK", strlen("snl_UNK") ) )
    {
        Status = -1;
        nFrames = atoi( Buffer + strlen("snl_UNK") ); 
    }
    else
    {
        printf( "Unrecognized status.\n" );
    }
    // found regs till the new line
    vNums = Vec_IntAlloc( 100 );
    while ( (c = fgetc(pFile)) != EOF )
    {
        if ( c == '\n' )
            break;
        if ( c == '0' || c == '1' )
            Vec_IntPush( vNums, c - '0' );
    }
    nRegs = Vec_IntSize(vNums);
    // skip till the new line
    while ( (c = fgetc(pFile)) != EOF )
    {
        if ( c == '0' || c == '1' )
            Vec_IntPush( vNums, c - '0' );
    }
    fclose( pFile );
    if ( Vec_IntSize(vNums) )
    {
        int iFrameCex = (nFrames2 == -1) ? nFrames : nFrames2;
        if ( nRegs < 0 )
        {
            printf( "Cannot read register number.\n" );
            Vec_IntFree( vNums );
            return -1;
        }
        if ( Vec_IntSize(vNums)-nRegs == 0 )
        {
            printf( "Cannot read counter example.\n" );
            Vec_IntFree( vNums );
            return -1;
        }
        if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
        {
            printf( "Incorrect number of bits.\n" );
            Vec_IntFree( vNums );
            return -1;
        }
        pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 );
        pCex->iPo    = iPo;
        pCex->iFrame = iFrameCex;
        assert( Vec_IntSize(vNums) == pCex->nBits );
        for ( c = 0; c < pCex->nBits; c++ )
            if ( Vec_IntEntry(vNums, c) )
                Abc_InfoSetBit( pCex->pData, c );
        Vec_IntFree( vNums );
        if ( ppCex )
            *ppCex = pCex;
        else
            ABC_FREE( pCex );
    }
    else
        Vec_IntFree( vNums );
    if ( pnFrames )
        *pnFrames = nFrames;
    return Status;
}

ABC_NAMESPACE_IMPL_START void Abc_NtkWriteLogFile	(	char *	pFileName,
		Abc_Cex_t *	pCex,
		int	Status,
		int	nFrames,
		char *	pCommand
	)

DECLARATIONS ///.

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

FileName [abcLog.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Log file printing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file abcLog.c.

{
    FILE * pFile;
    int i;
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Cannot open log file for writing \"%s\".\n" , pFileName );
        return;
    }
    // write <result>
    if ( Status == 1 )
        fprintf( pFile, "snl_UNSAT" );
    else if ( Status == 0 )
        fprintf( pFile, "snl_SAT" );
    else if ( Status == -1 )
        fprintf( pFile, "snl_UNK" );
    else 
        printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" );
    fprintf( pFile, " " );
    // write <bug_free_depth>
    fprintf( pFile, "%d", nFrames );
    fprintf( pFile, " " );
    // write <engine_name>
    fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
    if ( pCex && Status == 0 )
        fprintf( pFile, " %d", pCex->iPo );
    // write <cyc>
    if ( pCex && pCex->iFrame != nFrames )
        fprintf( pFile, " %d", pCex->iFrame );
    fprintf( pFile, "\n" );
    // write <INIT_STATE>
    if ( pCex == NULL )
        fprintf( pFile, "NULL" );
    else
    {
        for ( i = 0; i < pCex->nRegs; i++ )
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
    }
    fprintf( pFile, "\n" );
    // write <TRACE>
    if ( pCex == NULL )
        fprintf( pFile, "NULL" );
    else
    {
        assert( pCex->nBits - pCex->nRegs == pCex->nPis * (pCex->iFrame + 1) );
        for ( i = pCex->nRegs; i < pCex->nBits; i++ )
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
    }
    fprintf( pFile, "\n" );
    fclose( pFile );
}