From ff1fd41a474849af69fafb66fe1cac2cce7bb61b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Feb 2015 21:57:42 -0800 Subject: Modifications to read SMTLIB file from stdin. --- src/base/wlc/wlc.h | 39 ++++++------ src/base/wlc/wlcBlast.c | 8 +++ src/base/wlc/wlcCom.c | 36 +++++++---- src/base/wlc/wlcNtk.c | 47 ++++++++++++++ src/base/wlc/wlcReadSmt.c | 154 ++++++++++++++++++++++++++++++++++------------ 5 files changed, 214 insertions(+), 70 deletions(-) (limited to 'src/base/wlc') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index f789c03c..4e6c2255 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -68,24 +68,25 @@ typedef enum { WLC_OBJ_LOGIC_NOT, // 23: logic NOT WLC_OBJ_LOGIC_AND, // 24: logic AND WLC_OBJ_LOGIC_OR, // 25: logic OR - WLC_OBJ_COMP_EQU, // 26: compare equal - WLC_OBJ_COMP_NOTEQU, // 27: compare not equal - WLC_OBJ_COMP_LESS, // 28: compare less - WLC_OBJ_COMP_MORE, // 29: compare more - WLC_OBJ_COMP_LESSEQU, // 30: compare less or equal - WLC_OBJ_COMP_MOREEQU, // 31: compare more or equal - WLC_OBJ_REDUCT_AND, // 32: reduction AND - WLC_OBJ_REDUCT_OR, // 33: reduction OR - WLC_OBJ_REDUCT_XOR, // 34: reduction XOR - WLC_OBJ_ARI_ADD, // 35: arithmetic addition - WLC_OBJ_ARI_SUB, // 36: arithmetic subtraction - WLC_OBJ_ARI_MULTI, // 37: arithmetic multiplier - WLC_OBJ_ARI_DIVIDE, // 38: arithmetic division - WLC_OBJ_ARI_MODULUS, // 39: arithmetic modulus - WLC_OBJ_ARI_POWER, // 40: arithmetic power - WLC_OBJ_ARI_MINUS, // 41: arithmetic minus - WLC_OBJ_TABLE, // 42: bit table - WLC_OBJ_NUMBER // 43: unused + WLC_OBJ_LOGIC_XOR, // 26: logic XOR + WLC_OBJ_COMP_EQU, // 27: compare equal + WLC_OBJ_COMP_NOTEQU, // 28: compare not equal + WLC_OBJ_COMP_LESS, // 29: compare less + WLC_OBJ_COMP_MORE, // 30: compare more + WLC_OBJ_COMP_LESSEQU, // 31: compare less or equal + WLC_OBJ_COMP_MOREEQU, // 32: compare more or equal + WLC_OBJ_REDUCT_AND, // 33: reduction AND + WLC_OBJ_REDUCT_OR, // 34: reduction OR + WLC_OBJ_REDUCT_XOR, // 35: reduction XOR + WLC_OBJ_ARI_ADD, // 36: arithmetic addition + WLC_OBJ_ARI_SUB, // 37: arithmetic subtraction + WLC_OBJ_ARI_MULTI, // 38: arithmetic multiplier + WLC_OBJ_ARI_DIVIDE, // 39: arithmetic division + WLC_OBJ_ARI_MODULUS, // 40: arithmetic modulus + WLC_OBJ_ARI_POWER, // 41: arithmetic power + WLC_OBJ_ARI_MINUS, // 42: arithmetic minus + WLC_OBJ_TABLE, // 43: bit table + WLC_OBJ_NUMBER // 44: unused } Wlc_ObjType_t; @@ -135,6 +136,7 @@ struct Wlc_Ntk_t_ // object names Abc_Nam_t * pManName; // object names Vec_Int_t vNameIds; // object name IDs + Vec_Int_t vValues; // value objects // object attributes int nTravIds; // counter of traversal IDs Vec_Int_t vTravIds; // trav IDs of the objects @@ -257,6 +259,7 @@ extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); +extern void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign ); /*=== wlcReadSmt.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 333b64de..4a935f6b 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -658,6 +658,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ) for ( k = 1; k < nRange; k++ ) Vec_IntPush( vRes, 0 ); } + else if ( pObj->Type == WLC_OBJ_LOGIC_XOR ) + { + int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); + int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR ); + Vec_IntFill( vRes, 1, Gia_ManHashXor(pNew, iLit0, iLit1) ); + for ( k = 1; k < nRange; k++ ) + Vec_IntPush( vRes, 0 ); + } else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU ) { int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 84afb394..6d437f55 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -115,21 +115,34 @@ static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSi } Vec_Str_t * Wlc_GenerateSmtStdin() { - char * pLine = "(check-sat)"; - int c, LineSize = strlen(pLine); - Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); + //char * pLine = "(check-sat)"; + //int c, LineSize = strlen(pLine); + Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); int c; while ( (c = fgetc(stdin)) != EOF ) - { Vec_StrPush( vInput, (char)c ); - if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) ) - break; - } Vec_StrPush( vInput, '\0' ); return vInput; } void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc ) { - printf( "Output produced by SMT solver will be here.\n" ); + if ( Abc_FrameReadProbStatus(pAbc) == -1 ) + printf( "undecided\n" ); + else if ( Abc_FrameReadProbStatus(pAbc) == 1 ) + printf( "unsat\n" ); + else if ( Abc_FrameReadProbStatus(pAbc) == 0 ) + { + Vec_Int_t * vAssign = Vec_IntAlloc( 100 ); + Abc_Cex_t * pCex = Abc_FrameReadCex( pAbc ); int i; + if ( pCex == NULL ) + { + printf( "CEX is not found\n" ); + return; + } + for ( i = 0; i < pCex->nPis; i++ ) + Vec_IntPush( vAssign, Abc_InfoHasBit(pCex->pData, i) ); + Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, vAssign ); + Vec_IntFree( vAssign ); + } } /**Function******************************************************************** @@ -417,9 +430,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // transform - pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); - pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); - Wlc_AbcUpdateNtk( pAbc, pNtk ); + //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); + //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); + //Wlc_AbcUpdateNtk( pAbc, pNtk ); + Wlc_GenerateSmtStdout( pAbc ); return 0; usage: Abc_Print( -2, "usage: %%test [-vh]\n" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 48171c35..1576ef45 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -209,6 +209,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p ) Vec_IntFreeP( &p->vInits ); ABC_FREE( p->vTravIds.pArray ); ABC_FREE( p->vNameIds.pArray ); + ABC_FREE( p->vValues.pArray ); ABC_FREE( p->vCopies.pArray ); ABC_FREE( p->pInits ); ABC_FREE( p->pObjs ); @@ -496,6 +497,52 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) pNew->vTables = p->vTables; p->vTables = NULL; } +/**Function************************************************************* + + Synopsis [Report results.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign ) +{ + //sat +//((s0 #x12000000070000000000c0000085006b)) +//((s1 #x0e008f00ff0000000000ff0000ed0040)) +//((s2 #x96008f00ff0000000000ff0000ed0040)) + + int i, Name, Start, nBits, k; + Vec_Str_t * vNum = Vec_StrAlloc( 100 ); +// Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) +// printf( "Variable %s : %d %d\n", Abc_NamStr(p->pManName, Name), Start, nBits ); + printf( "sat\n" ); + Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) + { + Vec_StrClear( vNum ); + for ( k = Start; k < Start + nBits; ) + { + int j, Digit = 0; + for ( j = 0; j < 4 && k < Start + nBits; j++, k++ ) + Digit += (1 << j) * Vec_IntEntry(vAssign, k); + assert( Digit >= 0 && Digit < 16 ); + if ( Digit >= 0 && Digit <= 9 ) + Vec_StrPush( vNum, (char)('0' + Digit) ); + else + Vec_StrPush( vNum, (char)('a' + Digit - 10) ); + } + Vec_StrPush( vNum, 'x' ); + Vec_StrPush( vNum, '#' ); + Vec_StrReverseOrder( vNum ); + Vec_StrPush( vNum, '\0' ); + printf( "((%s %s))\n", Abc_NamStr(p->pManName, Name), Vec_StrArray(vNum) ); + } + Vec_StrFree( vNum ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 52d5e887..3a249ec6 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -32,7 +32,8 @@ typedef enum { PRS_SMT_INPUT, PRS_SMT_CONST, PRS_SMT_LET, - PRS_SMT_ASSERT + PRS_SMT_ASSERT, + PRS_SMT_VALUE } Prs_ManType_t; // parser @@ -46,7 +47,8 @@ struct Prs_Smt_t_ char * pCur; // current position Abc_Nam_t * pStrs; // string manager // network structure - Vec_Int_t vData; + Vec_Int_t vData; + Vec_Int_t vValues; // error handling char ErrorStr[1000]; }; @@ -117,6 +119,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p ) if ( p->pStrs ) Abc_NamDeref( p->pStrs ); Vec_IntErase( &p->vData ); + Vec_IntErase( &p->vValues ); ABC_FREE( p ); } @@ -234,8 +237,24 @@ static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type ) p->pCur = pLimit; return 1; } +static inline int Prs_SmtParseValue( Prs_Smt_t * p, char * pLimit, int Type ) +{ + char * pToken; + assert( *pLimit == ')' ); + *pLimit = 0; + pToken = strtok( p->pCur, " ()" ); + assert( pToken != NULL ); + Vec_IntPush( &p->vValues, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) ); + pToken = strtok( NULL, " ()" ); + assert( pToken == NULL ); + assert( *pLimit == 0 ); + *pLimit = ')'; + p->pCur = pLimit; + return 1; +} int Prs_SmtReadLines( Prs_Smt_t * p ) { + int fAssert = 0; Prs_SmtSkipSpaces( p ); while ( *p->pCur == '(' ) { @@ -263,25 +282,35 @@ int Prs_SmtReadLines( Prs_Smt_t * p ) assert( *p->pCur == ')' ); p->pCur++; } - else if ( Prs_SmtIsWord(p, "check-sat") ) + else if ( Prs_SmtIsWord(p, "get-value") ) { - Vec_IntPush( &p->vData, 0 ); - return 1; + if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) ) + return 0; + assert( *p->pCur == ')' ); + p->pCur++; } else if ( Prs_SmtIsWord(p, "assert") ) - {} - else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") ) + fAssert = 1; + else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") || Prs_SmtIsWord(p, "check-sat") ) p->pCur = Prs_SmtFindNextPar(p) + 1; - else - break; +// else //return Prs_SmtErrorSet(p, "Unsupported directive.", 0); Prs_SmtSkipSpaces( p ); + if ( *p->pCur != '(' && fAssert == 1 ) + { + fAssert = 0; + // finish parsing assert + if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) ) + return 0; + assert( *p->pCur == ')' ); + Vec_IntPush( &p->vData, 0 ); + // skip closing + while ( *p->pCur == ')' ) + p->pCur++; + Prs_SmtSkipSpaces( p ); + } } - // finish parsing assert - if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) ) - return 0; - assert( *p->pCur == ')' ); - Vec_IntPush( &p->vData, 0 ); + assert( fAssert == 0 ); return 1; } @@ -320,6 +349,8 @@ void Prs_SmtPrintParser( Prs_Smt_t * p ) } printf( " %s", Abc_NamStr(p->pStrs, Entry) ); } + Vec_IntForEachEntry( &p->vValues, Entry, i ) + printf( "get-value %s\n", Abc_NamStr(p->pStrs, Entry) ); } @@ -404,9 +435,9 @@ static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec return 1; } } -static inline int Prs_SmtStrToType( char * pName ) +static inline int Prs_SmtStrToType( char * pName, int * pfSigned ) { - int Type = 0; + int Type = 0; *pfSigned = 0; if ( !strcmp(pName, "ite") ) Type = WLC_OBJ_MUX; // 08: multiplexer else if ( !strcmp(pName, "bvlshr") ) @@ -436,56 +467,77 @@ static inline int Prs_SmtStrToType( char * pName ) else if ( !strcmp(pName, "zero_extend") ) Type = WLC_OBJ_BIT_ZEROPAD; // 21: zero padding else if ( !strcmp(pName, "sign_extend") ) - Type = WLC_OBJ_BIT_SIGNEXT; // 22: sign extension + Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension else if ( !strcmp(pName, "not") ) Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT else if ( !strcmp(pName, "and") ) Type = WLC_OBJ_LOGIC_AND; // 24: logic AND else if ( !strcmp(pName, "or") ) Type = WLC_OBJ_LOGIC_OR; // 25: logic OR + else if ( !strcmp(pName, "xor") ) + Type = WLC_OBJ_LOGIC_XOR; // 26: logic OR else if ( !strcmp(pName, "bvcomp") ) - Type = WLC_OBJ_COMP_EQU; // 26: compare equal + Type = WLC_OBJ_COMP_EQU; // 27: compare equal // else if ( !strcmp(pName, "") ) -// Type = WLC_OBJ_COMP_NOTEQU; // 27: compare not equal +// Type = WLC_OBJ_COMP_NOTEQU; // 28: compare not equal else if ( !strcmp(pName, "bvult") ) - Type = WLC_OBJ_COMP_LESS; // 28: compare less + Type = WLC_OBJ_COMP_LESS; // 29: compare less else if ( !strcmp(pName, "bvugt") ) - Type = WLC_OBJ_COMP_MORE; // 29: compare more + Type = WLC_OBJ_COMP_MORE; // 30: compare more else if ( !strcmp(pName, "bvule") ) - Type = WLC_OBJ_COMP_LESSEQU; // 30: compare less or equal + Type = WLC_OBJ_COMP_LESSEQU; // 31: compare less or equal else if ( !strcmp(pName, "bvuge") ) - Type = WLC_OBJ_COMP_MOREEQU; // 31: compare more or equal + Type = WLC_OBJ_COMP_MOREEQU; // 32: compare more or equal + else if ( !strcmp(pName, "bvslt") ) + Type = WLC_OBJ_COMP_LESS, *pfSigned = 1; // 29: compare less + else if ( !strcmp(pName, "bvsgt") ) + Type = WLC_OBJ_COMP_MORE, *pfSigned = 1; // 30: compare more + else if ( !strcmp(pName, "bvsle") ) + Type = WLC_OBJ_COMP_LESSEQU, *pfSigned = 1; // 31: compare less or equal + else if ( !strcmp(pName, "bvsge") ) + Type = WLC_OBJ_COMP_MOREEQU, *pfSigned = 1; // 32: compare more or equal else if ( !strcmp(pName, "bvredand") ) - Type = WLC_OBJ_REDUCT_AND; // 32: reduction AND + Type = WLC_OBJ_REDUCT_AND; // 33: reduction AND else if ( !strcmp(pName, "bvredor") ) - Type = WLC_OBJ_REDUCT_OR; // 33: reduction OR + Type = WLC_OBJ_REDUCT_OR; // 34: reduction OR else if ( !strcmp(pName, "bvredxor") ) - Type = WLC_OBJ_REDUCT_XOR; // 34: reduction XOR + Type = WLC_OBJ_REDUCT_XOR; // 35: reduction XOR else if ( !strcmp(pName, "bvadd") ) - Type = WLC_OBJ_ARI_ADD; // 35: arithmetic addition + Type = WLC_OBJ_ARI_ADD; // 36: arithmetic addition else if ( !strcmp(pName, "bvsub") ) - Type = WLC_OBJ_ARI_SUB; // 36: arithmetic subtraction + Type = WLC_OBJ_ARI_SUB; // 37: arithmetic subtraction else if ( !strcmp(pName, "bvmul") ) - Type = WLC_OBJ_ARI_MULTI; // 37: arithmetic multiplier - else if ( !strcmp(pName, "bvdiv") ) - Type = WLC_OBJ_ARI_DIVIDE; // 38: arithmetic division + Type = WLC_OBJ_ARI_MULTI; // 38: arithmetic multiplier + else if ( !strcmp(pName, "bvudiv") ) + Type = WLC_OBJ_ARI_DIVIDE; // 39: arithmetic division else if ( !strcmp(pName, "bvurem") ) - Type = WLC_OBJ_ARI_MODULUS; // 39: arithmetic modulus + Type = WLC_OBJ_ARI_MODULUS; // 40: arithmetic modulus + else if ( !strcmp(pName, "bvsdiv") ) + Type = WLC_OBJ_ARI_DIVIDE, *pfSigned = 1; // 39: arithmetic division + else if ( !strcmp(pName, "bvsrem") ) + Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus + else if ( !strcmp(pName, "bvsmod") ) + Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus // else if ( !strcmp(pName, "") ) -// Type = WLC_OBJ_ARI_POWER; // 40: arithmetic power +// Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power else if ( !strcmp(pName, "bvneg") ) - Type = WLC_OBJ_ARI_MINUS; // 41: arithmetic minus + Type = WLC_OBJ_ARI_MINUS; // 42: arithmetic minus // else if ( !strcmp(pName, "") ) -// Type = WLC_OBJ_TABLE; // 42: bit table - else assert( 0 ); +// Type = WLC_OBJ_TABLE; // 43: bit table + else + { + printf( "The following operations is currently not supported (%s)\n", pName ); + fflush( stdout ); + assert( 0 ); + } return Type; } -static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange ) +static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange, int * pfSigned ) { int Type, NameId; char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) ); // read type - Type = Prs_SmtStrToType( pName ); + Type = Prs_SmtStrToType( pName, pfSigned ); if ( Type == 0 ) return 0; *pRange = 0; @@ -499,7 +551,7 @@ static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * } else if ( Type == WLC_OBJ_LOGIC_NOT ) { - pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); + pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); if ( !strcmp(pName, "bvcomp") ) { *pRange = 1; @@ -558,7 +610,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) Wlc_Ntk_t * pNtk; char * pName, * pBits, * pConst; Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); - int i, iObj, Type, Entry, NameId, fFound, Range; + int i, k, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0; // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); @@ -567,12 +619,23 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) assert( Vec_IntEntry(&p->vData, i) == 0 ); if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT ) { + int NameOld = Vec_IntEntry(&p->vData, i+1); pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 ); NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( !fFound ); assert( iObj == NameId ); + // save values + Vec_IntForEachEntry( &p->vValues, Entry, k ) + if ( Entry == NameOld ) + { + Vec_IntPush( &pNtk->vValues, NameId ); + Vec_IntPush( &pNtk->vValues, nBits ); + Vec_IntPush( &pNtk->vValues, atoi(pBits) ); + break; + } + nBits += atoi(pBits); } while ( Vec_IntEntry(&p->vData, ++i) ); } @@ -595,13 +658,21 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) else if ( Entry == PRS_SMT_LET ) { pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); - Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range ); + Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range, &fSigned ); if ( Type == WLC_OBJ_NONE ) return NULL; assert( Range > 0 ); // create new node iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); + if ( fSigned ) + { + Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; + if ( Vec_IntSize(vFanins) > 0 ) + Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; + if ( Vec_IntSize(vFanins) > 1 ) + Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned; + } // add node's name NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( !fFound ); @@ -648,6 +719,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); Vec_IntAppend( &pNtk->vNameIds, vFanins ); Vec_IntFree( vFanins ); + //Wlc_NtkReport( pNtk, NULL ); return pNtk; } Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) -- cgit v1.2.3