initial commit of public abc

1 files changed, 78 insertions, 37 deletions

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
+