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