mainInt.h

/**CFile****************************************************************

  FileName    [mainInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The main package.]

  Synopsis    [Internal declarations of the main package.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]

***********************************************************************/

#ifndef ABC__base__main__mainInt_h
#define ABC__base__main__mainInt_h

 
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "main.h"
#include "misc/tim/tim.h"
#include "map/if/if.h"
#include "aig/aig/aig.h"
#include "aig/gia/gia.h"
#include "proof/ssw/ssw.h"
#include "proof/fra/fra.h"

#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
#endif

ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

// the current version
#define ABC_VERSION "UC Berkeley, ABC 1.01"

// the maximum length of an input line 
#define ABC_MAX_STR     (1<<15)

////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

typedef void (*Abc_Frame_Callback_BmcFrameDone_Func)(int frame, int po, int status);

struct Abc_Frame_t_
{
    // general info
    char *          sVersion;      // the name of the current version
    char *          sBinary;       // the name of the binary running
    // commands, aliases, etc
    st__table *      tCommands;     // the command table
    st__table *      tAliases;      // the alias table
    st__table *      tFlags;        // the flag table
    Vec_Ptr_t *     aHistory;      // the command history
    // the functionality
    Abc_Ntk_t *     pNtkCur;       // the current network
    Abc_Ntk_t *     pNtkBestDelay; // the current network
    Abc_Ntk_t *     pNtkBestArea;  // the current network
    Abc_Ntk_t *     pNtkBackup;    // the current network
    int             nSteps;        // the counter of different network processed
    int             fSource;       // marks the source mode
    int             fAutoexac;     // marks the autoexec mode
    int             fBatchMode;    // batch mode flag
    int             fBridgeMode;   // bridge mode flag
    // save/load
    Abc_Ntk_t *     pNtkBest;        // the current network
    float           nBestNtkArea;   // best area
    float           nBestNtkDelay;  // best delay
    int             nBestNtkNodes;  // best nodes
    int             nBestNtkLevels; // best levels

    // output streams
    FILE *          Out;
    FILE *          Err;
    FILE *          Hst;
    // used for runtime measurement
    double          TimeCommand;   // the runtime of the last command
    double          TimeTotal;     // the total runtime of all commands
    // temporary storage for structural choices
    Vec_Ptr_t *     vStore;        // networks to be used by choice
    // decomposition package    
    void *          pManDec;       // decomposition manager
    void *          pManDsd;       // decomposition manager
    void *          pManDsd2;      // decomposition manager
    // libraries for mapping
    void *          pLibLut;       // the current LUT library
    void *          pLibBox;       // the current box library
    void *          pLibGen;       // the current genlib
    void *          pLibGen2;      // the current genlib
    void *          pLibSuper;     // the current supergate library
    void *          pLibScl;       // the current Liberty library
    void *          pAbcCon;       // constraint manager
    // timing constraints
    char *          pDrivingCell;  // name of the driving cell
    float           MaxLoad;       // maximum output load
    // inductive don't-cares
    Vec_Int_t *     vIndFlops;
    int             nIndFrames;

    // new code
    Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
    Gia_Man_t *     pGia2;         // copy of the above
    Gia_Man_t *     pGiaBest;      // copy of the above
    Gia_Man_t *     pGiaBest2;     // copy of the above
    Gia_Man_t *     pGiaSaved;     // copy of the above
    int             nBestLuts;     // best LUT count
    int             nBestEdges;    // best edge count
    int             nBestLevels;   // best level count
    int             nBestLuts2;     // best LUT count
    int             nBestEdges2;    // best edge count
    int             nBestLevels2;   // best level count
    Abc_Cex_t *     pCex;          // a counter-example to fail the current network
    Abc_Cex_t *     pCex2;         // copy of the above
    Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails
    Vec_Ptr_t *     vPoEquivs;     // equivalence classes of isomorphic primary outputs
    Vec_Int_t *     vStatuses;     // problem status for each output
    Vec_Int_t *     vAbcObjIds;    // object IDs
    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
    Vec_Ptr_t *     vLTLProperties_global; // related to LTL
    Vec_Ptr_t *     vSignalNames;  // temporary storage for signal names
    char *          pSpecName;
    void *          pSave1; 
    void *          pSave2; 
    void *          pSave3; 
    void *          pSave4; 
    void *          pAbc85Ntl;
    void *          pAbc85Ntl2;
    void *          pAbc85Best;
    void *          pAbc85Delay;
    void *          pAbcWlc;
    Vec_Int_t *     pAbcWlcInv;
    void *          pAbcRtl;
    void *          pAbcBac;
    void *          pAbcCba;
    void *          pAbcPla;
    Abc_Nam_t *     pJsonStrs;
    Vec_Wec_t *     vJsonObjs;
#ifdef ABC_USE_CUDD
    DdManager *     dd;            // temporary BDD package
#endif
    Gia_Man_t *     pGiaMiniAig; 
    Gia_Man_t *     pGiaMiniLut; 
    Vec_Int_t *     vCopyMiniAig;
    Vec_Int_t *     vCopyMiniLut;
    int *           pArray;
    int *           pBoxes;
    void *          pNdr;
    int *           pNdrArray;

    Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
};

typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );

struct Abc_FrameInitializer_t_;
typedef struct Abc_FrameInitializer_t_ Abc_FrameInitializer_t;

struct Abc_FrameInitializer_t_
{
    Abc_Frame_Initialization_Func init;
    Abc_Frame_Initialization_Func destroy;

    Abc_FrameInitializer_t* next;
    Abc_FrameInitializer_t* prev;
};

////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                       MACRO DEFINITIONS                          ///
////////////////////////////////////////////////////////////////////////


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== mvMain.c ===========================================================*/
extern ABC_DLL int             main( int argc, char * argv[] );
/*=== mvInit.c ===================================================*/
extern ABC_DLL void            Abc_FrameInit( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_FrameEnd( Abc_Frame_t * pAbc );
extern ABC_DLL void            Abc_FrameAddInitializer( Abc_FrameInitializer_t* p );
/*=== mvFrame.c =====================================================*/
extern ABC_DLL Abc_Frame_t *   Abc_FrameAllocate();
extern ABC_DLL void            Abc_FrameDeallocate( Abc_Frame_t * p );
/*=== mvUtils.c =====================================================*/
extern ABC_DLL char *          Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
extern ABC_DLL char *          Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
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

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////