initial commit of public abc

10 files changed, 350 insertions, 133 deletions

diff --git a/src/base/main/libSupport.c b/src/base/main/libSupport.c
index 6bffc2bd..3c0b20c7 100644
--- a/src/base/main/libSupport.c
+++ b/src/base/main/libSupport.c
@@ -20,8 +20,12 @@
 
 #include <stdio.h>
 #include <string.h>
+
+#include "abc.h"
 #include "mainInt.h"
-#include "abc_global.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 #ifndef WIN32
 # include <sys/types.h>
@@ -29,6 +33,14 @@
 # include <dlfcn.h>
 #endif
 
+// fix by Paddy O'Brien  on Sep 22, 2009
+#ifdef __CYGWIN__
+#ifndef RTLD_LOCAL
+#define RTLD_LOCAL 0
+#endif
+#endif 
+
+
 #define MAX_LIBS 256
 static void* libHandles[MAX_LIBS+1]; // will be null terminated
 
@@ -192,3 +204,5 @@ void Libs_End(Abc_Frame_t * pAbc)
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/main.c b/src/base/main/main.c
index ebe7c755..42ea255d 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -17,9 +17,17 @@
   Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
- 
+
+#include "abc.h"
 #include "mainInt.h"
 
+#ifdef ABC_PYTHON_EMBED
+#include <Python.h>
+
+#endif /* ABC_PYTHON_EMBED */
+
+ABC_NAMESPACE_IMPL_START
+
 // this line should be included in the library project
 //#define ABC_LIB
 
@@ -29,7 +37,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static int TypeCheck( Abc_Frame_t * pAbc, char * s);
+static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,23 +56,20 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s);
   SeeAlso     []
 
 ***********************************************************************/
-#if defined(ABC_USE_BINARY)
-int main_( int argc, char * argv[] )
-#else
-int main( int argc, char * argv[] )
-#endif
+int Abc_RealMain( int argc, char * argv[] )
 {
     Abc_Frame_t * pAbc;
     char sCommandUsr[500], sCommandTmp[100], sReadCmd[20], sWriteCmd[20], c;
-    char * sCommand, * sOutFile, * sInFile;
+    const char * sOutFile, * sInFile;
+    char * sCommand;
     int  fStatus = 0;
-    bool fBatch, fInitSource, fInitRead, fFinalWrite;
+    int fBatch, fInitSource, fInitRead, fFinalWrite;
 
     // added to detect memory leaks:
 #if defined(_DEBUG) && defined(_MSC_VER) 
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-    
+     
 //    Npn_Experiment();
 //    Npn_Generate();
 
@@ -72,6 +77,23 @@ int main( int argc, char * argv[] )
     // will be initialized on first call
     pAbc = Abc_FrameGetGlobalFrame();
 
+#ifdef ABC_PYTHON_EMBED
+    {
+        PyObject* pName;
+        PyObject* pModule;
+        void init_pyabc(void);
+
+        Py_SetProgramName(argv[0]);
+        Py_NoSiteFlag = 1;
+        Py_Initialize();
+
+        init_pyabc();
+
+        pModule = PyImport_ImportModule("pyabc");
+        Py_DECREF(pModule);
+    }
+#endif /* ABC_PYTHON_EMBED */
+
     // default options
     fBatch      = 0;
     fInitSource = 1;
@@ -223,9 +245,15 @@ int main( int argc, char * argv[] )
                 break;
         }
     } 
-     
+
+#ifdef ABC_PYTHON_EMBED
+    {
+        Py_Finalize();
+    }
+#endif /* ABC_PYTHON_EMBED */
+
     // if the memory should be freed, quit packages
-    if ( fStatus < 0 ) 
+//    if ( fStatus < 0 ) 
     {
         Abc_Stop(); 
     }    
@@ -239,57 +267,6 @@ usage:
 
 #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:
-#if defined(_DEBUG) && defined(_MSC_VER) 
-    _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********************************************************************
 
   Synopsis    [Returns 1 if s is a file type recognized, else returns 0.]
@@ -300,7 +277,7 @@ void Abc_Stop()
   SideEffects []
 
 ******************************************************************************/
