Skip to content

A
abc
Commit f27979fc by Alan Mishchenko
Options

Improvements to the SMTLIB parser.

parent 2fcdd113
Showing with 669 additions and 515 deletions
src/base/wlc/wlcBlast.c
...@@ -107,6 +107,8 @@ void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, ...@@ -107,6 +107,8 @@ void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift,
int * pRes = Wlc_VecCopy( vRes, pNum, nNum ); int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
int Fill = fSticky ? pNum[nNum-1] : 0; int Fill = fSticky ? pNum[nNum-1] : 0;
int i, j, fShort = 0; int i, j, fShort = 0;
if ( nShift > 32 )
nShift = 32;
assert( nShift <= 32 ); assert( nShift <= 32 );
for( i = 0; i < nShift; i++ ) for( i = 0; i < nShift; i++ )
for( j = 0; j < nNum - fSticky; j++ ) for( j = 0; j < nNum - fSticky; j++ )
...@@ -126,6 +128,8 @@ void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, i ...@@ -126,6 +128,8 @@ void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, i
int * pRes = Wlc_VecCopy( vRes, pNum, nNum ); int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
int Fill = fSticky ? pNum[0] : 0; int Fill = fSticky ? pNum[0] : 0;
int i, j, fShort = 0; int i, j, fShort = 0;
if ( nShift > 32 )
nShift = 32;
assert( nShift <= 32 ); assert( nShift <= 32 );
for( i = 0; i < nShift; i++ ) for( i = 0; i < nShift; i++ )
for( j = nNum-1; j >= fSticky; j-- ) for( j = nNum-1; j >= fSticky; j-- )
......
src/base/wlc/wlcReadSmt.c
/**CFile**************************************************************** /**CFile****************************************************************
FileName [wlcReadSmt.c] FileName [wlcParse.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
...@@ -14,11 +14,12 @@ ...@@ -14,11 +14,12 @@
Date [Ver. 1.0. Started - August 22, 2014.] Date [Ver. 1.0. Started - August 22, 2014.]
Revision [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] Revision [$Id: wlcParse.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
#include "wlc.h" #include "wlc.h"
#include "misc/vec/vecWec.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -26,19 +27,9 @@ ABC_NAMESPACE_IMPL_START ...@@ -26,19 +27,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// parser name types
typedef enum {
PRS_SMT_NONE = 0,
PRS_SMT_INPUT,
PRS_SMT_CONST,
PRS_SMT_LET,
PRS_SMT_ASSERT,
PRS_SMT_VALUE
} Prs_ManType_t;
// parser // parser
typedef struct Prs_Smt_t_ Prs_Smt_t; typedef struct Smt_Prs_t_ Smt_Prs_t;
struct Prs_Smt_t_ struct Smt_Prs_t_
{ {
// input data // input data
char * pName; // file name char * pName; // file name
...@@ -47,81 +38,77 @@ struct Prs_Smt_t_ ...@@ -47,81 +38,77 @@ struct Prs_Smt_t_
char * pCur; // current position char * pCur; // current position
Abc_Nam_t * pStrs; // string manager Abc_Nam_t * pStrs; // string manager
// network structure // network structure
Vec_Int_t vData; Vec_Int_t vStack; // current node on each level
Vec_Int_t vValues; //Vec_Wec_t vDepth; // objects on each level
Vec_Wec_t vObjs; // objects
// error handling // error handling
char ErrorStr[1000]; char ErrorStr[1000];
}; };
// parser name types
// create error message typedef enum {
static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value ) SMT_PRS_NONE = 0,
{ SMT_PRS_SET_OPTION,
assert( !p->ErrorStr[0] ); SMT_PRS_SET_LOGIC,
sprintf( p->ErrorStr, "%s", pError ); SMT_PRS_SET_INFO,
return Value; SMT_PRS_DEFINE_FUN,
} SMT_PRS_DECLARE_FUN,
// clear error message SMT_PRS_ASSERT,
static inline void Prs_SmtErrorClear( Prs_Smt_t * p ) 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_
{ {
p->ErrorStr[0] = '\0'; Smt_LineType_t Type;
} char * pName;
// print error message };
static inline int Prs_SmtErrorPrint( Prs_Smt_t * p ) static Smt_Pair_t s_Types[SMT_PRS_END] =
{ {
char * pThis; int iLine = 0; { SMT_PRS_NONE, NULL },
if ( !p->ErrorStr[0] ) return 1; { SMT_PRS_SET_OPTION, "set-option" },
for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ ) { SMT_PRS_SET_LOGIC, "set-logic" },
iLine += (int)(*pThis == '\n'); { SMT_PRS_SET_INFO, "set-info" },
printf( "Line %d: %s\n", iLine, p->ErrorStr ); { SMT_PRS_DEFINE_FUN, "define-fun" },
return 0; { SMT_PRS_DECLARE_FUN, "declare-fun" },
} { SMT_PRS_ASSERT, "assert" },
static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit ) { 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 )
{ {
char * pBuffer; Smt_LineType_t i;
int nFileSize, RetValue; for ( i = 1; i < SMT_PRS_END; i++ )
FILE * pFile = fopen( pFileName, "rb" ); if ( s_Types[i].Type == Type )
if ( pFile == NULL ) return s_Types[i].pName;
{
printf( "Cannot open input file.\n" );
return NULL; 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 + 3 );
pBuffer[0] = '\n';
RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
// terminate the string with '\0'
pBuffer[nFileSize + 0] = '\n';
pBuffer[nFileSize + 1] = '\0';
*ppLimit = pBuffer + nFileSize + 2;
return pBuffer;
} }
static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName, char * pBuffer, char * pLimit ) static inline void Smt_AddTypes( Abc_Nam_t * p )
{ {
Prs_Smt_t * p; Smt_LineType_t Type;
p = ABC_CALLOC( Prs_Smt_t, 1 ); for ( Type = 1; Type < SMT_PRS_END; Type++ )
p->pName = pFileName; Abc_NamStrFindOrAdd( p, Smt_GetTypeName(Type), NULL );
p->pBuffer = pBuffer; assert( Abc_NamObjNumMax(p) == SMT_PRS_END );
p->pLimit = pLimit;
p->pCur = pBuffer;
p->pStrs = Abc_NamStart( 1000, 24 );
Vec_IntGrow ( &p->vData, 1000 );
return p;
} }
static inline void Prs_SmtFree( Prs_Smt_t * p ) 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; }
if ( p->pStrs ) static inline char * Smt_EntryName( Smt_Prs_t * p, int Fan ) { assert(Smt_EntryIsName(Fan)); return Abc_NamStr( p->pStrs, Abc_Lit2Var(Fan) ); }
Abc_NamDeref( p->pStrs ); 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) ); }
Vec_IntErase( &p->vData );
Vec_IntErase( &p->vValues ); 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); }
ABC_FREE( p ); 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 DEFINITIONS ///
...@@ -138,306 +125,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p ) ...@@ -138,306 +125,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Prs_SmtRemoveComments( Prs_Smt_t * p ) static inline int Smt_StrToType( char * pName, int * pfSigned )
{
char * pTemp;
for ( pTemp = p->pBuffer; pTemp < p->pLimit; pTemp++ )
if ( *pTemp == ';' )
while ( *pTemp && *pTemp != '\n' )
*pTemp++ = ' ';
}
static inline void Prs_SmtSkipSpaces( Prs_Smt_t * p )
{
while ( *p->pCur == ' ' || *p->pCur == '\t' || *p->pCur == '\r' || *p->pCur == '\n' )
p->pCur++;
}
static inline int Prs_SmtIsWord( Prs_Smt_t * p, char * pWord )
{
Prs_SmtSkipSpaces( p );
if ( strncmp( p->pCur, pWord, strlen(pWord) ) )
return 0;
p->pCur += strlen(pWord);
Prs_SmtSkipSpaces( p );
return 1;
}
static inline char * Prs_SmtFindNextPar( Prs_Smt_t * p )
{
char * pTemp; int Count = 1;
for ( pTemp = p->pCur; pTemp < p->pLimit; pTemp++ )
{
if ( *pTemp == '(' )
Count++;
else if ( *pTemp == ')' )
Count--;
if ( Count == 0 )
break;
}
assert( *pTemp == ')' );
return pTemp;
}
static inline int Prs_SmtParseLet( Prs_Smt_t * p, char * pLimit, int Type )
{
char * pToken;
assert( *pLimit == ')' );
*pLimit = 0;
Vec_IntPush( &p->vData, 0 );
Vec_IntPush( &p->vData, Type );
pToken = strtok( p->pCur, " ()" );
while ( pToken )
{
if ( pToken[0] != '_' && pToken[0] != '=' )
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
pToken = strtok( NULL, " ()" );
}
assert( *pLimit == 0 );
*pLimit = ')';
p->pCur = pLimit;
return 1;
}
static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type )
{
char * pToken;
assert( *pLimit == ')' );
*pLimit = 0;
Vec_IntPush( &p->vData, 0 );
Vec_IntPush( &p->vData, Type );
pToken = strtok( p->pCur, " ()" );
assert( pToken != NULL );
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
pToken = strtok( NULL, " ()" );
if ( pToken[0] == '_' )
pToken = strtok( NULL, " ()" );
if ( !strcmp(pToken, "Bool") )
{
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "1", NULL) );
pToken = strtok( NULL, " ()" );
if ( !strcmp(pToken, "false") )
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b0", NULL) );
else if ( !strcmp(pToken, "true") )
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b1", NULL) );
else assert( 0 );
}
else if ( !strcmp(pToken, "BitVec") )
{
pToken = strtok( NULL, " ()" );
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
pToken = strtok( NULL, " ()" );
if ( pToken )
{
Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
pToken = strtok( NULL, " ()" );
if ( pToken != NULL )
return Prs_SmtErrorSet(p, "Trailing symbols are not recognized.", 0);
}
}
else
return Prs_SmtErrorSet(p, "Expecting either \"Bool\" or \"BitVec\".", 0);
assert( *pLimit == 0 );
*pLimit = ')';
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 == '(' )
{
p->pCur++;
if ( Prs_SmtIsWord(p, "let") )
{
assert( *p->pCur == '(' );
p->pCur++;
if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_LET ) )
return 0;
assert( *p->pCur == ')' );
p->pCur++;
}
else if ( Prs_SmtIsWord(p, "declare-fun") )
{
if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_INPUT ) )
return 0;
assert( *p->pCur == ')' );
p->pCur++;
}
else if ( Prs_SmtIsWord(p, "define-fun") )
{
if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_CONST ) )
return 0;
assert( *p->pCur == ')' );
p->pCur++;
}
else if ( Prs_SmtIsWord(p, "get-value") )
{
if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) )
return 0;
assert( *p->pCur == ')' );
p->pCur++;
}
else if ( Prs_SmtIsWord(p, "assert") )
fAssert = 1;
else if ( Prs_SmtIsWord(p, "check-sat") )
break;
else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") )
p->pCur = Prs_SmtFindNextPar(p) + 1;
// 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 );
}
}
assert( fAssert == 0 );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Prs_SmtPrintParser( Prs_Smt_t * p )
{
int Entry, i;
Vec_IntForEachEntry( &p->vData, Entry, i )
{
if ( Entry == 0 )
{
printf( "\n" );
if ( i == Vec_IntSize(&p->vData) - 1 )
break;
Entry = Vec_IntEntry(&p->vData, ++i);
if ( Entry == PRS_SMT_INPUT )
printf( "declare-fun" );
else if ( Entry == PRS_SMT_CONST )
printf( "define-fun" );
else if ( Entry == PRS_SMT_LET )
printf( "let" );
else if ( Entry == PRS_SMT_ASSERT )
printf( "assert" );
else assert(0);
continue;
}
printf( " %s", Abc_NamStr(p->pStrs, Entry) );
}
Vec_IntForEachEntry( &p->vValues, Entry, i )
printf( "get-value %s\n", Abc_NamStr(p->pStrs, Entry) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Prs_SmtReadConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins, char * pName )
{
char Buffer[100];
int i, nDigits, iObj, NameId, fFound;
Vec_IntClear( vFanins );
if ( pStr[0] != '#' )
{
// handle decimal number
int Number = atoi( pStr );
nBits = Abc_Base2Log( Number+1 );
assert( nBits < 32 );
Vec_IntPush( vFanins, Number );
}
else if ( pStr[1] == 'b' )
{
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' )
return 0;
}
else if ( pStr[1] == 'x' )
{
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 )
assert( 0 );
}
else return 0;
// create constant node
iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_CONST, 0, nBits-1, 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
// add node's name
if ( pName == NULL )
{
sprintf( Buffer, "_c%d_", iObj );
pName = Buffer;
}
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound );
assert( iObj == NameId );
return NameId;
}
static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins )
{
if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' )
{
Vec_Int_t * vTemp = Vec_IntAlloc(0);
int NameId = Prs_SmtReadConstant( pNtk, pStr, nBits, vTemp, NULL );
Vec_IntFree( vTemp );
if ( !NameId )
return 0;
Vec_IntPush( vFanins, NameId );
return 1;
}
else
{
// read name
int fFound, NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
Vec_IntPush( vFanins, NameId );
return 1;
}
}
static inline int Prs_SmtStrToType( char * pName, int * pfSigned )
{ {
int Type = 0; *pfSigned = 0; int Type = 0; *pfSigned = 0;
if ( !strcmp(pName, "ite") ) if ( !strcmp(pName, "ite") )
...@@ -534,63 +222,203 @@ static inline int Prs_SmtStrToType( char * pName, int * pfSigned ) ...@@ -534,63 +222,203 @@ static inline int Prs_SmtStrToType( char * pName, int * pfSigned )
} }
return Type; 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, int * pfSigned ) static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int * Value1, int * Value2 )
{ {
int Type, NameId; if ( Smt_EntryIsName(iSig) )
char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) ); 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 // read type
Type = Prs_SmtStrToType( pName, pfSigned ); Type = Smt_StrToType( Smt_VecEntryName(p, vFans, 1), pfSigned );
if ( Type == 0 ) if ( Type == 0 )
return 0; return 0;
*pRange = 0; *Value1 = atoi( Smt_VecEntryName(p, vFans, 2) );
Vec_IntClear( vFanins ); if ( Vec_IntSize(vFans) > 3 )
if ( Type == WLC_OBJ_COMP_EQU ) *Value2 = atoi( Smt_VecEntryName(p, vFans, 3) );
return Type;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Smt_PrsCreateNode( 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 );
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;
}
if ( pName == NULL )
{
sprintf( Buffer, "_n%d_", iObj );
pName = Buffer;
}
// add node's name
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound );
assert( iObj == NameId );
return iObj;
}
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
{
int Number = atoi( pStr );
nBits = Abc_Base2Log( Number+1 );
assert( nBits < 32 );
Vec_IntPush( vFanins, Number );
}
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' )
return 0;
}
else if ( pStr[1] == 'x' ) // hexadecimal
{ {
*pRange = 1; if ( nBits == -1 )
Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); nBits = strlen(pStr+2)*4;
Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
return WLC_OBJ_COMP_EQU; nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 );
if ( nDigits != (nBits + 3)/4 )
return 0;
} }
else if ( Type == WLC_OBJ_LOGIC_NOT ) else 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
{ {
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
if ( !strcmp(pName, "bvcomp") ) if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' )
{ {
*pRange = 1; // (_ BitVec 8) #x19
Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins ); return Smt_PrsBuildConstant( pNtk, pStr, RangeOut, pName );
Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins );
return WLC_OBJ_COMP_NOTEQU; // 26: compare equal
} }
i--; else
{
// s3087
int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
return iObj;
} }
else if ( Type == WLC_OBJ_BIT_SELECT ) }
else // node
{ {
int End, Beg; Vec_Int_t * vFans = Smt_EntryNode( p, iNode );
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); char * pStr0 = Smt_VecEntryName( p, vFans, 0 );
End = atoi( pName ); char * pStr1 = Smt_VecEntryName( p, vFans, 1 );
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) ); if ( pStr0 && pStr1 && pStr0[0] == '_' && pStr1[0] == 'b' && pStr1[1] == 'v' )
Beg = atoi( pName );
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
Prs_SmtReadName( pNtk, pName, -1, vFanins );
Vec_IntPush( vFanins, (End << 16) | Beg );
*pRange = End - Beg + 1;
return WLC_OBJ_BIT_SELECT;
}
while ( Vec_IntEntry(vData, ++i) )
Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, i)), -1, vFanins );
if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L )
{ {
int * pArray = Vec_IntArray(vFanins); // (_ bv1 32)
assert( Vec_IntSize(vFanins) == 2 ); char * pStr2 = Smt_VecEntryName( p, vFans, 2 );
ABC_SWAP( int, pArray[0], pArray[1] ); assert( Vec_IntSize(vFans) == 3 );
return Smt_PrsBuildConstant( pNtk, pStr2+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_IntPush( vFanins, (Value1 << 16) | 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 ) if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR )
*pRange = 1; Range = 1;
else if ( Type == WLC_OBJ_BIT_SELECT )
Range = Value1 - Value2 + 1;
else if ( Type == WLC_OBJ_BIT_CONCAT ) else if ( Type == WLC_OBJ_BIT_CONCAT )
{ {
int k; Vec_IntForEachEntry( vFanins, NameId, i )
Vec_IntForEachEntry( vFanins, NameId, k ) Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
*pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
} }
else if ( Type == WLC_OBJ_MUX ) else if ( Type == WLC_OBJ_MUX )
{ {
...@@ -598,145 +426,466 @@ static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * ...@@ -598,145 +426,466 @@ static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t *
assert( Vec_IntSize(vFanins) == 3 ); assert( Vec_IntSize(vFanins) == 3 );
ABC_SWAP( int, pArray[1], pArray[2] ); ABC_SWAP( int, pArray[1], pArray[2] );
NameId = Vec_IntEntry(vFanins, 1); NameId = Vec_IntEntry(vFanins, 1);
*pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
} }
else // to determine range, look at the first argument else // to determine range, look at the first argument
{ {
NameId = Vec_IntEntry(vFanins, 0); NameId = Vec_IntEntry(vFanins, 0);
*pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) ); 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;
}
} }
return Type;
} }
Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
{ {
Wlc_Ntk_t * pNtk; Wlc_Ntk_t * pNtk;
char * pName, * pBits, * pConst; Vec_Int_t * vFans, * vFans2, * vFans3;
Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); Vec_Int_t * vAsserts = Vec_IntAlloc(100);
int i, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0; 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 // start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 ); pNtk = Wlc_NtkAlloc( p->pName, 1000 );
pNtk->pManName = Abc_NamStart( 1000, 24 ); pNtk->pManName = Abc_NamStart( 1000, 24 );
for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i )
{ {
assert( Vec_IntEntry(&p->vData, i) == 0 ); assert( Vec_IntSize(vFans) == 4 );
if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT ) 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
{ {
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); // (declare-fun s1 () (_ BitVec 64))
pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); // get range
iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 ); Fan = Vec_IntEntry(vFans, 3);
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( !Smt_EntryIsName(Fan) );
assert( !fFound ); 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 ); assert( iObj == NameId );
// save values // save values
Vec_IntPush( &pNtk->vValues, NameId ); Vec_IntPush( &pNtk->vValues, NameId );
Vec_IntPush( &pNtk->vValues, nBits ); Vec_IntPush( &pNtk->vValues, nBits );
Vec_IntPush( &pNtk->vValues, atoi(pBits) ); Vec_IntPush( &pNtk->vValues, Range );
nBits += atoi(pBits); 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);
} }
while ( Vec_IntEntry(&p->vData, ++i) );
} }
// create logic nodes // find name or create node
for ( i = 0; i < Vec_IntSize(&p->vData) - 1; ) iObj = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL );
if ( !iObj )
{ {
assert( Vec_IntEntry(&p->vData, i) == 0 ); Wlc_NtkFree( pNtk ); pNtk = NULL;
Entry = Vec_IntEntry(&p->vData, ++i); goto finish;
if ( Entry == PRS_SMT_INPUT ) }
{} Vec_IntPush( vAsserts, iObj );
else if ( Entry == PRS_SMT_CONST ) }
// 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 []
***********************************************************************/
// 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 )
{ {
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); printf( "Cannot open input file.\n" );
pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
pConst = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
// create new node
if ( !Prs_SmtReadConstant( pNtk, pConst, atoi(pBits), vFanins, pName ) )
return NULL; return NULL;
} }
else if ( Entry == PRS_SMT_LET ) // 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 + 3 );
pBuffer[0] = '\n';
RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
// terminate the string with '\0'
pBuffer[nFileSize + 0] = '\n';
pBuffer[nFileSize + 1] = '\0';
*ppLimit = pBuffer + nFileSize + 2;
return pBuffer;
}
static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit )
{
char * pTemp; int nCount1 = 0, nCount2 = 0;
for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
{ {
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) ); if ( *pTemp == '(' )
Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range, &fSigned ); nCount1++;
if ( Type == WLC_OBJ_NONE ) else if ( *pTemp == ')' )
nCount2++;
else if ( *pTemp == ';' )
while ( *pTemp && *pTemp != '\n' )
*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; return NULL;
assert( Range > 0 ); p = ABC_CALLOC( Smt_Prs_t, 1 );
// create new node p->pName = pFileName;
iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 ); p->pBuffer = pBuffer;
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins ); p->pLimit = pLimit;
if ( fSigned ) 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_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 )
{
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 ( *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 )
{ {
Wlc_NtkObj(pNtk, iObj)->Signed = fSigned; // add fanin
if ( Vec_IntSize(vFanins) > 0 ) int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned; Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) );
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 );
assert( iObj == NameId );
} }
else if ( Entry == PRS_SMT_ASSERT )
{
Type = WLC_OBJ_BUF;
Vec_IntClear( vFanins );
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
if ( !strcmp(pName, "not") )
{
Type = WLC_OBJ_LOGIC_NOT;
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
Range = 1;
} }
// add fanin assert( Vec_IntSize(&p->vStack) == 1 );
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound ); assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) );
assert( fFound ); }
Vec_IntPush( vFanins, NameId ); void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth )
// find range {
if ( Type == WLC_OBJ_BUF ) Vec_Int_t * vFans; int i, Fan;
printf( "%*s(\n", Depth, "" );
vFans = Vec_WecEntry( &p->vObjs, iObj );
Vec_IntForEachEntry( vFans, Fan, i )
{ {
// find range if ( Abc_LitIsCompl(Fan) )
iObj = Vec_IntEntry(vFanins, 0); {
Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ); printf( "%*s", Depth+2, "" );
assert( Range == 1 ); printf( "%s\n", Abc_NamStr(p->pStrs, Abc_Lit2Var(Fan)) );
}
// create new node
iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
// add node's name
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, "miter_output", &fFound );
assert( !fFound );
assert( iObj == NameId );
break;
} }
else assert( 0 ); else
while ( Vec_IntEntry(&p->vData, ++i) ); Smt_PrsPrintParser_rec( p, Abc_Lit2Var(Fan), Depth+4 );
} }
Vec_IntFree( vFanins ); printf( "%*s)\n", Depth, "" );
// create nameIDs
vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
Vec_IntAppend( &pNtk->vNameIds, vFanins );
Vec_IntFree( vFanins );
//Wlc_NtkReport( pNtk, NULL );
return pNtk;
} }
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 ) Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
{ {
Wlc_Ntk_t * pNtk = NULL; Wlc_Ntk_t * pNtk = NULL;
Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit ); int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount );
if ( p == NULL ) if ( p == NULL )
return NULL; return NULL;
Prs_SmtRemoveComments( p ); Smt_PrsReadLines( p );
Prs_SmtReadLines( p ); //Smt_PrsPrintParser( p );
//Prs_SmtPrintParser( p ); if ( Smt_PrsErrorPrint(p) )
if ( Prs_SmtErrorPrint(p) ) pNtk = Smt_PrsBuild( p );
pNtk = Prs_SmtBuild( p ); Smt_PrsFree( p );
Prs_SmtFree( p );
return pNtk; return pNtk;
} }
Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
{ {
Wlc_Ntk_t * pNtk = NULL; Wlc_Ntk_t * pNtk = NULL;
char * pBuffer, * pLimit; char * pBuffer, * pLimit;
pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
if ( pBuffer == NULL ) if ( pBuffer == NULL )
return NULL; return NULL;
pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit ); pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit );
...@@ -744,6 +893,7 @@ Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) ...@@ -744,6 +893,7 @@ Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
return pNtk; return pNtk;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment