summaryrefslogtreecommitdiffstats
path: root/src/aig/live/ltl_parser.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/live/ltl_parser.c')
-rw-r--r--src/aig/live/ltl_parser.c839
1 files changed, 0 insertions, 839 deletions
diff --git a/src/aig/live/ltl_parser.c b/src/aig/live/ltl_parser.c
deleted file mode 100644
index de113ba7..00000000
--- a/src/aig/live/ltl_parser.c
+++ /dev/null
@@ -1,839 +0,0 @@
-/**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");
- 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_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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 22:26:41 +0000