xsatCnfReader.c

Go to the documentation of this file.

#include <ctype.h>
 
#include "misc/util/abc_global.h"
#include "misc/vec/vecInt.h"
 
#include "xsatSolver.h"
 
ABC_NAMESPACE_IMPL_START


char * xSAT_FileRead( FILE * pFile )
{
    int nFileSize;
    char * pBuffer;
    int RetValue;
    // get the file size, in bytes
    fseek( pFile, 0, SEEK_END );
    nFileSize = ftell( pFile );
    // move the file current reading position to the beginning
    rewind( pFile );
    // load the contents of the file into memory
    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
    RetValue = fread( pBuffer, nFileSize, 1, pFile );
    // terminate the string with '\0'
    pBuffer[ nFileSize + 0] = '\n';
    pBuffer[ nFileSize + 1] = '\0';
    return pBuffer;
}

static void skipLine( char ** pIn )
{
    while ( 1 )
    {
        if (**pIn == 0)
            return;
        if (**pIn == '\n')
        {
            (*pIn)++;
            return;
        }
        (*pIn)++;
    }
}

static int xSAT_ReadInt( char ** pIn )
{
    int val = 0;
    int neg = 0;
 
    for(; isspace(**pIn); (*pIn)++);
    if ( **pIn == '-' )
        neg = 1,
        (*pIn)++;
    else if ( **pIn == '+' )
        (*pIn)++;
    if ( !isdigit(**pIn) )
        fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn),
        exit(1);
    while ( isdigit(**pIn) )
        val = val*10 + (**pIn - '0'),
        (*pIn)++;
    return neg ? -val : val;
}

static void xSAT_ReadClause( char ** pIn, xSAT_Solver_t * p, Vec_Int_t * vLits )
{
    int token, var, sign;
 
    Vec_IntClear( vLits );
    while ( 1 )
    {
        token = xSAT_ReadInt( pIn );
        if ( token == 0 )
            break;
        var = abs(token) - 1;
        sign = (token > 0);
        Vec_IntPush( vLits, xSAT_Var2Lit( var, !sign ) );
    }
}

static int xSAT_ParseDimacs( char * pText, xSAT_Solver_t ** pS )
{
    xSAT_Solver_t * p = NULL;
    Vec_Int_t * vLits = NULL;
    char * pIn = pText;
    int nVars, nClas;
    while ( 1 )
    {
        for(; isspace(*pIn); pIn++);
        if ( *pIn == 0 )
            break;
        else if ( *pIn == 'c' )
            skipLine( &pIn );
        else if ( *pIn == 'p' )
        {
            pIn++;
            for(; isspace(*pIn); pIn++);
            for(; !isspace(*pIn); pIn++);
 
            nVars = xSAT_ReadInt( &pIn );
            nClas = xSAT_ReadInt( &pIn );
            skipLine( &pIn );
 
            /* start the solver */
            p = xSAT_SolverCreate();
            /* allocate the vector */
            vLits = Vec_IntAlloc( nVars );
        }
        else
        {
            if ( p == NULL )
            {
                printf( "There is no parameter line.\n" );
                exit(1);
            }
            xSAT_ReadClause( &pIn, p, vLits );
            if ( !xSAT_SolverAddClause( p, vLits ) )
            {
                Vec_IntPrint(vLits);
                return 0;
            }
        }
    }
    Vec_IntFree( vLits );
    *pS = p;
    return xSAT_SolverSimplify( p );
}

int xSAT_SolverParseDimacs( FILE * pFile, xSAT_Solver_t ** p )
{
    char * pText;
    int  Value;
    pText = xSAT_FileRead( pFile );
    Value = xSAT_ParseDimacs( pText, p );
    ABC_FREE( pText );
    return Value;
}
 
ABC_NAMESPACE_IMPL_END