1 /**CFile****************************************************************
2
3 FileNameIn [parseCore.c]
4
5 PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
6
7 Synopsis [Boolean formula parser.]
8
9 Author [MVSIS Group]
10
11 Affiliation [UC Berkeley]
12
13 Date [Ver. 1.0. Started - February 1, 2003.]
14
15 Revision [$Id: parseCore.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
16
17 ***********************************************************************/
18
19 /*
20 Some aspects of Boolean Formula Parser:
21
22 1) The names in the boolean formulas can be any strings of symbols
23 that start with char or underscore and contain chars, digits
24 and underscores: For example: 1) a&b <+> c'&d => a + b;
25 2) a1 b2 c3' dummy' + (a2+b2')c3 dummy
26 2) Constant values 0 and 1 can be used just like normal variables
27 3) Any boolean operator (listed below) and parentheses can be used
28 any number of times provided there are equal number of opening
29 and closing parentheses.
30 4) By default, absence of an operator between vars and before and
31 after parentheses is taken for AND.
32 5) Both complementation prefix and complementation suffix can be
33 used at the same time (but who needs this?)
34 6) Spaces (tabs, end-of-lines) may be inserted anywhere,
35 except between characters of the operations: <=>, =>, <=, <+>
36 7) The stack size is defined by macro STACKSIZE and is used by the
37 stack constructor.
38 */
39
40 ////////////////////////////////////////////////////////////////////////
41 /// DECLARATIONS ///
42 ////////////////////////////////////////////////////////////////////////
43
44 #include "parseInt.h"
45
46 ABC_NAMESPACE_IMPL_START
47
48
49 // the list of operation symbols to be used in expressions
50 #define PARSE_SYM_OPEN '(' // opening parenthesis
51 #define PARSE_SYM_CLOSE ')' // closing parenthesis
52 #define PARSE_SYM_LOWER '[' // shifts one rank down
53 #define PARSE_SYM_RAISE ']' // shifts one rank up
54 #define PARSE_SYM_CONST0 '0' // constant 0
55 #define PARSE_SYM_CONST1 '1' // constant 1
56 #define PARSE_SYM_NEGBEF1 '!' // negation before the variable
57 #define PARSE_SYM_NEGBEF2 '~' // negation before the variable
58 #define PARSE_SYM_NEGAFT '\'' // negation after the variable
59 #define PARSE_SYM_AND1 '&' // logic AND
60 #define PARSE_SYM_AND2 '*' // logic AND
61 #define PARSE_SYM_XOR1 '<' // logic EXOR (the 1st symbol)
62 #define PARSE_SYM_XOR2 '+' // logic EXOR (the 2nd symbol)
63 #define PARSE_SYM_XOR3 '>' // logic EXOR (the 3rd symbol)
64 #define PARSE_SYM_XOR '^' // logic XOR
65 #define PARSE_SYM_OR1 '+' // logic OR
66 #define PARSE_SYM_OR2 '|' // logic OR
67 #define PARSE_SYM_EQU1 '<' // equvalence (the 1st symbol)
68 #define PARSE_SYM_EQU2 '=' // equvalence (the 2nd symbol)
69 #define PARSE_SYM_EQU3 '>' // equvalence (the 3rd symbol)
70 #define PARSE_SYM_FLR1 '=' // implication (the 1st symbol)
71 #define PARSE_SYM_FLR2 '>' // implication (the 2nd symbol)
72 #define PARSE_SYM_FLL1 '<' // backward imp (the 1st symbol)
73 #define PARSE_SYM_FLL2 '=' // backward imp (the 2nd symbol)
74 // PARSE_SYM_FLR1 and PARSE_SYM_FLR2 should be the same as PARSE_SYM_EQU2 and PARSE_SYM_EQU3!
75
76 // the list of opcodes (also specifying operation precedence)
77 #define PARSE_OPER_NEG 10 // negation
78 #define PARSE_OPER_AND 9 // logic AND
79 #define PARSE_OPER_XOR 8 // logic EXOR (a'b | ab')
80 #define PARSE_OPER_OR 7 // logic OR
81 #define PARSE_OPER_EQU 6 // equvalence (a'b'| ab )
82 #define PARSE_OPER_FLR 5 // implication ( a' | b )
83 #define PARSE_OPER_FLL 4 // backward imp ( 'b | a )
84 #define PARSE_OPER_MARK 1 // OpStack token standing for an opening parenthesis
85
86 // these are values of the internal Flag
87 #define PARSE_FLAG_START 1 // after the opening parenthesis
88 #define PARSE_FLAG_VAR 2 // after operation is received
89 #define PARSE_FLAG_OPER 3 // after operation symbol is received
90 #define PARSE_FLAG_ERROR 4 // when error is detected
91
92 #define STACKSIZE 1000
93
94 static DdNode * Parse_ParserPerformTopOp( DdManager * dd, Parse_StackFn_t * pStackFn, int Oper );
95
96 ////////////////////////////////////////////////////////////////////////
97 /// FUNCTION DEFINITIONS ///
98 ////////////////////////////////////////////////////////////////////////
99
100 /**Function*************************************************************
101
102 Synopsis [Derives the BDD corresponding to the formula in language L.]
103
104 Description [Takes the stream to output messages, the formula, the number
105 variables and the rank in the formula. The array of variable names is also
106 given. The BDD manager and the elementary 0-rank variable are the last two
107 arguments. The manager should have at least as many variables as
108 nVars * (nRanks + 1). The 0-rank variables should have numbers larger
109 than the variables of other ranks.]
110
111 SideEffects []
112
113 SeeAlso []
114
115 ***********************************************************************/
Parse_FormulaParser(FILE * pOutput,char * pFormulaInit,int nVars,int nRanks,char * ppVarNames[],DdManager * dd,DdNode * pbVars[])116 DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, int nRanks,
117 char * ppVarNames[], DdManager * dd, DdNode * pbVars[] )
118 {
119 char * pFormula;
120 Parse_StackFn_t * pStackFn;
121 Parse_StackOp_t * pStackOp;
122 DdNode * bFunc, * bTemp;
123 char * pTemp;
124 int nParans, fFound, Flag;
125 int Oper, Oper1, Oper2;
126 int i, fLower;
127 int v = -1; // Suppress "might be used uninitialized"
128
129 // make sure that the number of vars and ranks is correct
130 if ( nVars * (nRanks + 1) > dd->size )
131 {
132 printf( "Parse_FormulaParser(): The BDD manager does not have enough variables.\n" );
133 return NULL;
134 }
135
136 // make sure that the number of opening and closing parentheses is the same
137 nParans = 0;
138 for ( pTemp = pFormulaInit; *pTemp; pTemp++ )
139 if ( *pTemp == '(' )
140 nParans++;
141 else if ( *pTemp == ')' )
142 nParans--;
143 if ( nParans != 0 )
144 {
145 fprintf( pOutput, "Parse_FormulaParser(): Different number of opening and closing parentheses ().\n" );
146 return NULL;
147 }
148
149 nParans = 0;
150 for ( pTemp = pFormulaInit; *pTemp; pTemp++ )
151 if ( *pTemp == '[' )
152 nParans++;
153 else if ( *pTemp == ']' )
154 nParans--;
155 if ( nParans != 0 )
156 {
157 fprintf( pOutput, "Parse_FormulaParser(): Different number of opening and closing brackets [].\n" );
158 return NULL;
159 }
160
161 // copy the formula
162 pFormula = ABC_ALLOC( char, strlen(pFormulaInit) + 3 );
163 sprintf( pFormula, "(%s)", pFormulaInit );
164
165 // start the stacks
166 pStackFn = Parse_StackFnStart( STACKSIZE );
167 pStackOp = Parse_StackOpStart( STACKSIZE );
168
169 Flag = PARSE_FLAG_START;
170 fLower = 0;
171 for ( pTemp = pFormula; *pTemp; pTemp++ )
172 {
173 switch ( *pTemp )
174 {
175 // skip all spaces, tabs, and end-of-lines
176 case ' ':
177 case '\t':
178 case '\r':
179 case '\n':
180 continue;
181
182 // treat Constant 0 as a variable
183 case PARSE_SYM_CONST0:
184 Parse_StackFnPush( pStackFn, b0 ); Cudd_Ref( b0 );
185 if ( Flag == PARSE_FLAG_VAR )
186 {
187 fprintf( pOutput, "Parse_FormulaParser(): No operation symbol before constant 0.\n" );
188 Flag = PARSE_FLAG_ERROR;
189 break;
190 }
191 Flag = PARSE_FLAG_VAR;
192 break;
193
194 // the same for Constant 1
195 case PARSE_SYM_CONST1:
196 Parse_StackFnPush( pStackFn, b1 ); Cudd_Ref( b1 );
197 if ( Flag == PARSE_FLAG_VAR )
198 {
199 fprintf( pOutput, "Parse_FormulaParser(): No operation symbol before constant 1.\n" );
200 Flag = PARSE_FLAG_ERROR;
201 break;
202 }
203 Flag = PARSE_FLAG_VAR;
204 break;
205
206 case PARSE_SYM_NEGBEF1:
207 case PARSE_SYM_NEGBEF2:
208 if ( Flag == PARSE_FLAG_VAR )
209 {// if NEGBEF follows a variable, AND is assumed
210 Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
211 Flag = PARSE_FLAG_OPER;
212 }
213 Parse_StackOpPush( pStackOp, PARSE_OPER_NEG );
214 break;
215
216 case PARSE_SYM_NEGAFT:
217 if ( Flag != PARSE_FLAG_VAR )
218 {// if there is no variable before NEGAFT, it is an error
219 fprintf( pOutput, "Parse_FormulaParser(): No variable is specified before the negation suffix.\n" );
220 Flag = PARSE_FLAG_ERROR;
221 break;
222 }
223 else // if ( Flag == PARSE_FLAG_VAR )
224 Parse_StackFnPush( pStackFn, Cudd_Not( Parse_StackFnPop(pStackFn) ) );
225 break;
226
227 case PARSE_SYM_AND1:
228 case PARSE_SYM_AND2:
229 case PARSE_SYM_OR1:
230 case PARSE_SYM_OR2:
231 case PARSE_SYM_XOR:
232 if ( Flag != PARSE_FLAG_VAR )
233 {
234 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR.\n" );
235 Flag = PARSE_FLAG_ERROR;
236 break;
237 }
238 if ( *pTemp == PARSE_SYM_AND1 || *pTemp == PARSE_SYM_AND2 )
239 Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
240 else if ( *pTemp == PARSE_SYM_OR1 || *pTemp == PARSE_SYM_OR2 )
241 Parse_StackOpPush( pStackOp, PARSE_OPER_OR );
242 else //if ( Str[Pos] == PARSE_SYM_XOR )
243 Parse_StackOpPush( pStackOp, PARSE_OPER_XOR );
244 Flag = PARSE_FLAG_OPER;
245 break;
246
247 case PARSE_SYM_EQU1:
248 if ( Flag != PARSE_FLAG_VAR )
249 {
250 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before Equivalence or Implication\n" );
251 Flag = PARSE_FLAG_ERROR; break;
252 }
253 if ( pTemp[1] == PARSE_SYM_EQU2 )
254 { // check what is the next symbol in the string
255 pTemp++;
256 if ( pTemp[1] == PARSE_SYM_EQU3 )
257 {
258 pTemp++;
259 Parse_StackOpPush( pStackOp, PARSE_OPER_EQU );
260 }
261 else
262 {
263 Parse_StackOpPush( pStackOp, PARSE_OPER_FLL );
264 }
265 }
266 else if ( pTemp[1] == PARSE_SYM_XOR2 )
267 {
268 pTemp++;
269 if ( pTemp[1] == PARSE_SYM_XOR3 )
270 {
271 pTemp++;
272 Parse_StackOpPush( pStackOp, PARSE_OPER_XOR );
273 }
274 else
275 {
276 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c%c\"\n", PARSE_SYM_EQU1, PARSE_SYM_XOR2 );
277 Flag = PARSE_FLAG_ERROR;
278 break;
279 }
280 }
281 else
282 {
283 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c\"\n", PARSE_SYM_EQU1 );
284 Flag = PARSE_FLAG_ERROR;
285 break;
286 }
287 Flag = PARSE_FLAG_OPER;
288 break;
289
290 case PARSE_SYM_EQU2:
291 if ( Flag != PARSE_FLAG_VAR )
292 {
293 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before Reverse Implication\n" );
294 Flag = PARSE_FLAG_ERROR;
295 break;
296 }
297 if ( pTemp[1] == PARSE_SYM_EQU3 )
298 {
299 pTemp++;
300 Parse_StackOpPush( pStackOp, PARSE_OPER_FLR );
301 }
302 else
303 {
304 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c\"\n", PARSE_SYM_EQU2 );
305 Flag = PARSE_FLAG_ERROR;
306 break;
307 }
308 Flag = PARSE_FLAG_OPER;
309 break;
310
311 case PARSE_SYM_LOWER:
312 case PARSE_SYM_OPEN:
313 if ( Flag == PARSE_FLAG_VAR )
314 Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
315 Parse_StackOpPush( pStackOp, PARSE_OPER_MARK );
316 // after an opening bracket, it feels like starting over again
317 Flag = PARSE_FLAG_START;
318 break;
319
320 case PARSE_SYM_RAISE:
321 fLower = 1;
322 case PARSE_SYM_CLOSE:
323 if ( !Parse_StackOpIsEmpty( pStackOp ) )
324 {
325 while ( 1 )
326 {
327 if ( Parse_StackOpIsEmpty( pStackOp ) )
328 {
329 fprintf( pOutput, "Parse_FormulaParser(): There is no opening parenthesis\n" );
330 Flag = PARSE_FLAG_ERROR;
331 break;
332 }
333 Oper = Parse_StackOpPop( pStackOp );
334 if ( Oper == PARSE_OPER_MARK )
335 break;
336
337 // perform the given operation
338 if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper ) == NULL )
339 {
340 fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" );
341 ABC_FREE( pFormula );
342 return NULL;
343 }
344 }
345
346 if ( fLower )
347 {
348 bFunc = (DdNode *)Parse_StackFnPop( pStackFn );
349 bFunc = Extra_bddMove( dd, bTemp = bFunc, -nVars ); Cudd_Ref( bFunc );
350 Cudd_RecursiveDeref( dd, bTemp );
351 Parse_StackFnPush( pStackFn, bFunc );
352 }
353 }
354 else
355 {
356 fprintf( pOutput, "Parse_FormulaParser(): There is no opening parenthesis\n" );
357 Flag = PARSE_FLAG_ERROR;
358 break;
359 }
360 if ( Flag != PARSE_FLAG_ERROR )
361 Flag = PARSE_FLAG_VAR;
362 fLower = 0;
363 break;
364
365
366 default:
367 // scan the next name
368 /*
369 fFound = 0;
370 for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n'; i++ )
371 {
372 for ( v = 0; v < nVars; v++ )
373 if ( strncmp( pTemp, ppVarNames[v], i+1 ) == 0 && strlen(ppVarNames[v]) == (unsigned)(i+1) )
374 {
375 pTemp += i;
376 fFound = 1;
377 break;
378 }
379 if ( fFound )
380 break;
381 }
382 */
383 // bug fix by SV (9/11/08)
384 fFound = 0;
385 for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
386 pTemp[i] != PARSE_SYM_AND1 && pTemp[i] != PARSE_SYM_AND2 && pTemp[i] != PARSE_SYM_XOR1 &&
387 pTemp[i] != PARSE_SYM_XOR2 && pTemp[i] != PARSE_SYM_XOR3 && pTemp[i] != PARSE_SYM_XOR &&
388 pTemp[i] != PARSE_SYM_OR1 && pTemp[i] != PARSE_SYM_OR2 && pTemp[i] != PARSE_SYM_CLOSE &&
389 pTemp[i] != PARSE_SYM_NEGAFT;
390 i++ )
391 {}
392 for ( v = 0; v < nVars; v++ )
393 {
394 if ( strncmp( pTemp, ppVarNames[v], i ) == 0 && strlen(ppVarNames[v]) == (unsigned)(i) )
395 {
396 pTemp += i-1;
397 fFound = 1;
398 break;
399 }
400 }
401
402 if ( !fFound )
403 {
404 fprintf( pOutput, "Parse_FormulaParser(): The parser cannot find var \"%s\" in the input var list.\n", pTemp );
405 Flag = PARSE_FLAG_ERROR;
406 break;
407 }
408 // assume operation AND, if vars follow one another
409 if ( Flag == PARSE_FLAG_VAR )
410 Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
411 Parse_StackFnPush( pStackFn, pbVars[v] ); Cudd_Ref( pbVars[v] );
412 Flag = PARSE_FLAG_VAR;
413 break;
414 }
415
416 if ( Flag == PARSE_FLAG_ERROR )
417 break; // error exit
418 else if ( Flag == PARSE_FLAG_START )
419 continue; // go on parsing
420 else if ( Flag == PARSE_FLAG_VAR )
421 while ( 1 )
422 { // check if there are negations in the OpStack
423 if ( Parse_StackOpIsEmpty(pStackOp) )
424 break;
425 Oper = Parse_StackOpPop( pStackOp );
426 if ( Oper != PARSE_OPER_NEG )
427 {
428 Parse_StackOpPush( pStackOp, Oper );
429 break;
430 }
431 else
432 {
433 Parse_StackFnPush( pStackFn, Cudd_Not(Parse_StackFnPop(pStackFn)) );
434 }
435 }
436 else // if ( Flag == PARSE_FLAG_OPER )
437 while ( 1 )
438 { // execute all the operations in the OpStack
439 // with precedence higher or equal than the last one
440 Oper1 = Parse_StackOpPop( pStackOp ); // the last operation
441 if ( Parse_StackOpIsEmpty(pStackOp) )
442 { // if it is the only operation, push it back
443 Parse_StackOpPush( pStackOp, Oper1 );
444 break;
445 }
446 Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one
447 if ( Oper2 >= Oper1 )
448 { // if Oper2 precedence is higher or equal, execute it
449 // Parse_StackPush( pStackFn, Operation( FunStack.Pop(), FunStack.Pop(), Oper2 ) );
450 if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper2 ) == NULL )
451 {
452 fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" );
453 ABC_FREE( pFormula );
454 return NULL;
455 }
456 Parse_StackOpPush( pStackOp, Oper1 ); // push the last operation back
457 }
458 else
459 { // if Oper2 precedence is lower, push them back and done
460 Parse_StackOpPush( pStackOp, Oper2 );
461 Parse_StackOpPush( pStackOp, Oper1 );
462 break;
463 }
464 }
465 }
466
467 if ( Flag != PARSE_FLAG_ERROR )
468 {
469 if ( !Parse_StackFnIsEmpty(pStackFn) )
470 {
471 bFunc = (DdNode *)Parse_StackFnPop(pStackFn);
472 if ( Parse_StackFnIsEmpty(pStackFn) )
473 if ( Parse_StackOpIsEmpty(pStackOp) )
474 {
475 Parse_StackFnFree(pStackFn);
476 Parse_StackOpFree(pStackOp);
477 Cudd_Deref( bFunc );
478 ABC_FREE( pFormula );
479 return bFunc;
480 }
481 else
482 fprintf( pOutput, "Parse_FormulaParser(): Something is left in the operation stack\n" );
483 else
484 fprintf( pOutput, "Parse_FormulaParser(): Something is left in the function stack\n" );
485 }
486 else
487 fprintf( pOutput, "Parse_FormulaParser(): The input string is empty\n" );
488 }
489 ABC_FREE( pFormula );
490 return NULL;
491 }
492
493 /**Function*************************************************************
494
495 Synopsis [Performs the operation on the top entries in the stack.]
496
497 Description []
498
499 SideEffects []
500
501 SeeAlso []
502
503 ***********************************************************************/
Parse_ParserPerformTopOp(DdManager * dd,Parse_StackFn_t * pStackFn,int Oper)504 DdNode * Parse_ParserPerformTopOp( DdManager * dd, Parse_StackFn_t * pStackFn, int Oper )
505 {
506 DdNode * bArg1, * bArg2, * bFunc;
507 // perform the given operation
508 bArg2 = (DdNode *)Parse_StackFnPop( pStackFn );
509 bArg1 = (DdNode *)Parse_StackFnPop( pStackFn );
510 if ( Oper == PARSE_OPER_AND )
511 bFunc = Cudd_bddAnd( dd, bArg1, bArg2 );
512 else if ( Oper == PARSE_OPER_XOR )
513 bFunc = Cudd_bddXor( dd, bArg1, bArg2 );
514 else if ( Oper == PARSE_OPER_OR )
515 bFunc = Cudd_bddOr( dd, bArg1, bArg2 );
516 else if ( Oper == PARSE_OPER_EQU )
517 bFunc = Cudd_bddXnor( dd, bArg1, bArg2 );
518 else if ( Oper == PARSE_OPER_FLR )
519 bFunc = Cudd_bddOr( dd, Cudd_Not(bArg1), bArg2 );
520 else if ( Oper == PARSE_OPER_FLL )
521 bFunc = Cudd_bddOr( dd, Cudd_Not(bArg2), bArg1 );
522 else
523 return NULL;
524 Cudd_Ref( bFunc );
525 Cudd_RecursiveDeref( dd, bArg1 );
526 Cudd_RecursiveDeref( dd, bArg2 );
527 Parse_StackFnPush( pStackFn, bFunc );
528 return bFunc;
529 }
530
531
532 ////////////////////////////////////////////////////////////////////////
533 /// END OF FILE ///
534 ////////////////////////////////////////////////////////////////////////
535 ABC_NAMESPACE_IMPL_END
536
537