src/bdd/parse/parseEqn.c File Reference

#include "parseInt.h"
#include "vec.h"
#include "hop.h"
Include dependency graph for parseEqn.c:

Go to the source code of this file.

Defines

#define PARSE_EQN_SYM_OPEN   '('
#define PARSE_EQN_SYM_CLOSE   ')'
#define PARSE_EQN_SYM_CONST0   '0'
#define PARSE_EQN_SYM_CONST1   '1'
#define PARSE_EQN_SYM_NEG   '!'
#define PARSE_EQN_SYM_AND   '*'
#define PARSE_EQN_SYM_OR   '+'
#define PARSE_EQN_OPER_NEG   10
#define PARSE_EQN_OPER_AND   9
#define PARSE_EQN_OPER_OR   7
#define PARSE_EQN_OPER_MARK   1
#define PARSE_EQN_FLAG_START   1
#define PARSE_EQN_FLAG_VAR   2
#define PARSE_EQN_FLAG_OPER   3
#define PARSE_EQN_FLAG_ERROR   4
#define PARSE_EQN_STACKSIZE   1000

Functions

static Hop_Obj_t * Parse_ParserPerformTopOp (Hop_Man_t *pMan, Parse_StackFn_t *pStackFn, int Oper)
Hop_Obj_t * Parse_FormulaParserEqn (FILE *pOutput, char *pFormInit, Vec_Ptr_t *vVarNames, Hop_Man_t *pMan)

Define Documentation

#define PARSE_EQN_FLAG_ERROR   4

Definition at line 47 of file parseEqn.c.

#define PARSE_EQN_FLAG_OPER   3

Definition at line 46 of file parseEqn.c.

#define PARSE_EQN_FLAG_START   1

Definition at line 44 of file parseEqn.c.

#define PARSE_EQN_FLAG_VAR   2

Definition at line 45 of file parseEqn.c.

#define PARSE_EQN_OPER_AND   9

Definition at line 39 of file parseEqn.c.

#define PARSE_EQN_OPER_MARK   1

Definition at line 41 of file parseEqn.c.

#define PARSE_EQN_OPER_NEG   10

Definition at line 38 of file parseEqn.c.

#define PARSE_EQN_OPER_OR   7

Definition at line 40 of file parseEqn.c.

#define PARSE_EQN_STACKSIZE   1000

Definition at line 49 of file parseEqn.c.

#define PARSE_EQN_SYM_AND   '*'

Definition at line 34 of file parseEqn.c.

#define PARSE_EQN_SYM_CLOSE   ')'

Definition at line 30 of file parseEqn.c.

#define PARSE_EQN_SYM_CONST0   '0'

Definition at line 31 of file parseEqn.c.

#define PARSE_EQN_SYM_CONST1   '1'

Definition at line 32 of file parseEqn.c.

#define PARSE_EQN_SYM_NEG   '!'

Definition at line 33 of file parseEqn.c.

#define PARSE_EQN_SYM_OPEN   '('

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

FileNameIn [parseEqn.c]

PackageName [ABC: Logic synthesis and verification system.]

Synopsis [Boolean formula parser.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - December 18, 2006.]

