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

  FileName    [sim.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Simulation package.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#ifndef ABC__opt__sim__sim_h
#define ABC__opt__sim__sim_h


/*
    The ideas realized in this package are described in the paper:
    "Detecting Symmetries in Boolean Functions using Circuit Representation, 
    Simulation, and Satisfiability".
*/

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

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


ABC_NAMESPACE_HEADER_START


////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Sym_Man_t_ Sym_Man_t;
struct Sym_Man_t_
{
    // info about the network
    Abc_Ntk_t *       pNtk;          // the network 
    Vec_Ptr_t *       vNodes;        // internal nodes in topological order
    int               nInputs;
    int               nOutputs;
    // internal simulation information
    int               nSimWords;     // the number of bits in simulation info
    Vec_Ptr_t *       vSim;          // simulation info
    // support information
    Vec_Ptr_t *       vSuppFun;      // bit representation
    Vec_Vec_t *       vSupports;     // integer representation
    // symmetry info for each output
    Vec_Ptr_t *       vMatrSymms;    // symmetric pairs
    Vec_Ptr_t *       vMatrNonSymms; // non-symmetric pairs
    Vec_Int_t *       vPairsTotal;   // total pairs
    Vec_Int_t *       vPairsSym;     // symmetric pairs
    Vec_Int_t *       vPairsNonSym;  // non-symmetric pairs
    // temporary simulation info
    unsigned *        uPatRand;
    unsigned *        uPatCol;
    unsigned *        uPatRow;
    // temporary
    Vec_Int_t *       vVarsU;
    Vec_Int_t *       vVarsV;
    int               iOutput;
    int               iVar1;
    int               iVar2;
    int               iVar1Old;
    int               iVar2Old;
    // internal data structures
    int               nSatRuns;
    int               nSatRunsSat;
    int               nSatRunsUnsat;
    // pairs
    int               nPairsSymm;
    int               nPairsSymmStr;
    int               nPairsNonSymm;
    int               nPairsRem;
    int               nPairsTotal;
    // runtime statistics
    abctime           timeStruct;
    abctime           timeCount;
    abctime           timeMatr;
    abctime           timeSim;
    abctime           timeFraig;
    abctime           timeSat;
    abctime           timeTotal;
};

typedef struct Sim_Man_t_ Sim_Man_t;
struct Sim_Man_t_
{
    // info about the network
    Abc_Ntk_t *       pNtk;
    int               nInputs;
    int               nOutputs;
    int               fLightweight;
    // internal simulation information
    int               nSimBits;      // the number of bits in simulation info
    int               nSimWords;     // the number of words in simulation info
    Vec_Ptr_t *       vSim0;         // simulation info 1
    Vec_Ptr_t *       vSim1;         // simulation info 2
    // support information
    int               nSuppBits;     // the number of bits in support info
    int               nSuppWords;    // the number of words in support info
    Vec_Ptr_t *       vSuppStr;      // structural supports
    Vec_Ptr_t *       vSuppFun;      // functional supports
    // simulation targets
    Vec_Vec_t *       vSuppTargs;    // support targets
    int               iInput;        // the input current processed
    // internal data structures
    Extra_MmFixed_t * pMmPat;   
    Vec_Ptr_t *       vFifo;
    Vec_Int_t *       vDiffs;
    int               nSatRuns;
    int               nSatRunsSat;
    int               nSatRunsUnsat;
    // runtime statistics
    abctime           timeSim;
    abctime           timeTrav;
    abctime           timeFraig;
    abctime           timeSat;
    abctime           timeTotal;
};

typedef struct Sim_Pat_t_ Sim_Pat_t;
struct Sim_Pat_t_
{
    int              Input;         // the input which it has detected
    int              Output;        // the output for which it was collected
    unsigned *       pData;         // the simulation data
};

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

#define SIM_NUM_WORDS(n)      (((n)>>5) + (((n)&31) > 0))
#define SIM_LAST_BITS(n)      ((((n)&31) > 0)? (n)&31 : 32)

#define SIM_MASK_FULL         (0xFFFFFFFF)
#define SIM_MASK_BEG(n)       (SIM_MASK_FULL >> (32-n))
#define SIM_MASK_END(n)       (SIM_MASK_FULL << (n))
#define SIM_SET_0_FROM(m,n)   ((m) & ~SIM_MASK_BEG(n))
#define SIM_SET_1_FROM(m,n)   ((m) |  SIM_MASK_END(n))

// generating random unsigned (#define RAND_MAX 0x7fff)
#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))

// macros to get hold of bits in a bit string
#define Sim_SetBit(p,i)       ((p)[(i)>>5] |= (1<<((i) & 31)))
#define Sim_XorBit(p,i)       ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define Sim_HasBit(p,i)      (((p)[(i)>>5]  & (1<<((i) & 31))) > 0)

// macros to get hold of the support info
#define Sim_SuppStrSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SuppStrHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SuppFunSetVar(vSupps,Output,v)    Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))
#define Sim_SuppFunHasVar(vSupps,Output,v)    Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
#define Sim_SimInfoSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SimInfoHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define Sim_SimInfoGet(vInfo,pNode)           ((unsigned *)((vInfo)->pArray[(pNode)->Id]))

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== simMan.c ==========================================================*/
extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
extern void            Sym_ManStop( Sym_Man_t * p );
extern void            Sym_ManPrintStats( Sym_Man_t * p );
extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight );
extern void            Sim_ManStop( Sim_Man_t * p );
extern void            Sim_ManPrintStats( Sim_Man_t * p );
extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
/*=== simSeq.c ==========================================================*/
extern Vec_Ptr_t *     Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
extern Vec_Ptr_t *     Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
/*=== simSupp.c ==========================================================*/
extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
/*=== simSym.c ==========================================================*/
extern int             Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose );
/*=== simSymSat.c ==========================================================*/
extern int             Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern );
/*=== simSymStr.c ==========================================================*/
extern void            Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun );
/*=== simSymSim.c ==========================================================*/
extern void            Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
/*=== simUtil.c ==========================================================*/
extern Vec_Ptr_t *     Sim_UtilInfoAlloc( int nSize, int nWords, int  fClean );
extern void            Sim_UtilInfoFree( Vec_Ptr_t * p );
extern void            Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords );
extern void            Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
extern void            Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
extern void            Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
extern int             Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
extern void            Sim_UtilSimulate( Sim_Man_t * p, int  fFirst );
extern void            Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, int  fType, int  fType1, int  fType2 );
extern void            Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
extern void            Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
extern Vec_Int_t *     Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
extern void            Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
extern void            Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
extern void            Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
extern int             Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int             Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int             Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );


ABC_NAMESPACE_HEADER_END


#endif

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