-static int TypeCheck( Abc_Frame_t * pAbc, char * s )
+static int TypeCheck( Abc_Frame_t * pAbc, const char * s )
 {
     if (strcmp(s, "blif") == 0)
         return 1;
@@ -324,3 +301,13 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
+#if defined(ABC_USE_BINARY)
+int main_( int argc, char * argv[] )
+#else
+int main( int argc, char * argv[] )
+#endif
+{
+  return ABC_NAMESPACE_PREFIX Abc_RealMain(argc, argv);
+}
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 0c5aeb3e..f3e03b47 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -21,12 +21,6 @@
 #ifndef __MAIN_H__
 #define __MAIN_H__
 
-////////////////////////////////////////////////////////////////////////
-///                         TYPEDEFS                                 ///
-////////////////////////////////////////////////////////////////////////
-
-// the framework containing all data
-typedef struct Abc_Frame_t_      Abc_Frame_t;   
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
@@ -39,16 +33,24 @@ typedef struct Abc_Frame_t_      Abc_Frame_t;
 
 // core packages
 #include "abc.h"
+
+ABC_NAMESPACE_HEADER_START
+// the framework containing all data
+typedef struct Abc_Frame_t_      Abc_Frame_t;
+ABC_NAMESPACE_HEADER_END
+
 #include "cmd.h"
 #include "ioAbc.h"
 
+ABC_NAMESPACE_HEADER_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+////////////////////////////////////////////////////////////////////////
+///                         TYPEDEFS                                 ///
+////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
 ///                       GLOBAL VARIABLES                           ///
@@ -74,10 +76,11 @@ extern ABC_DLL void            Abc_Stop();
 extern ABC_DLL Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
 extern ABC_DLL FILE *          Abc_FrameReadOut( Abc_Frame_t * p );
 extern ABC_DLL FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
-extern ABC_DLL bool            Abc_FrameReadMode( Abc_Frame_t * p );
-extern ABC_DLL bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
+extern ABC_DLL int             Abc_FrameReadMode( Abc_Frame_t * p );
+extern ABC_DLL int             Abc_FrameSetMode( Abc_Frame_t * p, int fNameMode );
 extern ABC_DLL void            Abc_FrameRestart( Abc_Frame_t * p );
-extern ABC_DLL bool            Abc_FrameShowProgress( Abc_Frame_t * p );
+extern ABC_DLL int             Abc_FrameShowProgress( Abc_Frame_t * p );
+extern ABC_DLL void            Abc_FrameClearVerifStatus( Abc_Frame_t * p );
 
 extern ABC_DLL void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern ABC_DLL void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
@@ -99,7 +102,16 @@ extern ABC_DLL void *          Abc_FrameReadLibVer();
 extern ABC_DLL void *          Abc_FrameReadManDd();                     
 extern ABC_DLL void *          Abc_FrameReadManDec();                    
 extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
-extern ABC_DLL bool            Abc_FrameIsFlagEnabled( char * pFlag );
+extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
+
+extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
+extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              
+extern ABC_DLL void *          Abc_FrameReadCex( Abc_Frame_t * p );              
+
+extern ABC_DLL int             Abc_FrameReadCexPiNum( Abc_Frame_t * p );              
+extern ABC_DLL int             Abc_FrameReadCexRegNum( Abc_Frame_t * p );              
+extern ABC_DLL int             Abc_FrameReadCexPo( Abc_Frame_t * p );              
+extern ABC_DLL int             Abc_FrameReadCexFrame( Abc_Frame_t * p );              
 
 extern ABC_DLL void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
 extern ABC_DLL void            Abc_FrameSetNtkStoreSize( int nStored );  
@@ -110,9 +122,11 @@ extern ABC_DLL void            Abc_FrameSetLibSuper( void * pLib );
 extern ABC_DLL void            Abc_FrameSetLibVer( void * pLib );      
 extern ABC_DLL void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 81070bd8..6a2fe5b3 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -18,19 +18,20 @@
 
 ***********************************************************************/
 
-#include "mainInt.h"
 #include "abc.h"
+#include "mainInt.h"
 #include "dec.h"
 
+
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Frame_t * s_GlobalFrame = NULL;
 
-extern void * Aig_ManDupSimple( void * p );
-extern void Aig_ManStop( void * pAig );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,23 +47,32 @@ extern void Aig_ManStop( void * pAig );
   SeeAlso     []
 
 ***********************************************************************/
-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_FrameReadLibGen2()                   { return s_GlobalFrame->pLibGen2;     } 
-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; } 
-char *      Abc_FrameReadFlag( char * pFlag )        { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );  } 
-
-void        Abc_FrameSetLibLut( void * pLib )        { s_GlobalFrame->pLibLut   = pLib;    } 
-void        Abc_FrameSetLibGen( void * pLib )        { s_GlobalFrame->pLibGen   = pLib;    } 
-void        Abc_FrameSetLibGen2( void * pLib )       { s_GlobalFrame->pLibGen2  = 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 );  } 
+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_FrameReadLibGen2()                           { return s_GlobalFrame->pLibGen2;     } 
+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; } 
+char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   } 
+
+int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
+int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
+void *      Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
+       
+int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;      }               
+int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;     }               
+int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;       }               
+int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame;    }               
+
+void        Abc_FrameSetLibLut( void * pLib )                { s_GlobalFrame->pLibLut   = pLib;    } 
+void        Abc_FrameSetLibGen( void * pLib )                { s_GlobalFrame->pLibGen   = pLib;    } 
+void        Abc_FrameSetLibGen2( void * pLib )               { s_GlobalFrame->pLibGen2  = 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*************************************************************
 
@@ -75,7 +85,7 @@ void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateVal
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_FrameIsFlagEnabled( char * pFlag )
+int Abc_FrameIsFlagEnabled( char * pFlag )
 {
     char * pValue;
     // if flag is not defined, it is not enabled
@@ -105,17 +115,18 @@ Abc_Frame_t * Abc_FrameAllocate()
     extern void define_cube_size( int n );
     extern void set_espresso_flags();
     // allocate and clean
-    p = ABC_ALLOC( Abc_Frame_t, 1 );
-    memset( p, 0, sizeof(Abc_Frame_t) );
+    p = ABC_CALLOC( Abc_Frame_t, 1 );
     // get version
     p->sVersion = Abc_UtilsGetVersion( p );
     // set streams
     p->Err = stderr;
     p->Out = stdout;
     p->Hst = NULL;
+    p->Status     = -1;
+    p->nFrames    = -1;
     // set the starting step
-    p->nSteps = 1;
-    p->fBatchMode = 0;
+    p->nSteps     =  1;
+    p->fBatchMode =  0;
     // networks to be used by choice
     p->vStore = Vec_PtrAlloc( 16 );
     // initialize decomposition manager
@@ -123,6 +134,7 @@ Abc_Frame_t * Abc_FrameAllocate()
 //    set_espresso_flags();
     // initialize the trace manager
 //    Abc_HManStart();
+    p->vPlugInComBinPairs = Vec_PtrAlloc( 100 );
     return p;
 }
 
@@ -147,15 +159,24 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 //    undefine_cube_size();
     Rwt_ManGlobalStop();
 //    Ivy_TruthManStop();
-    if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL );
-    if ( p->pManDec ) Dec_ManStop( p->pManDec );
+    if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
+    if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     if ( p->vStore )  Vec_PtrFree( p->vStore );
-    if ( p->pSave1 )  Aig_ManStop( p->pSave1 );
-    if ( p->pSave2 )  Aig_ManStop( p->pSave2 );
-    if ( p->pSave3 )  Aig_ManStop( p->pSave3 );
-    if ( p->pSave4 )  Aig_ManStop( p->pSave4 );
+    if ( p->pSave1 )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
+    if ( p->pSave2 )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
+    if ( p->pSave3 )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );
+    if ( p->pSave4 )  Aig_ManStop( (Aig_Man_t *)p->pSave4 );
+    if ( p->vPlugInComBinPairs ) 
+    {
+        char * pTemp;
+        int i;
+        Vec_PtrForEachEntry( char *, p->vPlugInComBinPairs, pTemp, i )
+            ABC_FREE( pTemp );
+        Vec_PtrFree( p->vPlugInComBinPairs );
+    }
     Abc_FrameDeleteAllNetworks( p );
