abc/src/proof/live/ltl_parser.c - third_party/vtr-verilog-to-routing - Git at Google

 /**CFile****************************************************************

   FileName    [ltl_parser.c]

   SystemName  [ABC: Logic synthesis and verification system.]

   PackageName [Liveness property checking.]

   Synopsis    [LTL checker.]

   Author      [Sayak Ray]

   Affiliation [UC Berkeley]

   Date        [Ver. 1.0. Started - January 1, 2009.]

   Revision    [$Id: ltl_parser.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]

 ***********************************************************************/

 #include <stdio.h>
 #include <string.h>
 #include <assert.h>
 #include <stdlib.h>
 #include "aig/aig/aig.h"
 #include "base/abc/abc.h"
 #include "base/main/mainInt.h"

 ABC_NAMESPACE_IMPL_START


 enum ltlToken { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL };
 enum ltlGrammerToken { OPERAND, LTL, BINOP, UOP };
 typedef enum ltlToken tokenType;
 typedef enum ltlGrammerToken ltlGrammerTokenType;

 struct ltlNode_t
 {
     tokenType type;
     char *name;
     Aig_Obj_t *pObj;
     struct ltlNode_t *left;
     struct ltlNode_t *right;
 };

 typedef struct ltlNode_t ltlNode;

 ltlNode *generateTypedNode( tokenType new_type )
 //void generateTypedNode( ltlNode *new_node, tokenType new_type )
 {
     ltlNode *new_node;

     new_node = (ltlNode *)malloc( sizeof(ltlNode) );
     if( new_node )
     {
         new_node->type = new_type;
         new_node->pObj = NULL;
         new_node->name = NULL;
         new_node->left = NULL;
         new_node->right = NULL;
     }

     return new_node;
 }

 Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAig, ltlNode *pLtlNode );

 static inline int isNotVarNameSymbol( char c )
 {
     return ( c == ' ' || c == '\t' || c == '\n' || c == ':' || c == '\0' );
 }

 void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk )
 {
     char *pLtlFormula, *tempFormula;
     int i;

     if( pAbc->vLTLProperties_global != NULL )
     {
 //        printf("Deleting exisitng LTL database from the frame\n");
         Vec_PtrFree( pAbc->vLTLProperties_global );
         pAbc->vLTLProperties_global = NULL;
     }
     pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
     Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
     {
         tempFormula = (char *)malloc( sizeof(char)*(strlen(pLtlFormula)+1) );
         sprintf( tempFormula, "%s", pLtlFormula );
         Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
     }
 }

 char *getVarName( char *suffixFormula, int startLoc, int *endLocation )
 {
     int i = startLoc, length;
     char *name;

     if( isNotVarNameSymbol( suffixFormula[startLoc] ) )
         return NULL;

     while( !isNotVarNameSymbol( suffixFormula[i] ) )
         i++;
     *endLocation = i;
     length = i - startLoc;
     name = (char *)malloc( sizeof(char) * (length + 1));
     for( i=0; i<length; i++ )
         name[i] = suffixFormula[i+startLoc];
     name[i] = '\0';

     return name;
 }


 int startOfSuffixString = 0;

 int isUnexpectedEOS( char *formula, int index )
 {
     assert( formula );
     if( index >= (int)strlen( formula ) )
     {
         printf("\nInvalid LTL formula: unexpected end of string..." );
         return 1;
     }
     return 0;
 }

 int isTemporalOperator( char *formula, int index )
 {
     if( !(isUnexpectedEOS( formula, index ) || formula[ index ] == 'G' || formula[ index ] == 'F' || formula[ index ] == 'U' || formula[ index ] == 'X') )
     {
         printf("\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
         return 0;
     }
     return 1;
 }

 ltlNode *readLtlFormula( char *formula )
 {
     char ch;
     char *varName;
     int formulaLength, rememberEnd;
     int i = startOfSuffixString;
     ltlNode *curr_node, *temp_node_left, *temp_node_right;
     char prevChar;

     formulaLength = strlen( formula );
     if( isUnexpectedEOS( formula, startOfSuffixString ) )
     {
         printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
         return NULL;
     }

     while( i < formulaLength )
     {
         ch = formula[i];

         switch(ch){
             case ' ':
             case '\n':
             case '\r':
             case '\t':
             case '\v':
             case '\f':
                         i++;
                         startOfSuffixString = i;
                         break;
             case ':':
                         i++;
                         if( !isTemporalOperator( formula, i ) )
                             return NULL;
                         startOfSuffixString = i;
                         break;
             case 'G':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'G' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(GLOBALLY);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else    //i.e. 'G' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }
             case 'F':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'F' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(EVENTUALLY);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else //i.e. 'F' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }
             case 'X':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             else
                             {
                                 curr_node = generateTypedNode(NEXT);
                                 curr_node->left = temp_node_left;
                                 return curr_node;
                             }
                         }
                         else //i.e. 'X' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }
             case 'U':
                         prevChar = formula[i-1];
                         if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                         {
                             i++;
                             startOfSuffixString = i;
                             temp_node_left = readLtlFormula( formula );
                             if( temp_node_left == NULL )
                                 return NULL;
                             temp_node_right = readLtlFormula( formula );
                             if( temp_node_right == NULL )
                             {
                                 //need to do memory management: if right subtree is NULL then left
                                 //subtree must be freed.
                                 return NULL;
                             }
                             curr_node = generateTypedNode(UNTIL);
                             curr_node->left = temp_node_left;
                             curr_node->right = temp_node_right;
                             return curr_node;
                         }
                         else //i.e. 'U' must be starting a variable name
                         {
                             varName = getVarName( formula, i, &rememberEnd );
                             if( !varName )
                             {
                                 printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                 return NULL;
                             }
                             curr_node = generateTypedNode(BOOL);
                             curr_node->name = varName;
                             i = rememberEnd;
                             startOfSuffixString = i;
                             return curr_node;
                         }
             case '+':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         temp_node_right = readLtlFormula( formula );
                         if( temp_node_right == NULL )
                         {
                             //need to do memory management: if right subtree is NULL then left
                             //subtree must be freed.
                             return NULL;
                         }
                         curr_node = generateTypedNode(OR);
                         curr_node->left = temp_node_left;
                         curr_node->right = temp_node_right;
                         return curr_node;
             case '&':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         temp_node_right = readLtlFormula( formula );
                         if( temp_node_right == NULL )
                         {
                             //need to do memory management: if right subtree is NULL then left
                             //subtree must be freed.
                             return NULL;
                         }
                         curr_node = generateTypedNode(AND);
                         curr_node->left = temp_node_left;
                         curr_node->right = temp_node_right;
                         return curr_node;
             case '!':
                         i++;
                         startOfSuffixString = i;
                         temp_node_left = readLtlFormula( formula );
                         if( temp_node_left == NULL )
                             return NULL;
                         else
                         {
                             curr_node = generateTypedNode(NOT);
                             curr_node->left = temp_node_left;
                             return curr_node;
                         }
             default:
                 varName = getVarName( formula, i, &rememberEnd );
                 if( !varName )
                 {
                     printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                     return NULL;
                 }
                 curr_node = generateTypedNode(BOOL);
                 curr_node->name = varName;
                 i = rememberEnd;
                 startOfSuffixString = i;
                 return curr_node;
         }
     }
     return NULL;
 }

 void resetGlobalVar()
 {
     startOfSuffixString = 0;
 }

 ltlNode *parseFormulaCreateAST( char *inputFormula )
 {
     ltlNode *temp;

     temp = readLtlFormula( inputFormula );
     //if( temp == NULL )
     //    printf("\nAST creation failed for formula %s", inputFormula );
     resetGlobalVar();
     return temp;
 }

 void traverseAbstractSyntaxTree( ltlNode *node )
 {
     switch(node->type){
         case( AND ):
             printf("& ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( OR ):
             printf("+ ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( NOT ):
             printf("~ ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( GLOBALLY ):
             printf("G ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( EVENTUALLY ):
             printf("F ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( NEXT ):
             printf("X ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree( node->left );
             assert( node->right == NULL );
             return;
         case( UNTIL ):
             printf("U ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree( node->left );
             traverseAbstractSyntaxTree( node->right );
             return;
         case( BOOL ):
             printf("%s ", node->name);
             assert( node->left == NULL );
             assert( node->right == NULL );
             return;
         default:
             printf("\nUnsupported token type: Exiting execution\n");
             exit(0);
     }
 }

 void traverseAbstractSyntaxTree_postFix( ltlNode *node )
 {
     switch(node->type){
         case( AND ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("& ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( OR ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("+ ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( NOT ):
             printf("~ ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             return;
         case( GLOBALLY ):
             printf("G ");
             //printf("( ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             //printf(") ");
             return;
         case( EVENTUALLY ):
             printf("F ");
             //printf("( ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             //printf(") ");
             return;
         case( NEXT ):
             printf("X ");
             assert( node->left != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             assert( node->right == NULL );
             return;
         case( UNTIL ):
             printf("( ");
             assert( node->left != NULL );
             assert( node->right != NULL );
             traverseAbstractSyntaxTree_postFix( node->left );
             printf("U ");
             traverseAbstractSyntaxTree_postFix( node->right );
             printf(") ");
             return;
         case( BOOL ):
             printf("%s ", node->name);
             assert( node->left == NULL );
             assert( node->right == NULL );
             return;
         default:
             printf("\nUnsupported token type: Exiting execution\n");
             exit(0);
     }
 }

 void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap )
 {
     ltlNode *nextNode, *nextToNextNode;
     int serialNumSignal;

     switch( topASTNode->type ){
         case AND:
         case OR:
         case IMPLY:
             populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
             populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
             return;
         case NOT:
             populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
             return;
         case GLOBALLY:
             nextNode = topASTNode->left;
             assert( nextNode->type = EVENTUALLY );
             nextToNextNode = nextNode->left;
             if( nextToNextNode->type == BOOL )
             {
                 assert( nextToNextNode->pObj );
                 serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 if( serialNumSignal == -1 )
                 {
                     Vec_PtrPush( vSignal, nextToNextNode->pObj );
                     serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 }
                 //Vec_PtrPush( vGLOBALLY, topASTNode );
                 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
             }
             else
             {
                 assert( nextToNextNode->pObj == NULL );
                 buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
                 serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 if( serialNumSignal == -1 )
                 {
                     Vec_PtrPush( vSignal, nextToNextNode->pObj );
                     serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                 }
                 //Vec_PtrPush( vGLOBALLY, topASTNode );
                 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
             }
             return;
         case BOOL:
             return;
         default:
             printf("\nINVALID situation: aborting...\n");
             exit(0);
     }
 }

 Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAigNew, ltlNode *pLtlNode )
 {
     Aig_Obj_t *leftAigObj, *rightAigObj;

     if( pLtlNode->pObj != NULL )
         return pLtlNode->pObj;
     else
     {
         assert( pLtlNode->type != BOOL );
         switch( pLtlNode->type ){
             case AND:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_And( pAigNew, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case OR:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_Or( pAigNew, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case NOT:
                 assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
                 leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
                 assert( leftAigObj );
                 pLtlNode->pObj = Aig_Not( leftAigObj );
                 return pLtlNode->pObj;
             case GLOBALLY:
             case EVENTUALLY:
             case NEXT:
             case UNTIL:
                 printf("FORBIDDEN node: ABORTING!!\n");
                 exit(0);
             default:
                 printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
                 exit(0);
         }
     }
 }

 Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode )
 {
     Aig_Obj_t *leftAigObj, *rightAigObj;

     if( pLtlNode->pObj != NULL )
         return pLtlNode->pObj;
     else
     {
         assert( pLtlNode->type != BOOL );
         switch( pLtlNode->type ){
             case AND:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case OR:
                 assert( pLtlNode->left ); assert( pLtlNode->right );
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                 assert( leftAigObj ); assert( rightAigObj );
                 pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
                 return pLtlNode->pObj;
             case NOT:
                 assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
                 leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                 assert( leftAigObj );
                 pLtlNode->pObj = Aig_Not( leftAigObj );
                 return pLtlNode->pObj;
             case GLOBALLY:
             case EVENTUALLY:
             case NEXT:
             case UNTIL:
                 printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
                 exit(0);
             default:
                 printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
                 exit(0);
         }
     }
 }

 int isNonTemporalSubformula( ltlNode *topNode )
 {
     switch( topNode->type ){
         case AND:
         case OR:
         case IMPLY:
             return isNonTemporalSubformula( topNode->left) && isNonTemporalSubformula( topNode->right ) ;
         case NOT:
             assert( topNode->right == NULL );
             return isNonTemporalSubformula( topNode->left );
         case BOOL:
             return 1;
         default:
             return 0;
     }
 }

 int isWellFormed( ltlNode *topNode )
 {
     ltlNode *nextNode;

     switch( topNode->type ){
         case AND:
         case OR:
         case IMPLY:
             return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
         case NOT:
             assert( topNode->right == NULL );
             return isWellFormed( topNode->left );
         case BOOL:
             return 1;
         case GLOBALLY:
             nextNode = topNode->left;
             assert( topNode->right == NULL );
             if( nextNode->type != EVENTUALLY )
                 return 0;
             else
             {
                 assert( nextNode->right == NULL );
                 return isNonTemporalSubformula( nextNode->left );
             }
         default:
             return 0;
     }
 }

 int checkBooleanConstant( char *targetName )
 {
     if( strcmp( targetName, "true" ) == 0 )
         return 1;
     if( strcmp( targetName, "false" ) == 0 )
         return 0;
     return -1;
 }

 int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode )
 {
     char *targetName;
     Abc_Obj_t * pNode;
     int i;

     switch( topASTNode->type ){
         case BOOL:
             targetName = topASTNode->name;
             //printf("\nTrying to match name %s\n", targetName);
             if( checkBooleanConstant( targetName ) != -1 )
                 return 1;
             Abc_NtkForEachPo( pNtk, pNode, i )
             {
                 if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                 {
                     //printf("\nVariable name \"%s\" MATCHED\n", targetName);
                     return 1;
                 }
             }
             printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
             return 0;
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );

         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             return checkSignalNameExistence( pNtk, topASTNode->left );
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

 void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode )
 {
     char *targetName;
     Abc_Obj_t * pNode;
     int i;
     Aig_Obj_t *pObj, *pDriverImage;

     switch( topASTNode->type ){
         case BOOL:
             targetName = topASTNode->name;
             if( checkBooleanConstant( targetName ) == 1 )
             {
                 topASTNode->pObj = Aig_ManConst1( pAigNew );
                 return;
             }
             if( checkBooleanConstant( targetName ) == 0 )
             {
                 topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
                 return;
             }
             Abc_NtkForEachPo( pNtk, pNode, i )
                 if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                 {
                     pObj = Aig_ManCo( pAigOld, i );
                     assert( Aig_ObjIsCo( pObj ));
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                     topASTNode->pObj = pDriverImage;
                     return;
                 }
             assert(0);
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
             return;
         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
             return;
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

 int checkAllBoolHaveAIGPointer( ltlNode *topASTNode )
 {

     switch( topASTNode->type ){
         case BOOL:
             if( topASTNode->pObj != NULL )
                 return 1;
             else
             {
                 printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
                 return 0;
             }
         case AND:
         case OR:
         case IMPLY:
         case UNTIL:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right != NULL );
             return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );

         case NOT:
         case NEXT:
         case GLOBALLY:
         case EVENTUALLY:
             assert( topASTNode->left != NULL );
             assert( topASTNode->right == NULL );
             return checkAllBoolHaveAIGPointer( topASTNode->left );
         default:
             printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
             exit(0);
     }
 }

 void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo )
 {
     astNode->pObj = pObjLo;
 }

 Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode )
 {
     return astNode->pObj;
 }


 ABC_NAMESPACE_IMPL_END
	/CFile**************************************************************

	FileName [ltl_parser.c]

	SystemName [ABC: Logic synthesis and verification system.]

	PackageName [Liveness property checking.]

	Synopsis [LTL checker.]

	Author [Sayak Ray]

	Affiliation [UC Berkeley]

	Date [Ver. 1.0. Started - January 1, 2009.]

	Revision [$Id: ltl_parser.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]

	***********************************************************************/

	#include <stdio.h>
	#include <string.h>
	#include <assert.h>
	#include <stdlib.h>
	#include "aig/aig/aig.h"
	#include "base/abc/abc.h"
	#include "base/main/mainInt.h"

	ABC_NAMESPACE_IMPL_START


	enum ltlToken { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL };
	enum ltlGrammerToken { OPERAND, LTL, BINOP, UOP };
	typedef enum ltlToken tokenType;
	typedef enum ltlGrammerToken ltlGrammerTokenType;

	struct ltlNode_t
	{
	tokenType type;
	char *name;
	Aig_Obj_t *pObj;
	struct ltlNode_t *left;
	struct ltlNode_t *right;
	};

	typedef struct ltlNode_t ltlNode;

	ltlNode *generateTypedNode( tokenType new_type )
	//void generateTypedNode( ltlNode *new_node, tokenType new_type )
	{
	ltlNode *new_node;

	new_node = (ltlNode *)malloc( sizeof(ltlNode) );
	if( new_node )
	{
	new_node->type = new_type;
	new_node->pObj = NULL;
	new_node->name = NULL;
	new_node->left = NULL;
	new_node->right = NULL;
	}

	return new_node;
	}

	Aig_Obj_t buildLogicFromLTLNode_combinationalOnly( Aig_Man_t pAig, ltlNode *pLtlNode );

	static inline int isNotVarNameSymbol( char c )
	{
	return ( c == ' ' \|\| c == '\t' \|\| c == '\n' \|\| c == ':' \|\| c == '\0' );
	}

	void Abc_FrameCopyLTLDataBase( Abc_Frame_t pAbc, Abc_Ntk_t pNtk )
	{
	char pLtlFormula, tempFormula;
	int i;

	if( pAbc->vLTLProperties_global != NULL )
	{
	// printf("Deleting exisitng LTL database from the frame\n");
	Vec_PtrFree( pAbc->vLTLProperties_global );
	pAbc->vLTLProperties_global = NULL;
	}
	pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
	Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
	{
	tempFormula = (char )malloc( sizeof(char)(strlen(pLtlFormula)+1) );
	sprintf( tempFormula, "%s", pLtlFormula );
	Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
	}
	}

	char getVarName( char suffixFormula, int startLoc, int *endLocation )
	{
	int i = startLoc, length;
	char *name;

	if( isNotVarNameSymbol( suffixFormula[startLoc] ) )
	return NULL;

	while( !isNotVarNameSymbol( suffixFormula[i] ) )
	i++;
	*endLocation = i;
	length = i - startLoc;
	name = (char )malloc( sizeof(char) (length + 1));
	for( i=0; i<length; i++ )
	name[i] = suffixFormula[i+startLoc];
	name[i] = '\0';

	return name;
	}


	int startOfSuffixString = 0;

	int isUnexpectedEOS( char *formula, int index )
	{
	assert( formula );
	if( index >= (int)strlen( formula ) )
	{
	printf("\nInvalid LTL formula: unexpected end of string..." );
	return 1;
	}
	return 0;
	}

	int isTemporalOperator( char *formula, int index )
	{
	if( !(isUnexpectedEOS( formula, index ) \|\| formula[ index ] == 'G' \|\| formula[ index ] == 'F' \|\| formula[ index ] == 'U' \|\| formula[ index ] == 'X') )
	{
	printf("\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
	return 0;
	}
	return 1;
	}

	ltlNode readLtlFormula( char formula )
	{
	char ch;
	char *varName;
	int formulaLength, rememberEnd;
	int i = startOfSuffixString;
	ltlNode curr_node, temp_node_left, *temp_node_right;
	char prevChar;

	formulaLength = strlen( formula );
	if( isUnexpectedEOS( formula, startOfSuffixString ) )
	{
	printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
	return NULL;
	}

	while( i < formulaLength )
	{
	ch = formula[i];

	switch(ch){
	case ' ':
	case '\n':
	case '\r':
	case '\t':
	case '\v':
	case '\f':
	i++;
	startOfSuffixString = i;
	break;
	case ':':
	i++;
	if( !isTemporalOperator( formula, i ) )
	return NULL;
	startOfSuffixString = i;
	break;
	case 'G':
	prevChar = formula[i-1];
	if( prevChar == ':' ) //i.e. 'G' is a temporal operator
	{
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	else
	{
	curr_node = generateTypedNode(GLOBALLY);
	curr_node->left = temp_node_left;
	return curr_node;
	}
	}
	else //i.e. 'G' must be starting a variable name
	{
	varName = getVarName( formula, i, &rememberEnd );
	if( !varName )
	{
	printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
	return NULL;
	}
	curr_node = generateTypedNode(BOOL);
	curr_node->name = varName;
	i = rememberEnd;
	startOfSuffixString = i;
	return curr_node;
	}
	case 'F':
	prevChar = formula[i-1];
	if( prevChar == ':' ) //i.e. 'F' is a temporal operator
	{
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	else
	{
	curr_node = generateTypedNode(EVENTUALLY);
	curr_node->left = temp_node_left;
	return curr_node;
	}
	}
	else //i.e. 'F' must be starting a variable name
	{
	varName = getVarName( formula, i, &rememberEnd );
	if( !varName )
	{
	printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
	return NULL;
	}
	curr_node = generateTypedNode(BOOL);
	curr_node->name = varName;
	i = rememberEnd;
	startOfSuffixString = i;
	return curr_node;
	}
	case 'X':
	prevChar = formula[i-1];
	if( prevChar == ':' ) //i.e. 'X' is a temporal operator
	{
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	else
	{
	curr_node = generateTypedNode(NEXT);
	curr_node->left = temp_node_left;
	return curr_node;
	}
	}
	else //i.e. 'X' must be starting a variable name
	{
	varName = getVarName( formula, i, &rememberEnd );
	if( !varName )
	{
	printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
	return NULL;
	}
	curr_node = generateTypedNode(BOOL);
	curr_node->name = varName;
	i = rememberEnd;
	startOfSuffixString = i;
	return curr_node;
	}
	case 'U':
	prevChar = formula[i-1];
	if( prevChar == ':' ) //i.e. 'X' is a temporal operator
	{
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	temp_node_right = readLtlFormula( formula );
	if( temp_node_right == NULL )
	{
	//need to do memory management: if right subtree is NULL then left
	//subtree must be freed.
	return NULL;
	}
	curr_node = generateTypedNode(UNTIL);
	curr_node->left = temp_node_left;
	curr_node->right = temp_node_right;
	return curr_node;
	}
	else //i.e. 'U' must be starting a variable name
	{
	varName = getVarName( formula, i, &rememberEnd );
	if( !varName )
	{
	printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
	return NULL;
	}
	curr_node = generateTypedNode(BOOL);
	curr_node->name = varName;
	i = rememberEnd;
	startOfSuffixString = i;
	return curr_node;
	}
	case '+':
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	temp_node_right = readLtlFormula( formula );
	if( temp_node_right == NULL )
	{
	//need to do memory management: if right subtree is NULL then left
	//subtree must be freed.
	return NULL;
	}
	curr_node = generateTypedNode(OR);
	curr_node->left = temp_node_left;
	curr_node->right = temp_node_right;
	return curr_node;
	case '&':
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	temp_node_right = readLtlFormula( formula );
	if( temp_node_right == NULL )
	{
	//need to do memory management: if right subtree is NULL then left
	//subtree must be freed.
	return NULL;
	}
	curr_node = generateTypedNode(AND);
	curr_node->left = temp_node_left;
	curr_node->right = temp_node_right;
	return curr_node;
	case '!':
	i++;
	startOfSuffixString = i;
	temp_node_left = readLtlFormula( formula );
	if( temp_node_left == NULL )
	return NULL;
	else
	{
	curr_node = generateTypedNode(NOT);
	curr_node->left = temp_node_left;
	return curr_node;
	}
	default:
	varName = getVarName( formula, i, &rememberEnd );
	if( !varName )
	{
	printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
	return NULL;
	}
	curr_node = generateTypedNode(BOOL);
	curr_node->name = varName;
	i = rememberEnd;
	startOfSuffixString = i;
	return curr_node;
	}
	}
	return NULL;
	}

	void resetGlobalVar()
	{
	startOfSuffixString = 0;
	}

	ltlNode parseFormulaCreateAST( char inputFormula )
	{
	ltlNode *temp;

	temp = readLtlFormula( inputFormula );
	//if( temp == NULL )
	// printf("\nAST creation failed for formula %s", inputFormula );
	resetGlobalVar();
	return temp;
	}

	void traverseAbstractSyntaxTree( ltlNode *node )
	{
	switch(node->type){
	case( AND ):
	printf("& ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree( node->left );
	traverseAbstractSyntaxTree( node->right );
	return;
	case( OR ):
	printf("+ ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree( node->left );
	traverseAbstractSyntaxTree( node->right );
	return;
	case( NOT ):
	printf("~ ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree( node->left );
	assert( node->right == NULL );
	return;
	case( GLOBALLY ):
	printf("G ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree( node->left );
	assert( node->right == NULL );
	return;
	case( EVENTUALLY ):
	printf("F ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree( node->left );
	assert( node->right == NULL );
	return;
	case( NEXT ):
	printf("X ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree( node->left );
	assert( node->right == NULL );
	return;
	case( UNTIL ):
	printf("U ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree( node->left );
	traverseAbstractSyntaxTree( node->right );
	return;
	case( BOOL ):
	printf("%s ", node->name);
	assert( node->left == NULL );
	assert( node->right == NULL );
	return;
	default:
	printf("\nUnsupported token type: Exiting execution\n");
	exit(0);
	}
	}

	void traverseAbstractSyntaxTree_postFix( ltlNode *node )
	{
	switch(node->type){
	case( AND ):
	printf("( ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	printf("& ");
	traverseAbstractSyntaxTree_postFix( node->right );
	printf(") ");
	return;
	case( OR ):
	printf("( ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	printf("+ ");
	traverseAbstractSyntaxTree_postFix( node->right );
	printf(") ");
	return;
	case( NOT ):
	printf("~ ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	assert( node->right == NULL );
	return;
	case( GLOBALLY ):
	printf("G ");
	//printf("( ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	assert( node->right == NULL );
	//printf(") ");
	return;
	case( EVENTUALLY ):
	printf("F ");
	//printf("( ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	assert( node->right == NULL );
	//printf(") ");
	return;
	case( NEXT ):
	printf("X ");
	assert( node->left != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	assert( node->right == NULL );
	return;
	case( UNTIL ):
	printf("( ");
	assert( node->left != NULL );
	assert( node->right != NULL );
	traverseAbstractSyntaxTree_postFix( node->left );
	printf("U ");
	traverseAbstractSyntaxTree_postFix( node->right );
	printf(") ");
	return;
	case( BOOL ):
	printf("%s ", node->name);
	assert( node->left == NULL );
	assert( node->right == NULL );
	return;
	default:
	printf("\nUnsupported token type: Exiting execution\n");
	exit(0);
	}
	}

	void populateAigPointerUnitGF( Aig_Man_t pAigNew, ltlNode topASTNode, Vec_Ptr_t vSignal, Vec_Vec_t vAigGFMap )
	{
	ltlNode nextNode, nextToNextNode;
	int serialNumSignal;

	switch( topASTNode->type ){
	case AND:
	case OR:
	case IMPLY:
	populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
	populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
	return;
	case NOT:
	populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
	return;
	case GLOBALLY:
	nextNode = topASTNode->left;
	assert( nextNode->type = EVENTUALLY );
	nextToNextNode = nextNode->left;
	if( nextToNextNode->type == BOOL )
	{
	assert( nextToNextNode->pObj );
	serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
	if( serialNumSignal == -1 )
	{
	Vec_PtrPush( vSignal, nextToNextNode->pObj );
	serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
	}
	//Vec_PtrPush( vGLOBALLY, topASTNode );
	Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
	}
	else
	{
	assert( nextToNextNode->pObj == NULL );
	buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
	serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
	if( serialNumSignal == -1 )
	{
	Vec_PtrPush( vSignal, nextToNextNode->pObj );
	serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
	}
	//Vec_PtrPush( vGLOBALLY, topASTNode );
	Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
	}
	return;
	case BOOL:
	return;
	default:
	printf("\nINVALID situation: aborting...\n");
	exit(0);
	}
	}

	Aig_Obj_t buildLogicFromLTLNode_combinationalOnly( Aig_Man_t pAigNew, ltlNode *pLtlNode )
	{
	Aig_Obj_t leftAigObj, rightAigObj;

	if( pLtlNode->pObj != NULL )
	return pLtlNode->pObj;
	else
	{
	assert( pLtlNode->type != BOOL );
	switch( pLtlNode->type ){
	case AND:
	assert( pLtlNode->left ); assert( pLtlNode->right );
	leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
	rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
	assert( leftAigObj ); assert( rightAigObj );
	pLtlNode->pObj = Aig_And( pAigNew, leftAigObj, rightAigObj );
	return pLtlNode->pObj;
	case OR:
	assert( pLtlNode->left ); assert( pLtlNode->right );
	leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
	rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
	assert( leftAigObj ); assert( rightAigObj );
	pLtlNode->pObj = Aig_Or( pAigNew, leftAigObj, rightAigObj );
	return pLtlNode->pObj;
	case NOT:
	assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
	leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
	assert( leftAigObj );
	pLtlNode->pObj = Aig_Not( leftAigObj );
	return pLtlNode->pObj;
	case GLOBALLY:
	case EVENTUALLY:
	case NEXT:
	case UNTIL:
	printf("FORBIDDEN node: ABORTING!!\n");
	exit(0);
	default:
	printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
	exit(0);
	}
	}
	}

	Aig_Obj_t buildLogicFromLTLNode( Aig_Man_t pAig, ltlNode *pLtlNode )
	{
	Aig_Obj_t leftAigObj, rightAigObj;

	if( pLtlNode->pObj != NULL )
	return pLtlNode->pObj;
	else
	{
	assert( pLtlNode->type != BOOL );
	switch( pLtlNode->type ){
	case AND:
	assert( pLtlNode->left ); assert( pLtlNode->right );
	leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
	rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
	assert( leftAigObj ); assert( rightAigObj );
	pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
	return pLtlNode->pObj;
	case OR:
	assert( pLtlNode->left ); assert( pLtlNode->right );
	leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
	rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
	assert( leftAigObj ); assert( rightAigObj );
	pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
	return pLtlNode->pObj;
	case NOT:
	assert( pLtlNode->left ); assert( pLtlNode->right == NULL );
	leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
	assert( leftAigObj );
	pLtlNode->pObj = Aig_Not( leftAigObj );
	return pLtlNode->pObj;
	case GLOBALLY:
	case EVENTUALLY:
	case NEXT:
	case UNTIL:
	printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
	exit(0);
	default:
	printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
	exit(0);
	}
	}
	}

	int isNonTemporalSubformula( ltlNode *topNode )
	{
	switch( topNode->type ){
	case AND:
	case OR:
	case IMPLY:
	return isNonTemporalSubformula( topNode->left) && isNonTemporalSubformula( topNode->right ) ;
	case NOT:
	assert( topNode->right == NULL );
	return isNonTemporalSubformula( topNode->left );
	case BOOL:
	return 1;
	default:
	return 0;
	}
	}

	int isWellFormed( ltlNode *topNode )
	{
	ltlNode *nextNode;

	switch( topNode->type ){
	case AND:
	case OR:
	case IMPLY:
	return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
	case NOT:
	assert( topNode->right == NULL );
	return isWellFormed( topNode->left );
	case BOOL:
	return 1;
	case GLOBALLY:
	nextNode = topNode->left;
	assert( topNode->right == NULL );
	if( nextNode->type != EVENTUALLY )
	return 0;
	else
	{
	assert( nextNode->right == NULL );
	return isNonTemporalSubformula( nextNode->left );
	}
	default:
	return 0;
	}
	}

	int checkBooleanConstant( char *targetName )
	{
	if( strcmp( targetName, "true" ) == 0 )
	return 1;
	if( strcmp( targetName, "false" ) == 0 )
	return 0;
	return -1;
	}

	int checkSignalNameExistence( Abc_Ntk_t pNtk, ltlNode topASTNode )
	{
	char *targetName;
	Abc_Obj_t * pNode;
	int i;

	switch( topASTNode->type ){
	case BOOL:
	targetName = topASTNode->name;
	//printf("\nTrying to match name %s\n", targetName);
	if( checkBooleanConstant( targetName ) != -1 )
	return 1;
	Abc_NtkForEachPo( pNtk, pNode, i )
	{
	if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
	{
	//printf("\nVariable name \"%s\" MATCHED\n", targetName);
	return 1;
	}
	}
	printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
	return 0;
	case AND:
	case OR:
	case IMPLY:
	case UNTIL:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right != NULL );
	return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );

	case NOT:
	case NEXT:
	case GLOBALLY:
	case EVENTUALLY:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right == NULL );
	return checkSignalNameExistence( pNtk, topASTNode->left );
	default:
	printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
	exit(0);
	}
	}

	void populateBoolWithAigNodePtr( Abc_Ntk_t pNtk, Aig_Man_t pAigOld, Aig_Man_t pAigNew, ltlNode topASTNode )
	{
	char *targetName;
	Abc_Obj_t * pNode;
	int i;
	Aig_Obj_t pObj, pDriverImage;

	switch( topASTNode->type ){
	case BOOL:
	targetName = topASTNode->name;
	if( checkBooleanConstant( targetName ) == 1 )
	{
	topASTNode->pObj = Aig_ManConst1( pAigNew );
	return;
	}
	if( checkBooleanConstant( targetName ) == 0 )
	{
	topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
	return;
	}
	Abc_NtkForEachPo( pNtk, pNode, i )
	if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
	{
	pObj = Aig_ManCo( pAigOld, i );
	assert( Aig_ObjIsCo( pObj ));
	pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
	topASTNode->pObj = pDriverImage;
	return;
	}
	assert(0);
	case AND:
	case OR:
	case IMPLY:
	case UNTIL:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right != NULL );
	populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
	populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
	return;
	case NOT:
	case NEXT:
	case GLOBALLY:
	case EVENTUALLY:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right == NULL );
	populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
	return;
	default:
	printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
	exit(0);
	}
	}

	int checkAllBoolHaveAIGPointer( ltlNode *topASTNode )
	{

	switch( topASTNode->type ){
	case BOOL:
	if( topASTNode->pObj != NULL )
	return 1;
	else
	{
	printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
	return 0;
	}
	case AND:
	case OR:
	case IMPLY:
	case UNTIL:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right != NULL );
	return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );

	case NOT:
	case NEXT:
	case GLOBALLY:
	case EVENTUALLY:
	assert( topASTNode->left != NULL );
	assert( topASTNode->right == NULL );
	return checkAllBoolHaveAIGPointer( topASTNode->left );
	default:
	printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
	exit(0);
	}
	}

	void setAIGNodePtrOfGloballyNode( ltlNode astNode, Aig_Obj_t pObjLo )
	{
	astNode->pObj = pObjLo;
	}

	Aig_Obj_t retriveAIGPointerFromLTLNode( ltlNode astNode )
	{
	return astNode->pObj;
	}


	ABC_NAMESPACE_IMPL_END