Merged alanmi/abc into default

9 files changed, 458 insertions, 2 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 6605fc39..b181bc1d 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -48,6 +48,7 @@ static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadStatus  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadGig     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadJson    ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -74,6 +75,7 @@ static int IoCommandWriteTruth  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteSmv    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteJson   ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
 
@@ -114,6 +116,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_status",   IoCommandReadStatus,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "&read_gig",     IoCommandReadGig,      0 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_json",     IoCommandReadJson,     0 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
@@ -141,6 +144,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "&write_truths", IoCommandWriteTruths,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_status",  IoCommandWriteStatus,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_smv",     IoCommandWriteSmv,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_json",    IoCommandWriteJson,    0 );
 }
 
 /**Function*************************************************************
@@ -1334,6 +1338,67 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadJson( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Wec_t * Json_Read( char * pFileName, Abc_Nam_t ** ppStrs );
+    Vec_Wec_t * vObjs;
+    Abc_Nam_t * pStrs;
+    char * pFileName;
+    FILE * pFile;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    vObjs = Json_Read( pFileName, &pStrs );
+    if ( vObjs == NULL )
+        return 0;
+    Abc_FrameSetJsonStrs( pStrs );
+    Abc_FrameSetJsonObjs( vObjs );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_json [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads file in JSON format\n" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -2999,10 +3064,8 @@ usage:
 int IoCommandWriteSmv( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
-    int fUseLuts;
     int c;
 
-    fUseLuts = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
     {
@@ -3034,6 +3097,56 @@ usage:
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .smv)\n" );
     return 1;
 }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteJson( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    extern void Json_Write( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs );
+    char * pFileName;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()) == NULL )
+    {
+        fprintf( pAbc->Out, "No JSON info is available.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the output file name
+    pFileName = argv[globalUtilOptind];
+    // call the corresponding file writer
+    Json_Write( pFileName, Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()), Abc_FrameReadJsonObjs(Abc_FrameReadGlobalFrame()) );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_json [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the network in JSON format\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help message\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .json)\n" );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index ea4ad2c3..16980fbe 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -28,6 +28,7 @@
 
 #include "base/abc/abc.h"
 #include "misc/extra/extra.h"
+#include "misc/util/utilNam.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -57,6 +58,7 @@ typedef enum {
     IO_FILE_EDIF,      
     IO_FILE_EQN,      
     IO_FILE_GML,      
+    IO_FILE_JSON,      
     IO_FILE_LIST,      
     IO_FILE_PLA,      
     IO_FILE_MOPLA,      
@@ -152,6 +154,9 @@ extern Abc_Obj_t *        Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, ch
 extern Abc_Obj_t *        Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
 extern FILE *             Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
 
+/*=== ioJson.c ===========================================================*/
+extern void               Io_ReadJson( char * pFileName );
+extern void               Io_WriteJson( char * pFileName );
 
 
 
