src/bdd/parse/parse.h File Reference
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Functions | |
| DdNode * | Parse_FormulaParser (FILE *pOutput, char *pFormula, int nVars, int nRanks, char *ppVarNames[], DdManager *dd, DdNode *pbVars[]) |
Function Documentation
| DdNode* Parse_FormulaParser | ( | FILE * | pOutput, | |
| char * | pFormulaInit, | |||
| int | nVars, | |||
| int | nRanks, | |||
| char * | ppVarNames[], | |||
| DdManager * | dd, | |||
| DdNode * | pbVars[] | |||
| ) |
CFile****************************************************************
FileName [parse.h]
PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
Synopsis [Parsing symbolic Boolean formulas into BDDs.]
Author [MVSIS Group]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 8, 2003.]
Revision [
- Id
- parse.h,v 1.0 2003/09/08 00:00:00 alanmi Exp
] INCLUDES /// PARAMETERS /// STRUCTURE DEFINITIONS /// GLOBAL VARIABLES /// MACRO DEFINITIONS /// FUNCTION DEFINITIONS ///
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Derives the BDD corresponding to the formula in language L.]
Description [Takes the stream to output messages, the formula, the number variables and the rank in the formula. The array of variable names is also given. The BDD manager and the elementary 0-rank variable are the last two arguments. The manager should have at least as many variables as nVars * (nRanks + 1). The 0-rank variables should have numbers larger than the variables of other ranks.]
SideEffects []
SeeAlso []
Definition at line 111 of file parseCore.c.
00113 { 00114 char * pFormula; 00115 Parse_StackFn_t * pStackFn; 00116 Parse_StackOp_t * pStackOp; 00117 DdNode * bFunc, * bTemp; 00118 char * pTemp; 00119 int nParans, fFound, Flag; 00120 int Oper, Oper1, Oper2; 00121 int i, v, fLower; 00122 00123 // make sure that the number of vars and ranks is correct 00124 if ( nVars * (nRanks + 1) > dd->size ) 00125 { 00126 printf( "Parse_FormulaParser(): The BDD manager does not have enough variables.\n" ); 00127 return NULL; 00128 } 00129 00130 // make sure that the number of opening and closing parantheses is the same 00131 nParans = 0; 00132 for ( pTemp = pFormulaInit; *pTemp; pTemp++ ) 00133 if ( *pTemp == '(' ) 00134 nParans++; 00135 else if ( *pTemp == ')' ) 00136 nParans--; 00137 if ( nParans != 0 ) 00138 { 00139 fprintf( pOutput, "Parse_FormulaParser(): Different number of opening and closing parantheses ().\n" ); 00140 return NULL; 00141 } 00142 00143 nParans = 0; 00144 for ( pTemp = pFormulaInit; *pTemp; pTemp++ ) 00145 if ( *pTemp == '[' ) 00146 nParans++; 00147 else if ( *pTemp == ']' ) 00148 nParans--; 00149 if ( nParans != 0 ) 00150 { 00151 fprintf( pOutput, "Parse_FormulaParser(): Different number of opening and closing brackets [].\n" ); 00152 return NULL; 00153 } 00154 00155 // copy the formula 00156 pFormula = ALLOC( char, strlen(pFormulaInit) + 3 ); 00157 sprintf( pFormula, "(%s)", pFormulaInit ); 00158 00159 // start the stacks 00160 pStackFn = Parse_StackFnStart( STACKSIZE ); 00161 pStackOp = Parse_StackOpStart( STACKSIZE ); 00162 00163 Flag = PARSE_FLAG_START; 00164 fLower = 0; 00165 for ( pTemp = pFormula; *pTemp; pTemp++ ) 00166 { 00167 switch ( *pTemp ) 00168 { 00169 // skip all spaces, tabs, and end-of-lines 00170 case ' ': 00171 case '\t': 00172 case '\r': 00173 case '\n': 00174 continue; 00175 00176 // treat Constant 0 as a variable 00177 case PARSE_SYM_CONST0: 00178 Parse_StackFnPush( pStackFn, b0 ); Cudd_Ref( b0 ); 00179 if ( Flag == PARSE_FLAG_VAR ) 00180 { 00181 fprintf( pOutput, "Parse_FormulaParser(): No operation symbol before constant 0.\n" ); 00182 Flag = PARSE_FLAG_ERROR; 00183 break; 00184 } 00185 Flag = PARSE_FLAG_VAR; 00186 break; 00187 00188 // the same for Constant 1 00189 case PARSE_SYM_CONST1: 00190 Parse_StackFnPush( pStackFn, b1 ); Cudd_Ref( b1 ); 00191 if ( Flag == PARSE_FLAG_VAR ) 00192 { 00193 fprintf( pOutput, "Parse_FormulaParser(): No operation symbol before constant 1.\n" ); 00194 Flag = PARSE_FLAG_ERROR; 00195 break; 00196 } 00197 Flag = PARSE_FLAG_VAR; 00198 break; 00199 00200 case PARSE_SYM_NEGBEF1: 00201 case PARSE_SYM_NEGBEF2: 00202 if ( Flag == PARSE_FLAG_VAR ) 00203 {// if NEGBEF follows a variable, AND is assumed 00204 Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); 00205 Flag = PARSE_FLAG_OPER; 00206 } 00207 Parse_StackOpPush( pStackOp, PARSE_OPER_NEG ); 00208 break; 00209 00210 case PARSE_SYM_NEGAFT: 00211 if ( Flag != PARSE_FLAG_VAR ) 00212 {// if there is no variable before NEGAFT, it is an error 00213 fprintf( pOutput, "Parse_FormulaParser(): No variable is specified before the negation suffix.\n" ); 00214 Flag = PARSE_FLAG_ERROR; 00215 break; 00216 } 00217 else // if ( Flag == PARSE_FLAG_VAR ) 00218 Parse_StackFnPush( pStackFn, Cudd_Not( Parse_StackFnPop(pStackFn) ) ); 00219 break; 00220 00221 case PARSE_SYM_AND1: 00222 case PARSE_SYM_AND2: 00223 case PARSE_SYM_OR: 00224 if ( Flag != PARSE_FLAG_VAR ) 00225 { 00226 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR.\n" ); 00227 Flag = PARSE_FLAG_ERROR; 00228 break; 00229 } 00230 if ( *pTemp == PARSE_SYM_AND1 || *pTemp == PARSE_SYM_AND2 ) 00231 Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); 00232 else //if ( Str[Pos] == PARSE_SYM_OR ) 00233 Parse_StackOpPush( pStackOp, PARSE_OPER_OR ); 00234 Flag = PARSE_FLAG_OPER; 00235 break; 00236 00237 case PARSE_SYM_EQU1: 00238 if ( Flag != PARSE_FLAG_VAR ) 00239 { 00240 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before Equivalence or Implication\n" ); 00241 Flag = PARSE_FLAG_ERROR; break; 00242 } 00243 if ( pTemp[1] == PARSE_SYM_EQU2 ) 00244 { // check what is the next symbol in the string 00245 pTemp++; 00246 if ( pTemp[1] == PARSE_SYM_EQU3 ) 00247 { 00248 pTemp++; 00249 Parse_StackOpPush( pStackOp, PARSE_OPER_EQU ); 00250 } 00251 else 00252 { 00253 Parse_StackOpPush( pStackOp, PARSE_OPER_FLL ); 00254 } 00255 } 00256 else if ( pTemp[1] == PARSE_SYM_XOR2 ) 00257 { 00258 pTemp++; 00259 if ( pTemp[1] == PARSE_SYM_XOR3 ) 00260 { 00261 pTemp++; 00262 Parse_StackOpPush( pStackOp, PARSE_OPER_XOR ); 00263 } 00264 else 00265 { 00266 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c%c\"\n", PARSE_SYM_EQU1, PARSE_SYM_XOR2 ); 00267 Flag = PARSE_FLAG_ERROR; 00268 break; 00269 } 00270 } 00271 else 00272 { 00273 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c\"\n", PARSE_SYM_EQU1 ); 00274 Flag = PARSE_FLAG_ERROR; 00275 break; 00276 } 00277 Flag = PARSE_FLAG_OPER; 00278 break; 00279 00280 case PARSE_SYM_EQU2: 00281 if ( Flag != PARSE_FLAG_VAR ) 00282 { 00283 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before Reverse Implication\n" ); 00284 Flag = PARSE_FLAG_ERROR; 00285 break; 00286 } 00287 if ( pTemp[1] == PARSE_SYM_EQU3 ) 00288 { 00289 pTemp++; 00290 Parse_StackOpPush( pStackOp, PARSE_OPER_FLR ); 00291 } 00292 else 00293 { 00294 fprintf( pOutput, "Parse_FormulaParser(): Wrong symbol after \"%c\"\n", PARSE_SYM_EQU2 ); 00295 Flag = PARSE_FLAG_ERROR; 00296 break; 00297 } 00298 Flag = PARSE_FLAG_OPER; 00299 break; 00300 00301 case PARSE_SYM_LOWER: 00302 case PARSE_SYM_OPEN: 00303 if ( Flag == PARSE_FLAG_VAR ) 00304 Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); 00305 Parse_StackOpPush( pStackOp, PARSE_OPER_MARK ); 00306 // after an opening bracket, it feels like starting over again 00307 Flag = PARSE_FLAG_START; 00308 break; 00309 00310 case PARSE_SYM_RAISE: 00311 fLower = 1; 00312 case PARSE_SYM_CLOSE: 00313 if ( !Parse_StackOpIsEmpty( pStackOp ) ) 00314 { 00315 while ( 1 ) 00316 { 00317 if ( Parse_StackOpIsEmpty( pStackOp ) ) 00318 { 00319 fprintf( pOutput, "Parse_FormulaParser(): There is no opening paranthesis\n" ); 00320 Flag = PARSE_FLAG_ERROR; 00321 break; 00322 } 00323 Oper = Parse_StackOpPop( pStackOp ); 00324 if ( Oper == PARSE_OPER_MARK ) 00325 break; 00326 00327 // perform the given operation 00328 if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper ) == NULL ) 00329 { 00330 fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" ); 00331 free( pFormula ); 00332 return NULL; 00333 } 00334 } 00335 00336 if ( fLower ) 00337 { 00338 bFunc = Parse_StackFnPop( pStackFn ); 00339 bFunc = Extra_bddMove( dd, bTemp = bFunc, -nVars ); Cudd_Ref( bFunc ); 00340 Cudd_RecursiveDeref( dd, bTemp ); 00341 Parse_StackFnPush( pStackFn, bFunc ); 00342 } 00343 } 00344 else 00345 { 00346 fprintf( pOutput, "Parse_FormulaParser(): There is no opening paranthesis\n" ); 00347 Flag = PARSE_FLAG_ERROR; 00348 break; 00349 } 00350 if ( Flag != PARSE_FLAG_ERROR ) 00351 Flag = PARSE_FLAG_VAR; 00352 fLower = 0; 00353 break; 00354 00355 00356 default: 00357 // scan the next name 00358 fFound = 0; 00359 for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n'; i++ ) 00360 { 00361 for ( v = 0; v < nVars; v++ ) 00362 if ( strncmp( pTemp, ppVarNames[v], i+1 ) == 0 && strlen(ppVarNames[v]) == (unsigned)(i+1) ) 00363 { 00364 pTemp += i; 00365 fFound = 1; 00366 break; 00367 } 00368 if ( fFound ) 00369 break; 00370 } 00371 if ( !fFound ) 00372 { 00373 fprintf( pOutput, "Parse_FormulaParser(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); 00374 Flag = PARSE_FLAG_ERROR; 00375 break; 00376 } 00377 00378 // assume operation AND, if vars follow one another 00379 if ( Flag == PARSE_FLAG_VAR ) 00380 Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); 00381 Parse_StackFnPush( pStackFn, pbVars[v] ); Cudd_Ref( pbVars[v] ); 00382 Flag = PARSE_FLAG_VAR; 00383 break; 00384 } 00385 00386 if ( Flag == PARSE_FLAG_ERROR ) 00387 break; // error exit 00388 else if ( Flag == PARSE_FLAG_START ) 00389 continue; // go on parsing 00390 else if ( Flag == PARSE_FLAG_VAR ) 00391 while ( 1 ) 00392 { // check if there are negations in the OpStack 00393 if ( Parse_StackOpIsEmpty(pStackOp) ) 00394 break; 00395 Oper = Parse_StackOpPop( pStackOp ); 00396 if ( Oper != PARSE_OPER_NEG ) 00397 { 00398 Parse_StackOpPush( pStackOp, Oper ); 00399 break; 00400 } 00401 else 00402 { 00403 Parse_StackFnPush( pStackFn, Cudd_Not(Parse_StackFnPop(pStackFn)) ); 00404 } 00405 } 00406 else // if ( Flag == PARSE_FLAG_OPER ) 00407 while ( 1 ) 00408 { // execute all the operations in the OpStack 00409 // with precedence higher or equal than the last one 00410 Oper1 = Parse_StackOpPop( pStackOp ); // the last operation 00411 if ( Parse_StackOpIsEmpty(pStackOp) ) 00412 { // if it is the only operation, push it back 00413 Parse_StackOpPush( pStackOp, Oper1 ); 00414 break; 00415 } 00416 Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one 00417 if ( Oper2 >= Oper1 ) 00418 { // if Oper2 precedence is higher or equal, execute it 00419 // Parse_StackPush( pStackFn, Operation( FunStack.Pop(), FunStack.Pop(), Oper2 ) ); 00420 if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper2 ) == NULL ) 00421 { 00422 fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" ); 00423 free( pFormula ); 00424 return NULL; 00425 } 00426 Parse_StackOpPush( pStackOp, Oper1 ); // push the last operation back 00427 } 00428 else 00429 { // if Oper2 precedence is lower, push them back and done 00430 Parse_StackOpPush( pStackOp, Oper2 ); 00431 Parse_StackOpPush( pStackOp, Oper1 ); 00432 break; 00433 } 00434 } 00435 } 00436 00437 if ( Flag != PARSE_FLAG_ERROR ) 00438 { 00439 if ( !Parse_StackFnIsEmpty(pStackFn) ) 00440 { 00441 bFunc = Parse_StackFnPop(pStackFn); 00442 if ( Parse_StackFnIsEmpty(pStackFn) ) 00443 if ( Parse_StackOpIsEmpty(pStackOp) ) 00444 { 00445 Parse_StackFnFree(pStackFn); 00446 Parse_StackOpFree(pStackOp); 00447 Cudd_Deref( bFunc ); 00448 free( pFormula ); 00449 return bFunc; 00450 } 00451 else 00452 fprintf( pOutput, "Parse_FormulaParser(): Something is left in the operation stack\n" ); 00453 else 00454 fprintf( pOutput, "Parse_FormulaParser(): Something is left in the function stack\n" ); 00455 } 00456 else 00457 fprintf( pOutput, "Parse_FormulaParser(): The input string is empty\n" ); 00458 } 00459 free( pFormula ); 00460 return NULL; 00461 }
