abcLog.c 6.87 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**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 $]

***********************************************************************/

21 22
#include "src/base/abc/abc.h"
#include "src/aig/gia/gia.h"
23 24 25 26 27 28 29 30 31

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

/*
32
    Log file format (Jiang, Mon, 28 Sep 2009;  updated by Alan in Jan 2011)
33

34 35 36
    <result> <bug_free_depth>  <engine_name> <0-based_output_num> <0-based_frame>
    <INIT_STATE> : default is empty line.
    <TRACE> : default is empty line
37
   
38 39 40 41
    <result> is one of the following: "snl_SAT", "snl_UNSAT", "snl_UNK", "snl_ABORT".
    <bug_free_depth> is the number of timeframes exhaustively explored without counter-examples
    <0-based_output_num> only need to be given if the problem is SAT.
    <0-based_frame> only need to be given if the problem is SAT and <0-based_frame> is different from <bug_free_depth>.   
42 43
    <INIT_STATE>  : initial state
    <TRACE> : input vector
44

45 46 47
    <INIT_STATE>and <TRACE> are strings of 0/1/- ( - means don't care). The length is equivalent to #input*#<cyc>.
*/

48 49 50 51 52

         



53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
68
void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand )
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
{
    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, " " );
88 89
    // write <bug_free_depth>
    fprintf( pFile, "%d", nFrames );
90 91 92
    fprintf( pFile, " " );
    // write <engine_name>
    fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
93 94
    if ( Status == 0 )
        fprintf( pFile, " %d", pCex->iPo );
95 96 97
    // write <cyc>
    if ( pCex && pCex->iFrame != nFrames )
        fprintf( pFile, " %d", pCex->iFrame );
98 99 100 101 102 103 104
    fprintf( pFile, "\n" );
    // write <INIT_STATE>
    if ( pCex == NULL )
        fprintf( pFile, "NULL" );
    else
    {
        for ( i = 0; i < pCex->nRegs; i++ )
105
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
106 107 108 109 110 111 112 113 114
    }
    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++ )
115
            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
    }
    fprintf( pFile, "\n" );
    fclose( pFile );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
132
int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
133
{
134
    FILE * pFile;
135 136
    Abc_Cex_t * pCex;
    Vec_Int_t * vNums;
137
    char Buffer[1000], * pToken, * RetValue;
138
    int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1, nFrames2 = -1;
139 140 141 142 143 144
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
        return -1;
    }
145
    RetValue = fgets( Buffer, 1000, pFile );
146 147 148 149 150 151 152 153
    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;
154 155 156 157 158 159
//        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" );
        iPo     = atoi( pToken ); 
160 161 162
        pToken  = strtok( NULL, " \t\n" );
        if ( pToken )
            nFrames2 = atoi( pToken ); 
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
    }
    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) )
    {
192
        int iFrameCex = (nFrames2 == -1) ? nFrames : nFrames2;
193
        if ( nRegs < 0 )
194 195 196 197 198 199 200 201 202
        {
            printf( "Cannot read register number.\n" );
            return -1;
        }
        if ( Vec_IntSize(vNums)-nRegs == 0 )
        {
            printf( "Cannot read counter example.\n" );
            return -1;
        }
203
        if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
204 205 206 207
        {
            printf( "Incorrect number of bits.\n" );
            return -1;
        }
208
        pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 );
209
        pCex->iPo    = iPo;
210
        pCex->iFrame = iFrameCex;
211 212 213
        assert( Vec_IntSize(vNums) == pCex->nBits );
        for ( c = 0; c < pCex->nBits; c++ )
            if ( Vec_IntEntry(vNums, c) )
214
                Abc_InfoSetBit( pCex->pData, c );
215 216 217 218 219 220
        Vec_IntFree( vNums );
        if ( ppCex )
            *ppCex = pCex;
        else
            ABC_FREE( pCex );
    }
221 222
    if ( pnFrames )
        *pnFrames = nFrames;
223 224 225 226 227 228 229 230 231 232
    return Status;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END