/**CHeaderFile*****************************************************************

  FileName    [imc.h]

  PackageName [imc]

  Synopsis    [Model Check using over(under)-approximation with automatic
  iterative refinement.]

  Description []


  Author      [Jae-Young Jang]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

  Revision    [$Id:]

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

#ifndef _IMC
#define _IMC

#include "part.h"
#include "mc.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/**Enum************************************************************************

  Synopsis    [Verbosity Levels.]

******************************************************************************/
typedef enum {
  Imc_VerbosityNone_c,
  Imc_VerbosityMin_c,
  Imc_VerbosityMax_c
} Imc_VerbosityLevel;

/**Enum************************************************************************

  Synopsis    [Refinement method.]

******************************************************************************/
typedef enum {
  Imc_RefineSort_c,
  Imc_RefineLatchRelation_c
} Imc_RefineMethod;

/**Enum************************************************************************

  Synopsis    [Extent to which don't cares are used in Imc functions.]

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

typedef enum {
  Imc_DcLevelNone_c,
  Imc_DcLevelRch_c,
  Imc_DcLevelMax_c,
  Imc_DcLevelArdc_c
} Imc_DcLevel;

/**Enum************************************************************************

  Synopsis    [Type of a verification result.]

******************************************************************************/
typedef enum {
  Imc_VerificationTrue_c,
  Imc_VerificationFalse_c,
  Imc_VerificationInconclusive_c,
  Imc_VerificationRefine_c,
  Imc_VerificationError_c
} Imc_VerificationResult;

/**Enum************************************************************************

  Synopsis    [Type of an operational graph.]

******************************************************************************/
typedef enum {
  Imc_GraphNDOG_c,
  Imc_GraphPDOG_c,
  Imc_GraphMOG_c
} Imc_GraphType;

/**Enum************************************************************************

  Synopsis    [Type of a polarity in a graph.]

******************************************************************************/
typedef enum {
  Imc_PolarityNeg_c,
  Imc_PolarityPos_c,
  Imc_PolarityBoth_c
} Imc_Polarity;

/**Enum************************************************************************

  Synopsis    [Upper bound approximation computation method.]

******************************************************************************/
typedef enum {
  Imc_UpperExistentialQuantification_c
} Imc_UpperMethod;

/**Enum************************************************************************

  Synopsis    [Lower bound approximation computation method.]

******************************************************************************/
typedef enum {
  Imc_LowerSubsetTR_c,
  Imc_LowerUniversalQuantification_c
} Imc_LowerMethod;

/**Enum************************************************************************

  Synopsis    [Partition Method.]

******************************************************************************/
typedef enum {
  Imc_PartAll_c,
  Imc_PartDepend_c,
  Imc_PartInc_c
} Imc_PartMethod;

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct ImcInfoStruct Imc_Info_t;
typedef struct ImcUpperSystemInfo Imc_UpperSystemInfo_t;
typedef struct ImcLowerSystemInfo Imc_LowerSystemInfo_t;
typedef struct ImcSystemInfo Imc_SystemInfo_t;
typedef struct ImcNodeInfo Imc_NodeInfo_t;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN void Imc_Init(void);
EXTERN void Imc_End(void);
EXTERN Imc_VerificationResult Imc_ImcEvaluateFormulaLinearRefine(Ntk_Network_t *network, Ctlp_Formula_t *orgFormula, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, int incrementalSize, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Fsm_Fsm_t *exactFsm, Imc_DcLevel dcLevel, Imc_GraphType graphType, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName);
EXTERN Imc_VerificationResult Imc_ImcVerifyFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
EXTERN Imc_VerificationResult Imc_SatCheck(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
EXTERN Imc_Info_t * Imc_ImcInfoInitialize(Ntk_Network_t *network, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Imc_DcLevel dcLevel, int incrementalSize, Imc_GraphType graphType, Fsm_Fsm_t *exactFsm, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName);
EXTERN void Imc_ImcInfoFree(Imc_Info_t *imcInfo);
EXTERN void Imc_SystemInfoInitialize(Imc_Info_t *imcInfo, st_table *globalLatchNameTable, st_table *initialLatchNameTable);
EXTERN void Imc_SystemInfoFree(Imc_SystemInfo_t *systemInfo);
EXTERN void Imc_ImcSystemInfoUpdate(Imc_Info_t *imcInfo, st_table *newLatchNameTable);
EXTERN void Imc_UpperSystemInfoInitialize(Imc_Info_t *imcInfo, st_table *latchNameTable);
EXTERN void Imc_UpperSystemMinimize(Imc_Info_t *imcInfo, mdd_t *careStates);
EXTERN void Imc_UpperSystemInfoFree(Imc_UpperSystemInfo_t *upperSystem);
EXTERN void Imc_LowerSystemInfoInitialize(Imc_Info_t *imcInfo, st_table *latchNameTable);
EXTERN void Imc_LowerSystemMinimize(Imc_Info_t *imcInfo, mdd_t *careStates);
EXTERN void Imc_LowerSystemInfoFree(Imc_LowerSystemInfo_t *lowerSystem);
EXTERN Imc_NodeInfo_t * Imc_NodeInfoInitialize(Imc_Polarity polarity);
EXTERN void Imc_NodeInfoReset(Imc_Info_t *imcInfo);
EXTERN void Imc_NodeInfoFree(Imc_NodeInfo_t *nodeInfo);
EXTERN void Imc_ImcPrintSystemSize(Imc_Info_t *imcInfo);
EXTERN void Imc_ImcPrintApproxSystemSize(Imc_Info_t *imcInfo);
EXTERN mdd_t * Imc_GetUpperSat(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
EXTERN mdd_t * Imc_GetLowerSat(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula);
EXTERN int Imc_ImcEvaluateCTLFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *ctlFormula, Imc_Polarity polarity);
EXTERN int Imc_ImcEvaluateEXApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
EXTERN int Imc_ImcEvaluateEUApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
EXTERN int Imc_ImcEvaluateEGApprox(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation);
EXTERN mdd_t * Imc_ComputeUpperPreimage(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
EXTERN mdd_t * Imc_ComputeApproxPreimageByQuantification(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact, boolean computeLower);
EXTERN mdd_t * Imc_ComputeLowerPreimage(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
EXTERN mdd_t * Imc_ComputeLowerPreimageBySubsetTR(Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact);
EXTERN mdd_t * Imc_ProductAbstract(mdd_manager *mddMgr, array_t *relationArray, array_t *smoothVarsMddIdArray, mdd_t *toStates);

/**AutomaticEnd***************************************************************/

#endif /* _IMC */