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

  FileName    [abs.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Abstraction package.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#ifndef ABC__proof_abs__Abs_h
#define ABC__proof_abs__Abs_h


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

#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"

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


ABC_NAMESPACE_HEADER_START


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

// abstraction parameters
typedef struct Abs_Par_t_ Abs_Par_t;
struct Abs_Par_t_
{
    int            nFramesMax;         // maximum frames
    int            nFramesStart;       // starting frame 
    int            nFramesPast;        // overlap frames
    int            nConfLimit;         // conflict limit
    int            nLearnedMax;        // max number of learned clauses
    int            nLearnedStart;      // max number of learned clauses
    int            nLearnedDelta;      // delta increase of learned clauses
    int            nLearnedPerce;      // percentage of clauses to leave
    int            nTimeOut;           // timeout in seconds
    int            nRatioMin;          // stop when less than this % of object is unabstracted
    int            nRatioMin2;         // stop when less than this % of object is unabstracted during refinement
    int            nRatioMax;          // restart when the number of abstracted object is more than this
    int            fUseTermVars;       // use terminal variables
    int            fUseRollback;       // use rollback to the starting number of frames
    int            fPropFanout;        // propagate fanout implications
    int            fAddLayer;          // refinement strategy by adding layers
    int            fNewRefine;         // uses new refinement heuristics
    int            fUseSkip;           // skip proving intermediate timeframes
    int            fUseSimple;         // use simple CNF construction
    int            fSkipHash;          // skip hashing CNF while unrolling
    int            fUseFullProof;      // use full proof for UNSAT cores
    int            fDumpVabs;          // dumps the abstracted model
    int            fDumpMabs;          // dumps the original AIG with abstraction map
    int            fCallProver;        // calls the prover
    int            fSimpProver;        // calls simplification before prover
    char *         pFileVabs;          // dumps the abstracted model into this file
    int            fVerbose;           // verbose flag
    int            fVeryVerbose;       // print additional information
    int            iFrame;             // the number of frames covered
    int            iFrameProved;       // the number of frames proved
    int            nFramesNoChange;    // the number of last frames without changes
    int            nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
};

// old abstraction parameters
typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
struct Gia_ParAbs_t_
{
    int            Algo;               // the algorithm to be used
    int            nFramesMax;         // timeframes for PBA
    int            nConfMax;           // conflicts for PBA
    int            fDynamic;           // dynamic unfolding for PBA
    int            fConstr;            // use constraints
    int            nFramesBmc;         // timeframes for BMC
    int            nConfMaxBmc;        // conflicts for BMC
    int            nStableMax;         // the number of stable frames to quit
    int            nRatio;             // ratio of flops to quit
    int            TimeOut;            // approximate timeout in seconds
    int            TimeOutVT;          // approximate timeout in seconds
    int            nBobPar;            // Bob's parameter
    int            fUseBdds;           // use BDDs to refine abstraction
    int            fUseDprove;         // use 'dprove' to refine abstraction
    int            fUseStart;          // use starting frame
    int            fVerbose;           // verbose output
    int            fVeryVerbose;       // printing additional information
    int            Status;             // the problem status
    int            nFramesDone;        // the number of frames covered
};

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

static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )          { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                         }
static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                     }
static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                                }
static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )           { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);            }
static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )          { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);            }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )          { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;       }

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

/*=== abs.c =========================================================*/
/*=== absDup.c =========================================================*/
extern Gia_Man_t *       Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t *       Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void              Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern void              Gia_ManPrintFlopClasses( Gia_Man_t * p );
extern void              Gia_ManPrintObjClasses( Gia_Man_t * p );
extern void              Gia_ManPrintGateClasses( Gia_Man_t * p );
/*=== absGla.c =========================================================*/
extern int               Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
/*=== absGlaOld.c =========================================================*/
extern int               Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
/*=== absIter.c =========================================================*/
extern Gia_Man_t *       Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
/*=== absPth.c =========================================================*/
extern void              Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose );
extern void              Gia_GlaProveCancel( int fVerbose );
extern int               Gia_GlaProveCheck( int fVerbose );
/*=== absVta.c =========================================================*/
extern int               Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
/*=== absUtil.c =========================================================*/
extern void              Abs_ParSetDefaults( Abs_Par_t * p );
extern Vec_Int_t *       Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t *       Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t *       Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t *       Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int               Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int               Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );

/*=== absRpm.c =========================================================*/
extern Gia_Man_t *       Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose );
/*=== absRpmOld.c =========================================================*/
extern Gia_Man_t *       Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose );
extern void              Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );

/*=== absOldCex.c ==========================================================*/
extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
/*=== absOldRef.c ==========================================================*/
extern int               Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
/*=== absOldSat.c ==========================================================*/
extern Vec_Int_t *       Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
/*=== absOldSim.c ==========================================================*/
extern Vec_Int_t *       Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );


ABC_NAMESPACE_HEADER_END

#endif

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