Version abc80130_2

8 files changed, 432 insertions, 86 deletions

diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
new file mode 100644
index 00000000..471ea09e
--- /dev/null
+++ b/src/base/main/libSupport.c
@@ -0,0 +1,193 @@
+/**CFile****************************************************************
+
+  FileName    [libSupport.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The main package.]
+
+  Synopsis    [Support for external libaries.]
+
+  Author      [Mike Case]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: libSupport.c,v 1.1 2005/09/06 19:59:51 casem Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include <stdio.h>
+#include <string.h>
+
+#ifndef WIN32
+# include <sys/types.h>
+# include <dirent.h>
+# include <dlfcn.h>
+#endif
+
+#define MAX_LIBS 256
+static void* libHandles[MAX_LIBS+1]; // will be null terminated
+
+typedef void (*lib_init_end_func) (Abc_Frame_t * pAbc);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will find all the ABC library extensions in the current directory and load them all.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void open_libs() {
+    int curr_lib = 0;
+
+#ifdef WIN32
+//    printf("Warning: open_libs WIN32 not implemented.\n");
+#else
+    DIR* dirp;
+    struct dirent* dp;
+    char *env, *init_p, *p;
+    int done;
+
+    env = getenv ("ABC_LIB_PATH");
+    if (env == NULL) {
+//    printf("Warning: ABC_LIB_PATH not defined. Looking into the current directory.\n");
+      init_p = malloc (2*sizeof(char));
+      init_p[0]='.'; init_p[1] = 0;
+    } else {
+      init_p = malloc ((strlen(env)+1)*sizeof(char));
+      strcpy (init_p, env);
+    }
+
+    // Extract directories and read libraries
+    done = 0;
+    p = init_p;
+    while (!done) {
+      char *endp = strchr (p,':');
+      if (endp == NULL) done = 1; // last directory in the list
+      else *endp = 0; // end of string
+
+      dirp = opendir(p);
+      if (dirp == NULL) {
+//      printf("Warning: directory in ABC_LIB_PATH does not exist (%s).\n", p);
+        continue;
+      }
+
+      while ((dp = readdir(dirp)) != NULL) {
+        if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
+            (strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
+
+          // make sure we don't overflow the handle array
+          if (curr_lib >= MAX_LIBS) {
+            printf("Warning: maximum number of ABC libraries (%d) exceeded.  Not loading %s.\n",
+                   MAX_LIBS,
+                   dp->d_name);
+          }
+          
+          // attempt to load it
+          else {
+            char* szPrefixed = malloc((strlen(dp->d_name) + strlen(p) + 2) * 
+                                      sizeof(char));
+            sprintf(szPrefixed, "%s/", p);
+            strcat(szPrefixed, dp->d_name);
+            libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
+            
+            // did the load succeed?
+            if (libHandles[curr_lib] != 0) {
+              printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
+              curr_lib++;
+            } else {
+              printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
+            }
+            
+            free(szPrefixed);
+          }
+        }
+      }
+      closedir(dirp);
+      p = endp+1;
+    }
+
+    free(init_p);
+#endif
+    
+    // null terminate the list of handles
+    libHandles[curr_lib] = 0;    
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will close all open ABC library extensions
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void close_libs() {
+#ifdef WIN32
+    printf("Warning: close_libs WIN32 not implemented.\n");
+#else
+    int i;
+    for (i = 0; libHandles[i] != 0; i++) {
+        if (dlclose(libHandles[i]) != 0) {
+            printf("Warning: failed to close library %d\n", i);
+        }
+        libHandles[i] = 0;
+    }
+#endif
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will get a pointer to a function inside of an open library
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void* get_fnct_ptr(int lib_num, char* sym_name) {
+#ifdef WIN32
+    printf("Warning: get_fnct_ptr WIN32 not implemented.\n");
+    return 0;
+#else
+    return dlsym(libHandles[lib_num], sym_name);
+#endif
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will call an initialization function in every open library.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void call_inits(Abc_Frame_t* pAbc) {
+    int i;
+    lib_init_end_func init_func;
+    for (i = 0; libHandles[i] != 0; i++) {
+        init_func = (lib_init_end_func) get_fnct_ptr(i, "abc_init");
+        if (init_func == 0) {
+            printf("Warning: Failed to initialize library %d.\n", i);
+        } else {
+            (*init_func)(pAbc);
+        }
+    }
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// This will call a shutdown function in every open library.
+////////////////////////////////////////////////////////////////////////////////////////////////////
+void call_ends(Abc_Frame_t* pAbc) {
+    int i;
+    lib_init_end_func end_func;
+    for (i = 0; libHandles[i] != 0; i++) {
+        end_func = (lib_init_end_func) get_fnct_ptr(i, "abc_end");
+        if (end_func == 0) {
+            printf("Warning: Failed to end library %d.\n", i);
+        } else {
+            (*end_func)(pAbc);
+        }
+    }
+}
+
+void Libs_Init(Abc_Frame_t * pAbc)
+{
+    open_libs();
+    call_inits(pAbc);
+}
+
+void Libs_End(Abc_Frame_t * pAbc)
+{
+    call_ends(pAbc);
+
+    // It's good practice to close our libraries at this point, but this can mess up any backtrace printed by Valgind.
+    //    close_libs();
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 0622a3bd..8f43c605 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -20,6 +20,9 @@
 
 #include "mainInt.h"
 
+// this line should be included in the library project
+//#define _LIB
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -27,9 +30,11 @@
 static int TypeCheck( Abc_Frame_t * pAbc, char * s);
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef _LIB
+
 /**Function*************************************************************
 
   Synopsis    [The main() procedure.]
@@ -48,11 +53,14 @@ int main( int argc, char * argv[] )
     char * sCommand, * sOutFile, * sInFile;
     int  fStatus = 0;
     bool fBatch, fInitSource, fInitRead, fFinalWrite;
-    
+
     // added to detect memory leaks:
 #ifdef _DEBUG
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
+    
+//    Npn_Experiment();
+//    Npn_Generate();
 
     // get global frame (singleton pattern)
     // will be initialized on first call
@@ -64,24 +72,24 @@ int main( int argc, char * argv[] )
     fInitRead   = 0;
     fFinalWrite = 0;
     sInFile = sOutFile = NULL;
-    sprintf( sReadCmd,  "read_blif_mv"  );
-    sprintf( sWriteCmd, "write_blif_mv" );
+    sprintf( sReadCmd,  "read"  );
+    sprintf( sWriteCmd, "write" );
     
-    util_getopt_reset();
-    while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
+    Extra_UtilGetoptReset();
+    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
         switch(c) {
             case 'c':
-                strcpy( sCommandUsr, util_optarg );
+                strcpy( sCommandUsr, globalUtilOptarg );
                 fBatch = 1;
                 break;
                 
             case 'f':
-                sprintf(sCommandUsr, "source %s", util_optarg);
+                sprintf(sCommandUsr, "source %s", globalUtilOptarg);
                 fBatch = 1;
                 break;
 
             case 'F':
-                sprintf(sCommandUsr, "source -x %s", util_optarg);
+                sprintf(sCommandUsr, "source -x %s", globalUtilOptarg);
                 fBatch = 1;
                 break;
                 
@@ -90,7 +98,7 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 'o':
-                sOutFile = util_optarg;
+                sOutFile = globalUtilOptarg;
                 fFinalWrite = 1;
                 break;
                 
@@ -99,12 +107,12 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 't':
-                if ( TypeCheck( pAbc, util_optarg ) )
+                if ( TypeCheck( pAbc, globalUtilOptarg ) )
                 {
-                    if ( !strcmp(util_optarg, "none") == 0 )
+                    if ( !strcmp(globalUtilOptarg, "none") == 0 )
                     {
                         fInitRead = 1;
-                        sprintf( sReadCmd, "read_%s", util_optarg );
+                        sprintf( sReadCmd, "read_%s", globalUtilOptarg );
                     }
                 }
                 else {
@@ -114,12 +122,12 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 'T':
-                if ( TypeCheck( pAbc, util_optarg ) )
+                if ( TypeCheck( pAbc, globalUtilOptarg ) )
                 {
-                    if (!strcmp(util_optarg, "none") == 0)
+                    if (!strcmp(globalUtilOptarg, "none") == 0)
                     {
                         fFinalWrite = 1;
-                        sprintf( sWriteCmd, "write_%s", util_optarg);
+                        sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
                     }
                 }
                 else {
@@ -143,14 +151,14 @@ int main( int argc, char * argv[] )
     {
         pAbc->fBatchMode = 1;
 
-        if (argc - util_optind == 0)
+        if (argc - globalUtilOptind == 0)
         {
             sInFile = NULL;
         }
-        else if (argc - util_optind == 1)
+        else if (argc - globalUtilOptind == 1)
         {
             fInitRead = 1;
-            sInFile = argv[util_optind];
+            sInFile = argv[globalUtilOptind];
         }
         else
         {
@@ -209,14 +217,11 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-     
+      
     // if the memory should be freed, quit packages
-    if ( fStatus == -2 ) 
+    if ( fStatus < 0 ) 
     {
-        // perform uninitializations
-        Abc_FrameEnd( pAbc );
-        // stop the framework
-        Abc_FrameDeallocate( pAbc );
+        Abc_Stop();
     }
     return 0;
 
@@ -226,6 +231,58 @@ usage:
     return 1;
 }
 
+#endif
+
+/**Function*************************************************************
+
+  Synopsis    [Initialization procedure for the library project.]
+
+  Description [Note that when Abc_Start() is run in a static library
+  project, it does not load the resource file by default. As a result, 
+  ABC is not set up the same way, as when it is run on a command line. 
+  For example, some error messages while parsing files will not be 
+  produced, and intermediate networks will not be checked for consistancy. 
+  One possibility is to load the resource file after Abc_Start() as follows:
+  Abc_UtilsSource(  Abc_FrameGetGlobalFrame() );]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Start()
+{
+    Abc_Frame_t * pAbc;
+    // added to detect memory leaks:
+#ifdef _DEBUG
+    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
+#endif
+    // start the glocal frame
+    pAbc = Abc_FrameGetGlobalFrame();
+    // source the resource file
+//    Abc_UtilsSource( pAbc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocation procedure for the library project.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_Stop()
+{
+    Abc_Frame_t * pAbc;
+    pAbc = Abc_FrameGetGlobalFrame();
+    // perform uninitializations
+    Abc_FrameEnd( pAbc );
+    // stop the framework
+    Abc_FrameDeallocate( pAbc );
+}
 
 /**Function********************************************************************
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 0d47dec5..4433a8b4 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -21,6 +21,10 @@
 #ifndef __MAIN_H__
 #define __MAIN_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         TYPEDEFS                                 ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,17 +44,10 @@ typedef struct Abc_Frame_t_      Abc_Frame_t;
 // it is used to catch memory leaks on Windows
 #include "leaks.h"       
 
-// standard includes
-#include <stdio.h>
-#include <string.h>
-
-// includes from GLU
-#include "util.h"
-#include "st.h"
-
 // data structure packages
 #include "extra.h"
 #include "vec.h"
+#include "st.h"
 
 // core packages
 #include "abc.h"
@@ -66,20 +63,25 @@ typedef struct Abc_Frame_t_      Abc_Frame_t;
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== mvFrame.c ===========================================================*/
-extern Abc_Ntk_t *     Abc_FrameReadNet( Abc_Frame_t * p );
+/*=== main.c ===========================================================*/
+extern void            Abc_Start();
+extern void            Abc_Stop();
+
+/*=== mainFrame.c ===========================================================*/
+extern Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
 extern FILE *          Abc_FrameReadOut( Abc_Frame_t * p );
 extern FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
 extern bool            Abc_FrameReadMode( Abc_Frame_t * p );
 extern bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
 extern void            Abc_FrameRestart( Abc_Frame_t * p );