Revision [

Id
parseEqn.c,v 1.0 2006/12/18 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 29 of file parseEqn.c.

#define PARSE_EQN_SYM_OR   '+'

Definition at line 35 of file parseEqn.c.

Function Documentation

Hop_Obj_t* Parse_FormulaParserEqn ( FILE *  pOutput,
char *  pFormInit,
Vec_Ptr_t *  vVarNames,
Hop_Man_t *  pMan 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Derives the AIG corresponding to the equation.]

Description [Takes the stream to output messages, the formula, the vector of variable names and the AIG manager.]

SideEffects []

SeeAlso []

Definition at line 69 of file parseEqn.c.

00070 {
00071     char * pFormula;
00072     Parse_StackFn_t * pStackFn;
00073     Parse_StackOp_t * pStackOp;
00074     Hop_Obj_t * gFunc;
00075     char * pTemp, * pName;
00076     int nParans, fFound, Flag;
00077         int Oper, Oper1, Oper2;
00078     int i, v;
00079 
00080     // make sure that the number of opening and closing parantheses is the same
00081     nParans = 0;
00082     for ( pTemp = pFormInit; *pTemp; pTemp++ )
00083         if ( *pTemp == '(' )
00084             nParans++;
00085         else if ( *pTemp == ')' )
00086             nParans--;
00087     if ( nParans != 0 )
00088     {
00089         fprintf( pOutput, "Parse_FormulaParserEqn(): Different number of opening and closing parantheses ().\n" );
00090         return NULL;
00091     }
00092 
00093     // copy the formula
00094     pFormula = ALLOC( char, strlen(pFormInit) + 3 );
00095     sprintf( pFormula, "(%s)", pFormInit );
00096 
00097     // start the stacks
00098     pStackFn = Parse_StackFnStart( PARSE_EQN_STACKSIZE );
00099     pStackOp = Parse_StackOpStart( PARSE_EQN_STACKSIZE );
00100 
00101     Flag = PARSE_EQN_FLAG_START;
00102     for ( pTemp = pFormula; *pTemp; pTemp++ )
00103         {
00104                 switch ( *pTemp )
00105             {
00106                 // skip all spaces, tabs, and end-of-lines
00107         case ' ':
00108         case '\t':
00109         case '\r':
00110         case '\n':
00111                         continue;
00112                 case PARSE_EQN_SYM_CONST0:
00113                     Parse_StackFnPush( pStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( b0 );
00114                         if ( Flag == PARSE_EQN_FLAG_VAR )
00115                         {
00116                                 fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 0.\n" );
00117                                 Flag = PARSE_EQN_FLAG_ERROR; 
00118                 break;
00119                         }
00120             Flag = PARSE_EQN_FLAG_VAR; 
00121             break;
00122                 case PARSE_EQN_SYM_CONST1:
00123                     Parse_StackFnPush( pStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( b1 );
00124                         if ( Flag == PARSE_EQN_FLAG_VAR )
00125                         {
00126                                 fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 1.\n" );
00127                                 Flag = PARSE_EQN_FLAG_ERROR; 
00128                 break;
00129                         }
00130             Flag = PARSE_EQN_FLAG_VAR; 
00131             break;
00132                 case PARSE_EQN_SYM_NEG:
00133                         if ( Flag == PARSE_EQN_FLAG_VAR )
00134                         {// if NEGBEF follows a variable, AND is assumed
00135                                 Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
00136                                 Flag = PARSE_EQN_FLAG_OPER;
00137                         }
00138                 Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_NEG );
00139                         break;
00140         case PARSE_EQN_SYM_AND:
00141         case PARSE_EQN_SYM_OR:
00142                         if ( Flag != PARSE_EQN_FLAG_VAR )
00143                         {
00144                                 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no variable before AND, EXOR, or OR.\n" );
00145                                 Flag = PARSE_EQN_FLAG_ERROR; 
00146                 break;
00147                         }
00148                         if ( *pTemp == PARSE_EQN_SYM_AND )
00149                                 Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
00150                         else //if ( *pTemp == PARSE_EQN_SYM_OR )
00151                                 Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_OR );
00152                         Flag = PARSE_EQN_FLAG_OPER; 
00153             break;
00154                 case PARSE_EQN_SYM_OPEN:
00155                         if ( Flag == PARSE_EQN_FLAG_VAR )
00156             {
00157 //                              Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
00158                                 fprintf( pOutput, "Parse_FormulaParserEqn(): An opening paranthesis follows a var without operation sign.\n" ); 
00159                                 Flag = PARSE_EQN_FLAG_ERROR; 
00160                 break; 
00161             }
00162                         Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_MARK );
00163                         // after an opening bracket, it feels like starting over again
00164                         Flag = PARSE_EQN_FLAG_START; 
00165             break;
00166                 case PARSE_EQN_SYM_CLOSE:
00167                         if ( !Parse_StackOpIsEmpty( pStackOp ) )
00168             {
00169                                 while ( 1 )
00170                             {
00171                                     if ( Parse_StackOpIsEmpty( pStackOp ) )
00172                                         {
00173                                                 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" );
00174                                                 Flag = PARSE_EQN_FLAG_ERROR; 
00175                         break;
00176                                         }
00177                                         Oper = Parse_StackOpPop( pStackOp );
00178                                         if ( Oper == PARSE_EQN_OPER_MARK )
00179                                                 break;
00180 
00181                     // perform the given operation
00182                     if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL )
00183                         {
00184                                 fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
00185                         free( pFormula );
00186                                 return NULL;
00187                         }
00188                             }
00189             }
00190                     else
00191                         {
00192                                 fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" );
00193                                 Flag = PARSE_EQN_FLAG_ERROR; 
00194                 break;
00195                         }
00196                         if ( Flag != PARSE_EQN_FLAG_ERROR )
00197                             Flag = PARSE_EQN_FLAG_VAR; 
00198                         break;
00199 
00200 
00201                 default:
00202             // scan the next name
00203             for ( i = 0; pTemp[i] && 
00204                          pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
00205                          pTemp[i] != PARSE_EQN_SYM_AND && pTemp[i] != PARSE_EQN_SYM_OR && pTemp[i] != PARSE_EQN_SYM_CLOSE; i++ )
00206               {
00207                                     if ( pTemp[i] == PARSE_EQN_SYM_NEG || pTemp[i] == PARSE_EQN_SYM_OPEN )
00208                                     {
00209                                             fprintf( pOutput, "Parse_FormulaParserEqn(): The negation sign or an opening paranthesis inside the variable name.\n" );
00210                                             Flag = PARSE_EQN_FLAG_ERROR; 
00211                         break;
00212                                     }
00213               }
00214             // variable name is found
00215             fFound = 0;
00216             Vec_PtrForEachEntry( vVarNames, pName, v )
00217                 if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i )
00218                 {
00219                     pTemp += i-1;
00220                     fFound = 1;
00221                     break;
00222                 }
00223             if ( !fFound )
00224                         { 
00225                                 fprintf( pOutput, "Parse_FormulaParserEqn(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); 
00226                                 Flag = PARSE_EQN_FLAG_ERROR; 
00227                 break; 
00228                         }
00229                         if ( Flag == PARSE_EQN_FLAG_VAR )
00230             {
00231                                 fprintf( pOutput, "Parse_FormulaParserEqn(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); 
00232                                 Flag = PARSE_EQN_FLAG_ERROR; 
00233                 break; 
00234             }
00235                         Parse_StackFnPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
00236             Flag = PARSE_EQN_FLAG_VAR; 
00237             break;
00238             }
00239 
00240                 if ( Flag == PARSE_EQN_FLAG_ERROR )
00241                         break;      // error exit
00242                 else if ( Flag == PARSE_EQN_FLAG_START )
00243                         continue;  //  go on parsing
00244                 else if ( Flag == PARSE_EQN_FLAG_VAR )
00245                         while ( 1 )
00246                         {  // check if there are negations in the OpStack     
00247                                 if ( Parse_StackOpIsEmpty(pStackOp) )
00248                                         break;
00249                 Oper = Parse_StackOpPop( pStackOp );
00250                                 if ( Oper != PARSE_EQN_OPER_NEG )
00251                 {
00252                                         Parse_StackOpPush( pStackOp, Oper );
00253                                         break;
00254                 }
00255                                 else
00256                                 {
00257                                 Parse_StackFnPush( pStackFn, Hop_Not(Parse_StackFnPop(pStackFn)) );
00258                                 }
00259                         }
00260                 else // if ( Flag == PARSE_EQN_FLAG_OPER )
00261                         while ( 1 )
00262                         {  // execute all the operations in the OpStack
00263                            // with precedence higher or equal than the last one
00264                                 Oper1 = Parse_StackOpPop( pStackOp ); // the last operation
00265                                 if ( Parse_StackOpIsEmpty(pStackOp) ) 
00266                                 {  // if it is the only operation, push it back
00267                                         Parse_StackOpPush( pStackOp, Oper1 );
00268                                         break;
00269                                 }
00270                                 Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one
00271                                 if ( Oper2 >= Oper1 )  
00272                                 {  // if Oper2 precedence is higher or equal, execute it
00273                     if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper2 ) == NULL )
00274                         {
00275                                 fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
00276                         free( pFormula );
00277                                 return NULL;
00278                         }
00279                                         Parse_StackOpPush( pStackOp,  Oper1 );     // push the last operation back
00280                                 }
00281                                 else
00282                                 {  // if Oper2 precedence is lower, push them back and done
00283                                         Parse_StackOpPush( pStackOp, Oper2 );
00284                                         Parse_StackOpPush( pStackOp, Oper1 );
00285                                         break;
00286                                 }
00287                         }
00288     }
00289 
00290         if ( Flag != PARSE_EQN_FLAG_ERROR )
00291     {
00292                 if ( !Parse_StackFnIsEmpty(pStackFn) )
00293             {   
00294                         gFunc = Parse_StackFnPop(pStackFn);
00295                         if ( Parse_StackFnIsEmpty(pStackFn) )
00296                                 if ( Parse_StackOpIsEmpty(pStackOp) )
00297                 {
00298                     Parse_StackFnFree(pStackFn);
00299                     Parse_StackOpFree(pStackOp);
00300 //                    Cudd_Deref( gFunc );
00301                     free( pFormula );
00302                                         return gFunc;
00303                 }
00304                                 else
00305                                         fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the operation stack\n" );
00306                         else
00307                                 fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the function stack\n" );
00308             }
00309             else
00310                         fprintf( pOutput, "Parse_FormulaParserEqn(): The input string is empty\n" );
00311     }
00312     free( pFormula );
00313         return NULL;
00314 }

Hop_Obj_t * Parse_ParserPerformTopOp ( Hop_Man_t *  pMan,
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 327 of file parseEqn.c.

00328 {
00329     Hop_Obj_t * gArg1, * gArg2, * gFunc;
00330     // perform the given operation
00331     gArg2 = Parse_StackFnPop( pStackFn );
00332     gArg1 = Parse_StackFnPop( pStackFn );
00333         if ( Oper == PARSE_EQN_OPER_AND )
00334                 gFunc = Hop_And( pMan, gArg1, gArg2 );
00335         else if ( Oper == PARSE_EQN_OPER_OR )
00336                 gFunc = Hop_Or( pMan, gArg1, gArg2 );
00337         else
00338                 return NULL;
00339 //    Cudd_Ref( gFunc );
00340 //    Cudd_RecursiveDeref( dd, gArg1 );
00341 //    Cudd_RecursiveDeref( dd, gArg2 );
00342         Parse_StackFnPush( pStackFn,  gFunc );
00343     return gFunc;
00344 }

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