From ea2d82ab141c5a162f2c2cf0adce74a21d911d8a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Feb 2015 18:09:15 -0800 Subject: Modifications to read SMTLIB file from stdin. --- src/base/main/mainReal.c | 33 +++++++++++++++++++++++++++-- src/base/wlc/wlc.h | 6 ++++++ src/base/wlc/wlcCom.c | 53 +++++++++++++++++++++++++++++++++++++++++++++++ src/base/wlc/wlcNtk.c | 2 +- src/base/wlc/wlcReadSmt.c | 25 +++++++++++++--------- 5 files changed, 106 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 204e7491..04152ae6 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -51,6 +51,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS. #include "base/abc/abc.h" #include "mainInt.h" +#include "base/wlc/wlc.h" ABC_NAMESPACE_IMPL_START @@ -90,7 +91,8 @@ int Abc_RealMain( int argc, char * argv[] ) INTERACTIVE, // interactive mode BATCH, // batch mode, run a command and quit BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode - BATCH_QUIET // as in batch mode, but don't echo the command + BATCH_QUIET, // as in batch mode, but don't echo the command + BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin } fBatch; // added to detect memory leaks @@ -138,7 +140,7 @@ int Abc_RealMain( int argc, char * argv[] ) sprintf( sWriteCmd, "write" ); Extra_UtilGetoptReset(); - while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:hf:F:o:st:T:xb")) != EOF) { + while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:S:hf:F:o:st:T:xb")) != EOF) { switch(c) { case 'c': strcpy( sCommandUsr, globalUtilOptarg ); @@ -155,6 +157,11 @@ int Abc_RealMain( int argc, char * argv[] ) fBatch = BATCH_THEN_INTERACTIVE; break; + case 'S': + strcpy( sCommandUsr, globalUtilOptarg ); + fBatch = BATCH_SMT; + break; + case 'f': sprintf(sCommandUsr, "source %s", globalUtilOptarg); fBatch = BATCH; @@ -223,6 +230,28 @@ int Abc_RealMain( int argc, char * argv[] ) } } + if ( fBatch == BATCH_SMT ) + { + Wlc_Ntk_t * pNtk; + Vec_Str_t * vInput; + // collect stdin + vInput = Wlc_GenerateSmtStdin(); + // parse the input + pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput) ); + Vec_StrFree( vInput ); + // install current network + Wlc_SetNtk( pAbc, pNtk ); + // execute command + fStatus = Cmd_CommandExecute( pAbc, sCommandUsr ); + // generate output + if ( !fStatus ) + Wlc_GenerateSmtStdout( pAbc ); + else + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", sCommandUsr ); + Abc_Stop(); + return 0; + } + if ( Abc_FrameIsBridgeMode() ) { extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit ); 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 /// -- cgit v1.2.3