+extern bool            Abc_FrameShowProgress( Abc_Frame_t * p );
 
 extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
@@ -90,11 +92,12 @@ extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
 extern Abc_Frame_t *   Abc_FrameGetGlobalFrame();
 
-extern Abc_Ntk_t *     Abc_FrameReadNtkStore();                  
-extern int             Abc_FrameReadNtkStoreSize();              
+extern Vec_Ptr_t *     Abc_FrameReadStore();                  
+extern int             Abc_FrameReadStoreSize();              
 extern void *          Abc_FrameReadLibLut();                    
 extern void *          Abc_FrameReadLibGen();                    
 extern void *          Abc_FrameReadLibSuper();                  
+extern void *          Abc_FrameReadLibVer();                  
 extern void *          Abc_FrameReadManDd();                     
 extern void *          Abc_FrameReadManDec();                    
 extern char *          Abc_FrameReadFlag( char * pFlag ); 
@@ -105,10 +108,15 @@ extern void            Abc_FrameSetNtkStoreSize( int nStored );
 extern void            Abc_FrameSetLibLut( void * pLib );        
 extern void            Abc_FrameSetLibGen( void * pLib );        
 extern void            Abc_FrameSetLibSuper( void * pLib );      
+extern void            Abc_FrameSetLibVer( void * pLib );      
 extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 77c9f579..eae8b7a6 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -29,7 +29,7 @@
 static Abc_Frame_t * s_GlobalFrame = NULL;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -43,20 +43,20 @@ static Abc_Frame_t * s_GlobalFrame = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNtkStore()                  { return s_GlobalFrame->pStored;      } 