+    ABC_FREE( p->pCex );
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }
@@ -187,7 +208,25 @@ void Abc_FrameRestart( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_FrameShowProgress( Abc_Frame_t * p )
+void Abc_FrameClearVerifStatus( Abc_Frame_t * p )
+{
+    p->nFrames = -1;
+    p->Status  = -1;
+    ABC_FREE( p->pCex );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_FrameShowProgress( Abc_Frame_t * p )
 {
     return Abc_FrameIsFlagEnabled( "progressbar" );
 }
@@ -275,10 +314,10 @@ int Abc_FrameReadMode( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode )
+int Abc_FrameSetMode( Abc_Frame_t * p, int fNameMode )
 {
     char Buffer[2];
-    bool fNameModeOld;
+    int fNameModeOld;
     fNameModeOld = Abc_FrameReadMode( p );
     Buffer[0] = '0' + fNameMode;
     Buffer[1] = 0;
@@ -536,7 +575,7 @@ void Abc_FrameSetSave1( void * pAig )
 {
     Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
     if ( pFrame->pSave1 )
-        Aig_ManStop( pFrame->pSave1 );
+        Aig_ManStop( (Aig_Man_t *)pFrame->pSave1 );
     pFrame->pSave1 = pAig;
 }
 
@@ -555,7 +594,7 @@ void Abc_FrameSetSave2( void * pAig )
 {
     Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
     if ( pFrame->pSave2 )
-        Aig_ManStop( pFrame->pSave2 );
+        Aig_ManStop( (Aig_Man_t *)pFrame->pSave2 );
     pFrame->pSave2 = pAig;
 }
 
@@ -578,3 +617,5 @@ void * Abc_FrameReadSave2()  { void * pAig = Abc_FrameGetGlobalFrame()->pSave2;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index 03953e5b..a6f4b9e1 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -18,8 +18,12 @@
 
 ***********************************************************************/
 
+#include "abc.h"
 #include "mainInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+ 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,8 +42,10 @@ 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);
+extern void Libs_Init( Abc_Frame_t * pAbc );
+extern void Libs_End( Abc_Frame_t * pAbc );
+extern void Load_Init( Abc_Frame_t * pAbc );
+extern void Load_End( Abc_Frame_t * pAbc );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -59,6 +65,7 @@ extern void Libs_End(Abc_Frame_t * pAbc);
 void Abc_FrameInit( Abc_Frame_t * pAbc )
 {
     Cmd_Init( pAbc );
+    Cmd_CommandExecute( pAbc, "set checkread" ); 
     Io_Init( pAbc );
     Abc_Init( pAbc );
     Fpga_Init( pAbc );
@@ -66,6 +73,8 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Mio_Init( pAbc );
     Super_Init( pAbc );
     Libs_Init( pAbc );
+    Load_Init( pAbc );
+    EXT_ABC_INIT(pAbc) // plugin for external functionality
 }
 
 
@@ -90,6 +99,8 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Mio_End( pAbc );
     Super_End( pAbc );
     Libs_End( pAbc );
+    Load_End( pAbc );
+    EXT_ABC_END(pAbc) // plugin for external functionality
 }
 
 
@@ -98,3 +109,5 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 01bf5eb2..21fe407d 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -20,12 +20,24 @@
 
 #ifndef __MAIN_INT_H__
 #define __MAIN_INT_H__
+
  
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
 #include "main.h"
+#include "tim.h"
+#include "if.h"
+#include "aig.h"
+#include "gia.h"
+#include "ssw.h"
+#include "fra.h"
+#include "nwkMerge.h"
+#include "ntlnwk.h"
+#include "ext.h"
+
+ABC_NAMESPACE_HEADER_START
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -75,21 +87,33 @@ struct Abc_Frame_t_
     void *          pLibVer;     // the current Verilog library
 
     // new code
-    void *          pAbc8Ntl;    // the current design
-    void *          pAbc8Nwk;    // the current mapped network
-    void *          pAbc8Aig;    // the current AIG
-    void *          pAbc8Lib;    // the current LUT library
-    void *          pAig;
-    void *          pCex; 
+    Ntl_Man_t *     pAbc8Ntl;    // the current design
+    Nwk_Man_t *     pAbc8Nwk;    // the current mapped network
+    Aig_Man_t *     pAbc8Aig;    // the current AIG
+    If_Lib_t *      pAbc8Lib;    // the current LUT library
+
+    EXT_ABC_FRAME                // plugin for external functionality
+    If_Lib_t *      pAbc85Lib;   // the current LUT library
+
+    Gia_Man_t *     pGia;
+    Gia_Man_t *     pGia2;
+    Abc_Cex_t *     pCex; 
 
     void *          pSave1; 
     void *          pSave2; 
     void *          pSave3; 
     void *          pSave4; 
 
+    // related to LTL
+    Vec_Ptr_t *     vLTLProperties_global;
+
     // the addition to keep the best Ntl that can be used to restore
     void *            pAbc8NtlBestDelay;    // the best delay, Ntl
     void *            pAbc8NtlBestArea;    // the best area
+    int             Status;             // the status of verification problem (proved=1, disproved=0, undecided=-1)
+    int             nFrames;            // the number of time frames completed by BMC
+
+    Vec_Ptr_t *     vPlugInComBinPairs; // pairs of command and its binary name
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -120,6 +144,10 @@ extern ABC_DLL void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
 extern ABC_DLL void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
 extern ABC_DLL void            Abc_UtilsSource( Abc_Frame_t * pAbc );
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainLib.c b/src/base/main/mainLib.c
new file mode 100644
index 00000000..39078ed9
--- /dev/null
+++ b/src/base/main/mainLib.c
@@ -0,0 +1,93 @@
+/**CFile****************************************************************
+
+  FileName    [main.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The main package.]
+
+  Synopsis    [Here everything starts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "mainInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**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:
+#if defined(_DEBUG) && defined(_MSC_VER) 
+    _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 );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index 7761d428..5e77db57 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -24,6 +24,9 @@
 #include "fra.h"
 #include "ioa.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -196,3 +199,5 @@ int main( int argc, char * argv[] )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index f6751b6b..dadcbdd1 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -7,7 +7,7 @@
   PackageName [The main package.]
 
   Synopsis    [Miscellaneous utilities.]
-
+ 
   Author      [Alan Mishchenko]
   
   Affiliation [UC Berkeley]
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "abc.h"
 #include "mainInt.h"
 
 #ifndef _WIN32
@@ -25,10 +26,14 @@
 #include <readline/history.h>
 #endif
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
-static char * DateReadFromDateString(char * datestr);
+
+static char * DateReadFromDateString( char * datestr );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -181,6 +186,22 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
     }
 #endif
 
+#ifdef ABC_PYTHON_EMBED
+    if ( getenv("ABC_PYTHON_ABC_RC") )
+    {
+        /* read script file from $ABC_PYTHON_ABC_RC */
+
+        char * sPath = getenv("ABC_PYTHON_ABC_RC");
+        
+        if (sPath){
+            char * sCmd = ABC_ALLOC(char, strlen(sPath) + 50);
+            (void) sprintf(sCmd, "source -s %s", sPath);
+            (void) Cmd_CommandExecute(pAbc, sCmd);
+            ABC_FREE(sCmd);
+        }
+    }
+    else
+#endif /* #ifdef ABC_PYTHON_EMBED */
     {
         char * sPath1, * sPath2;
         char * home;
@@ -228,13 +249,13 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
         /* execute the abc script which can be open with the "open_path" */
         Cmd_CommandExecute( pAbc, "source -s abc.rc" );
     }
-
+    
 #endif //WIN32
     {
         // reset command history
         char * pName; 
         int i;
-        Vec_PtrForEachEntry( pAbc->aHistory, pName, i )
+        Vec_PtrForEachEntry( char *, pAbc->aHistory, pName, i )
             ABC_FREE( pName );
         pAbc->aHistory->nSize = 0;
     }
@@ -250,9 +271,7 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
   SideEffects []
 
 ******************************************************************************/
-char *
-DateReadFromDateString(
-  char * datestr)
+char * DateReadFromDateString( char * datestr )
 {
   static char result[25];
   char        day[10];
@@ -291,3 +310,5 @@ DateReadFromDateString(
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/main/module.make b/src/base/main/module.make
index 367f89f6..3d03cc12 100644
--- a/src/base/main/module.make
+++ b/src/base/main/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/base/main/main.c \
     src/base/main/mainFrame.c \
     src/base/main/mainInit.c \
+    src/base/main/mainLib.c \
     src/base/main/libSupport.c \
     src/base/main/mainUtils.c