| /**CFile**************************************************************** |
| |
| FileName [msatRead.c] |
| |
| PackageName [A C version of SAT solver MINISAT, originally developed |
| in C++ by Niklas Een and Niklas Sorensson, Chalmers University of |
| Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] |
| |
| Synopsis [The reader of the CNF formula in DIMACS format.] |
| |
| Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - January 1, 2004.] |
| |
| Revision [$Id: msatRead.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "msatInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static char * Msat_FileRead( FILE * pFile ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Read the file into the internal buffer.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| char * Msat_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 Msat_ReadWhitespace( char ** pIn ) |
| { |
| while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32) |
| (*pIn)++; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static void Msat_ReadNotWhitespace( char ** pIn ) |
| { |
| while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) ) |
| (*pIn)++; |
| } |
| |
| /**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 Msat_ReadInt( char ** pIn ) |
| { |
| int val = 0; |
| int neg = 0; |
| |
| Msat_ReadWhitespace( pIn ); |
| if ( **pIn == '-' ) |
| neg = 1, |
| (*pIn)++; |
| else if ( **pIn == '+' ) |
| (*pIn)++; |
| if ( **pIn < '0' || **pIn > '9' ) |
| fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn), |
| exit(1); |
| while ( **pIn >= '0' && **pIn <= '9' ) |
| val = val*10 + (**pIn - '0'), |
| (*pIn)++; |
| return neg ? -val : val; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLits ) |
| { |
| int nVars = Msat_SolverReadVarNum( p ); |
| int parsed_lit, var, sign; |
| |
| Msat_IntVecClear( pLits ); |
| while ( 1 ) |
| { |
| parsed_lit = Msat_ReadInt(pIn); |
| if ( parsed_lit == 0 ) |
| break; |
| var = abs(parsed_lit) - 1; |
| sign = (parsed_lit > 0); |
| if ( var >= nVars ) |
| { |
| printf( "Variable %d is larger than the number of allocated variables (%d).\n", var+1, nVars ); |
| exit(1); |
| } |
| Msat_IntVecPush( pLits, MSAT_VAR2LIT(var, !sign) ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static int Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, int fVerbose ) |
| { |
| Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized" |
| Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized" |
| char * pIn = pText; |
| int nVars, nClas; |
| while ( 1 ) |
| { |
| Msat_ReadWhitespace( &pIn ); |
| if ( *pIn == 0 ) |
| break; |
| else if ( *pIn == 'c' ) |
| skipLine( &pIn ); |
| else if ( *pIn == 'p' ) |
| { |
| pIn++; |
| Msat_ReadWhitespace( &pIn ); |
| Msat_ReadNotWhitespace( &pIn ); |
| |
| nVars = Msat_ReadInt( &pIn ); |
| nClas = Msat_ReadInt( &pIn ); |
| skipLine( &pIn ); |
| // start the solver |
| p = Msat_SolverAlloc( nVars, 1, 1, 1, 1, 0 ); |
| Msat_SolverClean( p, nVars ); |
| Msat_SolverSetVerbosity( p, fVerbose ); |
| // allocate the vector |
| pLits = Msat_IntVecAlloc( nVars ); |
| } |
| else |
| { |
| if ( p == NULL ) |
| { |
| printf( "There is no parameter line.\n" ); |
| exit(1); |
| } |
| Msat_ReadClause( &pIn, p, pLits ); |
| if ( !Msat_SolverAddClause( p, pLits ) ) |
| return 0; |
| } |
| } |
| Msat_IntVecFree( pLits ); |
| *pS = p; |
| return Msat_SolverSimplifyDB( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Starts the solver and reads the DIMAC file.] |
| |
| Description [Returns FALSE upon immediate conflict.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) |
| { |
| char * pText; |
| int Value; |
| pText = Msat_FileRead( pFile ); |
| Value = Msat_ReadDimacs( pText, p, fVerbose ); |
| ABC_FREE( pText ); |
| return Value; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
