abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions
parseCore.c File Reference
#include "parseInt.h"

Go to the source code of this file.

Macros

#define PARSE_SYM_OPEN   '('
 DECLARATIONS ///. More...
 
#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_XOR   '^'
 
#define PARSE_SYM_OR1   '+'
 
#define PARSE_SYM_OR2   '|'
 
#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[])
 FUNCTION DEFINITIONS ///. More...
 

Macro Definition Documentation

#define PARSE_FLAG_ERROR   4

Definition at line 90 of file parseCore.c.

#define PARSE_FLAG_OPER   3

Definition at line 89 of file parseCore.c.

#define PARSE_FLAG_START   1

Definition at line 87 of file parseCore.c.

#define PARSE_FLAG_VAR   2

Definition at line 88 of file parseCore.c.

#define PARSE_OPER_AND   9

Definition at line 78 of file parseCore.c.

#define PARSE_OPER_EQU   6

Definition at line 81 of file parseCore.c.

#define PARSE_OPER_FLL   4

Definition at line 83 of file parseCore.c.

#define PARSE_OPER_FLR   5

Definition at line 82 of file parseCore.c.

#define PARSE_OPER_MARK   1

Definition at line 84 of file parseCore.c.

#define PARSE_OPER_NEG   10

Definition at line 77 of file parseCore.c.

#define PARSE_OPER_OR   7

Definition at line 80 of file parseCore.c.

#define PARSE_OPER_XOR   8

Definition at line 79 of file parseCore.c.

#define PARSE_SYM_AND1   '&'

Definition at line 59 of file parseCore.c.

#define PARSE_SYM_AND2   '*'

Definition at line 60 of file parseCore.c.

#define PARSE_SYM_CLOSE   ')'

Definition at line 51 of file parseCore.c.

#define PARSE_SYM_CONST0   '0'

Definition at line 54 of file parseCore.c.

#define PARSE_SYM_CONST1   '1'

Definition at line 55 of file parseCore.c.

#define PARSE_SYM_EQU1   '<'

Definition at line 67 of file parseCore.c.

#define PARSE_SYM_EQU2   '='

Definition at line 68 of file parseCore.c.

#define PARSE_SYM_EQU3   '>'

Definition at line 69 of file parseCore.c.

#define PARSE_SYM_FLL1   '<'

Definition at line 72 of file parseCore.c.

#define PARSE_SYM_FLL2   '='

Definition at line 73 of file parseCore.c.

#define PARSE_SYM_FLR1   '='

Definition at line 70 of file parseCore.c.

#define PARSE_SYM_FLR2   '>'

Definition at line 71 of file parseCore.c.

#define PARSE_SYM_LOWER   '['

Definition at line 52 of file parseCore.c.

#define PARSE_SYM_NEGAFT   '\''

Definition at line 58 of file parseCore.c.

#define PARSE_SYM_NEGBEF1   '!'

Definition at line 56 of file parseCore.c.

#define PARSE_SYM_NEGBEF2   '~'

Definition at line 57 of file parseCore.c.

#define PARSE_SYM_OPEN   '('

DECLARATIONS ///.

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

]

Definition at line 50 of file parseCore.c.

#define PARSE_SYM_OR1   '+'

Definition at line 65 of file parseCore.c.

#define PARSE_SYM_OR2   '|'

Definition at line 66 of file parseCore.c.

#define PARSE_SYM_RAISE   ']'

Definition at line 53 of file parseCore.c.

#define PARSE_SYM_XOR   '^'

Definition at line 64 of file parseCore.c.

#define PARSE_SYM_XOR1   '<'

Definition at line 61 of file parseCore.c.

#define PARSE_SYM_XOR2   '+'

Definition at line 62 of file parseCore.c.

#define PARSE_SYM_XOR3   '>'

Definition at line 63 of file parseCore.c.

#define STACKSIZE   1000

Definition at line 92 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 ///.