-int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nStored;      }
+Vec_Ptr_t * Abc_FrameReadStore()                     { return s_GlobalFrame->vStore;       } 
+int         Abc_FrameReadStoreSize()                 { return Vec_PtrSize(s_GlobalFrame->vStore); }
 void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
 void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
 void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
-void *      Abc_FrameReadManDd()                     { return s_GlobalFrame->dd;           } 
-void *      Abc_FrameReadManDec()                    { return s_GlobalFrame->pManDec;      } 
+void *      Abc_FrameReadLibVer()                    { return s_GlobalFrame->pLibVer;      } 
+void *      Abc_FrameReadManDd()                     { if ( s_GlobalFrame->dd == NULL )      s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );  return s_GlobalFrame->dd;      } 
+void *      Abc_FrameReadManDec()                    { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
 
-void        Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored  = pNtk;     } 
-void        Abc_FrameSetNtkStoreSize( int nStored )  { s_GlobalFrame->nStored  = nStored;  }
 void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
 void        Abc_FrameSetLibSuper( void * pLib )      { s_GlobalFrame->pLibSuper = pLib;    } 
+void        Abc_FrameSetLibVer( void * pLib )        { s_GlobalFrame->pLibVer   = pLib;    } 
 void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );  } 
 
 /**Function*************************************************************
@@ -97,7 +97,8 @@ bool Abc_FrameIsFlagEnabled( char * pFlag )
 Abc_Frame_t * Abc_FrameAllocate()
 {
     Abc_Frame_t * p;
-
+    extern void define_cube_size( int n );
+    extern void set_espresso_flags();
     // allocate and clean
     p = ALLOC( Abc_Frame_t, 1 );
     memset( p, 0, sizeof(Abc_Frame_t) );
@@ -110,9 +111,13 @@ Abc_Frame_t * Abc_FrameAllocate()
     // set the starting step
     p->nSteps = 1;
     p->fBatchMode = 0;
+    // networks to be used by choice
+    p->vStore = Vec_PtrAlloc( 16 );
     // initialize decomposition manager
-    p->pManDec = Dec_ManStart();
-    p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    define_cube_size(20);
+    set_espresso_flags();
+    // initialize the trace manager
+//    Abc_HManStart();
     return p;
 }
 
@@ -130,11 +135,20 @@ Abc_Frame_t * Abc_FrameAllocate()
 ***********************************************************************/
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
-    Dec_ManStop( p->pManDec );
-    Extra_StopManager( p->dd );
+    extern void Rwt_ManGlobalStop();
+    extern void undefine_cube_size();
+//    extern void Ivy_TruthManStop();
+//    Abc_HManStop();
+    undefine_cube_size();
+    Rwt_ManGlobalStop();
+//    Ivy_TruthManStop();
+    if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL );
+    if ( p->pManDec ) Dec_ManStop( p->pManDec );
+    if ( p->dd )      Extra_StopManager( p->dd );
+    if ( p->vStore )  Vec_PtrFree( p->vStore );
     Abc_FrameDeleteAllNetworks( p );
     free( p );
