| /**CFile**************************************************************** |
| |
| FileName [wlcParse.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Verilog parser.] |
| |
| Synopsis [Parses several flavors of word-level Verilog.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - August 22, 2014.] |
| |
| Revision [$Id: wlcParse.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "wlc.h" |
| #include "misc/vec/vecWec.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // parser |
| typedef struct Smt_Prs_t_ Smt_Prs_t; |
| struct Smt_Prs_t_ |
| { |
| // input data |
| char * pName; // file name |
| char * pBuffer; // file contents |
| char * pLimit; // end of file |
| char * pCur; // current position |
| Abc_Nam_t * pStrs; // string manager |
| // network structure |
| Vec_Int_t vStack; // current node on each level |
| //Vec_Wec_t vDepth; // objects on each level |
| Vec_Wec_t vObjs; // objects |
| int NameCount; |
| int nDigits; |
| Vec_Int_t vTempFans; |
| // error handling |
| char ErrorStr[1000]; |
| }; |
| |
| //#define SMT_GLO_SUFFIX "_glb" |
| #define SMT_GLO_SUFFIX "" |
| |
| // parser name types |
| typedef enum { |
| SMT_PRS_NONE = 0, |
| SMT_PRS_SET_OPTION, |
| SMT_PRS_SET_LOGIC, |
| SMT_PRS_SET_INFO, |
| SMT_PRS_DEFINE_FUN, |
| SMT_PRS_DECLARE_FUN, |
| SMT_PRS_ASSERT, |
| SMT_PRS_LET, |
| SMT_PRS_CHECK_SAT, |
| SMT_PRS_GET_VALUE, |
| SMT_PRS_EXIT, |
| SMT_PRS_END |
| } Smt_LineType_t; |
| |
| typedef struct Smt_Pair_t_ Smt_Pair_t; |
| struct Smt_Pair_t_ |
| { |
| Smt_LineType_t Type; |
| char * pName; |
| }; |
| static Smt_Pair_t s_Types[SMT_PRS_END] = |
| { |
| { SMT_PRS_NONE, NULL }, |
| { SMT_PRS_SET_OPTION, "set-option" }, |
| { SMT_PRS_SET_LOGIC, "set-logic" }, |
| { SMT_PRS_SET_INFO, "set-info" }, |
| { SMT_PRS_DEFINE_FUN, "define-fun" }, |
| { SMT_PRS_DECLARE_FUN, "declare-fun" }, |
| { SMT_PRS_ASSERT, "assert" }, |
| { SMT_PRS_LET, "let" }, |
| { SMT_PRS_CHECK_SAT, "check-sat" }, |
| { SMT_PRS_GET_VALUE, "get-value" }, |
| { SMT_PRS_EXIT, "exit" } |
| }; |
| static inline char * Smt_GetTypeName( Smt_LineType_t Type ) |
| { |
| int i; |
| for ( i = 1; i < SMT_PRS_END; i++ ) |
| if ( s_Types[i].Type == Type ) |
| return s_Types[i].pName; |
| return NULL; |
| } |
| static inline void Smt_AddTypes( Abc_Nam_t * p ) |
| { |
| int Type; |
| for ( Type = 1; Type < SMT_PRS_END; Type++ ) |
| Abc_NamStrFindOrAdd( p, Smt_GetTypeName((Smt_LineType_t)Type), NULL ); |
| assert( Abc_NamObjNumMax(p) == SMT_PRS_END ); |
| } |
| |
| static inline int Smt_EntryIsName( int Fan ) { return Abc_LitIsCompl(Fan); } |
| static inline int Smt_EntryIsType( int Fan, Smt_LineType_t Type ) { assert(Smt_EntryIsName(Fan)); return Abc_Lit2Var(Fan) == Type; } |
| static inline char * Smt_EntryName( Smt_Prs_t * p, int Fan ) { assert(Smt_EntryIsName(Fan)); return Abc_NamStr( p->pStrs, Abc_Lit2Var(Fan) ); } |
| static inline Vec_Int_t * Smt_EntryNode( Smt_Prs_t * p, int Fan ) { assert(!Smt_EntryIsName(Fan)); return Vec_WecEntry( &p->vObjs, Abc_Lit2Var(Fan) ); } |
| |
| static inline int Smt_VecEntryIsType( Vec_Int_t * vFans, int i, Smt_LineType_t Type ) { return i < Vec_IntSize(vFans) && Smt_EntryIsName(Vec_IntEntry(vFans, i)) && Smt_EntryIsType(Vec_IntEntry(vFans, i), Type); } |
| static inline char * Smt_VecEntryName( Smt_Prs_t * p, Vec_Int_t * vFans, int i ) { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? Smt_EntryName(p, Vec_IntEntry(vFans, i)) : NULL; } |
| static inline Vec_Int_t * Smt_VecEntryNode( Smt_Prs_t * p, Vec_Int_t * vFans, int i ) { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? NULL : Smt_EntryNode(p, Vec_IntEntry(vFans, i)); } |
| |
| #define Smt_ManForEachDir( p, Type, vVec, i ) \ |
| for ( i = 0; (i < Vec_WecSize(&p->vObjs)) && (((vVec) = Vec_WecEntry(&p->vObjs, i)), 1); i++ ) \ |
| if ( !Smt_VecEntryIsType(vVec, 0, Type) ) {} else |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Smt_StrToType( char * pName, int * pfSigned ) |
| { |
| int Type = 0; *pfSigned = 0; |
| if ( !strcmp(pName, "ite") ) |
| Type = WLC_OBJ_MUX; // 08: multiplexer |
| else if ( !strcmp(pName, "bvlshr") ) |
| Type = WLC_OBJ_SHIFT_R; // 09: shift right |
| else if ( !strcmp(pName, "bvashr") ) |
| Type = WLC_OBJ_SHIFT_RA , *pfSigned = 1; // 10: shift right (arithmetic) |
| else if ( !strcmp(pName, "bvshl") ) |
| Type = WLC_OBJ_SHIFT_L; // 11: shift left |
| // else if ( !strcmp(pName, "") ) |
| // Type = WLC_OBJ_SHIFT_LA; // 12: shift left (arithmetic) |
| else if ( !strcmp(pName, "rotate_right") ) |
| Type = WLC_OBJ_ROTATE_R; // 13: rotate right |
| else if ( !strcmp(pName, "rotate_left") ) |
| Type = WLC_OBJ_ROTATE_L; // 14: rotate left |
| else if ( !strcmp(pName, "bvnot") ) |
| Type = WLC_OBJ_BIT_NOT; // 15: bitwise NOT |
| else if ( !strcmp(pName, "bvand") ) |
| Type = WLC_OBJ_BIT_AND; // 16: bitwise AND |
| else if ( !strcmp(pName, "bvor") ) |
| Type = WLC_OBJ_BIT_OR; // 17: bitwise OR |
| else if ( !strcmp(pName, "bvxor") ) |
| Type = WLC_OBJ_BIT_XOR; // 18: bitwise XOR |
| else if ( !strcmp(pName, "bvnand") ) |
| Type = WLC_OBJ_BIT_NAND; // 16: bitwise NAND |
| else if ( !strcmp(pName, "bvnor") ) |
| Type = WLC_OBJ_BIT_NOR; // 17: bitwise NOR |
| else if ( !strcmp(pName, "bvxnor") ) |
| Type = WLC_OBJ_BIT_NXOR; // 18: bitwise NXOR |
| else if ( !strcmp(pName, "extract") ) |
| Type = WLC_OBJ_BIT_SELECT; // 19: bit selection |
| else if ( !strcmp(pName, "concat") ) |
| Type = WLC_OBJ_BIT_CONCAT; // 20: bit concatenation |
| 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 |
| else if ( !strcmp(pName, "not") ) |
| Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT |
| else if ( !strcmp(pName, "=>") ) |
| Type = WLC_OBJ_LOGIC_IMPL; // 24: logic AND |
| 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") || !strcmp(pName, "=") ) |
| Type = WLC_OBJ_COMP_EQU; // 27: compare equal |
| else if ( !strcmp(pName, "distinct") ) |
| Type = WLC_OBJ_COMP_NOTEQU; // 28: compare not equal |
| else if ( !strcmp(pName, "bvult") ) |
| Type = WLC_OBJ_COMP_LESS; // 29: compare less |
| else if ( !strcmp(pName, "bvugt") ) |
| Type = WLC_OBJ_COMP_MORE; // 30: compare more |
| else if ( !strcmp(pName, "bvule") ) |
| Type = WLC_OBJ_COMP_LESSEQU; // 31: compare less or equal |
| else if ( !strcmp(pName, "bvuge") ) |
| 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; // 33: reduction AND |
| else if ( !strcmp(pName, "bvredor") ) |
| Type = WLC_OBJ_REDUCT_OR; // 34: reduction OR |
| else if ( !strcmp(pName, "bvredxor") ) |
| Type = WLC_OBJ_REDUCT_XOR; // 35: reduction XOR |
| else if ( !strcmp(pName, "bvadd") ) |
| Type = WLC_OBJ_ARI_ADD; // 36: arithmetic addition |
| else if ( !strcmp(pName, "bvsub") ) |
| Type = WLC_OBJ_ARI_SUB; // 37: arithmetic subtraction |
| else if ( !strcmp(pName, "bvmul") ) |
| 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_REM; // 40: arithmetic remainder |
| else if ( !strcmp(pName, "bvsdiv") ) |
| Type = WLC_OBJ_ARI_DIVIDE, *pfSigned = 1; // 39: arithmetic division |
| else if ( !strcmp(pName, "bvsrem") ) |
| Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder |
| else if ( !strcmp(pName, "bvsmod") ) |
| Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus |
| else if ( !strcmp(pName, "=") ) |
| Type = WLC_OBJ_COMP_EQU; // 40: arithmetic modulus |
| // else if ( !strcmp(pName, "") ) |
| // Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power |
| else if ( !strcmp(pName, "bvneg") ) |
| Type = WLC_OBJ_ARI_MINUS; // 42: arithmetic minus |
| // else if ( !strcmp(pName, "") ) |
| // Type = WLC_OBJ_TABLE; // 43: bit table |
| else |
| { |
| printf( "The following operations is currently not supported (%s)\n", pName ); |
| fflush( stdout ); |
| } |
| return Type; |
| } |
| static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int * Value1, int * Value2 ) |
| { |
| if ( Smt_EntryIsName(iSig) ) |
| return Smt_StrToType( Smt_EntryName(p, iSig), pfSigned ); |
| else |
| { |
| Vec_Int_t * vFans = Smt_EntryNode( p, iSig ); |
| char * pStr = Smt_VecEntryName( p, vFans, 0 ); int Type; |
| assert( Vec_IntSize(vFans) >= 3 ); |
| assert( !strcmp(pStr, "_") ); // special op |
| *Value1 = *Value2 = -1; |
| assert( pStr[0] != 'b' || pStr[1] != 'v' ); |
| // read type |
| Type = Smt_StrToType( Smt_VecEntryName(p, vFans, 1), pfSigned ); |
| if ( Type == 0 ) |
| return 0; |
| *Value1 = atoi( Smt_VecEntryName(p, vFans, 2) ); |
| if ( Vec_IntSize(vFans) > 3 ) |
| *Value2 = atoi( Smt_VecEntryName(p, vFans, 3) ); |
| return Type; |
| } |
| } |
| |
| static inline int Smt_StrType( char * str ) { return Smt_StrToType(str, NULL); } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) |
| { |
| char Buffer[100]; |
| int NameId, fFound; |
| int iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); |
| assert( Type > 0 ); |
| assert( Range >= 0 ); |
| assert( fSigned >= 0 ); |
| |
| // add node's name |
| if ( pName == NULL ) |
| { |
| sprintf( Buffer, "_n%d_", iObj ); |
| pName = Buffer; |
| } |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); |
| assert( !fFound ); |
| assert( iObj == NameId ); |
| |
| 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; |
| } |
| |
| return iObj; |
| } |
| static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName ) |
| { |
| char Buffer[100]; |
| char * pNameFanin; |
| int NameId, fFound, old_size, new_size; |
| int iObj, iFanin0, iFanin1; |
| Vec_Int_t * v2Fanins = Vec_IntStartFull(2); |
| |
| assert( Type > 0 ); |
| assert( Range >= 0 ); |
| assert( fSigned >= 0 ); |
| |
| //if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX ) |
| // explicitely secify allowed multi operators |
| if (Vec_IntSize(vFanins)<=2 || |
| !( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND |
| Type == WLC_OBJ_BIT_OR || // 17: bitwise OR |
| Type == WLC_OBJ_BIT_XOR || // 18: bitwise XOR |
| Type == WLC_OBJ_BIT_NAND || // 19: bitwise AND |
| Type == WLC_OBJ_BIT_NOR || // 20: bitwise OR |
| Type == WLC_OBJ_BIT_NXOR || // 21: bitwise NXOR |
| |
| Type == WLC_OBJ_LOGIC_IMPL || // 27: logic implication |
| Type == WLC_OBJ_LOGIC_AND || // 28: logic AND |
| Type == WLC_OBJ_LOGIC_OR || // 29: logic OR |
| Type == WLC_OBJ_LOGIC_XOR || // 30: logic XOR |
| Type == WLC_OBJ_COMP_EQU || // 31: compare equal |
| // Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal -- bug fix |
| Type == WLC_OBJ_COMP_LESS || // 33: compare less |
| Type == WLC_OBJ_COMP_MORE || // 34: compare more |
| Type == WLC_OBJ_COMP_LESSEQU || // 35: compare less or equal |
| Type == WLC_OBJ_COMP_MOREEQU || // 36: compare more or equal |
| |
| Type == WLC_OBJ_ARI_ADD || // 43: arithmetic addition |
| Type == WLC_OBJ_ARI_SUB || // 44: arithmetic subtraction |
| Type == WLC_OBJ_ARI_MULTI || // 45: arithmetic multiplier |
| Type == WLC_OBJ_ARI_DIVIDE // 46: arithmetic division |
| )) |
| goto FINISHED_WITH_FANINS; |
| |
| // we will be creating nodes backwards. this way we can pop from vFanins easier |
| while (Vec_IntSize(vFanins)>2) |
| { |
| // getting 2 fanins at a time |
| old_size = Vec_IntSize(vFanins); |
| iFanin0 = Vec_IntPop(vFanins); |
| iFanin1 = Vec_IntPop(vFanins); |
| |
| Vec_IntWriteEntry(v2Fanins,0,iFanin0); |
| Vec_IntWriteEntry(v2Fanins,1,iFanin1); |
| |
| iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); |
| sprintf( Buffer, "_n%d_", iObj ); |
| pNameFanin = Buffer; |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); |
| |
| assert( !fFound ); |
| assert( iObj == NameId ); |
| |
| Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), v2Fanins ); |
| |
| // pushing the new node |
| Vec_IntPush(vFanins, iObj); |
| new_size = Vec_IntSize(vFanins); |
| assert(new_size<old_size); |
| } |
| |
| FINISHED_WITH_FANINS: |
| |
| Vec_IntFree(v2Fanins); |
| |
| //added to deal with long shifts create extra bit select (ROTATE as well ??) |
| // this is a temporary hack |
| // basically we keep only 32 bits. |
| // bit[31] will be the copy of original MSB (sign bit, just in case) UPDATE: assume it is unsigned first???? |
| // bit[31] will be the reduction or of any bits from [31] to Range |
| if (Type == WLC_OBJ_SHIFT_R || Type == WLC_OBJ_SHIFT_RA || Type == WLC_OBJ_SHIFT_L) |
| { |
| int range1, iObj1, iObj2, iObj3; |
| assert(Vec_IntSize(vFanins)>=2); |
| iFanin1 = Vec_IntEntry(vFanins,1); |
| range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) ); |
| if (range1>32) |
| { |
| Vec_Int_t * newFanins = Vec_IntAlloc(10); |
| Vec_IntPush(newFanins,iFanin1); |
| Vec_IntPushTwo( newFanins, 30, 0 ); |
| |
| iObj1 = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_SELECT, 0, 30, 0 ); |
| sprintf( Buffer, "_n%d_", iObj1 ); |
| pNameFanin = Buffer; |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); |
| |
| assert( !fFound ); |
| assert( iObj1 == NameId ); |
| |
| Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins ); |
| |
| //printf("obj1: %d\n",iObj1); |
| |
| // bit select of larger bits |
| Vec_IntPop(newFanins); |
| Vec_IntPop(newFanins); |
| Vec_IntPushTwo( newFanins, range1-1, 31 ); |
| iObj2 = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_SELECT, 0, range1-1, 31 ); |
| sprintf( Buffer, "_n%d_", iObj2 ); |
| pNameFanin = Buffer; |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); |
| |
| assert( !fFound ); |
| assert( iObj2 == NameId ); |
| |
| Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins ); |
| //printf("obj2: %d\n",iObj2); |
| |
| // reduction or |
| Vec_IntPop( newFanins ); |
| Vec_IntPop( newFanins ); |
| Vec_IntWriteEntry( newFanins, 0, iObj2 ); |
| iObj3 = Wlc_ObjAlloc( pNtk, WLC_OBJ_REDUCT_OR, 0, 0, 0 ); |
| sprintf( Buffer, "_n%d_", iObj3 ); |
| pNameFanin = Buffer; |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); |
| |
| assert( !fFound ); |
| assert( iObj3 == NameId ); |
| |
| Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins ); |
| //printf("obj3: %d\n",iObj3); |
| |
| // concat all together |
| Vec_IntWriteEntry( newFanins, 0, iObj3 ); |
| Vec_IntPush( newFanins, iObj1 ); |
| iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_BIT_CONCAT, 0, 31, 0 ); |
| sprintf( Buffer, "_n%d_", iObj ); |
| pNameFanin = Buffer; |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pNameFanin, &fFound ); |
| |
| assert( !fFound ); |
| assert( iObj == NameId ); |
| |
| Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins ); |
| //printf("obj: %d\n",iObj); |
| |
| // pushing the new node |
| Vec_IntWriteEntry(vFanins, 1, iObj); |
| Vec_IntFree(newFanins); |
| } |
| } |
| |
| iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 ); |
| |
| // add node's name |
| if ( pName == NULL ) |
| { |
| sprintf( Buffer, "_n%d_", iObj ); |
| pName = Buffer; |
| } |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); |
| assert( !fFound ); |
| assert( iObj == NameId ); |
| |
| 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; |
| } |
| |
| return iObj; |
| } |
| |
| static inline char * Smt_GetHexFromDecimalString(char * pStr) |
| { |
| int i,k=0, nDigits = strlen(pStr); |
| int digit, carry = 0; |
| int metNonZeroBit = 0; |
| |
| Vec_Int_t * decimal = Vec_IntAlloc(nDigits); |
| Vec_Int_t * rev; |
| int nBits; |
| char * hex; |
| |
| for (i=0;i<nDigits;i++) |
| Vec_IntPush(decimal,pStr[i]-'0'); |
| |
| // firstly fillin the reversed vector |
| rev = Vec_IntAlloc(10); |
| while(k<nDigits) |
| { |
| digit = Vec_IntEntry(decimal,k); |
| if (!digit && !carry) |
| { |
| k++; |
| if (k>=nDigits) |
| { |
| if (!metNonZeroBit) |
| break; |
| else |
| { |
| Vec_IntPush(rev,carry); |
| carry = 0; |
| k = 0; |
| metNonZeroBit = 0; |
| } |
| } |
| continue; |
| } |
| |
| if (!metNonZeroBit) |
| metNonZeroBit = 1; |
| |
| digit = carry*10 + digit; |
| carry = digit%2; |
| digit = digit / 2; |
| Vec_IntWriteEntry(decimal,k,digit); |
| |
| k++; |
| if (k>=nDigits) |
| { |
| Vec_IntPush(rev,carry); |
| carry = 0; |
| k = 0; |
| metNonZeroBit = 0; |
| } |
| } |
| |
| Vec_IntFree(decimal); |
| |
| if (!Vec_IntSize(rev)) |
| Vec_IntPush(rev,0); |
| |
| while (Vec_IntSize(rev)%4) |
| Vec_IntPush(rev,0); |
| |
| nBits = Vec_IntSize(rev); |
| hex = (char *)malloc((nBits/4+1)*sizeof(char)); |
| |
| for (k=0;k<nBits/4;k++) |
| { |
| int number = Vec_IntEntry(rev,k*4) + 2*Vec_IntEntry(rev,k*4+1) + 4*Vec_IntEntry(rev,k*4+2) + 8*Vec_IntEntry(rev,k*4+3); |
| char letter; |
| |
| switch(number) { |
| case 0: letter = '0'; break; |
| case 1: letter = '1'; break; |
| case 2: letter = '2'; break; |
| case 3: letter = '3'; break; |
| case 4: letter = '4'; break; |
| case 5: letter = '5'; break; |
| case 6: letter = '6'; break; |
| case 7: letter = '7'; break; |
| case 8: letter = '8'; break; |
| case 9: letter = '9'; break; |
| case 10: letter = 'a'; break; |
| case 11: letter = 'b'; break; |
| case 12: letter = 'c'; break; |
| case 13: letter = 'd'; break; |
| case 14: letter = 'e'; break; |
| case 15: letter = 'f'; break; |
| default: assert(0); |
| } |
| hex[nBits/4-1-k] = letter; |
| //if (k<Vec_IntSize(rev)) |
| // Vec_IntPush(vFanins,Vec_IntEntry(rev,k)); |
| //else |
| // Vec_IntPush(vFanins,0); |
| } |
| hex[nBits/4] = '\0'; |
| Vec_IntFree(rev); |
| |
| return hex; |
| } |
| |
| static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName ) |
| { |
| int i, nDigits, iObj; |
| Vec_Int_t * vFanins = Vec_IntAlloc( 10 ); |
| if ( pStr[0] != '#' ) // decimal |
| { |
| if ( pStr[0] >= '0' && pStr[0] <= '9' ) |
| { |
| // added: sanity check for large constants |
| /* |
| Vec_Int_t * temp = Vec_IntAlloc(10); |
| int fullBits = -1; |
| Smt_GetBinaryFromDecimalString(pStr,temp,&fullBits); |
| Vec_IntFree(temp); |
| assert(fullBits < 32);*/ |
| |
| char * pHex = Smt_GetHexFromDecimalString(pStr); |
| |
| if ( nBits == -1 ) |
| nBits = strlen(pHex)*4; |
| |
| //printf("nbits: %d\n",nBits); |
| |
| Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); |
| nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex ); |
| ABC_FREE( pHex ); |
| |
| /* |
| int w, nWords, Number = atoi( pStr ); |
| if ( nBits == -1 ) |
| { |
| nBits = Abc_Base2Log( Number+1 ); |
| assert( nBits < 32 ); |
| } |
| nWords = Abc_BitWordNum( nBits ); |
| for ( w = 0; w < nWords; w++ ) |
| Vec_IntPush( vFanins, w ? 0 : Number ); |
| */ |
| } |
| else |
| { |
| int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); |
| assert( fFound ); |
| Vec_IntFree( vFanins ); |
| return iObj; |
| } |
| } |
| else if ( pStr[1] == 'b' ) // binary |
| { |
| if ( nBits == -1 ) |
| nBits = strlen(pStr+2); |
| Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); |
| for ( i = 0; i < nBits; i++ ) |
| if ( pStr[2+i] == '1' ) |
| Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i ); |
| else if ( pStr[2+i] != '0' ) |
| { |
| Vec_IntFree( vFanins ); |
| return 0; |
| } |
| } |
| else if ( pStr[1] == 'x' ) // hexadecimal |
| { |
| if ( nBits == -1 ) |
| nBits = strlen(pStr+2)*4; |
| Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 ); |
| nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 ); |
| if ( nDigits != (nBits + 3)/4 ) |
| { |
| Vec_IntFree( vFanins ); |
| return 0; |
| } |
| } |
| else |
| { |
| Vec_IntFree( vFanins ); |
| return 0; |
| } |
| // create constant node |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, vFanins, pName ); |
| Vec_IntFree( vFanins ); |
| return iObj; |
| } |
| int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, char * pName ) |
| { |
| if ( Smt_EntryIsName(iNode) ) // name or constant |
| { |
| char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); |
| if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' ) |
| { |
| // (_ BitVec 8) #x19 |
| return Smt_PrsBuildConstant( pNtk, pStr, RangeOut, pName ); |
| } |
| else |
| { |
| // s3087 |
| int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); |
| assert( fFound ); |
| return iObj; |
| } |
| } |
| else // node |
| { |
| Vec_Int_t * vFans = Smt_EntryNode( p, iNode ); |
| char * pStr0 = Smt_VecEntryName( p, vFans, 0 ); |
| char * pStr1 = Smt_VecEntryName( p, vFans, 1 ); |
| if ( pStr0 && pStr1 && pStr0[0] == '_' && pStr1[0] == 'b' && pStr1[1] == 'v' ) |
| { |
| // (_ bv1 32) |
| char * pStr2 = Smt_VecEntryName( p, vFans, 2 ); |
| assert( Vec_IntSize(vFans) == 3 ); |
| return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName ); |
| } |
| else if ( pStr0 && pStr0[0] == '=' ) |
| { |
| assert( Vec_IntSize(vFans) == 3 ); |
| iNode = Vec_IntEntry(vFans, 2); |
| assert( Smt_EntryIsName(iNode) ); |
| pStr0 = Smt_EntryName(p, iNode); |
| // check the last one is "#b1" |
| if ( !strcmp("#b1", pStr0) ) |
| { |
| iNode = Vec_IntEntry(vFans, 1); |
| return Smt_PrsBuildNode( pNtk, p, iNode, -1, pName ); |
| } |
| else |
| { |
| Vec_Int_t * vFanins = Vec_IntAlloc( 2 ); |
| // get the constant |
| int iObj, iOper, iConst = Smt_PrsBuildConstant( pNtk, pStr0, -1, NULL ); |
| // check the middle one is an operator |
| iNode = Vec_IntEntry(vFans, 1); |
| iOper = Smt_PrsBuildNode( pNtk, p, iNode, -1, pName ); |
| // build comparator |
| Vec_IntPushTwo( vFanins, iOper, iConst ); |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_COMP_EQU, 0, 1, vFanins, pName ); |
| Vec_IntFree( vFanins ); |
| return iObj; |
| } |
| } |
| else |
| { |
| int i, Fan, NameId, iFanin, fSigned, Range, Value1 = -1, Value2 = -1; |
| int Type = Smt_PrsReadType( p, Vec_IntEntry(vFans, 0), &fSigned, &Value1, &Value2 ); |
| // collect fanins |
| Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); |
| Vec_IntForEachEntryStart( vFans, Fan, i, 1 ) |
| { |
| iFanin = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL ); |
| if ( iFanin == 0 ) |
| { |
| Vec_IntFree( vFanins ); |
| return 0; |
| } |
| Vec_IntPush( vFanins, iFanin ); |
| } |
| // update specialized nodes |
| assert( Type != WLC_OBJ_BIT_SIGNEXT && Type != WLC_OBJ_BIT_ZEROPAD ); |
| if ( Type == WLC_OBJ_BIT_SELECT ) |
| { |
| assert( Value1 >= 0 && Value2 >= 0 && Value1 >= Value2 ); |
| Vec_IntPushTwo( vFanins, Value1, Value2 ); |
| } |
| else if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L ) |
| { |
| char Buffer[10]; |
| assert( Value1 >= 0 ); |
| sprintf( Buffer, "%d", Value1 ); |
| NameId = Smt_PrsBuildConstant( pNtk, Buffer, -1, NULL ); |
| Vec_IntPush( vFanins, NameId ); |
| } |
| // find range |
| Range = 0; |
| if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR ) |
| Range = 1; |
| else if ( Type == WLC_OBJ_BIT_SELECT ) |
| Range = Value1 - Value2 + 1; |
| else if ( Type == WLC_OBJ_BIT_CONCAT ) |
| { |
| Vec_IntForEachEntry( vFanins, NameId, i ) |
| Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); |
| } |
| else if ( Type == WLC_OBJ_MUX ) |
| { |
| int * pArray = Vec_IntArray(vFanins); |
| assert( Vec_IntSize(vFanins) == 3 ); |
| ABC_SWAP( int, pArray[1], pArray[2] ); |
| NameId = Vec_IntEntry(vFanins, 1); |
| Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); |
| } |
| else // to determine range, look at the first argument |
| { |
| NameId = Vec_IntEntry(vFanins, 0); |
| Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); |
| } |
| // create node |
| assert( Range > 0 ); |
| NameId = Smt_PrsCreateNode( pNtk, Type, fSigned, Range, vFanins, pName ); |
| Vec_IntFree( vFanins ); |
| return NameId; |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p ) |
| { |
| Wlc_Ntk_t * pNtk; |
| Vec_Int_t * vFans, * vFans2, * vFans3; |
| Vec_Int_t * vAsserts = Vec_IntAlloc(100); |
| char * pName, * pRange, * pValue; |
| int i, k, Fan, Fan3, iObj, Status, Range, NameId, nBits = 0; |
| // issue warnings about unknown dirs |
| vFans = Vec_WecEntry( &p->vObjs, 0 ); |
| Vec_IntForEachEntry( vFans, Fan, i ) |
| { |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_VecEntryNode( p, vFans, i ); |
| Fan = Vec_IntEntry(vFans2, 0); |
| assert( Smt_EntryIsName(Fan) ); |
| if ( Abc_Lit2Var(Fan) >= SMT_PRS_END ) |
| printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) ); |
| } |
| // start network and create primary inputs |
| pNtk = Wlc_NtkAlloc( p->pName, 1000 ); |
| pNtk->pManName = Abc_NamStart( 1000, 24 ); |
| pNtk->fSmtLib = 1; |
| Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i ) |
| { |
| assert( Vec_IntSize(vFans) == 4 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) ); |
| // get name |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( Smt_EntryIsName(Fan) ); |
| pName = Smt_EntryName(p, Fan); |
| // skip () |
| Fan = Vec_IntEntry(vFans, 2); |
| assert( !Smt_EntryIsName(Fan) ); |
| // check type (Bool or BitVec) |
| Fan = Vec_IntEntry(vFans, 3); |
| if ( Smt_EntryIsName(Fan) ) |
| { |
| //(declare-fun s1 () Bool) |
| assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); |
| Range = 1; |
| } |
| else |
| { |
| // (declare-fun s1 () (_ BitVec 64)) |
| // get range |
| Fan = Vec_IntEntry(vFans, 3); |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_EntryNode(p, Fan); |
| assert( Vec_IntSize(vFans2) == 3 ); |
| assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); |
| assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); |
| Fan = Vec_IntEntry(vFans2, 2); |
| assert( Smt_EntryIsName(Fan) ); |
| pRange = Smt_EntryName(p, Fan); |
| Range = atoi(pRange); |
| } |
| // create node |
| iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 ); |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL ); |
| assert( iObj == NameId ); |
| // save values |
| Vec_IntPush( &pNtk->vValues, NameId ); |
| Vec_IntPush( &pNtk->vValues, nBits ); |
| Vec_IntPush( &pNtk->vValues, Range ); |
| nBits += Range; |
| } |
| // create constants |
| Smt_ManForEachDir( p, SMT_PRS_DEFINE_FUN, vFans, i ) |
| { |
| assert( Vec_IntSize(vFans) == 5 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); |
| // get name |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( Smt_EntryIsName(Fan) ); |
| pName = Smt_EntryName(p, Fan); |
| // skip () |
| Fan = Vec_IntEntry(vFans, 2); |
| assert( !Smt_EntryIsName(Fan) ); |
| // check type (Bool or BitVec) |
| Fan = Vec_IntEntry(vFans, 3); |
| if ( Smt_EntryIsName(Fan) ) |
| { |
| // (define-fun s_2 () Bool false) |
| assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); |
| Range = 1; |
| pValue = Smt_VecEntryName(p, vFans, 4); |
| if ( !strcmp("false", pValue) ) |
| pValue = "#b0"; |
| else if ( !strcmp("true", pValue) ) |
| pValue = "#b1"; |
| else assert( 0 ); |
| Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); |
| } |
| else |
| { |
| // (define-fun s702 () (_ BitVec 4) #xe) |
| // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) |
| // get range |
| Fan = Vec_IntEntry(vFans, 3); |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_VecEntryNode(p, vFans, 3); |
| assert( Vec_IntSize(vFans2) == 3 ); |
| assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); |
| assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); |
| // get range |
| Fan = Vec_IntEntry(vFans2, 2); |
| assert( Smt_EntryIsName(Fan) ); |
| pRange = Smt_EntryName(p, Fan); |
| Range = atoi(pRange); |
| // get constant |
| Fan = Vec_IntEntry(vFans, 4); |
| Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName ); |
| } |
| if ( !Status ) |
| { |
| Wlc_NtkFree( pNtk ); pNtk = NULL; |
| goto finish; |
| } |
| } |
| // process let-statements |
| Smt_ManForEachDir( p, SMT_PRS_LET, vFans, i ) |
| { |
| // let ((s35550 (bvor s48 s35549))) |
| assert( Vec_IntSize(vFans) == 3 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_LET) ); |
| // get parts |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_EntryNode(p, Fan); |
| if ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) ) |
| continue; |
| // iterate through the parts |
| Vec_IntForEachEntry( vFans2, Fan, k ) |
| { |
| // s35550 (bvor s48 s35549) |
| Fan = Vec_IntEntry(vFans2, 0); |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans3 = Smt_EntryNode(p, Fan); |
| // get the name |
| Fan3 = Vec_IntEntry(vFans3, 0); |
| assert( Smt_EntryIsName(Fan3) ); |
| pName = Smt_EntryName(p, Fan3); |
| // get function |
| Fan3 = Vec_IntEntry(vFans3, 1); |
| assert( !Smt_EntryIsName(Fan3) ); |
| Status = Smt_PrsBuildNode( pNtk, p, Fan3, -1, pName ); |
| if ( !Status ) |
| { |
| Wlc_NtkFree( pNtk ); pNtk = NULL; |
| goto finish; |
| } |
| } |
| } |
| // process assert-statements |
| Vec_IntClear( vAsserts ); |
| Smt_ManForEachDir( p, SMT_PRS_ASSERT, vFans, i ) |
| { |
| //(assert ; no quantifiers |
| // (let ((s2 (bvsge s0 s1))) |
| // (not s2))) |
| //(assert (not (= s0 #x00))) |
| assert( Vec_IntSize(vFans) == 2 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); |
| // get second directive |
| Fan = Vec_IntEntry(vFans, 1); |
| if ( !Smt_EntryIsName(Fan) ) |
| { |
| // find the final let-statement |
| vFans2 = Smt_VecEntryNode(p, vFans, 1); |
| while ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) ) |
| { |
| Fan = Vec_IntEntry(vFans2, 2); |
| if ( Smt_EntryIsName(Fan) ) |
| break; |
| vFans2 = Smt_VecEntryNode(p, vFans2, 2); |
| } |
| } |
| // find name or create node |
| iObj = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL ); |
| if ( !iObj ) |
| { |
| Wlc_NtkFree( pNtk ); pNtk = NULL; |
| goto finish; |
| } |
| Vec_IntPush( vAsserts, iObj ); |
| } |
| // build AND of asserts |
| if ( Vec_IntSize(vAsserts) == 1 ) |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" ); |
| else |
| { |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); |
| Vec_IntFill( vAsserts, 1, iObj ); |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" ); |
| } |
| Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); |
| // create nameIDs |
| vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); |
| Vec_IntAppend( &pNtk->vNameIds, vFans ); |
| Vec_IntFree( vFans ); |
| //Wlc_NtkReport( pNtk, NULL ); |
| finish: |
| // cleanup |
| Vec_IntFree(vAsserts); |
| return pNtk; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| char * Smt_PrsGenName( Smt_Prs_t * p ) |
| { |
| static char Buffer[16]; |
| sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount ); |
| return Buffer; |
| } |
| int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName ) |
| { |
| char suffix[100]; |
| sprintf(suffix,"_as%d",pNtk->nAssert); |
| |
| //char * prepStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); |
| //printf("prestr: %s\n",prepStr); |
| |
| //printf("inode: %d %d\n",iNode,Smt_EntryIsName(iNode)); |
| |
| if ( Smt_EntryIsName(iNode) ) |
| { |
| char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode)); |
| // handle built-in constants |
| if ( !strcmp(pStr, "false") ) |
| pStr = "#b0"; |
| else if ( !strcmp(pStr, "true") ) |
| pStr = "#b1"; |
| if ( pStr[0] == '#' ) |
| return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) ); |
| else |
| { |
| int fFound, iObj; |
| // look either for global DECLARE-FUN variable or local LET |
| char * pStr_glb = (char *)malloc(strlen(pStr) + 4 +1); //glb |
| char * pStr_loc = (char *)malloc(strlen(pStr) + strlen(suffix) +1); |
| strcpy(pStr_glb,pStr); |
| strcat(pStr_glb,SMT_GLO_SUFFIX); |
| strcpy(pStr_loc,pStr); |
| strcat(pStr_loc,suffix); |
| |
| fFound = Abc_NamStrFind( pNtk->pManName, pStr_glb ); |
| |
| if (fFound) |
| pStr = pStr_glb; |
| else |
| { |
| assert( Abc_NamStrFind( pNtk->pManName, pStr_loc )); |
| pStr = pStr_loc; |
| } |
| // FIXME: delete memory of pStr |
| |
| iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); |
| assert( fFound ); |
| // create buffer if the name of the fanin has different name |
| if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) ) |
| { |
| Vec_IntFill( &p->vTempFans, 1, iObj ); |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName ); |
| } |
| ABC_FREE( pStr_glb ); |
| ABC_FREE( pStr_loc ); |
| return iObj; |
| } |
| } |
| else |
| { |
| Vec_Int_t * vRoots, * vRoots1, * vFans3; |
| int iObj, iRoot0, iRoot1, iRoot2, Fan, Fan3, k; |
| assert( !Smt_EntryIsName(iNode) ); |
| vRoots = Smt_EntryNode( p, iNode ); |
| iRoot0 = Vec_IntEntry( vRoots, 0 ); |
| if ( Smt_EntryIsName(iRoot0) ) |
| { |
| char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0)); |
| if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let |
| { |
| // let ((s35550 (bvor s48 s35549))) |
| assert( Vec_IntSize(vRoots) == 3 ); |
| assert( Smt_VecEntryIsType(vRoots, 0, SMT_PRS_LET) ); |
| // get parts |
| iRoot1 = Vec_IntEntry(vRoots, 1); |
| assert( !Smt_EntryIsName(iRoot1) ); |
| vRoots1 = Smt_EntryNode(p, iRoot1); |
| // iterate through the parts |
| Vec_IntForEachEntry( vRoots1, Fan, k ) |
| { |
| char * temp; |
| // s35550 (bvor s48 s35549) |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans3 = Smt_EntryNode(p, Fan); |
| assert( Vec_IntSize(vFans3) == 2 ); |
| // get the name |
| Fan3 = Vec_IntEntry(vFans3, 0); |
| assert( Smt_EntryIsName(Fan3) ); |
| pName2 = Smt_EntryName(p, Fan3); |
| // create a local name with suffix |
| if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET ) |
| { |
| temp = (char *)malloc(strlen(pName2) + strlen(suffix) + 1); |
| strcpy(temp, pName2); |
| strcat(temp,suffix); |
| } |
| else |
| { temp = (char *)malloc(strlen(pName2) + 4 + 1); |
| strcpy(temp, pName2); |
| strcat(temp,SMT_GLO_SUFFIX); |
| } |
| // FIXME: need to delete memory of pName2 |
| pName2 = temp; |
| // get function |
| Fan3 = Vec_IntEntry(vFans3, 1); |
| //assert( !Smt_EntryIsName(Fan3) ); |
| // solve the problem |
| iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 ); |
| ABC_FREE( temp ); |
| if ( iObj == 0 ) |
| return 0; |
| // create buffer |
| //Vec_IntFill( &p->vTempFans, 1, iObj ); |
| //Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName2 ); |
| } |
| // process the final part of let |
| iRoot2 = Vec_IntEntry(vRoots, 2); |
| return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1, pName ); |
| } |
| else if ( pStr0[0] == '_' ) |
| { |
| char * pStr1 = Smt_VecEntryName( p, vRoots, 1 ); |
| if ( pStr1[0] == 'b' && pStr1[1] == 'v' ) |
| { |
| // (_ bv1 32) |
| char * pStr2 = Smt_VecEntryName( p, vRoots, 2 ); |
| assert( Vec_IntSize(vRoots) == 3 ); |
| return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName ? pName : Smt_PrsGenName(p) ); |
| } |
| else |
| { |
| int Type1, fSigned = 0, Range = -1; |
| assert( iObjPrev != -1 ); |
| Type1 = Smt_StrToType( pStr1, &fSigned ); |
| if ( Type1 == 0 ) |
| return 0; |
| // find out this branch |
| Vec_IntFill( &p->vTempFans, 1, iObjPrev ); |
| if ( Type1 == WLC_OBJ_BIT_SIGNEXT || Type1 == WLC_OBJ_BIT_ZEROPAD || Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L ) |
| { |
| int iRoot2 = Vec_IntEntry(vRoots, 2); |
| char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2)); |
| int Num = atoi( pStr2 ); |
| //fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT); |
| if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L ) |
| { |
| int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) ); |
| Vec_IntClear( &p->vTempFans ); |
| Vec_IntPushTwo( &p->vTempFans, iObjPrev, iConst ); |
| Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); |
| } |
| else |
| Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) ); |
| } |
| else if ( Type1 == WLC_OBJ_BIT_SELECT ) |
| { |
| int iRoot2 = Vec_IntEntry( vRoots, 2 ); |
| int iRoot3 = Vec_IntEntry( vRoots, 3 ); |
| char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2)); |
| char * pStr3 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot3)); |
| int Num1 = atoi( pStr2 ); |
| int Num2 = atoi( pStr3 ); |
| assert( Num1 >= Num2 ); |
| Range = Num1 - Num2 + 1; |
| Vec_IntPushTwo( &p->vTempFans, Num1, Num2 ); |
| } |
| else assert( 0 ); |
| iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, pName ? pName : Smt_PrsGenName(p) ); |
| return iObj; |
| } |
| } |
| else |
| { |
| Vec_Int_t * vFanins; |
| int i, Fan, fSigned = 0, Range, Type0; |
| int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 ); |
| if ( iObj ) |
| return iObj; |
| Type0 = Smt_StrToType( pStr0, &fSigned ); |
| if ( Type0 == 0 ) |
| return 0; |
| assert( Type0 != WLC_OBJ_BIT_SIGNEXT && Type0 != WLC_OBJ_BIT_ZEROPAD && Type0 != WLC_OBJ_BIT_SELECT && Type0 != WLC_OBJ_ROTATE_R && Type0 != WLC_OBJ_ROTATE_L ); |
| |
| // collect fanins |
| vFanins = Vec_IntAlloc( 100 ); |
| Vec_IntForEachEntryStart( vRoots, Fan, i, 1 ) |
| { |
| iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1, NULL ); |
| if ( iObj == 0 ) |
| { |
| Vec_IntFree( vFanins ); |
| return 0; |
| } |
| Vec_IntPush( vFanins, iObj ); |
| } |
| // find range |
| Range = 0; |
| if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR ) |
| Range = 1; |
| else if ( Type0 == WLC_OBJ_BIT_CONCAT ) |
| { |
| Vec_IntForEachEntry( vFanins, Fan, i ) |
| Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, Fan) ); |
| } |
| else if ( Type0 == WLC_OBJ_MUX ) |
| { |
| int * pArray = Vec_IntArray(vFanins); |
| assert( Vec_IntSize(vFanins) == 3 ); |
| ABC_SWAP( int, pArray[1], pArray[2] ); |
| iObj = Vec_IntEntry(vFanins, 1); |
| Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); |
| } |
| else // to determine range, look at the first argument |
| { |
| iObj = Vec_IntEntry(vFanins, 0); |
| Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); |
| } |
| // create node |
| assert( Range > 0 ); |
| iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, pName ? pName : Smt_PrsGenName(p) ); |
| Vec_IntFree( vFanins ); |
| return iObj; |
| } |
| } |
| else if ( Vec_IntSize(vRoots) == 2 ) // could be ((_ extract 48 16) (bvmul ?v_5 ?v_12)) |
| { |
| int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1, NULL ); |
| if ( iObjPrev == 0 ) |
| return 0; |
| return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev, pName ); |
| } |
| else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 ); |
| return 0; |
| } |
| } |
| Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) |
| { |
| Wlc_Ntk_t * pNtk; |
| Vec_Int_t * vFansRoot, * vFans, * vFans2; |
| Vec_Int_t * vAsserts = Vec_IntAlloc(100); |
| int i, Root, Fan, iObj, NameId, Range, nBits = 0; |
| char * pName, * pRange; |
| // start network and create primary inputs |
| pNtk = Wlc_NtkAlloc( p->pName, 1000 ); |
| pNtk->pManName = Abc_NamStart( 1000, 24 ); |
| pNtk->fSmtLib = 1; |
| // collect top-level asserts |
| vFansRoot = Vec_WecEntry( &p->vObjs, 0 ); |
| Vec_IntForEachEntry( vFansRoot, Root, i ) |
| { |
| assert( !Smt_EntryIsName(Root) ); |
| vFans = Smt_VecEntryNode( p, vFansRoot, i ); |
| Fan = Vec_IntEntry(vFans, 0); |
| assert( Smt_EntryIsName(Fan) ); |
| // create variables |
| if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN ) |
| { |
| char * pName_glb; |
| assert( Vec_IntSize(vFans) == 4 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) ); |
| // get name |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( Smt_EntryIsName(Fan) ); |
| pName = Smt_EntryName(p, Fan); |
| // added: giving a global suffix |
| pName_glb = (char *) malloc(strlen(pName) + 4 + 1); |
| strcpy(pName_glb,pName); |
| strcat(pName_glb,SMT_GLO_SUFFIX); |
| // FIXME: delete memory of pName |
| pName = pName_glb; |
| // skip () |
| Fan = Vec_IntEntry(vFans, 2); |
| assert( !Smt_EntryIsName(Fan) ); |
| // check type (Bool or BitVec) |
| Fan = Vec_IntEntry(vFans, 3); |
| if ( Smt_EntryIsName(Fan) ) |
| { //(declare-fun s1 () Bool) |
| assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); |
| Range = 1; |
| } |
| else |
| { // (declare-fun s1 () (_ BitVec 64)) |
| Fan = Vec_IntEntry(vFans, 3); |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_EntryNode(p, Fan); |
| assert( Vec_IntSize(vFans2) == 3 ); |
| assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); |
| assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); |
| Fan = Vec_IntEntry(vFans2, 2); |
| assert( Smt_EntryIsName(Fan) ); |
| pRange = Smt_EntryName(p, Fan); |
| Range = atoi(pRange); |
| } |
| // create node |
| iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 ); |
| NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL ); |
| assert( iObj == NameId ); |
| // save values |
| Vec_IntPush( &pNtk->vValues, NameId ); |
| Vec_IntPush( &pNtk->vValues, nBits ); |
| Vec_IntPush( &pNtk->vValues, Range ); |
| nBits += Range; |
| ABC_FREE( pName_glb ); |
| } |
| // create constants |
| /* |
| else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) // added: we parse DEFINE_FUN in LET |
| { |
| assert( Vec_IntSize(vFans) == 5 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); |
| // get name |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( Smt_EntryIsName(Fan) ); |
| pName = Smt_EntryName(p, Fan); |
| |
| // added: giving a global suffix |
| char * pName_glb = (char *) malloc(strlen(pName) + 4 + 1); |
| strcpy(pName_glb,pName); |
| strcat(pName_glb,SMT_GLO_SUFFIX); |
| // FIXME: delete memory of pName |
| pName = pName_glb; |
| |
| // skip () |
| Fan = Vec_IntEntry(vFans, 2); |
| assert( !Smt_EntryIsName(Fan) ); |
| // check type (Bool or BitVec) |
| Fan = Vec_IntEntry(vFans, 3); |
| if ( Smt_EntryIsName(Fan) ) |
| { |
| // (define-fun s_2 () Bool false) |
| assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); |
| Range = 1; |
| pValue = Smt_VecEntryName(p, vFans, 4); |
| |
| //printf("value: %s\n",pValue); |
| |
| if ( !strcmp("false", pValue) ) |
| pValue = "#b0"; |
| else if ( !strcmp("true", pValue) ) |
| pValue = "#b1"; |
| else assert( 0 ); |
| Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); |
| } |
| else |
| { |
| // (define-fun s702 () (_ BitVec 4) #xe) |
| // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) |
| // get range |
| Fan = Vec_IntEntry(vFans, 3); |
| |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_VecEntryNode(p, vFans, 3); |
| assert( Vec_IntSize(vFans2) == 3 ); |
| assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); |
| assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); |
| // get range |
| Fan = Vec_IntEntry(vFans2, 2); |
| |
| assert( Smt_EntryIsName(Fan) ); |
| pRange = Smt_EntryName(p, Fan); |
| Range = atoi(pRange); |
| |
| // added: can parse functions too |
| Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4); |
| Fan = Vec_IntEntry(vFans3, 0); |
| |
| // get constant |
| //Fan = Vec_IntEntry(vFans, 4); |
| |
| //printf("fan3: %s\n",Fan); |
| //printf("fan0: %s\n",Smt_VecEntryName(p, vFans3, 0)); |
| //printf("fan1: %s\n",Smt_VecEntryName(p, vFans3, 1)); |
| //printf("fan2: %s\n",Smt_VecEntryName(p, vFans3, 2)); |
| //printf("fan3: %s\n",Smt_VecEntryName(p, vFans3, 3)); |
| |
| Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName ); |
| } |
| if ( !Status ) |
| { |
| Wlc_NtkFree( pNtk ); pNtk = NULL; |
| goto finish; |
| } |
| } |
| */ |
| // added: new way to parse define-fun |
| // create constants |
| else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) |
| { |
| char * pName_glb; |
| // (define-fun def_16001 () Bool (or def_15999 def_16000)) |
| // (define-fun def_15990 () (_ BitVec 24) (concat def_15988 def_15989)) |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) ); |
| assert( Vec_IntSize(vFans) == 5 ); // const or definition |
| |
| // get name |
| Fan = Vec_IntEntry(vFans, 1); |
| assert( Smt_EntryIsName(Fan) ); |
| pName = Smt_EntryName(p, Fan); |
| // added: giving a global suffix |
| pName_glb = (char *) malloc(strlen(pName) + 4 + 1); |
| strcpy(pName_glb,pName); |
| strcat(pName_glb,SMT_GLO_SUFFIX); |
| // FIXME: delete memory of pName |
| pName = pName_glb; |
| |
| //get range |
| Fan = Vec_IntEntry(vFans, 3); |
| if ( Smt_EntryIsName(Fan) ) |
| { |
| // (define-fun s_2 () Bool false) |
| assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); |
| Range = 1; |
| } |
| else |
| { |
| // (define-fun s702 () (_ BitVec 4) #xe) |
| // (define-fun s1 () (_ BitVec 8) (bvneg #x7f)) |
| assert( !Smt_EntryIsName(Fan) ); |
| vFans2 = Smt_VecEntryNode(p, vFans, 3); |
| assert( Vec_IntSize(vFans2) == 3 ); |
| assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) ); |
| assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) ); |
| // get range |
| Fan = Vec_IntEntry(vFans2, 2); |
| assert( Smt_EntryIsName(Fan) ); |
| pRange = Smt_EntryName(p, Fan); |
| Range = atoi(pRange); |
| } |
| |
| iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), Range, pName ); |
| assert( iObj ); |
| ABC_FREE( pName_glb ); |
| } |
| |
| // collect assertion outputs |
| else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT ) |
| { |
| //(assert ; no quantifiers |
| // (let ((s2 (bvsge s0 s1))) |
| // (not s2))) |
| //(assert (not (= s0 #x00))) |
| assert( Vec_IntSize(vFans) == 2 ); |
| assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) ); |
| pNtk->nAssert++; // added |
| iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL ); |
| if ( iObj == 0 ) |
| { |
| Wlc_NtkFree( pNtk ); pNtk = NULL; |
| goto finish; |
| } |
| Vec_IntPush( vAsserts, iObj ); |
| } |
| // issue warnings about unknown dirs |
| else if ( Abc_Lit2Var(Fan) >= SMT_PRS_END ) |
| printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) ); |
| } |
| // build AND of asserts |
| if ( Vec_IntSize(vAsserts) == 1 ) |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" ); |
| // added: 0 asserts |
| else if ( Vec_IntSize(vAsserts) == 0 ) |
| iObj = Smt_PrsBuildConstant( pNtk, "#b1", 1, "miter" ); |
| else |
| { |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL ); |
| Vec_IntFill( vAsserts, 1, iObj ); |
| iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter" ); |
| } |
| Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 ); |
| // create nameIDs |
| vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) ); |
| Vec_IntAppend( &pNtk->vNameIds, vFans ); |
| Vec_IntFree( vFans ); |
| //Wlc_NtkReport( pNtk, NULL ); |
| finish: |
| // cleanup |
| Vec_IntFree(vAsserts); |
| return pNtk; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| // create error message |
| static inline int Smt_PrsErrorSet( Smt_Prs_t * p, char * pError, int Value ) |
| { |
| assert( !p->ErrorStr[0] ); |
| sprintf( p->ErrorStr, "%s", pError ); |
| return Value; |
| } |
| // print error message |
| static inline int Smt_PrsErrorPrint( Smt_Prs_t * p ) |
| { |
| char * pThis; int iLine = 0; |
| if ( !p->ErrorStr[0] ) return 1; |
| for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ ) |
| iLine += (int)(*pThis == '\n'); |
| printf( "Line %d: %s\n", iLine, p->ErrorStr ); |
| return 0; |
| } |
| static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit ) |
| { |
| char * pBuffer; |
| int nFileSize, RetValue; |
| FILE * pFile = fopen( pFileName, "rb" ); |
| if ( pFile == NULL ) |
| { |
| printf( "Cannot open input file.\n" ); |
| return NULL; |
| } |
| // get the file size, in bytes |
| fseek( pFile, 0, SEEK_END ); |
| nFileSize = ftell( pFile ); |
| // move the file current reading position to the beginning |
| rewind( pFile ); |
| // load the contents of the file into memory |
| pBuffer = ABC_ALLOC( char, nFileSize + 16 ); |
| pBuffer[0] = '\n'; |
| RetValue = fread( pBuffer+1, nFileSize, 1, pFile ); |
| fclose( pFile ); |
| // terminate the string with '\0' |
| pBuffer[nFileSize + 1] = '\n'; |
| pBuffer[nFileSize + 2] = '\0'; |
| *ppLimit = pBuffer + nFileSize + 2; |
| return pBuffer; |
| } |
| static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit ) |
| { |
| char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0; |
| int backslash = 0; |
| for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ ) |
| { |
| if ( *pTemp == '(' ) |
| { if ( !fHaveBar ) nCount1++; } |
| else if ( *pTemp == ')' ) |
| { if ( !fHaveBar ) nCount2++; } |
| else if ( *pTemp == '|' ) |
| fHaveBar ^= 1; |
| else if ( *pTemp == ';' && !fHaveBar ) |
| while ( *pTemp && *pTemp != '\n' ) |
| *pTemp++ = ' '; |
| // added: hack to remove quotes |
| else if ( *pTemp == '\"' && *(pTemp-1) != '\\' && !fHaveBar ) |
| { |
| *pTemp++ = ' '; |
| while ( *pTemp && (*pTemp != '\"' || backslash)) |
| { |
| if (*pTemp == '\\') |
| backslash = 1; |
| else |
| backslash = 0; |
| *pTemp++ = ' '; |
| } |
| // remove the last quote symbol |
| *pTemp = ' '; |
| } |
| } |
| |
| if ( nCount1 != nCount2 ) |
| printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", nCount1, nCount2 ); |
| else if ( nCount1 == 0 ) |
| printf( "The input SMTLIB file has no opening or closing parentheses.\n" ); |
| return nCount1 == nCount2 ? nCount1 : 0; |
| } |
| static inline Smt_Prs_t * Smt_PrsAlloc( char * pFileName, char * pBuffer, char * pLimit, int nObjs ) |
| { |
| Smt_Prs_t * p; |
| if ( nObjs == 0 ) |
| return NULL; |
| p = ABC_CALLOC( Smt_Prs_t, 1 ); |
| p->pName = pFileName; |
| p->pBuffer = pBuffer; |
| p->pLimit = pLimit; |
| p->pCur = pBuffer; |
| p->pStrs = Abc_NamStart( 1000, 24 ); |
| Smt_AddTypes( p->pStrs ); |
| Vec_IntGrow( &p->vStack, 100 ); |
| //Vec_WecGrow( &p->vDepth, 100 ); |
| Vec_WecGrow( &p->vObjs, nObjs+1 ); |
| return p; |
| } |
| static inline void Smt_PrsFree( Smt_Prs_t * p ) |
| { |
| if ( p->pStrs ) |
| Abc_NamDeref( p->pStrs ); |
| Vec_IntErase( &p->vStack ); |
| Vec_IntErase( &p->vTempFans ); |
| //Vec_WecErase( &p->vDepth ); |
| Vec_WecErase( &p->vObjs ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Smt_PrsIsSpace( char c ) |
| { |
| return c == ' ' || c == '\t' || c == '\r' || c == '\n'; |
| } |
| static inline void Smt_PrsSkipSpaces( Smt_Prs_t * p ) |
| { |
| while ( Smt_PrsIsSpace(*p->pCur) ) |
| p->pCur++; |
| } |
| static inline void Smt_PrsSkipNonSpaces( Smt_Prs_t * p ) |
| { |
| while ( p->pCur < p->pLimit && !Smt_PrsIsSpace(*p->pCur) && *p->pCur != '(' && *p->pCur != ')' ) |
| p->pCur++; |
| } |
| void Smt_PrsReadLines( Smt_Prs_t * p ) |
| { |
| int fFirstTime = 1; |
| assert( Vec_IntSize(&p->vStack) == 0 ); |
| //assert( Vec_WecSize(&p->vDepth) == 0 ); |
| assert( Vec_WecSize(&p->vObjs) == 0 ); |
| // add top node at level 0 |
| //Vec_WecPushLevel( &p->vDepth ); |
| //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) ); |
| // add top node |
| Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) ); |
| Vec_WecPushLevel( &p->vObjs ); |
| // add other nodes |
| for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ ) |
| { |
| Smt_PrsSkipSpaces( p ); |
| if ( fFirstTime && *p->pCur == '|' ) |
| { |
| fFirstTime = 0; |
| *p->pCur = ' '; |
| while ( *p->pCur && *p->pCur != '|' ) |
| *p->pCur++ = ' '; |
| if ( *p->pCur == '|' ) |
| *p->pCur = ' '; |
| continue; |
| } |
| if ( *p->pCur == '(' ) |
| { |
| // add new node at this depth |
| //assert( Vec_WecSize(&p->vDepth) >= Vec_IntSize(&p->vStack) ); |
| //if ( Vec_WecSize(&p->vDepth) == Vec_IntSize(&p->vStack) ) |
| // Vec_WecPushLevel(&p->vDepth); |
| //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) ); |
| // add fanin to node on the previous level |
| Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(Vec_WecSize(&p->vObjs), 0) ); |
| // add node to the stack |
| Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) ); |
| Vec_WecPushLevel( &p->vObjs ); |
| } |
| else if ( *p->pCur == ')' ) |
| { |
| Vec_IntPop( &p->vStack ); |
| } |
| else // token |
| { |
| char * pStart = p->pCur; |
| Smt_PrsSkipNonSpaces( p ); |
| if ( p->pCur < p->pLimit ) |
| { |
| // remove strange characters (this can lead to name clashes) |
| int iToken; |
| /* commented out for SMT comp |
| char * pTemp; |
| if ( *pStart == '?' ) |
| *pStart = '_'; |
| for ( pTemp = pStart; pTemp < p->pCur; pTemp++ ) |
| if ( *pTemp == '.' ) |
| *pTemp = '_';*/ |
| // create and save token for this string |
| iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL ); |
| Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) ); |
| } |
| } |
| } |
| assert( Vec_IntSize(&p->vStack) == 1 ); |
| assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) ); |
| p->nDigits = Abc_Base16Log( Vec_WecSize(&p->vObjs) ); |
| } |
| void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth ) |
| { |
| Vec_Int_t * vFans; int i, Fan; |
| printf( "%*s(\n", Depth, "" ); |
| vFans = Vec_WecEntry( &p->vObjs, iObj ); |
| Vec_IntForEachEntry( vFans, Fan, i ) |
| { |
| if ( Abc_LitIsCompl(Fan) ) |
| { |
| printf( "%*s", Depth+2, "" ); |
| printf( "%s\n", Abc_NamStr(p->pStrs, Abc_Lit2Var(Fan)) ); |
| } |
| else |
| Smt_PrsPrintParser_rec( p, Abc_Lit2Var(Fan), Depth+4 ); |
| } |
| printf( "%*s)\n", Depth, "" ); |
| } |
| void Smt_PrsPrintParser( Smt_Prs_t * p ) |
| { |
| // Vec_WecPrint( &p->vDepth, 0 ); |
| Smt_PrsPrintParser_rec( p, 0, 0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree ) |
| { |
| Wlc_Ntk_t * pNtk = NULL; |
| int nCount = Smt_PrsRemoveComments( pBuffer, pLimit ); |
| Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount ); |
| if ( p == NULL ) |
| return NULL; |
| Smt_PrsReadLines( p ); |
| if ( fPrintTree ) |
| Smt_PrsPrintParser( p ); |
| if ( Smt_PrsErrorPrint(p) ) |
| pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p); |
| Smt_PrsFree( p ); |
| return pNtk; |
| } |
| Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree ) |
| { |
| Wlc_Ntk_t * pNtk = NULL; |
| char * pBuffer, * pLimit; |
| pBuffer = Smt_PrsLoadFile( pFileName, &pLimit ); |
| if ( pBuffer == NULL ) |
| return NULL; |
| pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree ); |
| ABC_FREE( pBuffer ); |
| return pNtk; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
