src/sat/msat/msatRead.c File Reference

#include "msatInt.h"

Include dependency graph for msatRead.c:

Go to the source code of this file.

Functions
static char *	Msat_FileRead (FILE *pFile)
static void	Msat_ReadWhitespace (char **pIn)
static void	Msat_ReadNotWhitespace (char **pIn)
static void	skipLine (char **pIn)
static int	Msat_ReadInt (char **pIn)
static void	Msat_ReadClause (char **pIn, Msat_Solver_t *p, Msat_IntVec_t *pLits)
static bool	Msat_ReadDimacs (char *pText, Msat_Solver_t **pS, bool fVerbose)
bool	Msat_SolverParseDimacs (FILE *pFile, Msat_Solver_t **p, int fVerbose)

---

Function Documentation

char * Msat_FileRead

(

FILE *

pFile

)

[static]

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

] DECLARATIONS ///

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Read the file into the internal buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file msatRead.c.

{
    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;
}

static void Msat_ReadClause	(	char **	pIn,
		Msat_Solver_t *	p,
		Msat_IntVec_t *	pLits
	)			[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file msatRead.c.

{
    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) );
    }
}

static bool Msat_ReadDimacs	(	char *	pText,
		Msat_Solver_t **	pS,
		bool	fVerbose
	)			[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file msatRead.c.

{
    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 );
}

static int Msat_ReadInt

(

char **

pIn

)

[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file msatRead.c.

{
    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; 
}

static void Msat_ReadNotWhitespace

(

char **

pIn

)

[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file msatRead.c.

{
    while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) )
        (*pIn)++; 
}

static void Msat_ReadWhitespace

(

char **

pIn

)

[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file msatRead.c.

{
    while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32)
        (*pIn)++; 
}

bool Msat_SolverParseDimacs	(	FILE *	pFile,
		Msat_Solver_t **	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Starts the solver and reads the DIMAC file.]

Description [Returns FALSE upon immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 254 of file msatRead.c.

{
    char * pText;
    bool Value;
    pText = Msat_FileRead( pFile );
    Value = Msat_ReadDimacs( pText, p, fVerbose );
    free( pText );
    return Value;
}

static void skipLine

(

char **

pIn

)

[static]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file msatRead.c.

{
    while ( 1 )
    {
        if (**pIn == 0) 
            return;
        if (**pIn == '\n') 
        { 
            (*pIn)++; 
            return; 
        }
        (*pIn)++; 
    } 
}