-    p = NULL;
+    s_GlobalFrame = NULL;
 }
 
 /**Function*************************************************************
@@ -152,6 +166,22 @@ void Abc_FrameRestart( Abc_Frame_t * p )
 {
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FrameShowProgress( Abc_Frame_t * p )
+{
+    return Abc_FrameIsFlagEnabled( "progressbar" );
+}
+
 
 /**Function*************************************************************
 
@@ -164,7 +194,7 @@ void Abc_FrameRestart( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p )
+Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p )
 {
     return p->pNtkCur;
 }
@@ -397,7 +427,7 @@ void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
     Abc_Ntk_t * pNtk;
     for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
         if ( Abc_NtkHasMapping(pNtk) )
-            Abc_NtkUnmap( pNtk );
+            Abc_NtkMapToSop( pNtk );
 }
 
 /**Function*************************************************************
@@ -423,7 +453,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
         Abc_NtkDelete( pNtk );
     // set the current network empty
     p->pNtkCur = NULL;
-    fprintf( p->Out, "All networks have been deleted.\n" );
+//    fprintf( p->Out, "All networks have been deleted.\n" );
 }
 
 /**Function*************************************************************
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index 13710dcb..03953e5b 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: mainInit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: mainInit.c,v 1.3 2005/09/14 22:53:37 casem Exp $]
 
 ***********************************************************************/
 