diff --git a/src/base/io/ioJson.c b/src/base/io/ioJson.c
new file mode 100644
index 00000000..07c152bc
--- /dev/null
+++ b/src/base/io/ioJson.c
@@ -0,0 +1,270 @@
+/**CFile****************************************************************
+
+  FileName    [ioJson.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read JSON.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioJson.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ioAbc.h"
+#include "misc/vec/vecWec.h"
+#include "misc/util/utilNam.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int         Json_EntryIsName( int Fan )                     { return Abc_LitIsCompl(Fan);                                                       }
+static inline char *      Json_EntryName( Abc_Nam_t * pStrs, int Fan )    { assert(Json_EntryIsName(Fan));  return Abc_NamStr( pStrs, Abc_Lit2Var(Fan) );     }
+static inline Vec_Int_t * Json_EntryNode( Vec_Wec_t * vObjs, int Fan )    { assert(!Json_EntryIsName(Fan)); return Vec_WecEntry( vObjs, Abc_Lit2Var(Fan) );   }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Parsing.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Json_CharIsSpace( char c )   
+{ 
+    return (c == ' ' || c == '\t' || c == '\r' || c == '\n');   
+}
+static inline char * Json_SkipSpaces( char * pCur )
+{
+    while ( Json_CharIsSpace(*pCur) )
+        pCur++;    
+    return pCur;
+}
+static inline char * Json_SkipNonSpaces( char * pCur )
+{
+    while ( !Json_CharIsSpace(*pCur) )
+        pCur++;    
+    return pCur;
+}
+static inline int Json_TokenCompare( char * pCur, char * pNext, char ** ppCur2, char ** ppNext2 )
+{
+//    int i;
+    if ( *pCur == '\"' )
+        pCur++;
+    if ( *(pNext-1) == ',' )
+        pNext--;
+    if ( *(pNext-1) == '\"' )
+        pNext--;
+    *ppCur2 = pCur;
+    *ppNext2 = pNext;
+//    for ( i = 1; i < JSON_NUM_LINES; i++ )
+//        if ( !strncmp( s_Types[i].pName, pCur, pNext - pCur ) )
+//            return i;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes JSON into a file.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Json_Write_rec( FILE * pFile, Abc_Nam_t * pStr, Vec_Wec_t * vObjs, Vec_Int_t * vArray, int Level, int fAddComma, int fSpaces )
+{
+    int i, Entry1, Entry2, fComma;
+    if ( Vec_IntEntry(vArray, 0) ) // array
+    {
+        if ( Vec_IntSize(vArray) == 1 )
+            fprintf( pFile, "[]" );
+        else if ( Vec_IntSize(vArray) == 2 && Json_EntryIsName(Vec_IntEntry(vArray,1)) )
+            fprintf( pFile, "[ \"%s\" ]", Json_EntryName(pStr, Vec_IntEntry(vArray,1)) );
+        else
+        {
+            if ( fSpaces )
+                fprintf( pFile, "%*s", 3*(Level-1), "" );
+            fprintf( pFile, "[\n" );
+            Vec_IntForEachEntryStart( vArray, Entry1, i, 1 )
+            {
+                fComma = (i < Vec_IntSize(vArray) - 1);
+                if ( Json_EntryIsName(Entry1) )
+                    fprintf( pFile, "%*s\"%s\"%s\n", 3*Level, "", Json_EntryName(pStr, Entry1), fComma ? ",":"" );
+                else
+                    Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry1), Level+1, fComma, 1 );
+            }
+            fprintf( pFile, "%*s]", 3*(Level-1), "" );
+        }
+        fprintf( pFile, "%s\n", fAddComma ? ",":"" );
+    }
+    else // list of pairs
+    {
+        if ( fSpaces )
+            fprintf( pFile, "%*s", 3*(Level-1), "" );
+        fprintf( pFile, "{\n" );
+        assert( Vec_IntSize(vArray) % 2 != 0 );
+        Vec_IntForEachEntryDoubleStart( vArray, Entry1, Entry2, i, 1 )
+        {
+            fComma = (i < Vec_IntSize(vArray) - 3);
+            if ( Json_EntryIsName(Entry1) )
+                fprintf( pFile, "%*s\"%s\"", 3*Level, "", Json_EntryName(pStr, Entry1) );
+            else
+                Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry1), Level+1, 0, 1 );
+            fprintf( pFile, " : " );
+            if ( Json_EntryIsName(Entry2) )
+                fprintf( pFile, "\"%s\"%s\n", Json_EntryName(pStr, Entry2), fComma ? ",":"" );
+            else
+                Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry2), Level+1, fComma, 0 );
+        }
+        fprintf( pFile, "%*s}%s\n", 3*(Level-1), "", fAddComma ? ",":"" );
+    }
+}
+void Json_Write( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs )
+{
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    Json_Write_rec( pFile, pStr, vObjs, Vec_WecEntry(vObjs, 0), 1, 0, 1 );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads JSON from a file.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Json_Read( char * pFileName, Abc_Nam_t ** ppStrs )
+{
+    Abc_Nam_t * pStrs; 
+    Vec_Wec_t * vObjs; 
+    Vec_Int_t * vStack, * vTemp;
+    char * pContents, * pCur, * pNext, * pCur2, * pNext2;
+    int nFileSize, RetValue, iToken;
+    FILE * pFile;
+
+    // read the file into the buffer
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    nFileSize = Extra_FileSize( pFileName );
+    pContents = pCur = ABC_ALLOC( char, nFileSize+1 );
+    RetValue = fread( pContents, nFileSize, 1, pFile );
+    pContents[nFileSize] = 0;
+    fclose( pFile );
+
+    // start data-structures
+    vObjs  = Vec_WecAlloc( 1000 );
+    vStack = Vec_IntAlloc( 100 );
+    pStrs  = Abc_NamStart( 1000, 24 );
+    //Json_AddTypes( pStrs );
+
+    // read lines
+    assert( Vec_WecSize(vObjs) == 0 );
+    assert( Vec_IntSize(vStack) == 0 );
+    while ( pCur < pContents + nFileSize )
+    {
+        pCur  = Json_SkipSpaces( pCur );
+        if ( *pCur == '\0' )
+            break;
+        pNext = Json_SkipNonSpaces( pCur );
+        if ( *pCur == '{' || *pCur == '[' )
+        {
+            // add fanin to node on the previous level
+            if ( Vec_IntSize(vStack) > 0 )
+                Vec_IntPush( Vec_WecEntry(vObjs, Vec_IntEntryLast(vStack)), Abc_Var2Lit(Vec_WecSize(vObjs), 0) );            
+            // add node to the stack
+            Vec_IntPush( vStack, Vec_WecSize(vObjs) );
+            vTemp = Vec_WecPushLevel( vObjs );
+            Vec_IntGrow( vTemp, 4 );
+            // remember it as an array
+            Vec_IntPush( vTemp, (int)(*pCur == '[') );
+            pCur++;
+            continue;
+        }
+        if ( *pCur == '}' || *pCur == ']' )
+        {
+            Vec_IntPop( vStack );
+            pCur++;
+            continue;
+        }
+        if ( *pCur == ',' || *pCur == ':' )
+        {
+            pCur++;
+            continue;
+        }
+        iToken = Json_TokenCompare( pCur, pNext, &pCur2, &pNext2 );
+        if ( iToken == 0 )
+            iToken = Abc_NamStrFindOrAddLim( pStrs, pCur2, pNext2, NULL );
+        Vec_IntPush( Vec_WecEntry(vObjs, Vec_IntEntryLast(vStack)), Abc_Var2Lit(iToken, 1) );
+        pCur = pNext;
+    }
+    Vec_IntFree( vStack );
+    ABC_FREE( pContents );
+    *ppStrs = pStrs;
+    return vObjs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Json_ReadTest( char * pFileName )
+{
+    Abc_Nam_t * pStrs;
+    Vec_Wec_t * vObjs;
+    vObjs = Json_Read( pFileName, &pStrs );
+    if ( vObjs == NULL )
+        return;
+    Json_Write( "test.json", pStrs, vObjs );
+    Abc_NamDeref( pStrs );
+    Vec_WecFree( vObjs );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index b3fcc198..47c9701a 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/base/io/io.c \
+    src/base/io/ioJson.c \
     src/base/io/ioReadAiger.c \
     src/base/io/ioReadBaf.c \
     src/base/io/ioReadBblif.c \
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 4fc2f87a..89353fa6 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -122,6 +122,8 @@ extern ABC_DLL Vec_Int_t *     Abc_FrameReadStatusVec( Abc_Frame_t * p );
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadPoEquivs( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Int_t *     Abc_FrameReadPoStatuses( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Int_t *     Abc_FrameReadObjIds( Abc_Frame_t * p );
+extern ABC_DLL Abc_Nam_t *     Abc_FrameReadJsonStrs( Abc_Frame_t * p );  
+extern ABC_DLL Vec_Wec_t *     Abc_FrameReadJsonObjs( Abc_Frame_t * p );
 
 extern ABC_DLL int             Abc_FrameReadCexPiNum( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadCexRegNum( Abc_Frame_t * p );              
@@ -145,6 +147,8 @@ extern ABC_DLL void            Abc_FrameSetManDsd2( void * pMan );
 extern ABC_DLL void            Abc_FrameSetInv( Vec_Int_t * vInv );
 extern ABC_DLL void            Abc_FrameSetCnf( Vec_Int_t * vInv );
 extern ABC_DLL void            Abc_FrameSetStr( Vec_Str_t * vInv );
+extern ABC_DLL void            Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs );
+extern ABC_DLL void            Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs );
 
 extern ABC_DLL int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 16c11288..05cb09c1 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -75,6 +75,8 @@ Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p )        { return s_GlobalFr
 Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p )         { return s_GlobalFrame->vPoEquivs;    }        
 Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p )       { return s_GlobalFrame->vStatuses;    }        
 Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p )           { return s_GlobalFrame->vAbcObjIds;   }        
+Abc_Nam_t * Abc_FrameReadJsonStrs( Abc_Frame_t * p )         { return s_GlobalFrame->pJsonStrs;    }     
+Vec_Wec_t * Abc_FrameReadJsonObjs( Abc_Frame_t * p )         { return s_GlobalFrame->vJsonObjs;    }   
        
 int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;   }               
 int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;  }               
@@ -95,6 +97,8 @@ void        Abc_FrameSetManDsd2( void * pMan )               { if (s_GlobalFrame
 void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
 void        Abc_FrameSetCnf( Vec_Int_t * vCnf )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
 void        Abc_FrameSetStr( Vec_Str_t * vStr )              { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
+void        Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs )        { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
+void        Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs )        { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
 
 int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
 
@@ -225,6 +229,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Vec_IntFreeP( &p->pAbcWlcInv );
     Vec_IntFreeP( &p->pAbcWlcCnf );
     Vec_StrFreeP( &p->pAbcWlcStr );
+    Abc_NamDeref( s_GlobalFrame->pJsonStrs );
+    Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );    
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 4082bab0..ff59b81a 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -134,6 +134,8 @@ struct Abc_Frame_t_
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;
+    Abc_Nam_t *     pJsonStrs;
+    Vec_Wec_t *     vJsonObjs;
 #ifdef ABC_USE_CUDD
     DdManager *     dd;            // temporary BDD package
 #endif
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 7bc7aa39..081be200 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -2,6 +2,7 @@ SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcAbc.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
+    src/base/wlc/wlcJson.c \
     src/base/wlc/wlcNtk.c \
     src/base/wlc/wlcReadSmt.c \
     src/base/wlc/wlcReadVer.c \
diff --git a/src/base/wlc/wlcJson.c b/src/base/wlc/wlcJson.c
new file mode 100644
index 00000000..a65741ce
--- /dev/null
+++ b/src/base/wlc/wlcJson.c
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+
+  FileName    [wlcJson.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Experimental procedures.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcJson.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_JsonTest()
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+