INCLUDES ///.

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 116 of file parseCore.c.

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 parantheses 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 parantheses ().\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 paranthesis\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 paranthesis\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 }
PARSE_SYM_CLOSE
#define PARSE_SYM_CLOSE
Definition: parseCore.c:51
PARSE_SYM_XOR
#define PARSE_SYM_XOR
Definition: parseCore.c:64
PARSE_SYM_OR2
#define PARSE_SYM_OR2
Definition: parseCore.c:66
PARSE_SYM_OR1
#define PARSE_SYM_OR1
Definition: parseCore.c:65
PARSE_SYM_OPEN
#define PARSE_SYM_OPEN
DECLARATIONS ///.
Definition: parseCore.c:50
Parse_StackOpStart
Parse_StackOp_t * Parse_StackOpStart(int nDepth)
Definition: parseStack.c:156
PARSE_OPER_FLL
#define PARSE_OPER_FLL
Definition: parseCore.c:83
STACKSIZE
#define STACKSIZE
Definition: parseCore.c:92
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
PARSE_SYM_NEGBEF2
#define PARSE_SYM_NEGBEF2
Definition: parseCore.c:57
Parse_StackFnPop
void * Parse_StackFnPop(Parse_StackFn_t *p)
Definition: parseStack.c:115
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdManager::size
int size
Definition: cuddInt.h:361
b1
#define b1
Definition: extraBdd.h:76
PARSE_FLAG_OPER
#define PARSE_FLAG_OPER
Definition: parseCore.c:89
PARSE_SYM_EQU3
#define PARSE_SYM_EQU3
Definition: parseCore.c:69
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
PARSE_OPER_OR
#define PARSE_OPER_OR
Definition: parseCore.c:80
Parse_StackFnFree
void Parse_StackFnFree(Parse_StackFn_t *p)
Definition: parseStack.c:136
PARSE_OPER_EQU
#define PARSE_OPER_EQU
Definition: parseCore.c:81
PARSE_SYM_CONST0
#define PARSE_SYM_CONST0
Definition: parseCore.c:54
PARSE_SYM_AND2
#define PARSE_SYM_AND2
Definition: parseCore.c:60
PARSE_SYM_EQU1
#define PARSE_SYM_EQU1
Definition: parseCore.c:67
PARSE_FLAG_START
#define PARSE_FLAG_START
Definition: parseCore.c:87
PARSE_SYM_XOR1
#define PARSE_SYM_XOR1
Definition: parseCore.c:61
Parse_StackFnIsEmpty
int Parse_StackFnIsEmpty(Parse_StackFn_t *p)
Definition: parseStack.c:78
Parse_StackOpIsEmpty
int Parse_StackOpIsEmpty(Parse_StackOp_t *p)
Definition: parseStack.c:177
Parse_ParserPerformTopOp
static DdNode * Parse_ParserPerformTopOp(DdManager *dd, Parse_StackFn_t *pStackFn, int Oper)
Definition: parseCore.c:504
PARSE_SYM_CONST1
#define PARSE_SYM_CONST1
Definition: parseCore.c:55
PARSE_OPER_FLR
#define PARSE_OPER_FLR
Definition: parseCore.c:82
PARSE_SYM_NEGBEF1
#define PARSE_SYM_NEGBEF1
Definition: parseCore.c:56
Extra_bddMove
DdNode * Extra_bddMove(DdManager *dd, DdNode *bF, int nVars)
Definition: extraBddMisc.c:187
PARSE_OPER_AND
#define PARSE_OPER_AND
Definition: parseCore.c:78
PARSE_FLAG_VAR
#define PARSE_FLAG_VAR
Definition: parseCore.c:88
Parse_StackOpPush
void Parse_StackOpPush(Parse_StackOp_t *p, int Oper)
Definition: parseStack.c:193
sprintf
char * sprintf()
PARSE_SYM_XOR3
#define PARSE_SYM_XOR3
Definition: parseCore.c:63
Parse_StackFn_t
typedefABC_NAMESPACE_HEADER_START struct ParseStackFnStruct Parse_StackFn_t
INCLUDES ///.
Definition: parseInt.h:43
PARSE_SYM_NEGAFT
#define PARSE_SYM_NEGAFT
Definition: parseCore.c:58
PARSE_SYM_AND1
#define PARSE_SYM_AND1
Definition: parseCore.c:59
PARSE_SYM_RAISE
#define PARSE_SYM_RAISE
Definition: parseCore.c:53
PARSE_OPER_MARK
#define PARSE_OPER_MARK
Definition: parseCore.c:84
Parse_StackOpFree
void Parse_StackOpFree(Parse_StackOp_t *p)
Definition: parseStack.c:235
b0
#define b0
Definition: extraBdd.h:75
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
PARSE_OPER_XOR
#define PARSE_OPER_XOR
Definition: parseCore.c:79
strncmp
int strncmp()
Parse_StackFnPush
void Parse_StackFnPush(Parse_StackFn_t *p, void *bFunc)
Definition: parseStack.c:94
Parse_StackFnStart
Parse_StackFn_t * Parse_StackFnStart(int nDepth)
GLOBAL VARIABLES ///.
Definition: parseStack.c:57
PARSE_SYM_XOR2
#define PARSE_SYM_XOR2
Definition: parseCore.c:62
PARSE_SYM_LOWER
#define PARSE_SYM_LOWER
Definition: parseCore.c:52
strlen
int strlen()
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
PARSE_SYM_EQU2
#define PARSE_SYM_EQU2
Definition: parseCore.c:68
Parse_StackOpPop
int Parse_StackOpPop(Parse_StackOp_t *p)
Definition: parseStack.c:214
PARSE_FLAG_ERROR
#define PARSE_FLAG_ERROR
Definition: parseCore.c:90
PARSE_OPER_NEG
#define PARSE_OPER_NEG
Definition: parseCore.c:77
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 504 of file parseCore.c.

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 }
PARSE_OPER_FLL
#define PARSE_OPER_FLL
Definition: parseCore.c:83
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Parse_StackFnPop
void * Parse_StackFnPop(Parse_StackFn_t *p)
Definition: parseStack.c:115
PARSE_OPER_OR
#define PARSE_OPER_OR
Definition: parseCore.c:80
PARSE_OPER_EQU
#define PARSE_OPER_EQU
Definition: parseCore.c:81
PARSE_OPER_FLR
#define PARSE_OPER_FLR
Definition: parseCore.c:82
PARSE_OPER_AND
#define PARSE_OPER_AND
Definition: parseCore.c:78
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
PARSE_OPER_XOR
#define PARSE_OPER_XOR
Definition: parseCore.c:79
Parse_StackFnPush
void Parse_StackFnPush(Parse_StackFn_t *p, void *bFunc)
Definition: parseStack.c:94
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129