diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/wlc.h | 6 | ||||
-rw-r--r-- | src/base/wlc/wlcCom.c | 53 | ||||
-rw-r--r-- | src/base/wlc/wlcNtk.c | 2 | ||||
-rw-r--r-- | src/base/wlc/wlcReadSmt.c | 25 |
4 files changed, 75 insertions, 11 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 5954ec18..f789c03c 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -32,6 +32,7 @@ #include "misc/mem/mem.h" #include "misc/extra/extra.h" #include "misc/util/utilTruth.h" +#include "base/main/mainInt.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -238,6 +239,10 @@ extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs ); /*=== wlcBlast.c ========================================================*/ extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ); +/*=== wlcCom.c ========================================================*/ +extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); +extern Vec_Str_t * Wlc_GenerateSmtStdin(); +extern void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc ); /*=== wlcNtk.c ========================================================*/ extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ); extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg ); @@ -253,6 +258,7 @@ extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbo extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); /*=== wlcReadSmt.c ========================================================*/ +extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); /*=== wlcReadVer.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 88c91c51..84afb394 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -78,6 +78,59 @@ void Wlc_End( Abc_Frame_t * pAbc ) Wlc_AbcFreeNtk( pAbc ); } +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) +{ + Wlc_AbcUpdateNtk( pAbc, pNtk ); +} + + +/**Function******************************************************************** + + Synopsis [Reads stdin and stops when "(check-sat)" is observed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSize ) +{ + char * pStr = Vec_StrArray(vInput) + Vec_StrSize(vInput) - LineSize; + if ( Vec_StrSize(vInput) < LineSize ) + return 0; + return !strncmp( pStr, pLine, LineSize ); +} +Vec_Str_t * Wlc_GenerateSmtStdin() +{ + char * pLine = "(check-sat)"; + int c, LineSize = strlen(pLine); + Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); + while ( (c = fgetc(stdin)) != EOF ) + { + Vec_StrPush( vInput, (char)c ); + if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) ) + break; + } + Vec_StrPush( vInput, '\0' ); + return vInput; +} +void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc ) +{ + printf( "Output produced by SMT solver will be here.\n" ); +} /**Function******************************************************************** diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 8c09467e..48171c35 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -95,7 +95,7 @@ Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ) { Wlc_Ntk_t * p; p = ABC_CALLOC( Wlc_Ntk_t, 1 ); - p->pName = Extra_FileNameGeneric( pName ); + p->pName = pName ? Extra_FileNameGeneric( pName ) : NULL; Vec_IntGrow( &p->vPis, 111 ); Vec_IntGrow( &p->vPos, 111 ); Vec_IntGrow( &p->vCis, 111 ); diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 35d3ed87..ec1ec567 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -99,13 +99,9 @@ static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit ) *ppLimit = pBuffer + nFileSize + 2; return pBuffer; } -static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName ) +static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName, char * pBuffer, char * pLimit ) { Prs_Smt_t * p; - char * pBuffer, * pLimit; - pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); - if ( pBuffer == NULL ) - return NULL; p = ABC_CALLOC( Prs_Smt_t, 1 ); p->pName = pFileName; p->pBuffer = pBuffer; @@ -121,7 +117,6 @@ static inline void Prs_SmtFree( Prs_Smt_t * p ) if ( p->pStrs ) Abc_NamDeref( p->pStrs ); Vec_IntErase( &p->vData ); - ABC_FREE( p->pBuffer ); ABC_FREE( p ); } @@ -655,22 +650,32 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p ) Vec_IntFree( vFanins ); return pNtk; } -Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) +Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ) { Wlc_Ntk_t * pNtk = NULL; - Prs_Smt_t * p = Prs_SmtAlloc( pFileName ); + Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit ); if ( p == NULL ) return NULL; Prs_SmtRemoveComments( p ); Prs_SmtReadLines( p ); //Prs_SmtPrintParser( p ); if ( Prs_SmtErrorPrint(p) ) - { pNtk = Prs_SmtBuild( p ); - } Prs_SmtFree( p ); return pNtk; } +Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ) +{ + Wlc_Ntk_t * pNtk = NULL; + Prs_Smt_t * p = NULL; + char * pBuffer, * pLimit; + pBuffer = Prs_SmtLoadFile( pFileName, &pLimit ); + if ( pBuffer == NULL ) + return NULL; + pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit ); + ABC_FREE( pBuffer ); + return pNtk; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |