From 6b0accd22a7d28282ba35b10572fd188cad2d629 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Feb 2015 20:42:48 -0800 Subject: Modifications to read SMTLIB file from stdin. --- src/base/main/mainReal.c | 17 +-- src/base/wlc/module.make | 1 + src/base/wlc/wlc.h | 5 +- src/base/wlc/wlcCom.c | 52 +--------- src/base/wlc/wlcNtk.c | 46 --------- src/base/wlc/wlcReadSmt.c | 4 +- src/base/wlc/wlcStdin.c | 257 ++++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 265 insertions(+), 117 deletions(-) create mode 100644 src/base/wlc/wlcStdin.c (limited to 'src/base') diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 04152ae6..abe1f453 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -232,22 +232,7 @@ 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 ); + Wlc_StdinProcessSmt( pAbc, sCommandUsr ); Abc_Stop(); return 0; } diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make index 717444d0..6945046a 100644 --- a/src/base/wlc/module.make +++ b/src/base/wlc/module.make @@ -4,4 +4,5 @@ SRC += src/base/wlc/wlcAbs.c \ src/base/wlc/wlcNtk.c \ src/base/wlc/wlcReadSmt.c \ src/base/wlc/wlcReadVer.c \ + src/base/wlc/wlcStdin.c \ src/base/wlc/wlcWriteVer.c diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 4e6c2255..a5e1692d 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -243,8 +243,6 @@ extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs 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 ); @@ -259,10 +257,11 @@ extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); -extern void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign ); /*=== wlcReadSmt.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName ); +/*=== wlcStdin.c ========================================================*/ +extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ); /*=== wlcReadVer.c ========================================================*/ extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName ); /*=== wlcWriteVer.c ========================================================*/ diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 6d437f55..3681d41b 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -95,56 +95,6 @@ void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * 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 ); int c; - while ( (c = fgetc(stdin)) != EOF ) - Vec_StrPush( vInput, (char)c ); - Vec_StrPush( vInput, '\0' ); - return vInput; -} -void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc ) -{ - if ( Abc_FrameReadProbStatus(pAbc) == -1 ) - printf( "undecided\n" ); - else if ( Abc_FrameReadProbStatus(pAbc) == 1 ) - printf( "unsat\n" ); - else if ( Abc_FrameReadProbStatus(pAbc) == 0 ) - { - Vec_Int_t * vAssign = Vec_IntAlloc( 100 ); - Abc_Cex_t * pCex = Abc_FrameReadCex( pAbc ); int i; - if ( pCex == NULL ) - { - printf( "CEX is not found\n" ); - return; - } - for ( i = 0; i < pCex->nPis; i++ ) - Vec_IntPush( vAssign, Abc_InfoHasBit(pCex->pData, i) ); - Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, vAssign ); - Vec_IntFree( vAssign ); - } -} - /**Function******************************************************************** Synopsis [] @@ -433,7 +383,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); //Wlc_AbcUpdateNtk( pAbc, pNtk ); - Wlc_GenerateSmtStdout( pAbc ); + //Wlc_GenerateSmtStdout( pAbc ); return 0; usage: Abc_Print( -2, "usage: %%test [-vh]\n" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 1576ef45..578ee58b 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -497,52 +497,6 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) pNew->vTables = p->vTables; p->vTables = NULL; } -/**Function************************************************************* - - Synopsis [Report results.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign ) -{ - //sat -//((s0 #x12000000070000000000c0000085006b)) -//((s1 #x0e008f00ff0000000000ff0000ed0040)) -//((s2 #x96008f00ff0000000000ff0000ed0040)) - - int i, Name, Start, nBits, k; - Vec_Str_t * vNum = Vec_StrAlloc( 100 ); -// Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) -// printf( "Variable %s : %d %d\n", Abc_NamStr(p->pManName, Name), Start, nBits ); - printf( "sat\n" ); - Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) - { - Vec_StrClear( vNum ); - for ( k = Start; k < Start + nBits; ) - { - int j, Digit = 0; - for ( j = 0; j < 4 && k < Start + nBits; j++, k++ ) - Digit += (1 << j) * Vec_IntEntry(vAssign, k); - assert( Digit >= 0 && Digit < 16 ); - if ( Digit >= 0 && Digit <= 9 ) - Vec_StrPush( vNum, (char)('0' + Digit) ); - else - Vec_StrPush( vNum, (char)('a' + Digit - 10) ); - } - Vec_StrPush( vNum, 'x' ); - Vec_StrPush( vNum, '#' ); - Vec_StrReverseOrder( vNum ); - Vec_StrPush( vNum, '\0' ); - printf( "((%s %s))\n", Abc_NamStr(p->pManName, Name), Vec_StrArray(vNum) ); - } - Vec_StrFree( vNum ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 3a249ec6..a3614dde 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -291,7 +291,9 @@ int Prs_SmtReadLines( Prs_Smt_t * p ) } else if ( Prs_SmtIsWord(p, "assert") ) fAssert = 1; - else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") || Prs_SmtIsWord(p, "check-sat") ) + 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); diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c new file mode 100644 index 00000000..6eea5f08 --- /dev/null +++ b/src/base/wlc/wlcStdin.c @@ -0,0 +1,257 @@ +/**CFile**************************************************************** + + FileName [wlcStdin.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [stdin processing for STM interface.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcStdin.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts a bit-string into a number in a given radix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_ComputeSum( char * pRes, char * pAdd, int nBits, int Radix ) +{ + char Carry = 0; int i; + for ( i = 0; i < nBits; i++ ) + { + char Sum = pRes[i] + pAdd[i] + Carry; + if ( Sum >= Radix ) + { + Sum -= Radix; + Carry = 1; + } + else + Carry = 0; + assert( Sum >= 0 && Sum < Radix ); + pRes[i] = Sum; + } + assert( Carry == 0 ); +} +Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radix ) +{ + Vec_Str_t * vRes = Vec_StrStart( nBits ); + Vec_Str_t * vSum = Vec_StrStart( nBits ); + char * pRes = Vec_StrArray( vRes ); + char * pSum = Vec_StrArray( vSum ); int i; + assert( Radix > 2 && Radix < 36 ); + pSum[0] = 1; + // compute number + for ( i = 0; i < nBits; i++ ) + { + if ( Abc_InfoHasBit(pBits, Start + i) ) + Wlc_ComputeSum( pRes, pSum, nBits, Radix ); + Wlc_ComputeSum( pSum, pSum, nBits, Radix ); + } + Vec_StrFree( vSum ); + // remove zeros + for ( i = nBits - 1; i >= 0; i-- ) + if ( pRes[i] ) + break; + Vec_StrShrink( vRes, i+1 ); + // convert to chars + for ( ; i >= 0; i-- ) + { + if ( pRes[i] < 10 ) + pRes[i] += '0'; + else + pRes[i] += 'a' - 10; + } + Vec_StrReverseOrder( vRes ); + if ( Vec_StrSize(vRes) == 0 ) + Vec_StrPush( vRes, '0' ); + Vec_StrPush( vRes, '\0' ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Report results.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix ) +{ + Vec_Str_t * vNum; + Wlc_Obj_t * pObj; + int i, ObjId, Start, nBits; + assert( pCex->nRegs == 0 ); + // get the node ID + ObjId = Abc_NamStrFind( p->pManName, pName ); + if ( ObjId <= 0 ) + { + printf( "Cannot find \"%s\" among nodes of the network.\n", pName ); + return; + } + // find the PI + Start = 0; + Wlc_NtkForEachPi( p, pObj, i ) + { + nBits = Wlc_ObjRange( pObj ); + if ( Wlc_ObjId(p, pObj) == ObjId ) + break; + Start += nBits; + } + if ( i == Wlc_NtkPiNum(p) ) + { + printf( "Cannot find \"%s\" among primary inputs of the network.\n", pName ); + return; + } + // print value + assert( Radix == 10 || Radix == 16 ); + vNum = Wlc_ConvertToRadix( pCex->pData, Start, nBits, Radix ); + printf( "((%s %s%s))\n", pName, Radix == 16 ? "#x" : "", Vec_StrArray(vNum) ); + Vec_StrFree( vNum ); +} + +/**Function******************************************************************** + + Synopsis [Reads stdin and stops when "(check-sat)" is observed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static inline int Wlc_StdinCollectStop( 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_StdinCollectProblem( char * pDir ) +{ + int c, DirSize = strlen(pDir); + Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); + while ( (c = fgetc(stdin)) != EOF ) + { + Vec_StrPush( vInput, (char)c ); + if ( c == ')' && Wlc_StdinCollectStop(vInput, pDir, DirSize) ) + break; + } + Vec_StrPush( vInput, '\0' ); + return vInput; +} +Vec_Str_t * Wlc_StdinCollectQuery() +{ + int c, Count = 0, fSomeInput = 0; + Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); + while ( (c = fgetc(stdin)) != EOF ) + { + Vec_StrPush( vInput, (char)c ); + if ( c == '(' ) + Count++, fSomeInput = 1; + else if ( c == ')' ) + Count--; + if ( Count == 0 && fSomeInput ) + break; + } + if ( c == EOF ) + Vec_StrFreeP( &vInput ); + else + Vec_StrPush( vInput, '\0' ); + return vInput; +} +int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ) +{ + // collect stdin until (check-sat) + Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" ); + // parse input + Wlc_Ntk_t * 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 + if ( Cmd_CommandExecute(pAbc, pCmd) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCmd ); + return 0; + } + // solver finished + if ( Abc_FrameReadProbStatus(pAbc) == -1 ) + printf( "undecided\n" ); + else if ( Abc_FrameReadProbStatus(pAbc) == 1 ) + printf( "unsat\n" ); + else if ( Abc_FrameReadProbStatus(pAbc) == 0 ) + printf( "sat\n" ); + else assert( 0 ); + // wait for stdin for give directions + while ( (vInput = Wlc_StdinCollectQuery()) != NULL ) + { + char * pName = strtok( Vec_StrArray(vInput), " \n\t\r()" ); + // check directive + if ( strcmp(pName, "get-value") ) + { + Abc_Print( 1, "ABC is expecting \"get-value\" in a follow-up input of the satisfiable problem.\n" ); + Vec_StrFree( vInput ); + return 0; + } + // check status + if ( Abc_FrameReadProbStatus(pAbc) != 0 ) + { + Abc_Print( 1, "ABC received a follow-up input for a problem that is not known to be satisfiable.\n" ); + Vec_StrFree( vInput ); + return 0; + } + // get the variable number + pName = strtok( NULL, "() \n\t\r" ); + // get the counter-example + if ( Abc_FrameReadCex(pAbc) == NULL ) + { + Abc_Print( 1, "ABC does not have a counter-example available to process a \"get-value\" request.\n" ); + Vec_StrFree( vInput ); + return 0; + } + // report value of this variable + Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 ); + Vec_StrFree( vInput ); + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3