abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatRead.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatRead.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [The reader of the CNF formula in DIMACS format.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatRead.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static char * Msat_FileRead( FILE * pFile );
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38  Synopsis [Read the file into the internal buffer.]
39 
40  Description []
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
47 char * Msat_FileRead( FILE * pFile )
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 }
65 
66 /**Function*************************************************************
67 
68  Synopsis []
69 
70  Description []
71 
72  SideEffects []
73 
74  SeeAlso []
75 
76 ***********************************************************************/
77 static void Msat_ReadWhitespace( char ** pIn )
78 {
79  while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32)
80  (*pIn)++;
81 }
82 
83 /**Function*************************************************************
84 
85  Synopsis []
86 
87  Description []
88 
89  SideEffects []
90 
91  SeeAlso []
92 
93 ***********************************************************************/
94 static void Msat_ReadNotWhitespace( char ** pIn )
95 {
96  while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) )
97  (*pIn)++;
98 }
99 
100 /**Function*************************************************************
101 
102  Synopsis []
103 
104  Description []
105 
106  SideEffects []
107 
108  SeeAlso []
109 
110 ***********************************************************************/
111 static void skipLine( char ** pIn )
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 }
125 
126 /**Function*************************************************************
127 
128  Synopsis []
129 
130  Description []
131 
132  SideEffects []
133 
134  SeeAlso []
135 
136 ***********************************************************************/
137 static int Msat_ReadInt( char ** pIn )
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 }
156 
157 /**Function*************************************************************
158 
159  Synopsis []
160 
161  Description []
162 
163  SideEffects []
164 
165  SeeAlso []
166 
167 ***********************************************************************/
168 static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLits )
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 }
189 
190 /**Function*************************************************************
191 
192  Synopsis []
193 
194  Description []
195 
196  SideEffects []
197 
198  SeeAlso []
199 
200 ***********************************************************************/
201 static int Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, int fVerbose )
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 }
246 
247 /**Function*************************************************************
248 
249  Synopsis [Starts the solver and reads the DIMAC file.]
250 
251  Description [Returns FALSE upon immediate conflict.]
252 
253  SideEffects []
254 
255  SeeAlso []
256 
257 ***********************************************************************/
258 int Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
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 }
267 
268 ////////////////////////////////////////////////////////////////////////
269 /// END OF FILE ///
270 ////////////////////////////////////////////////////////////////////////
271 
272 
273 ABC_NAMESPACE_IMPL_END
274 
exit
VOID_HACK exit()
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
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
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
SEEK_END
#define SEEK_END
Definition: zconf.h:392
Msat_IntVec_t_
Definition: msatInt.h:162
Msat_SolverSimplifyDB
int Msat_SolverSimplifyDB(Msat_Solver_t *p)
Definition: msatSolverSearch.c:282
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Minisat::sign
bool sign(Lit p)
Definition: SolverTypes.h:61
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_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
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
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
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
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
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Msat_SolverClean
void Msat_SolverClean(Msat_Solver_t *p, int nVars)
Definition: msatSolverApi.c:307
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
Msat_SolverParseDimacs
int Msat_SolverParseDimacs(FILE *pFile, Msat_Solver_t **p, int fVerbose)
GLOBAL VARIABLES ///.
Definition: msatRead.c:258
rewind
VOID_HACK rewind()
Msat_Solver_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42