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

  FileName    [bmc.h]

  PackageName [bmc]

  Synopsis    [bounded model checking (BMC) header file.]

  Description []

  Author      [Mohammad Awedh]

  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: bmc.h,v 1.26 2010/04/09 23:50:57 fabio Exp $]

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

#ifndef _BMC
#define _BMC

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "ntk.h"
#include "ntmaig.h"
#include "ctlspInt.h"
#include "mcInt.h"
#include "fsm.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define BMC_INITIAL_STATES 1
#define BMC_NO_INITIAL_STATES 0

#define CirCUs 0
#define cusp 1


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct BmcOption     BmcOption_t;
typedef struct BmcCnfClauses BmcCnfClauses_t;
typedef struct BmcCnfStates  BmcCnfStates_t; 
typedef struct BmcCheckForTermination BmcCheckForTermination_t;
/**AutomaticStart*************************************************************/

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

EXTERN boolean Bmc_AbstractCheckAbstractPath(Ntk_Network_t *network, McPath_t *abstractPath, array_t *supportList, Ctlsp_Formula_t *formula);
EXTERN void Bmc_Init(void);
EXTERN void Bmc_End(void);
EXTERN mdd_t * Bmc_ComputeCloseCube(mdd_t *states, mdd_t *target, int *dist, Fsm_Fsm_t *modelFsm);
EXTERN MvfAig_Function_t * Bmc_NodeBuildMVF(Ntk_Network_t *network, Ntk_Node_t *node);
EXTERN MvfAig_Function_t * Bmc_ReadMvfAig(Ntk_Node_t * node, st_table * nodeToMvfAigTable);
 BmcOption_t * ParseBmcOptions(int argc, char **argv);
/**AutomaticEnd***************************************************************/

#endif /* _BMC */