abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
msatRead.c File Reference
#include "msatInt.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START char * 		Msat_FileRead (FILE *pFile)
 DECLARATIONS ///. More...
 
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 int Msat_ReadDimacs (char *pText, Msat_Solver_t **pS, int fVerbose)
 
int Msat_SolverParseDimacs (FILE *pFile, Msat_Solver_t **p, int fVerbose)
 GLOBAL VARIABLES ///. More...
 

Function Documentation

char * Msat_FileRead ( FILE *  pFile)
static

DECLARATIONS ///.

FUNCTION DEFINITIONS ///.

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 alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

]

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

Synopsis [Read the file into the internal buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatRead.c.

48 {
49  int nFileSize;
50  char * pBuffer;
51  int RetValue;
52  // get the file size, in bytes
53  fseek( pFile, 0, SEEK_END );
54  nFileSize = ftell( pFile );
55  // move the file current reading position to the beginning
56  rewind( pFile );
57  // load the contents of the file into memory
58  pBuffer = ABC_ALLOC( char, nFileSize + 3 );
59  RetValue = fread( pBuffer, nFileSize, 1, pFile );
60  // terminate the string with '\0'
61  pBuffer[ nFileSize + 0] = '\n';
62  pBuffer[ nFileSize + 1] = '\0';
63  return pBuffer;
64 }
SEEK_END
#define SEEK_END
Definition: zconf.h:392
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
rewind
VOID_HACK rewind()
static void Msat_ReadClause ( char **  pIn,
Msat_Solver_t *  p,
Msat_IntVec_t *  pLits 
)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file msatRead.c.

169 {
170  int nVars = Msat_SolverReadVarNum( p );
171  int parsed_lit, var, sign;
172 
173  Msat_IntVecClear( pLits );
174  while ( 1 )
175  {
176  parsed_lit = Msat_ReadInt(pIn);
177  if ( parsed_lit == 0 )
178  break;
179  var = abs(parsed_lit) - 1;
180  sign = (parsed_lit > 0);
181  if ( var >= nVars )
182  {
183  printf( "Variable %d is larger than the number of allocated variables (%d).\n", var+1, nVars );
184  exit(1);
185  }
186  Msat_IntVecPush( pLits, MSAT_VAR2LIT(var, !sign) );
187  }
188 }
exit
VOID_HACK exit()
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
Minisat::sign
bool sign(Lit p)
Definition: SolverTypes.h:61
Msat_IntVecPush
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:351
Msat_ReadInt
static int Msat_ReadInt(char **pIn)
Definition: msatRead.c:137
Msat_SolverReadVarNum
int Msat_SolverReadVarNum(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSolverApi.c:47
MSAT_VAR2LIT
#define MSAT_VAR2LIT(v, s)
Definition: msat.h:56
static int Msat_ReadDimacs ( char *  pText,
Msat_Solver_t **  pS,
int  fVerbose 
)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file msatRead.c.

202 {
203  Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized"
204  Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized"
205  char * pIn = pText;
206  int nVars, nClas;
207  while ( 1 )
208  {
209  Msat_ReadWhitespace( &pIn );
210  if ( *pIn == 0 )
211  break;
212  else if ( *pIn == 'c' )
213  skipLine( &pIn );
214  else if ( *pIn == 'p' )
215  {
216  pIn++;
217  Msat_ReadWhitespace( &pIn );
218  Msat_ReadNotWhitespace( &pIn );
219 
220  nVars = Msat_ReadInt( &pIn );
221  nClas = Msat_ReadInt( &pIn );
222  skipLine( &pIn );
223  // start the solver
224  p = Msat_SolverAlloc( nVars, 1, 1, 1, 1, 0 );
225  Msat_SolverClean( p, nVars );
226  Msat_SolverSetVerbosity( p, fVerbose );
227  // allocate the vector
228  pLits = Msat_IntVecAlloc( nVars );
229  }
230  else
231  {
232  if ( p == NULL )
233  {
234  printf( "There is no parameter line.\n" );
235  exit(1);
236  }
237  Msat_ReadClause( &pIn, p, pLits );
238  if ( !Msat_SolverAddClause( p, pLits ) )
239  return 0;
240  }
241  }
242  Msat_IntVecFree( pLits );
243  *pS = p;
244  return Msat_SolverSimplifyDB( p );
245 }
exit
VOID_HACK exit()
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_SolverAddClause
int Msat_SolverAddClause(Msat_Solver_t *p, Msat_IntVec_t *pLits)
Definition: msatSolverCore.c:65
Msat_ReadWhitespace
static void Msat_ReadWhitespace(char **pIn)
Definition: msatRead.c:77
Msat_IntVec_t_
Definition: msatInt.h:162
Msat_SolverSimplifyDB
int Msat_SolverSimplifyDB(Msat_Solver_t *p)
Definition: msatSolverSearch.c:282
Msat_SolverAlloc
Msat_Solver_t * Msat_SolverAlloc(int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose)
Definition: msatSolverApi.c:154
Msat_ReadNotWhitespace
static void Msat_ReadNotWhitespace(char **pIn)
Definition: msatRead.c:94
Msat_ReadInt
static int Msat_ReadInt(char **pIn)
Definition: msatRead.c:137
skipLine
static void skipLine(char **pIn)
Definition: msatRead.c:111
Msat_IntVecAlloc
Msat_IntVec_t * Msat_IntVecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: msatVec.c:48
Msat_IntVecFree
void Msat_IntVecFree(Msat_IntVec_t *p)
Definition: msatVec.c:160
Msat_ReadClause
static void Msat_ReadClause(char **pIn, Msat_Solver_t *p, Msat_IntVec_t *pLits)
Definition: msatRead.c:168
Msat_SolverSetVerbosity
void Msat_SolverSetVerbosity(Msat_Solver_t *p, int fVerbose)
Definition: msatSolverApi.c:63
Msat_SolverClean
void Msat_SolverClean(Msat_Solver_t *p, int nVars)
Definition: msatSolverApi.c:307
Msat_Solver_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
static int Msat_ReadInt ( char **  pIn)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file msatRead.c.

138 {
139  int val = 0;
140  int neg = 0;
141 
142  Msat_ReadWhitespace( pIn );
143  if ( **pIn == '-' )
144  neg = 1,
145  (*pIn)++;
146  else if ( **pIn == '+' )
147  (*pIn)++;
148  if ( **pIn < '0' || **pIn > '9' )
149  fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn),
150  exit(1);
151  while ( **pIn >= '0' && **pIn <= '9' )
152  val = val*10 + (**pIn - '0'),
153  (*pIn)++;
154  return neg ? -val : val;
155 }
exit
VOID_HACK exit()
Msat_ReadWhitespace
static void Msat_ReadWhitespace(char **pIn)
Definition: msatRead.c:77
static void Msat_ReadNotWhitespace ( char **  pIn)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file msatRead.c.

95 {
96  while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) )
97  (*pIn)++;
98 }
static void Msat_ReadWhitespace ( char **  pIn)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file msatRead.c.

78 {
79  while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32)
80  (*pIn)++;
81 }
int Msat_SolverParseDimacs ( FILE *  pFile,
Msat_Solver_t **  p,
int  fVerbose 
)

GLOBAL VARIABLES ///.

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

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

Description [Returns FALSE upon immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 258 of file msatRead.c.

259 {
260  char * pText;
261  int Value;
262  pText = Msat_FileRead( pFile );
263  Value = Msat_ReadDimacs( pText, p, fVerbose );
264  ABC_FREE( pText );
265  return Value;
266 }
Msat_FileRead
static ABC_NAMESPACE_IMPL_START char * Msat_FileRead(FILE *pFile)
DECLARATIONS ///.
Definition: msatRead.c:47
Msat_ReadDimacs
static int Msat_ReadDimacs(char *pText, Msat_Solver_t **pS, int fVerbose)
Definition: msatRead.c:201
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void skipLine ( char **  pIn)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file msatRead.c.

112 {
113  while ( 1 )
114  {
115  if (**pIn == 0)
116  return;
117  if (**pIn == '\n')
118  {
119  (*pIn)++;
120  return;
121  }
122  (*pIn)++;
123  }
124 }