summaryrefslogtreecommitdiffstats
path: root/src/proof/live/ltl_parser.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/live/ltl_parser.c')
-rw-r--r--src/proof/live/ltl_parser.c839
1 files changed, 839 insertions, 0 deletions
diff --git a/src/proof/live/ltl_parser.c b/src/proof/live/ltl_parser.c
new file mode 100644
index 00000000..5572611f
--- /dev/null
+++ b/src/proof/live/ltl_parser.c
@@ -0,0 +1,839 @@
+/**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 "src/aig/aig/aig.h"
+#include "src/base/abc/abc.h"
+#include "src/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_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-06-30 19:01:41 +0000