@@ -38,9 +38,11 @@ extern void Mio_Init( Abc_Frame_t * pAbc );
 extern void Mio_End ( Abc_Frame_t * pAbc );
 extern void Super_Init( Abc_Frame_t * pAbc );
 extern void Super_End ( Abc_Frame_t * pAbc );
+extern void Libs_Init(Abc_Frame_t * pAbc);
+extern void Libs_End(Abc_Frame_t * pAbc);
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -63,6 +65,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Map_Init( pAbc );
     Mio_Init( pAbc );
     Super_Init( pAbc );
+    Libs_Init( pAbc );
 }
 
 
@@ -86,6 +89,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Map_End( pAbc );
     Mio_End( pAbc );
     Super_End( pAbc );
+    Libs_End( pAbc );
 }
 
 
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 6b929854..09ad96f3 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __Abc_INT_H__
-#define __Abc_INT_H__
+#ifndef __MAIN_INT_H__
+#define __MAIN_INT_H__
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
@@ -63,8 +63,7 @@ struct Abc_Frame_t_
     int             TimeCommand; // the runtime of the last command
     int             TimeTotal;   // the total runtime of all commands
     // temporary storage for structural choices
-    Abc_Ntk_t *     pStored;     // the stored networks
-    int             nStored;     // the number of stored networks
+    Vec_Ptr_t *     vStore;      // networks to be used by choice
     // decomposition package
     void *          pManDec;     // decomposition manager
     DdManager *     dd;          // temporary BDD package
@@ -72,6 +71,7 @@ struct Abc_Frame_t_
     void *          pLibLut;     // the current LUT library
     void *          pLibGen;     // the current genlib
     void *          pLibSuper;   // the current supergate library
+    void *          pLibVer;     // the current Verilog library
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -79,12 +79,12 @@ struct Abc_Frame_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== mvMain.c ===========================================================*/
@@ -102,8 +102,8 @@ extern void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
 extern void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
 extern void            Abc_UtilsSource( Abc_Frame_t * pAbc );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index 9d1201fa..58cc33ec 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -20,13 +20,17 @@
 
 #include "mainInt.h"
 
