diff options
Diffstat (limited to 'src/sat/xsat/xsatCnfReader.c')
| -rw-r--r-- | src/sat/xsat/xsatCnfReader.c | 236 |
1 files changed, 236 insertions, 0 deletions
diff --git a/src/sat/xsat/xsatCnfReader.c b/src/sat/xsat/xsatCnfReader.c new file mode 100644 index 00000000..d23e8a0a --- /dev/null +++ b/src/sat/xsat/xsatCnfReader.c @@ -0,0 +1,236 @@ +/**CFile**************************************************************** + + FileName [xsatCnfReader.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [CNF DIMACS file format parser.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <ctype.h> + +#include "misc/util/abc_global.h" +#include "misc/vec/vecInt.h" + +#include "xsatSolver.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Read the file into the internal buffer.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void skipLine( char ** pIn ) +{ + while ( 1 ) + { + if (**pIn == 0) + return; + if (**pIn == '\n') + { + (*pIn)++; + return; + } + (*pIn)++; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); +} + +/**Function************************************************************* + + Synopsis [Starts the solver and reads the DIMAC file.] + + Description [Returns FALSE upon immediate conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// |