| /**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 ); |
| if ( i < nBits - 1 ) |
| 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; |
| int i, NameId, Name, Start = -1, nBits = -1; |
| assert( pCex->nRegs == 0 ); |
| // get the name ID |
| NameId = Abc_NamStrFind( p->pManName, pName ); |
| if ( NameId <= 0 ) |
| { |
| printf( "Cannot find \"%s\" among nodes of the network.\n", pName ); |
| return; |
| } |
| // get the primary input |
| Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i ) |
| if ( Name == NameId ) |
| break; |
| // find the PI |
| if ( i == Vec_IntSize(&p->vValues) ) |
| { |
| printf( "Cannot find \"%s\" among primary inputs of the network.\n", pName ); |
| return; |
| } |
| // print value |
| assert( Radix == 2 || Radix == 10 || Radix == 16 ); |
| vNum = Wlc_ConvertToRadix( pCex->pData, Start, nBits, Radix ); |
| printf( "((%s %s%s))\n", pName, Radix == 16 ? "#x" : (Radix == 2 ? "#b" : ""), 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( "top", Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput), 0, 0 ); |
| 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 ); |
| fflush( stdout ); |
| // 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_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 ); |
| Vec_StrFree( vInput ); |
| fflush( stdout ); |
| } |
| return 1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
