/**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