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

  FileName    [dchInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC__aig__dch__dchInt_h
#define ABC__aig__dch__dchInt_h


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

#include "aig/aig/aig.h"
#include "sat/bsat/satSolver.h"
#include "dch.h"

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


ABC_NAMESPACE_HEADER_START


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

// equivalence classes
typedef struct Dch_Cla_t_ Dch_Cla_t;

// choicing manager
typedef struct Dch_Man_t_ Dch_Man_t;
struct Dch_Man_t_
{
    // parameters
    Dch_Pars_t *     pPars;          // choicing parameters
    // AIGs used in the package
//    Vec_Ptr_t *      vAigs;          // user-given AIGs
    Aig_Man_t *      pAigTotal;      // intermediate AIG
    Aig_Man_t *      pAigFraig;      // final AIG
    // equivalence classes
    Dch_Cla_t *      ppClasses;      // equivalence classes of nodes
    Aig_Obj_t **     pReprsProved;   // equivalences proved
    // SAT solving
    sat_solver *     pSat;           // recyclable SAT solver
    int              nSatVars;       // the counter of SAT variables
    int *            pSatVars;       // mapping of each node into its SAT var
    Vec_Ptr_t *      vUsedNodes;     // nodes whose SAT vars are assigned
    int              nRecycles;      // the number of times SAT solver was recycled
    int              nCallsSince;    // the number of calls since the last recycle
    Vec_Ptr_t *      vFanins;        // fanins of the CNF node
    Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
    Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
    // solver cone size
    int              nConeThis;
    int              nConeMax;
    // SAT calls statistics
    int              nSatCalls;      // the number of SAT calls
    int              nSatProof;      // the number of proofs
    int              nSatFailsReal;  // the number of timeouts
    int              nSatCallsUnsat; // the number of unsat SAT calls
    int              nSatCallsSat;   // the number of sat SAT calls
    // choice node statistics
    int              nLits;          // the number of lits in the cand equiv classes
    int              nReprs;         // the number of proved equivalent pairs
    int              nEquivs;        // the number of final equivalences
    int              nChoices;       // the number of final choice nodes
    // runtime stats
    abctime          timeSimInit;    // simulation and class computation
    abctime          timeSimSat;     // simulation of the counter-examples
    abctime          timeSat;        // solving SAT
    abctime          timeSatSat;     // sat
    abctime          timeSatUnsat;   // unsat
    abctime          timeSatUndec;   // undecided
    abctime          timeChoice;     // choice computation
    abctime          timeOther;      // other runtime
    abctime          timeTotal;      // total runtime
};

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

static inline int  Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }

static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj )                       { return (Aig_Obj_t *)pObj->pData;  }
static inline void        Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }

static inline int  Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
}
static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}

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

/*=== dchAig.c ===================================================*/
/*=== dchChoice.c ===================================================*/
extern int           Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
extern int           Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
extern Aig_Man_t *   Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps );
/*=== dchClass.c =================================================*/
extern Dch_Cla_t *   Dch_ClassesStart( Aig_Man_t * pAig );
extern void          Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
                         unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
                         int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
                         int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void          Dch_ClassesStop( Dch_Cla_t * p );
extern int           Dch_ClassesLitNum( Dch_Cla_t * p );
extern Aig_Obj_t **  Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void          Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
extern void          Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
extern int           Dch_ClassesRefine( Dch_Cla_t * p );
extern int           Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern void          Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots );
extern void          Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots );
extern int           Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
/*=== dchCnf.c ===================================================*/
extern void          Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
/*=== dchMan.c ===================================================*/
extern Dch_Man_t *   Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
extern void          Dch_ManStop( Dch_Man_t * p );
extern void          Dch_ManSatSolverRecycle( Dch_Man_t * p );
/*=== dchSat.c ===================================================*/
extern int           Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
/*=== dchSim.c ===================================================*/
extern Dch_Cla_t *   Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
/*=== dchSimSat.c ===================================================*/
extern void          Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void          Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
/*=== dchSweep.c ===================================================*/
extern void          Dch_ManSweep( Dch_Man_t * p );


ABC_NAMESPACE_HEADER_END


#endif

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