56 new_node->
type = new_type;
57 new_node->
pObj = NULL;
58 new_node->
name = NULL;
59 new_node->
left = NULL;
60 new_node->
right = NULL;
70 return ( c ==
' ' || c ==
'\t' || c ==
'\n' || c ==
':' || c ==
'\0' );
75 char *pLtlFormula, *tempFormula;
78 if( pAbc->vLTLProperties_global != NULL )
82 pAbc->vLTLProperties_global = NULL;
87 tempFormula = (
char *)
malloc(
sizeof(
char)*(
strlen(pLtlFormula)+1) );
88 sprintf( tempFormula,
"%s", pLtlFormula );
89 Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
93 char *
getVarName(
char *suffixFormula,
int startLoc,
int *endLocation )
95 int i = startLoc, length;
104 length = i - startLoc;
105 name = (
char *)
malloc(
sizeof(
char) * (length + 1));
106 for( i=0; i<length; i++ )
107 name[i] = suffixFormula[i+startLoc];
119 if( index >= (
int)
strlen( formula ) )
121 printf(
"\nInvalid LTL formula: unexpected end of string..." );
129 if( !(
isUnexpectedEOS( formula, index ) || formula[ index ] ==
'G' || formula[ index ] ==
'F' || formula[ index ] ==
'U' || formula[ index ] ==
'X') )
131 printf(
"\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
141 int formulaLength, rememberEnd;
143 ltlNode *curr_node, *temp_node_left, *temp_node_right;
146 formulaLength =
strlen( formula );
153 while( i < formulaLength )
174 prevChar = formula[i-1];
175 if( prevChar ==
':' )
180 if( temp_node_left == NULL )
185 curr_node->
left = temp_node_left;
191 varName =
getVarName( formula, i, &rememberEnd );
194 printf(
"\nInvalid LTL formula: expecting valid variable name token...aborting" );
198 curr_node->
name = varName;
204 prevChar = formula[i-1];
205 if( prevChar ==
':' )
210 if( temp_node_left == NULL )
215 curr_node->
left = temp_node_left;
221 varName =
getVarName( formula, i, &rememberEnd );
224 printf(
"\nInvalid LTL formula: expecting valid variable name token...aborting" );
228 curr_node->
name = varName;
234 prevChar = formula[i-1];
235 if( prevChar ==
':' )
240 if( temp_node_left == NULL )
245 curr_node->
left = temp_node_left;
251 varName =
getVarName( formula, i, &rememberEnd );
254 printf(
"\nInvalid LTL formula: expecting valid variable name token...aborting" );
258 curr_node->
name = varName;
264 prevChar = formula[i-1];
265 if( prevChar ==
':' )
270 if( temp_node_left == NULL )
273 if( temp_node_right == NULL )
280 curr_node->
left = temp_node_left;
281 curr_node->
right = temp_node_right;
286 varName =
getVarName( formula, i, &rememberEnd );
289 printf(
"\nInvalid LTL formula: expecting valid variable name token...aborting" );
293 curr_node->
name = varName;
302 if( temp_node_left == NULL )
305 if( temp_node_right == NULL )
312 curr_node->
left = temp_node_left;
313 curr_node->
right = temp_node_right;
319 if( temp_node_left == NULL )
322 if( temp_node_right == NULL )
329 curr_node->
left = temp_node_left;
330 curr_node->
right = temp_node_right;
336 if( temp_node_left == NULL )
341 curr_node->
left = temp_node_left;
345 varName =
getVarName( formula, i, &rememberEnd );
348 printf(
"\nInvalid LTL formula: expecting valid variable name token...aborting" );
352 curr_node->
name = varName;
426 printf(
"%s ", node->
name);
431 printf(
"\nUnsupported token type: Exiting execution\n");
495 printf(
"%s ", node->
name);
500 printf(
"\nUnsupported token type: Exiting execution\n");
507 ltlNode *nextNode, *nextToNextNode;
510 switch( topASTNode->
type ){
521 nextNode = topASTNode->
left;
523 nextToNextNode = nextNode->
left;
528 if( serialNumSignal == -1 )
534 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
541 if( serialNumSignal == -1 )
547 Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
553 printf(
"\nINVALID situation: aborting...\n");
562 if( pLtlNode->
pObj != NULL )
563 return pLtlNode->
pObj;
567 switch( pLtlNode->
type ){
573 pLtlNode->
pObj =
Aig_And( pAigNew, leftAigObj, rightAigObj );
574 return pLtlNode->
pObj;
580 pLtlNode->
pObj =
Aig_Or( pAigNew, leftAigObj, rightAigObj );
581 return pLtlNode->
pObj;
587 return pLtlNode->
pObj;
592 printf(
"FORBIDDEN node: ABORTING!!\n");
595 printf(
"\nSerious ERROR: attempting to create AIG node from a temporal node\n");
605 if( pLtlNode->
pObj != NULL )
606 return pLtlNode->
pObj;
610 switch( pLtlNode->
type ){
616 pLtlNode->
pObj =
Aig_And( pAig, leftAigObj, rightAigObj );
617 return pLtlNode->
pObj;
623 pLtlNode->
pObj =
Aig_Or( pAig, leftAigObj, rightAigObj );
624 return pLtlNode->
pObj;
630 return pLtlNode->
pObj;
635 printf(
"\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
638 printf(
"\nSerious ERROR: attempting to create AIG node from a temporal node\n");
646 switch( topNode->
type ){
665 switch( topNode->
type ){
676 nextNode = topNode->
left;
692 if(
strcmp( targetName,
"true" ) == 0 )
694 if(
strcmp( targetName,
"false" ) == 0 )
705 switch( topASTNode->
type ){
707 targetName = topASTNode->
name;
719 printf(
"\nVariable name \"%s\" not found in the PO name list\n", targetName);
737 printf(
"\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
749 switch( topASTNode->
type ){
751 targetName = topASTNode->
name;
768 topASTNode->
pObj = pDriverImage;
790 printf(
"\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
798 switch( topASTNode->
type ){
800 if( topASTNode->
pObj != NULL )
804 printf(
"\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->
name);
823 printf(
"\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
830 astNode->
pObj = pObjLo;
835 return astNode->
pObj;
Aig_Obj_t * buildLogicFromLTLNode_combinationalOnly(Aig_Man_t *pAig, ltlNode *pLtlNode)
ltlNode * generateTypedNode(tokenType new_type)
Vec_Ptr_t * vLtlProperties
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
int checkAllBoolHaveAIGPointer(ltlNode *topASTNode)
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
int isNonTemporalSubformula(ltlNode *topNode)
int isTemporalOperator(char *formula, int index)
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
ltlNode * readLtlFormula(char *formula)
static avl_node * new_node()
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
static int Vec_PtrSize(Vec_Ptr_t *p)
void setAIGNodePtrOfGloballyNode(ltlNode *astNode, Aig_Obj_t *pObjLo)
void traverseAbstractSyntaxTree(ltlNode *node)
static int Vec_PtrFind(Vec_Ptr_t *p, void *Entry)
int isUnexpectedEOS(char *formula, int index)
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
int isWellFormed(ltlNode *topNode)
int checkBooleanConstant(char *targetName)
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
void populateBoolWithAigNodePtr(Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode)
static int isNotVarNameSymbol(char c)
#define ABC_NAMESPACE_IMPL_END
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
#define ABC_NAMESPACE_IMPL_START
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
void populateAigPointerUnitGF(Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap)
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
int checkSignalNameExistence(Abc_Ntk_t *pNtk, ltlNode *topASTNode)
enum ltlGrammerToken ltlGrammerTokenType
Aig_Obj_t * buildLogicFromLTLNode(Aig_Man_t *pAig, ltlNode *pLtlNode)
#define Abc_NtkForEachPo(pNtk, pPo, i)
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
ltlNode * parseFormulaCreateAST(char *inputFormula)
Aig_Obj_t * retriveAIGPointerFromLTLNode(ltlNode *astNode)
char * getVarName(char *suffixFormula, int startLoc, int *endLocation)
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
void Abc_FrameCopyLTLDataBase(Abc_Frame_t *pAbc, Abc_Ntk_t *pNtk)
static void Vec_PtrFree(Vec_Ptr_t *p)
void traverseAbstractSyntaxTree_postFix(ltlNode *node)