abc70930: src/base/ver/verFormula.c Source File

00001 
00021 #include "ver.h"
00022 
00026 
00027 // the list of operation symbols to be used in expressions
00028 #define VER_PARSE_SYM_OPEN    '('   // opening paranthesis
00029 #define VER_PARSE_SYM_CLOSE   ')'   // closing paranthesis
00030 #define VER_PARSE_SYM_CONST0  '0'   // constant 0
00031 #define VER_PARSE_SYM_CONST1  '1'   // constant 1
00032 #define VER_PARSE_SYM_NEGBEF1 '!'   // negation before the variable
00033 #define VER_PARSE_SYM_NEGBEF2 '~'   // negation before the variable
00034 #define VER_PARSE_SYM_AND     '&'   // logic AND
00035 #define VER_PARSE_SYM_OR      '|'   // logic OR
00036 #define VER_PARSE_SYM_XOR     '^'   // logic XOR
00037 #define VER_PARSE_SYM_MUX1    '?'   // first symbol of MUX
00038 #define VER_PARSE_SYM_MUX2    ':'   // second symbol of MUX
00039 
00040 // the list of opcodes (also specifying operation precedence)
00041 #define VER_PARSE_OPER_NEG     7    // negation (highest precedence)
00042 #define VER_PARSE_OPER_AND     6    // logic AND
00043 #define VER_PARSE_OPER_XOR     5    // logic EXOR   (a'b | ab')   
00044 #define VER_PARSE_OPER_OR      4    // logic OR
00045 #define VER_PARSE_OPER_EQU     3    // equvalence   (a'b'| ab )
00046 #define VER_PARSE_OPER_MUX     2    // MUX(a,b,c)   (ab | a'c )
00047 #define VER_PARSE_OPER_MARK    1    // OpStack token standing for an opening paranthesis
00048 
00049 // these are values of the internal Flag
00050 #define VER_PARSE_FLAG_START   1    // after the opening parenthesis 
00051 #define VER_PARSE_FLAG_VAR     2    // after operation is received
00052 #define VER_PARSE_FLAG_OPER    3    // after operation symbol is received
00053 #define VER_PARSE_FLAG_ERROR   4    // when error is detected
00054 
00055 static Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper );
00056 static int         Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );
00057 
00061 
00073 void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
00074 {
00075     char * pTemp;
00076     Hop_Obj_t * bFunc, * bTemp;
00077     int nParans, Flag;
00078         int Oper, Oper1, Oper2;
00079     int v;
00080 
00081     // clear the stacks and the names
00082     Vec_PtrClear( vNames );
00083     Vec_PtrClear( vStackFn );
00084     Vec_IntClear( vStackOp );
00085 
00086     if ( !strcmp(pFormula, "0") || !strcmp(pFormula, "1\'b0") )
00087         return Hop_ManConst0(pMan);
00088     if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") )
00089         return Hop_ManConst1(pMan);
00090 
00091     // make sure that the number of opening and closing parantheses is the same
00092     nParans = 0;
00093     for ( pTemp = pFormula; *pTemp; pTemp++ )
00094         if ( *pTemp == '(' )
00095             nParans++;
00096         else if ( *pTemp == ')' )
00097             nParans--;
00098     if ( nParans != 0 )
00099     {
00100         sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." );
00101         return NULL;
00102     }
00103  
00104     // add parantheses
00105     pTemp = pFormula + strlen(pFormula) + 2;
00106     *pTemp-- = 0; *pTemp = ')';
00107     while ( --pTemp != pFormula )
00108         *pTemp = *(pTemp - 1);
00109     *pTemp = '(';
00110 
00111     // perform parsing
00112     Flag = VER_PARSE_FLAG_START;
00113     for ( pTemp = pFormula; *pTemp; pTemp++ )
00114         {
00115                 switch ( *pTemp )
00116             {
00117                 // skip all spaces, tabs, and end-of-lines
00118         case ' ':
00119         case '\t':
00120         case '\r':
00121         case '\n':
00122                         continue;
00123 /*
00124                 // treat Constant 0 as a variable
00125                 case VER_PARSE_SYM_CONST0:
00126                     Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( Hop_ManConst0(pMan) );
00127                         if ( Flag == VER_PARSE_FLAG_VAR )
00128                         {
00129                                 sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
00130                                 Flag = VER_PARSE_FLAG_ERROR; 
00131                 break;
00132                         }
00133             Flag = VER_PARSE_FLAG_VAR; 
00134             break;
00135 
00136                 // the same for Constant 1
00137                 case VER_PARSE_SYM_CONST1:
00138                     Vec_PtrPush( vStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( Hop_ManConst1(pMan) );
00139                         if ( Flag == VER_PARSE_FLAG_VAR )
00140                         {
00141                                 sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
00142                                 Flag = VER_PARSE_FLAG_ERROR; 
00143                 break;
00144                         }
00145             Flag = VER_PARSE_FLAG_VAR; 
00146             break;
00147 */
00148                 case VER_PARSE_SYM_NEGBEF1:
00149                 case VER_PARSE_SYM_NEGBEF2:
00150                         if ( Flag == VER_PARSE_FLAG_VAR )
00151                         {// if NEGBEF follows a variable, AND is assumed
00152                                 sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
00153                                 Flag = VER_PARSE_FLAG_ERROR; 
00154                 break;
00155                         }
00156                 Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
00157                         break;
00158 
00159         case VER_PARSE_SYM_AND:
00160         case VER_PARSE_SYM_OR:
00161         case VER_PARSE_SYM_XOR:
00162         case VER_PARSE_SYM_MUX1:
00163         case VER_PARSE_SYM_MUX2:
00164                         if ( Flag != VER_PARSE_FLAG_VAR )
00165                         {
00166                                 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
00167                                 Flag = VER_PARSE_FLAG_ERROR; 
00168                 break;
00169                         }
00170                         if ( *pTemp == VER_PARSE_SYM_AND )
00171                                 Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
00172                         else if ( *pTemp == VER_PARSE_SYM_OR )
00173                                 Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
00174                         else if ( *pTemp == VER_PARSE_SYM_XOR )
00175                                 Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
00176                         else if ( *pTemp == VER_PARSE_SYM_MUX1 )
00177                                 Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
00178 //                      else if ( *pTemp == VER_PARSE_SYM_MUX2 )
00179 //                              Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
00180                         Flag = VER_PARSE_FLAG_OPER; 
00181             break;
00182 
00183         case VER_PARSE_SYM_OPEN:
00184                         if ( Flag == VER_PARSE_FLAG_VAR )
00185                         {
00186                                 sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." );
00187                                 Flag = VER_PARSE_FLAG_ERROR; 
00188                 break;
00189                         }
00190                         Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
00191                         // after an opening bracket, it feels like starting over again
00192                         Flag = VER_PARSE_FLAG_START; 
00193             break;
00194 
00195                 case VER_PARSE_SYM_CLOSE:
00196                         if ( Vec_IntSize( vStackOp ) )
00197             {
00198                                 while ( 1 )
00199                             {
00200                                     if ( !Vec_IntSize( vStackOp ) )
00201                                         {
00202                                                 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
00203                                                 Flag = VER_PARSE_FLAG_ERROR; 
00204                         break;
00205                                         }
00206                                         Oper = Vec_IntPop( vStackOp );
00207                                         if ( Oper == VER_PARSE_OPER_MARK )
00208                                                 break;
00209                     // skip the second MUX operation
00210 //                    if ( Oper == VER_PARSE_OPER_MUX2 )
00211 //                    {
00212 //                                          Oper = Vec_IntPop( vStackOp );
00213 //                        assert( Oper == VER_PARSE_OPER_MUX1 );
00214 //                    }
00215 
00216                     // perform the given operation
00217                     if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper ) == NULL )
00218                         {
00219                                 sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
00220                                 return NULL;
00221                         }
00222                             }
00223             }
00224                     else
00225                         {
00226                                 sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
00227                                 Flag = VER_PARSE_FLAG_ERROR; 
00228                 break;
00229                         }
00230                         if ( Flag != VER_PARSE_FLAG_ERROR )
00231                             Flag = VER_PARSE_FLAG_VAR; 
00232                         break;
00233 
00234 
00235                 default:
00236             // scan the next name
00237             v = Ver_FormulaParserFindVar( pTemp, vNames );
00238             if ( *pTemp == '\\' )
00239                 pTemp++;
00240             pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
00241 
00242                         // assume operation AND, if vars follow one another
00243                         if ( Flag == VER_PARSE_FLAG_VAR )
00244             {
00245                         sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
00246                 return NULL;
00247             }
00248             bTemp = Hop_IthVar( pMan, v );
00249                         Vec_PtrPush( vStackFn, bTemp ); //  Cudd_Ref( bTemp );
00250             Flag = VER_PARSE_FLAG_VAR; 
00251             break;
00252             }
00253 
00254                 if ( Flag == VER_PARSE_FLAG_ERROR )
00255                         break;      // error exit
00256                 else if ( Flag == VER_PARSE_FLAG_START )
00257                         continue;  //  go on parsing
00258                 else if ( Flag == VER_PARSE_FLAG_VAR )
00259                         while ( 1 )
00260                         {  // check if there are negations in the OpStack     
00261                                 if ( !Vec_IntSize(vStackOp) )
00262                                         break;
00263                 Oper = Vec_IntPop( vStackOp );
00264                                 if ( Oper != VER_PARSE_OPER_NEG )
00265                 {
00266                                         Vec_IntPush( vStackOp, Oper );
00267                                         break;
00268                 }
00269                                 else
00270                                 {
00271 //                                      Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
00272                                 Vec_PtrPush( vStackFn, Hop_Not(Vec_PtrPop(vStackFn)) );
00273                                 }
00274                         }
00275                 else // if ( Flag == VER_PARSE_FLAG_OPER )
00276                         while ( 1 )
00277                         {  // execute all the operations in the OpStack
00278                            // with precedence higher or equal than the last one
00279                                 Oper1 = Vec_IntPop( vStackOp ); // the last operation
00280                                 if ( !Vec_IntSize(vStackOp) ) 
00281                                 {  // if it is the only operation, push it back
00282                                         Vec_IntPush( vStackOp, Oper1 );
00283                                         break;
00284                                 }
00285                                 Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
00286                                 if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )  
00287                                 {  // if Oper2 precedence is higher or equal, execute it
00288                     if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL )
00289                         {
00290                                 sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
00291                                 return NULL;
00292                         }
00293                                         Vec_IntPush( vStackOp,  Oper1 );     // push the last operation back
00294                                 }
00295                                 else
00296                                 {  // if Oper2 precedence is lower, push them back and done
00297                                         Vec_IntPush( vStackOp, Oper2 );
00298                                         Vec_IntPush( vStackOp, Oper1 );
00299                                         break;
00300                                 }
00301                         }
00302     }
00303 
00304         if ( Flag != VER_PARSE_FLAG_ERROR )
00305     {
00306                 if ( Vec_PtrSize(vStackFn) )
00307             {   
00308                         bFunc = Vec_PtrPop(vStackFn);
00309                         if ( !Vec_PtrSize(vStackFn) )
00310                                 if ( !Vec_IntSize(vStackOp) )
00311                 {
00312 //                    Cudd_Deref( bFunc );
00313                                         return bFunc;
00314                 }
00315                                 else
00316                                         sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
00317                         else
00318                                 sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
00319             }
00320             else
00321                         sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
00322     }
00323 //    Cudd_Ref( bFunc );
00324 //    Cudd_RecursiveDeref( dd, bFunc );
00325         return NULL;
00326 }
00327 
00339 Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper )
00340 {
00341     Hop_Obj_t * bArg0, * bArg1, * bArg2, * bFunc;
00342     // perform the given operation
00343     bArg2 = Vec_PtrPop( vStackFn );
00344     bArg1 = Vec_PtrPop( vStackFn );
00345         if ( Oper == VER_PARSE_OPER_AND )
00346                 bFunc = Hop_And( pMan, bArg1, bArg2 );
00347         else if ( Oper == VER_PARSE_OPER_XOR )
00348                 bFunc = Hop_Exor( pMan, bArg1, bArg2 );
00349         else if ( Oper == VER_PARSE_OPER_OR )
00350                 bFunc = Hop_Or( pMan, bArg1, bArg2 );
00351         else if ( Oper == VER_PARSE_OPER_EQU )
00352                 bFunc = Hop_Not( Hop_Exor( pMan, bArg1, bArg2 ) );
00353         else if ( Oper == VER_PARSE_OPER_MUX )
00354     {
00355         bArg0 = Vec_PtrPop( vStackFn );
00356 //              bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 );  Cudd_Ref( bFunc );
00357                 bFunc = Hop_Mux( pMan, bArg0, bArg1, bArg2 ); 
00358 //        Cudd_RecursiveDeref( dd, bArg0 );
00359 //        Cudd_Deref( bFunc );
00360     }
00361         else
00362                 return NULL;
00363 //    Cudd_Ref( bFunc );
00364 //    Cudd_RecursiveDeref( dd, bArg1 );
00365 //    Cudd_RecursiveDeref( dd, bArg2 );
00366         Vec_PtrPush( vStackFn,  bFunc );
00367     return bFunc;
00368 }
00369 
00381 int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
00382 {
00383     char * pTemp, * pTemp2;
00384     int nLength, nLength2, i;
00385     // start the string
00386     pTemp = pString;
00387     // find the end of the string delimited by other characters
00388     if ( *pTemp == '\\' )
00389     {
00390         pString++;
00391         while ( *pTemp && *pTemp != ' ' )
00392             pTemp++;
00393     }
00394     else
00395     {
00396         while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && 
00397                 *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && 
00398                 *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && 
00399                 *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && 
00400                 *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
00401                 pTemp++;
00402     }
00403     // look for this string in the array
00404     nLength = pTemp - pString;
00405     for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
00406     {
00407         nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 );
00408         if ( nLength2 != nLength )
00409             continue;
00410         pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
00411         if ( strncmp( pString, pTemp2, nLength ) )
00412             continue;
00413         return i;
00414     }
00415     // could not find - add and return the number
00416     Vec_PtrPush( vNames, (void *)nLength );
00417     Vec_PtrPush( vNames, pString );
00418     return i;
00419 }
00420 
00432 void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
00433 {
00434     Hop_Obj_t * pRes;
00435     int v, fCompl;
00436     char Symbol;
00437 
00438     // get the operation
00439     Symbol = *pFormula++;
00440     fCompl = ( Symbol == '~' );
00441     if ( fCompl )
00442         Symbol = *pFormula++;
00443     // check the operation
00444     if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
00445     {
00446                 sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
00447                 return NULL;
00448     }
00449     // skip the brace
00450     while ( *pFormula++ != '{' );
00451     // parse the names
00452     Vec_PtrClear( vNames );
00453     while ( *pFormula != '}' )
00454     {
00455         v = Ver_FormulaParserFindVar( pFormula, vNames );
00456         pFormula += (int)Vec_PtrEntry( vNames, 2*v );
00457         while ( *pFormula == ' ' || *pFormula == ',' )
00458             pFormula++;
00459     }
00460     // compute the function
00461     if ( Symbol == '&' )
00462         pRes = Hop_CreateAnd( pMan, Vec_PtrSize(vNames)/2 );
00463     else if ( Symbol == '|' )
00464         pRes = Hop_CreateOr( pMan, Vec_PtrSize(vNames)/2 );
00465     else if ( Symbol == '^' )
00466         pRes = Hop_CreateExor( pMan, Vec_PtrSize(vNames)/2 );
00467     return Hop_NotCond( pRes, fCompl );
00468 }
00469 
00473 
00474