diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/sat/msat/msatRead.c | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/sat/msat/msatRead.c')
-rw-r--r-- | src/sat/msat/msatRead.c | 268 |
1 files changed, 0 insertions, 268 deletions
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c deleted file mode 100644 index 738562ef..00000000 --- a/src/sat/msat/msatRead.c +++ /dev/null @@ -1,268 +0,0 @@ -/**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" - -//////////////////////////////////////////////////////////////////////// -/// 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; - // 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 = ALLOC( char, nFileSize + 3 ); - 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; - bool 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 bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) -{ - Msat_Solver_t * p; - Msat_IntVec_t * pLits; - 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 [] - -***********************************************************************/ -bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ) -{ - char * pText; - bool Value; - pText = Msat_FileRead( pFile ); - Value = Msat_ReadDimacs( pText, p, fVerbose ); - free( pText ); - return Value; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |