diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
commit | 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch) | |
tree | 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/aig/live/ltl_parser.c | |
parent | f0e77f6797c0504b0da25a56152b707d3357f386 (diff) | |
download | abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip |
initial commit of public abc
Diffstat (limited to 'src/aig/live/ltl_parser.c')
-rw-r--r-- | src/aig/live/ltl_parser.c | 838 |
1 files changed, 838 insertions, 0 deletions
diff --git a/src/aig/live/ltl_parser.c b/src/aig/live/ltl_parser.c new file mode 100644 index 00000000..66d7f72d --- /dev/null +++ b/src/aig/live/ltl_parser.c @@ -0,0 +1,838 @@ +/**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.h> +#include <abc.h> +#include <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"); + 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_ManPo( pAigOld, i ); + assert( Aig_ObjIsPo( 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 |