abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ltl_parser.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ltl_parser.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Liveness property checking.]
8 
9  Synopsis [LTL checker.]
10 
11  Author [Sayak Ray]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2009.]
16 
17  Revision [$Id: ltl_parser.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <string.h>
23 #include <assert.h>
24 #include <stdlib.h>
25 #include "aig/aig/aig.h"
26 #include "base/abc/abc.h"
27 #include "base/main/mainInt.h"
28 
30 
31 
34 typedef enum ltlToken tokenType;
36 
37 struct ltlNode_t
38 {
40  char *name;
42  struct ltlNode_t *left;
43  struct ltlNode_t *right;
44 };
45 
46 typedef struct ltlNode_t ltlNode;
47 
49 //void generateTypedNode( ltlNode *new_node, tokenType new_type )
50 {
52 
53  new_node = (ltlNode *)malloc( sizeof(ltlNode) );
54  if( new_node )
55  {
56  new_node->type = new_type;
57  new_node->pObj = NULL;
58  new_node->name = NULL;
59  new_node->left = NULL;
60  new_node->right = NULL;
61  }
62 
63  return new_node;
64 }
65 
67 
68 static inline int isNotVarNameSymbol( char c )
69 {
70  return ( c == ' ' || c == '\t' || c == '\n' || c == ':' || c == '\0' );
71 }
72 
74 {
75  char *pLtlFormula, *tempFormula;
76  int i;
77 
78  if( pAbc->vLTLProperties_global != NULL )
79  {
80 // printf("Deleting exisitng LTL database from the frame\n");
81  Vec_PtrFree( pAbc->vLTLProperties_global );
82  pAbc->vLTLProperties_global = NULL;
83  }
84  pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
85  Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
86  {
87  tempFormula = (char *)malloc( sizeof(char)*(strlen(pLtlFormula)+1) );
88  sprintf( tempFormula, "%s", pLtlFormula );
89  Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
90  }
91 }
92 
93 char *getVarName( char *suffixFormula, int startLoc, int *endLocation )
94 {
95  int i = startLoc, length;
96  char *name;
97 
98  if( isNotVarNameSymbol( suffixFormula[startLoc] ) )
99  return NULL;
100 
101  while( !isNotVarNameSymbol( suffixFormula[i] ) )
102  i++;
103  *endLocation = i;
104  length = i - startLoc;
105  name = (char *)malloc( sizeof(char) * (length + 1));
106  for( i=0; i<length; i++ )
107  name[i] = suffixFormula[i+startLoc];
108  name[i] = '\0';
109 
110  return name;
111 }
112 
113 
115 
116 int isUnexpectedEOS( char *formula, int index )
117 {
118  assert( formula );
119  if( index >= (int)strlen( formula ) )
120  {
121  printf("\nInvalid LTL formula: unexpected end of string..." );
122  return 1;
123  }
124  return 0;
125 }
126 
127 int isTemporalOperator( char *formula, int index )
128 {
129  if( !(isUnexpectedEOS( formula, index ) || formula[ index ] == 'G' || formula[ index ] == 'F' || formula[ index ] == 'U' || formula[ index ] == 'X') )
130  {
131  printf("\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
132  return 0;
133  }
134  return 1;
135 }
136 
137 ltlNode *readLtlFormula( char *formula )
138 {
139  char ch;
140  char *varName;
141  int formulaLength, rememberEnd;
142  int i = startOfSuffixString;
143  ltlNode *curr_node, *temp_node_left, *temp_node_right;
144  char prevChar;
145 
146  formulaLength = strlen( formula );
147  if( isUnexpectedEOS( formula, startOfSuffixString ) )
148  {
149  printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
150  return NULL;
151  }
152 
153  while( i < formulaLength )
154  {
155  ch = formula[i];
156 
157  switch(ch){
158  case ' ':
159  case '\n':
160  case '\r':
161  case '\t':
162  case '\v':
163  case '\f':
164  i++;
166  break;
167  case ':':
168  i++;
169  if( !isTemporalOperator( formula, i ) )
170  return NULL;
172  break;
173  case 'G':
174  prevChar = formula[i-1];
175  if( prevChar == ':' ) //i.e. 'G' is a temporal operator
176  {
177  i++;
179  temp_node_left = readLtlFormula( formula );
180  if( temp_node_left == NULL )
181  return NULL;
182  else
183  {
184  curr_node = generateTypedNode(GLOBALLY);
185  curr_node->left = temp_node_left;
186  return curr_node;
187  }
188  }
189  else //i.e. 'G' must be starting a variable name
190  {
191  varName = getVarName( formula, i, &rememberEnd );
192  if( !varName )
193  {
194  printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
195  return NULL;
196  }
197  curr_node = generateTypedNode(BOOL);
198  curr_node->name = varName;
199  i = rememberEnd;
201  return curr_node;
202  }
203  case 'F':
204  prevChar = formula[i-1];
205  if( prevChar == ':' ) //i.e. 'F' is a temporal operator
206  {
207  i++;
209  temp_node_left = readLtlFormula( formula );
210  if( temp_node_left == NULL )
211  return NULL;
212  else
213  {
214  curr_node = generateTypedNode(EVENTUALLY);
215  curr_node->left = temp_node_left;
216  return curr_node;
217  }
218  }
219  else //i.e. 'F' must be starting a variable name
220  {
221  varName = getVarName( formula, i, &rememberEnd );
222  if( !varName )
223  {
224  printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
225  return NULL;
226  }
227  curr_node = generateTypedNode(BOOL);
228  curr_node->name = varName;
229  i = rememberEnd;
231  return curr_node;
232  }
233  case 'X':
234  prevChar = formula[i-1];
235  if( prevChar == ':' ) //i.e. 'X' is a temporal operator
236  {
237  i++;
239  temp_node_left = readLtlFormula( formula );
240  if( temp_node_left == NULL )
241  return NULL;
242  else
243  {
244  curr_node = generateTypedNode(NEXT);
245  curr_node->left = temp_node_left;
246  return curr_node;
247  }
248  }
249  else //i.e. 'X' must be starting a variable name
250  {
251  varName = getVarName( formula, i, &rememberEnd );
252  if( !varName )
253  {
254  printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
255  return NULL;
256  }
257  curr_node = generateTypedNode(BOOL);
258  curr_node->name = varName;
259  i = rememberEnd;
261  return curr_node;
262  }
263  case 'U':
264  prevChar = formula[i-1];
265  if( prevChar == ':' ) //i.e. 'X' is a temporal operator
266  {
267  i++;
269  temp_node_left = readLtlFormula( formula );
270  if( temp_node_left == NULL )
271  return NULL;
272  temp_node_right = readLtlFormula( formula );
273  if( temp_node_right == NULL )
274  {
275  //need to do memory management: if right subtree is NULL then left
276  //subtree must be freed.
277  return NULL;
278  }
279  curr_node = generateTypedNode(UNTIL);
280  curr_node->left = temp_node_left;
281  curr_node->right = temp_node_right;
282  return curr_node;
283  }
284  else //i.e. 'U' must be starting a variable name
285  {
286  varName = getVarName( formula, i, &rememberEnd );
287  if( !varName )
288  {
289  printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
290  return NULL;
291  }
292  curr_node = generateTypedNode(BOOL);
293  curr_node->name = varName;
294  i = rememberEnd;
296  return curr_node;
297  }
298  case '+':
299  i++;
301  temp_node_left = readLtlFormula( formula );
302  if( temp_node_left == NULL )
303  return NULL;
304  temp_node_right = readLtlFormula( formula );
305  if( temp_node_right == NULL )
306  {
307  //need to do memory management: if right subtree is NULL then left
308  //subtree must be freed.
309  return NULL;
310  }
311  curr_node = generateTypedNode(OR);
312  curr_node->left = temp_node_left;
313  curr_node->right = temp_node_right;
314  return curr_node;
315  case '&':
316  i++;
318  temp_node_left = readLtlFormula( formula );
319  if( temp_node_left == NULL )
320  return NULL;
321  temp_node_right = readLtlFormula( formula );
322  if( temp_node_right == NULL )
323  {
324  //need to do memory management: if right subtree is NULL then left
325  //subtree must be freed.
326  return NULL;
327  }
328  curr_node = generateTypedNode(AND);
329  curr_node->left = temp_node_left;
330  curr_node->right = temp_node_right;
331  return curr_node;
332  case '!':
333  i++;
335  temp_node_left = readLtlFormula( formula );
336  if( temp_node_left == NULL )
337  return NULL;
338  else
339  {
340  curr_node = generateTypedNode(NOT);
341  curr_node->left = temp_node_left;
342  return curr_node;
343  }
344  default:
345  varName = getVarName( formula, i, &rememberEnd );
346  if( !varName )
347  {
348  printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
349  return NULL;
350  }
351  curr_node = generateTypedNode(BOOL);
352  curr_node->name = varName;
353  i = rememberEnd;
355  return curr_node;
356  }
357  }
358  return NULL;
359 }
360 
362 {
364 }
365 
366 ltlNode *parseFormulaCreateAST( char *inputFormula )
367 {
368  ltlNode *temp;
369 
370  temp = readLtlFormula( inputFormula );
371  //if( temp == NULL )
372  // printf("\nAST creation failed for formula %s", inputFormula );
373  resetGlobalVar();
374  return temp;
375 }
376 
378 {
379  switch(node->type){
380  case( AND ):
381  printf("& ");
382  assert( node->left != NULL );
383  assert( node->right != NULL );
386  return;
387  case( OR ):
388  printf("+ ");
389  assert( node->left != NULL );
390  assert( node->right != NULL );
393  return;
394  case( NOT ):
395  printf("~ ");
396  assert( node->left != NULL );
398  assert( node->right == NULL );
399  return;
400  case( GLOBALLY ):
401  printf("G ");
402  assert( node->left != NULL );
404  assert( node->right == NULL );
405  return;
406  case( EVENTUALLY ):
407  printf("F ");
408  assert( node->left != NULL );
410  assert( node->right == NULL );
411  return;
412  case( NEXT ):
413  printf("X ");
414  assert( node->left != NULL );
416  assert( node->right == NULL );
417  return;
418  case( UNTIL ):
419  printf("U ");
420  assert( node->left != NULL );
421  assert( node->right != NULL );
424  return;
425  case( BOOL ):
426  printf("%s ", node->name);
427  assert( node->left == NULL );
428  assert( node->right == NULL );
429  return;
430  default:
431  printf("\nUnsupported token type: Exiting execution\n");
432  exit(0);
433  }
434 }
435 
437 {
438  switch(node->type){
439  case( AND ):
440  printf("( ");
441  assert( node->left != NULL );
442  assert( node->right != NULL );
444  printf("& ");
446  printf(") ");
447  return;
448  case( OR ):
449  printf("( ");
450  assert( node->left != NULL );
451  assert( node->right != NULL );
453  printf("+ ");
455  printf(") ");
456  return;
457  case( NOT ):
458  printf("~ ");
459  assert( node->left != NULL );
461  assert( node->right == NULL );
462  return;
463  case( GLOBALLY ):
464  printf("G ");
465  //printf("( ");
466  assert( node->left != NULL );
468  assert( node->right == NULL );
469  //printf(") ");
470  return;
471  case( EVENTUALLY ):
472  printf("F ");
473  //printf("( ");
474  assert( node->left != NULL );
476  assert( node->right == NULL );
477  //printf(") ");
478  return;
479  case( NEXT ):
480  printf("X ");
481  assert( node->left != NULL );
483  assert( node->right == NULL );
484  return;
485  case( UNTIL ):
486  printf("( ");
487  assert( node->left != NULL );
488  assert( node->right != NULL );
490  printf("U ");
492  printf(") ");
493  return;
494  case( BOOL ):
495  printf("%s ", node->name);
496  assert( node->left == NULL );
497  assert( node->right == NULL );
498  return;
499  default:
500  printf("\nUnsupported token type: Exiting execution\n");
501  exit(0);
502  }
503 }
504 
505 void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap )
506 {
507  ltlNode *nextNode, *nextToNextNode;
508  int serialNumSignal;
509 
510  switch( topASTNode->type ){
511  case AND:
512  case OR:
513  case IMPLY:
514  populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
515  populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
516  return;
517  case NOT:
518  populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
519  return;
520  case GLOBALLY:
521  nextNode = topASTNode->left;
522  assert( nextNode->type = EVENTUALLY );
523  nextToNextNode = nextNode->left;
524  if( nextToNextNode->type == BOOL )
525  {
526  assert( nextToNextNode->pObj );
527  serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
528  if( serialNumSignal == -1 )
529  {
530  Vec_PtrPush( vSignal, nextToNextNode->pObj );
531  serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
532  }
533  //Vec_PtrPush( vGLOBALLY, topASTNode );
534  Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
535  }
536  else
537  {
538  assert( nextToNextNode->pObj == NULL );
539  buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
540  serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
541  if( serialNumSignal == -1 )
542  {
543  Vec_PtrPush( vSignal, nextToNextNode->pObj );
544  serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
545  }
546  //Vec_PtrPush( vGLOBALLY, topASTNode );
547  Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
548  }
549  return;
550  case BOOL:
551  return;
552  default:
553  printf("\nINVALID situation: aborting...\n");
554  exit(0);
555  }
556 }
557 
559 {
560  Aig_Obj_t *leftAigObj, *rightAigObj;
561 
562  if( pLtlNode->pObj != NULL )
563  return pLtlNode->pObj;
564  else
565  {
566  assert( pLtlNode->type != BOOL );
567  switch( pLtlNode->type ){
568  case AND:
569  assert( pLtlNode->left ); assert( pLtlNode->right );
570  leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
571  rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
572  assert( leftAigObj ); assert( rightAigObj );
573  pLtlNode->pObj = Aig_And( pAigNew, leftAigObj, rightAigObj );
574  return pLtlNode->pObj;
575  case OR:
576  assert( pLtlNode->left ); assert( pLtlNode->right );
577  leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
578  rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
579  assert( leftAigObj ); assert( rightAigObj );
580  pLtlNode->pObj = Aig_Or( pAigNew, leftAigObj, rightAigObj );
581  return pLtlNode->pObj;
582  case NOT:
583  assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
584  leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
585  assert( leftAigObj );
586  pLtlNode->pObj = Aig_Not( leftAigObj );
587  return pLtlNode->pObj;
588  case GLOBALLY:
589  case EVENTUALLY:
590  case NEXT:
591  case UNTIL:
592  printf("FORBIDDEN node: ABORTING!!\n");
593  exit(0);
594  default:
595  printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
596  exit(0);
597  }
598  }
599 }
600 
602 {
603  Aig_Obj_t *leftAigObj, *rightAigObj;
604 
605  if( pLtlNode->pObj != NULL )
606  return pLtlNode->pObj;
607  else
608  {
609  assert( pLtlNode->type != BOOL );
610  switch( pLtlNode->type ){
611  case AND:
612  assert( pLtlNode->left ); assert( pLtlNode->right );
613  leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
614  rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
615  assert( leftAigObj ); assert( rightAigObj );
616  pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
617  return pLtlNode->pObj;
618  case OR:
619  assert( pLtlNode->left ); assert( pLtlNode->right );
620  leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
621  rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
622  assert( leftAigObj ); assert( rightAigObj );
623  pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
624  return pLtlNode->pObj;
625  case NOT:
626  assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
627  leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
628  assert( leftAigObj );
629  pLtlNode->pObj = Aig_Not( leftAigObj );
630  return pLtlNode->pObj;
631  case GLOBALLY:
632  case EVENTUALLY:
633  case NEXT:
634  case UNTIL:
635  printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
636  exit(0);
637  default:
638  printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
639  exit(0);
640  }
641  }
642 }
643 
645 {
646  switch( topNode->type ){
647  case AND:
648  case OR:
649  case IMPLY:
650  return isNonTemporalSubformula( topNode->left) && isNonTemporalSubformula( topNode->right ) ;
651  case NOT:
652  assert( topNode->right == NULL );
653  return isNonTemporalSubformula( topNode->left );
654  case BOOL:
655  return 1;
656  default:
657  return 0;
658  }
659 }
660 
661 int isWellFormed( ltlNode *topNode )
662 {
663  ltlNode *nextNode;
664 
665  switch( topNode->type ){
666  case AND:
667  case OR:
668  case IMPLY:
669  return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
670  case NOT:
671  assert( topNode->right == NULL );
672  return isWellFormed( topNode->left );
673  case BOOL:
674  return 1;
675  case GLOBALLY:
676  nextNode = topNode->left;
677  assert( topNode->right == NULL );
678  if( nextNode->type != EVENTUALLY )
679  return 0;
680  else
681  {
682  assert( nextNode->right == NULL );
683  return isNonTemporalSubformula( nextNode->left );
684  }
685  default:
686  return 0;
687  }
688 }
689 
690 int checkBooleanConstant( char *targetName )
691 {
692  if( strcmp( targetName, "true" ) == 0 )
693  return 1;
694  if( strcmp( targetName, "false" ) == 0 )
695  return 0;
696  return -1;
697 }
698 
699 int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode )
700 {
701  char *targetName;
702  Abc_Obj_t * pNode;
703  int i;
704 
705  switch( topASTNode->type ){
706  case BOOL:
707  targetName = topASTNode->name;
708  //printf("\nTrying to match name %s\n", targetName);
709  if( checkBooleanConstant( targetName ) != -1 )
710  return 1;
711  Abc_NtkForEachPo( pNtk, pNode, i )
712  {
713  if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
714  {
715  //printf("\nVariable name \"%s\" MATCHED\n", targetName);
716  return 1;
717  }
718  }
719  printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
720  return 0;
721  case AND:
722  case OR:
723  case IMPLY:
724  case UNTIL:
725  assert( topASTNode->left != NULL );
726  assert( topASTNode->right != NULL );
727  return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );
728 
729  case NOT:
730  case NEXT:
731  case GLOBALLY:
732  case EVENTUALLY:
733  assert( topASTNode->left != NULL );
734  assert( topASTNode->right == NULL );
735  return checkSignalNameExistence( pNtk, topASTNode->left );
736  default:
737  printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
738  exit(0);
739  }
740 }
741 
742 void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode )
743 {
744  char *targetName;
745  Abc_Obj_t * pNode;
746  int i;
747  Aig_Obj_t *pObj, *pDriverImage;
748 
749  switch( topASTNode->type ){
750  case BOOL:
751  targetName = topASTNode->name;
752  if( checkBooleanConstant( targetName ) == 1 )
753  {
754  topASTNode->pObj = Aig_ManConst1( pAigNew );
755  return;
756  }
757  if( checkBooleanConstant( targetName ) == 0 )
758  {
759  topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
760  return;
761  }
762  Abc_NtkForEachPo( pNtk, pNode, i )
763  if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
764  {
765  pObj = Aig_ManCo( pAigOld, i );
766  assert( Aig_ObjIsCo( pObj ));
767  pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
768  topASTNode->pObj = pDriverImage;
769  return;
770  }
771  assert(0);
772  case AND:
773  case OR:
774  case IMPLY:
775  case UNTIL:
776  assert( topASTNode->left != NULL );
777  assert( topASTNode->right != NULL );
778  populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
779  populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
780  return;
781  case NOT:
782  case NEXT:
783  case GLOBALLY:
784  case EVENTUALLY:
785  assert( topASTNode->left != NULL );
786  assert( topASTNode->right == NULL );
787  populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
788  return;
789  default:
790  printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
791  exit(0);
792  }
793 }
794 
796 {
797 
798  switch( topASTNode->type ){
799  case BOOL:
800  if( topASTNode->pObj != NULL )
801  return 1;
802  else
803  {
804  printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
805  return 0;
806  }
807  case AND:
808  case OR:
809  case IMPLY:
810  case UNTIL:
811  assert( topASTNode->left != NULL );
812  assert( topASTNode->right != NULL );
813  return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );
814 
815  case NOT:
816  case NEXT:
817  case GLOBALLY:
818  case EVENTUALLY:
819  assert( topASTNode->left != NULL );
820  assert( topASTNode->right == NULL );
821  return checkAllBoolHaveAIGPointer( topASTNode->left );
822  default:
823  printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
824  exit(0);
825  }
826 }
827 
829 {
830  astNode->pObj = pObjLo;
831 }
832 
834 {
835  return astNode->pObj;
836 }
837 
838 
Aig_Obj_t * buildLogicFromLTLNode_combinationalOnly(Aig_Man_t *pAig, ltlNode *pLtlNode)
Definition: ltl_parser.c:558
ltlNode * generateTypedNode(tokenType new_type)
Definition: ltl_parser.c:48
char * malloc()
VOID_HACK exit()
Vec_Ptr_t * vLtlProperties
Definition: abc.h:169
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
int checkAllBoolHaveAIGPointer(ltlNode *topASTNode)
Definition: ltl_parser.c:795
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
int isNonTemporalSubformula(ltlNode *topNode)
Definition: ltl_parser.c:644
int isTemporalOperator(char *formula, int index)
Definition: ltl_parser.c:127
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
ltlNode * readLtlFormula(char *formula)
Definition: ltl_parser.c:137
static avl_node * new_node()
struct ltlNode_t * left
Definition: ltl_parser.c:42
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
void setAIGNodePtrOfGloballyNode(ltlNode *astNode, Aig_Obj_t *pObjLo)
Definition: ltl_parser.c:828
void traverseAbstractSyntaxTree(ltlNode *node)
Definition: ltl_parser.c:377
static int Vec_PtrFind(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:694
int isUnexpectedEOS(char *formula, int index)
Definition: ltl_parser.c:116
ltlGrammerToken
Definition: ltl_parser.c:33
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
int strcmp()
Definition: ltl_parser.c:33
int isWellFormed(ltlNode *topNode)
Definition: ltl_parser.c:661
int checkBooleanConstant(char *targetName)
Definition: ltl_parser.c:690
char * name
Definition: ltl_parser.c:40
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
void populateBoolWithAigNodePtr(Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode)
Definition: ltl_parser.c:742
tokenType type
Definition: ltl_parser.c:39
static int isNotVarNameSymbol(char c)
Definition: ltl_parser.c:68
char * name
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Definition: ltl_parser.c:33
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
char * sprintf()
struct ltlNode_t * right
Definition: ltl_parser.c:43
Definition: ltl_parser.c:32
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
void populateAigPointerUnitGF(Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap)
Definition: ltl_parser.c:505
enum ltlToken tokenType
Definition: ltl_parser.c:34
Definition: ltl_parser.c:32
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void resetGlobalVar()
Definition: ltl_parser.c:361
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
int checkSignalNameExistence(Abc_Ntk_t *pNtk, ltlNode *topASTNode)
Definition: ltl_parser.c:699
ltlToken
Definition: ltl_parser.c:32
enum ltlGrammerToken ltlGrammerTokenType
Definition: ltl_parser.c:35
Aig_Obj_t * buildLogicFromLTLNode(Aig_Man_t *pAig, ltlNode *pLtlNode)
Definition: ltl_parser.c:601
Aig_Obj_t * pObj
Definition: ltl_parser.c:41
Definition: ltl_parser.c:32
#define assert(ex)
Definition: util_old.h:213
int strlen()
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
ltlNode * parseFormulaCreateAST(char *inputFormula)
Definition: ltl_parser.c:366
Aig_Obj_t * retriveAIGPointerFromLTLNode(ltlNode *astNode)
Definition: ltl_parser.c:833
char * getVarName(char *suffixFormula, int startLoc, int *endLocation)
Definition: ltl_parser.c:93
int startOfSuffixString
Definition: ltl_parser.c:114
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
void Abc_FrameCopyLTLDataBase(Abc_Frame_t *pAbc, Abc_Ntk_t *pNtk)
Definition: ltl_parser.c:73
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void traverseAbstractSyntaxTree_postFix(ltlNode *node)
Definition: ltl_parser.c:436