Version abc80130

8 files changed, 86 insertions, 432 deletions

diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
deleted file mode 100644
index 471ea09e..00000000
--- a/src/base/main/libSupport.c
+++ /dev/null
@@ -1,193 +0,0 @@
-/**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 8f43c605..0622a3bd 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -20,9 +20,6 @@
 
 #include "mainInt.h"
 
-// this line should be included in the library project
-//#define _LIB
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -30,11 +27,9 @@
 static int TypeCheck( Abc_Frame_t * pAbc, char * s);
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifndef _LIB
-
 /**Function*************************************************************
 
   Synopsis    [The main() procedure.]
@@ -53,14 +48,11 @@ 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
@@ -72,24 +64,24 @@ int main( int argc, char * argv[] )
     fInitRead   = 0;
     fFinalWrite = 0;
     sInFile = sOutFile = NULL;
-    sprintf( sReadCmd,  "read"  );
-    sprintf( sWriteCmd, "write" );
+    sprintf( sReadCmd,  "read_blif_mv"  );
+    sprintf( sWriteCmd, "write_blif_mv" );
     
-    Extra_UtilGetoptReset();
-    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
+    util_getopt_reset();
+    while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
         switch(c) {
             case 'c':
-                strcpy( sCommandUsr, globalUtilOptarg );
+                strcpy( sCommandUsr, util_optarg );
                 fBatch = 1;
                 break;
                 
             case 'f':
-                sprintf(sCommandUsr, "source %s", globalUtilOptarg);
+                sprintf(sCommandUsr, "source %s", util_optarg);
                 fBatch = 1;
                 break;
 
             case 'F':
-                sprintf(sCommandUsr, "source -x %s", globalUtilOptarg);
+                sprintf(sCommandUsr, "source -x %s", util_optarg);
                 fBatch = 1;
                 break;
                 
@@ -98,7 +90,7 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 'o':
-                sOutFile = globalUtilOptarg;
+                sOutFile = util_optarg;
                 fFinalWrite = 1;
                 break;
                 
@@ -107,12 +99,12 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 't':
-                if ( TypeCheck( pAbc, globalUtilOptarg ) )
+                if ( TypeCheck( pAbc, util_optarg ) )
                 {
-                    if ( !strcmp(globalUtilOptarg, "none") == 0 )
+                    if ( !strcmp(util_optarg, "none") == 0 )
                     {
                         fInitRead = 1;
-                        sprintf( sReadCmd, "read_%s", globalUtilOptarg );
+                        sprintf( sReadCmd, "read_%s", util_optarg );
                     }
                 }
                 else {
@@ -122,12 +114,12 @@ int main( int argc, char * argv[] )
                 break;
                 
             case 'T':
-                if ( TypeCheck( pAbc, globalUtilOptarg ) )
+                if ( TypeCheck( pAbc, util_optarg ) )
                 {
-                    if (!strcmp(globalUtilOptarg, "none") == 0)
+                    if (!strcmp(util_optarg, "none") == 0)
                     {
                         fFinalWrite = 1;
-                        sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
+                        sprintf( sWriteCmd, "write_%s", util_optarg);
                     }
                 }
                 else {
@@ -151,14 +143,14 @@ int main( int argc, char * argv[] )
     {
         pAbc->fBatchMode = 1;
 
-        if (argc - globalUtilOptind == 0)
+        if (argc - util_optind == 0)
         {
             sInFile = NULL;
         }
-        else if (argc - globalUtilOptind == 1)
+        else if (argc - util_optind == 1)
         {
             fInitRead = 1;
-            sInFile = argv[globalUtilOptind];
+            sInFile = argv[util_optind];
         }
         else
         {
@@ -217,11 +209,14 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-      
+     
     // if the memory should be freed, quit packages
-    if ( fStatus < 0 ) 
+    if ( fStatus == -2 ) 
     {
-        Abc_Stop();
+        // perform uninitializations
+        Abc_FrameEnd( pAbc );
+        // stop the framework
+        Abc_FrameDeallocate( pAbc );
     }
     return 0;
 
@@ -231,58 +226,6 @@ 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 4433a8b4..0d47dec5 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -21,10 +21,6 @@
 #ifndef __MAIN_H__
 #define __MAIN_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                         TYPEDEFS                                 ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,10 +40,17 @@ 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"
@@ -63,25 +66,20 @@ typedef struct Abc_Frame_t_      Abc_Frame_t;
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== main.c ===========================================================*/
-extern void            Abc_Start();
-extern void            Abc_Stop();
-
-/*=== mainFrame.c ===========================================================*/
-extern Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
+/*=== mvFrame.c ===========================================================*/
+extern Abc_Ntk_t *     Abc_FrameReadNet( 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 );
@@ -92,12 +90,11 @@ extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
 extern Abc_Frame_t *   Abc_FrameGetGlobalFrame();
 
