/**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