src/bdd/parse/parseCore.c File Reference

#include "parseInt.h"
Include dependency graph for parseCore.c:

Go to the source code of this file.

Defines

#define PARSE_SYM_OPEN   '('
#define PARSE_SYM_CLOSE   ')'
#define PARSE_SYM_LOWER   '['
#define PARSE_SYM_RAISE   ']'
#define PARSE_SYM_CONST0   '0'
#define PARSE_SYM_CONST1   '1'
#define PARSE_SYM_NEGBEF1   '!'
#define PARSE_SYM_NEGBEF2   '~'
#define PARSE_SYM_NEGAFT   '\''
#define PARSE_SYM_AND1   '&'
#define PARSE_SYM_AND2   '*'
#define PARSE_SYM_XOR1   '<'
#define PARSE_SYM_XOR2   '+'
#define PARSE_SYM_XOR3   '>'
#define PARSE_SYM_OR   '+'
#define PARSE_SYM_EQU1   '<'
#define PARSE_SYM_EQU2   '='
#define PARSE_SYM_EQU3   '>'
#define PARSE_SYM_FLR1   '='
#define PARSE_SYM_FLR2   '>'
#define PARSE_SYM_FLL1   '<'
#define PARSE_SYM_FLL2   '='
#define PARSE_OPER_NEG   10
#define PARSE_OPER_AND   9
#define PARSE_OPER_XOR   8
#define PARSE_OPER_OR   7
#define PARSE_OPER_EQU   6
#define PARSE_OPER_FLR   5
#define PARSE_OPER_FLL   4
#define PARSE_OPER_MARK   1
#define PARSE_FLAG_START   1
#define PARSE_FLAG_VAR   2
#define PARSE_FLAG_OPER   3
#define PARSE_FLAG_ERROR   4
#define STACKSIZE   1000

Functions

static DdNode * Parse_ParserPerformTopOp (DdManager *dd, Parse_StackFn_t *pStackFn, int Oper)
DdNode * Parse_FormulaParser (FILE *pOutput, char *pFormulaInit, int nVars, int nRanks, char *ppVarNames[], DdManager *dd, DdNode *pbVars[])

Define Documentation

#define PARSE_FLAG_ERROR   4

Definition at line 85 of file parseCore.c.

#define PARSE_FLAG_OPER   3

Definition at line 84 of file parseCore.c.

#define PARSE_FLAG_START   1

Definition at line 82 of file parseCore.c.

#define PARSE_FLAG_VAR   2

Definition at line 83 of file parseCore.c.

#define PARSE_OPER_AND   9

Definition at line 73 of file parseCore.c.

#define PARSE_OPER_EQU   6

Definition at line 76 of file parseCore.c.

#define PARSE_OPER_FLL   4

Definition at line 78 of file parseCore.c.

#define PARSE_OPER_FLR   5

Definition at line 77 of file parseCore.c.

#define PARSE_OPER_MARK   1

Definition at line 79 of file parseCore.c.

#define PARSE_OPER_NEG   10

Definition at line 72 of file parseCore.c.

#define PARSE_OPER_OR   7

Definition at line 75 of file parseCore.c.

#define PARSE_OPER_XOR   8

Definition at line 74 of file parseCore.c.

#define PARSE_SYM_AND1   '&'

Definition at line 56 of file parseCore.c.

#define PARSE_SYM_AND2   '*'

Definition at line 57 of file parseCore.c.

#define PARSE_SYM_CLOSE   ')'

Definition at line 48 of file parseCore.c.

#define PARSE_SYM_CONST0   '0'

Definition at line 51 of file parseCore.c.

#define PARSE_SYM_CONST1   '1'

Definition at line 52 of file parseCore.c.

#define PARSE_SYM_EQU1   '<'

Definition at line 62 of file parseCore.c.

#define PARSE_SYM_EQU2   '='

Definition at line 63 of file parseCore.c.

#define PARSE_SYM_EQU3   '>'

Definition at line 64 of file parseCore.c.

#define PARSE_SYM_FLL1   '<'

Definition at line 67 of file parseCore.c.

#define PARSE_SYM_FLL2   '='

Definition at line 68 of file parseCore.c.

#define PARSE_SYM_FLR1   '='

Definition at line 65 of file parseCore.c.

#define PARSE_SYM_FLR2   '>'

Definition at line 66 of file parseCore.c.

#define PARSE_SYM_LOWER   '['

Definition at line 49 of file parseCore.c.

#define PARSE_SYM_NEGAFT   '\''

Definition at line 55 of file parseCore.c.

#define PARSE_SYM_NEGBEF1   '!'

Definition at line 53 of file parseCore.c.

#define PARSE_SYM_NEGBEF2   '~'

Definition at line 54 of file parseCore.c.

#define PARSE_SYM_OPEN   '('

CFile****************************************************************

FileNameIn [parseCore.c]

PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]

Synopsis [Boolean formula parser.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id
parseCore.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 47 of file parseCore.c.

#define PARSE_SYM_OR   '+'

Definition at line 61 of file parseCore.c.

#define PARSE_SYM_RAISE   ']'

Definition at line 50 of file parseCore.c.

#define PARSE_SYM_XOR1   '<'

Definition at line 58 of file parseCore.c.

#define PARSE_SYM_XOR2   '+'

Definition at line 59 of file parseCore.c.

#define PARSE_SYM_XOR3   '>'

Definition at line 60 of file parseCore.c.

#define STACKSIZE   1000

Definition at line 87 of file parseCore.c.

Function Documentation

DdNode* Parse_FormulaParser ( FILE *  pOutput,
char *  pFormulaInit,
int  nVars,
int  nRanks,
char *  ppVarNames[],
DdManager *  dd,
DdNode *  pbVars[] 
)

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 }

DdNode * Parse_ParserPerformTopOp ( DdManager *  dd,
Parse_StackFn_t *  pStackFn,
int  Oper 
) [static]

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

Synopsis [Performs the operation on the top entries in the stack.]

Description []

SideEffects []

SeeAlso []

Definition at line 474 of file parseCore.c.

00475 {
00476     DdNode * bArg1, * bArg2, * bFunc;
00477     // perform the given operation
00478     bArg2 = Parse_StackFnPop( pStackFn );
00479     bArg1 = Parse_StackFnPop( pStackFn );
00480         if ( Oper == PARSE_OPER_AND )
00481                 bFunc = Cudd_bddAnd( dd, bArg1, bArg2 );
00482         else if ( Oper == PARSE_OPER_XOR )
00483                 bFunc = Cudd_bddXor( dd, bArg1, bArg2 );
00484         else if ( Oper == PARSE_OPER_OR )
00485                 bFunc = Cudd_bddOr( dd, bArg1, bArg2 );
00486         else if ( Oper == PARSE_OPER_EQU )
00487                 bFunc = Cudd_bddXnor( dd, bArg1, bArg2 );
00488         else if ( Oper == PARSE_OPER_FLR )
00489                 bFunc = Cudd_bddOr( dd, Cudd_Not(bArg1), bArg2 );
00490         else if ( Oper == PARSE_OPER_FLL )
00491                 bFunc = Cudd_bddOr( dd, Cudd_Not(bArg2), bArg1 );
00492         else
00493                 return NULL;
00494     Cudd_Ref( bFunc );
00495     Cudd_RecursiveDeref( dd, bArg1 );
00496     Cudd_RecursiveDeref( dd, bArg2 );
00497         Parse_StackFnPush( pStackFn,  bFunc );
00498     return bFunc;
00499 }

Generated on Tue Jan 5 12:19:00 2010 for abc70930 by  doxygen 1.6.1