-extern Vec_Ptr_t *     Abc_FrameReadStore();                  
-extern int             Abc_FrameReadStoreSize();              
+extern Abc_Ntk_t *     Abc_FrameReadNtkStore();                  
+extern int             Abc_FrameReadNtkStoreSize();              
 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 ); 
@@ -108,15 +105,10 @@ 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 eae8b7a6..77c9f579 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -43,20 +43,20 @@ static Abc_Frame_t * s_GlobalFrame = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_FrameReadStore()                     { return s_GlobalFrame->vStore;       } 
-int         Abc_FrameReadStoreSize()                 { return Vec_PtrSize(s_GlobalFrame->vStore); }
+Abc_Ntk_t * Abc_FrameReadNtkStore()                  { return s_GlobalFrame->pStored;      } 
+int         Abc_FrameReadNtkStoreSize()              { return s_GlobalFrame->nStored;      }
 void *      Abc_FrameReadLibLut()                    { return s_GlobalFrame->pLibLut;      } 
 void *      Abc_FrameReadLibGen()                    { return s_GlobalFrame->pLibGen;      } 
 void *      Abc_FrameReadLibSuper()                  { return s_GlobalFrame->pLibSuper;    } 
-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; } 
+void *      Abc_FrameReadManDd()                     { return s_GlobalFrame->dd;           } 
+void *      Abc_FrameReadManDec()                    { 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,8 +97,7 @@ 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) );
@@ -111,13 +110,9 @@ 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
-    define_cube_size(20);
-    set_espresso_flags();
-    // initialize the trace manager
-//    Abc_HManStart();
+    p->pManDec = Dec_ManStart();
+    p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     return p;
 }
 
@@ -135,20 +130,11 @@ Abc_Frame_t * Abc_FrameAllocate()
 ***********************************************************************/
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
-    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 );
+    Dec_ManStop( p->pManDec );
+    Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
     free( p );
-    s_GlobalFrame = NULL;
+    p = NULL;
 }
 
 /**Function*************************************************************
@@ -166,22 +152,6 @@ void Abc_FrameRestart( Abc_Frame_t * p )
 {
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-bool Abc_FrameShowProgress( Abc_Frame_t * p )
-{
-    return Abc_FrameIsFlagEnabled( "progressbar" );
-}
-
 
 /**Function*************************************************************
 
@@ -194,7 +164,7 @@ bool Abc_FrameShowProgress( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p )
+Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p )
 {
     return p->pNtkCur;
 }
@@ -427,7 +397,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_NtkMapToSop( pNtk );
+            Abc_NtkUnmap( pNtk );
 }
 
 /**Function*************************************************************
@@ -453,7 +423,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 03953e5b..13710dcb 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.3 2005/09/14 22:53:37 casem Exp $]
+  Revision    [$Id: mainInit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -38,11 +38,9 @@ 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -65,7 +63,6 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Map_Init( pAbc );
     Mio_Init( pAbc );
     Super_Init( pAbc );
-    Libs_Init( pAbc );
 }
 
 
@@ -89,7 +86,6 @@ 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 09ad96f3..6b929854 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __MAIN_INT_H__
-#define __MAIN_INT_H__
+#ifndef __Abc_INT_H__
+#define __Abc_INT_H__
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
@@ -63,7 +63,8 @@ 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
-    Vec_Ptr_t *     vStore;      // networks to be used by choice
+    Abc_Ntk_t *     pStored;     // the stored networks
+    int             nStored;     // the number of stored networks
     // decomposition package
     void *          pManDec;     // decomposition manager
     DdManager *     dd;          // temporary BDD package
@@ -71,7 +72,6 @@ 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 DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== 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 58cc33ec..9d1201fa 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -20,17 +20,13 @@
 
 #include "mainInt.h"
 
-#ifndef _WIN32
-#include "readline/readline.h"
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 static char * DateReadFromDateString(char * datestr);
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -66,18 +62,9 @@ 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*************************************************************
@@ -147,72 +134,32 @@ 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 = Extra_UtilFileSearch(".rc", "~/", "r");
-        sPath2 = Extra_UtilFileSearch(".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 = util_file_search(".rc", "~/", "r");
+    sPath2 = util_file_search(".rc", ".",  "r");
   
-        if ( sPath1 && sPath2 ) {
-            /* ~/.rc == .rc : Source the file only once */
+    if ( sPath1 && sPath2 ) {
+        /* ~/.rc == .rc : Source the file only once */
+        (void) Cmd_CommandExecute(pAbc, "source -s ~/.rc");
+    }
+    else {
+        if (sPath1) {
             (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 (sPath2) {
+            (void) Cmd_CommandExecute(pAbc, "source -s .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
-
-    {
-        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" );
+    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 367f89f6..59e1315e 100644
--- a/src/base/main/module.make
+++ b/src/base/main/module.make
@@ -1,5 +1,4 @@
 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