+#ifndef _WIN32
+#include "readline/readline.h"
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 static char * DateReadFromDateString(char * datestr);
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -62,9 +66,18 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc )
 {
     static char Buffer[1000], Prompt[1000];
     sprintf( Prompt, "abc %02d> ", pAbc->nSteps );
+#ifdef _WIN32
     fprintf( pAbc->Out, "%s", Prompt );
     fgets( Buffer, 999, stdin );
     return Buffer;
+#else
+    static char* line = NULL;
+    if (line != NULL) free(line);
+    line = readline(Prompt);  
+    if (line == NULL){ printf("***EOF***\n"); exit(0); }
+    add_history(line);
+    return line;
+#endif
 }
 
 /**Function*************************************************************
@@ -134,32 +147,72 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
             printf( "Loaded \"abc.rc\" from the grandparent directory.\n" );
     }
 #else
+
+#if 0
     {
-    char * sPath1, * sPath2;
+        char * sPath1, * sPath2;
 
-     // If .rc is present in both the home and current directories, then read
-     // it from the home directory.  Otherwise, read it from wherever it's located.
-    sPath1 = util_file_search(".rc", "~/", "r");
-    sPath2 = util_file_search(".rc", ".",  "r");
+         // If .rc is present in both the home and current directories, then read
+         // it from the home directory.  Otherwise, read it from wherever it's located.
+        sPath1 = Extra_UtilFileSearch(".rc", "~/", "r");
+        sPath2 = Extra_UtilFileSearch(".rc", ".",  "r");
   
-    if ( sPath1 && sPath2 ) {
-        /* ~/.rc == .rc : Source the file only once */
-        (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
-    }
-    else {
-        if (sPath1) {
+        if ( sPath1 && sPath2 ) {
+            /* ~/.rc == .rc : Source the file only once */
             (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
         }
-        if (sPath2) {
-            (void) Cmd_CommandExecute(pAbc, "source -s .rc");
+        else {
+            if (sPath1) {
+                (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
+            }
+            if (sPath2) {
+                (void) Cmd_CommandExecute(pAbc, "source -s .rc");
+            }
         }
-    }
-    if ( sPath1 ) FREE(sPath1);
-    if ( sPath2 ) FREE(sPath2);
+        if ( sPath1 ) FREE(sPath1);
+        if ( sPath2 ) FREE(sPath2);
     
-    /* execute the abc script which can be open with the "open_path" */
-    Cmd_CommandExecute( pAbc, "source -s abc.rc" );
+        /* execute the abc script which can be open with the "open_path" */
+        Cmd_CommandExecute( pAbc, "source -s abc.rc" );
     }
+#endif
+
+    {
+        char * sPath1, * sPath2;
+        char * home;
+
+         // If .rc is present in both the home and current directories, then read
+         // it from the home directory.  Otherwise, read it from wherever it's located.
+        home = getenv("HOME");
+        if (home){
+            char * sPath3 = ALLOC(char, strlen(home) + 2);
+            (void) sprintf(sPath3, "%s/", home);
+            sPath1 = Extra_UtilFileSearch(".abc.rc", sPath3, "r");
+            FREE(sPath3);
+        }else
+            sPath1 = NULL;
+
+        sPath2 = Extra_UtilFileSearch(".abc.rc", ".",  "r");
+
+        if ( sPath1 && sPath2 ) {
+            /* ~/.rc == .rc : Source the file only once */
+            (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc");
+        }
+        else {
+            if (sPath1) {
+                (void) Cmd_CommandExecute(pAbc, "source -s ~/.abc.rc");
+            }
+            if (sPath2) {
+                (void) Cmd_CommandExecute(pAbc, "source -s .abc.rc");
+            }
+        }
+        if ( sPath1 ) FREE(sPath1);
+        if ( sPath2 ) FREE(sPath2);
+
+        /* execute the abc script which can be open with the "open_path" */
+        Cmd_CommandExecute( pAbc, "source -s abc.rc" );
+    }
+
 #endif //WIN32
     {
         // reset command history
diff --git a/src/base/main/module.make b/src/base/main/module.make
index 59e1315e..367f89f6 100644
--- a/src/base/main/module.make
+++ b/src/base/main/module.make
@@ -1,4 +1,5 @@
 SRC +=  src/base/main/main.c \
     src/base/main/mainFrame.c \
     src/base/main/mainInit.c \
+    src/base/main/libSupport.c \
     src/base/main/mainUtils.c