Modifications to read SMTLIB file from stdin.

abclib.dsp

@@ -771,6 +771,10 @@ SOURCE=.\src\base\wlc\wlcReadVer.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wlc\wlcStdin.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wlc\wlcWriteVer.c
 # End Source File
 # End Group

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;
     }

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 

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 ========================================================*/

src/base/wlc/wlcCom.c

@@ -97,56 +97,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    []
 
   Description []
@@ -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" );

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                                ///
 ////////////////////////////////////////////////////////////////////////

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);

src/base/wlc/wlcStdin.c

+/**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
+