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

  FileName    [grabInt.h]

  PackageName [grab]

  Synopsis    [Internal declarations.]

  Author      [Chao Wang.]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.
  ]
  
******************************************************************************/

#ifndef _GRABINT
#define _GRABINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "grab.h"
#include "cmd.h"
#include "ctlp.h"
#include "ctlsp.h"
#include "mc.h"
#include "img.h"
#include "ntk.h"
#include "ntm.h"
#include "part.h"
#include "mvf.h"
#include <string.h>
#include "bmc.h"
#include "mdd.h"
#include "epd.h"
#include "fsm.h"
#include "partInt.h"
#include "fsmInt.h"



/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define GRAB_PARTITION_NOCHANGE    0
#define GRAB_PARTITION_BUILD       1
#define GRAB_PARTITION_UPDATE      2

#define GRAB_CEX_MINTERM             0
#define GRAB_CEX_CUBE                1
#define GRAB_CEX_SOR                 2

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/
struct mAigManagerStateStruct{
  mAig_Manager_t   *manager;
  st_table         *nodeToMvfAigTable;
  st_table         *nodeToMAigIdTable;
};

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct mAigManagerStateStruct mAigManagerState_t;

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

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

#define DBGMSG1(msg)         fprintf(vis_stdout, "\n<<%s>>\n", msg)
#define DBGMSG2(msg,msg2)         fprintf(vis_stdout, msg, msg2)

#define CHKPRINT(flag, msg)   if(flag) fprintf(vis_stdout, msg) 
#define CHKPRINT1(flag, msg)   if(flag) fprintf(vis_stdout, msg) 
#define CHKPRINT2(flag, msg, msg2)   if(flag) fprintf(vis_stdout, msg, msg2) 
#define CHKPRINT3(flag, msg, msg2, msg3)   if(flag) fprintf(vis_stdout,msg,msg2,msg3) 
#define CHKPRINT4(flag, msg, msg2, msg3, msg4)   if(flag) fprintf(vis_stdout,msg,msg2,msg3,msg4) 
#define CHKPRINT5(flag, msg, msg2, msg3, msg4, msg5)   if(flag) fprintf(vis_stdout,msg,msg2,msg3,msg4,msg5)

#if 0

#define DBGMSG(msg)         fprintf(vis_stdout, "\n<<%s>>\n", msg)
#define CHKCPUTIME(flag, startTime, msg) \
        if (flag) { \
            long thisTime = util_cpu_ctime();\
            fprintf(vis_stdout, "\n-- elapsed time %5g  (%s)\n",\
                    (double)(thisTime - startTime)/1000.0, msg); \
            fflush(vis_stdout);\
        }

#else 

#define DBGMSG(msg)         
#define CHKCPUTIME(flag,startTime,msg)  

#endif

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

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

EXTERN boolean Bmc_AbstractCheckAbstractTraces(Ntk_Network_t *network, array_t *synOnionRings, st_table *absLatches, int verbose, int dbgLevel, int printInputs);
EXTERN boolean Bmc_AbstractCheckAbstractTracesWithFineGrain(Ntk_Network_t *network, st_table *coiBnvTable, array_t *synOnionRings, st_table *absLatches, st_table *absBnvs);
EXTERN void GrabRefineAbstractionByGrab(Fsm_Fsm_t *absFsm, array_t *SORs, st_table *absVarTable, st_table *BnvTable, array_t *addedVars, array_t *addedBnvs, int refine_direction, st_table *nodeToFaninNumberTable, int verbose);
EXTERN int GrabNodeComputeFaninNumberTableItem(Ntk_Network_t *network, st_table *nodeToFaninNumberTable, Ntk_Node_t *node);
EXTERN st_table * GrabComputeCOIAbstraction(Ntk_Network_t *network, Ctlp_Formula_t *invFormula);
EXTERN st_table * GrabComputeInitialAbstraction(Ntk_Network_t *network, Ctlp_Formula_t *invFormula);
EXTERN void GrabUpdateAbstractPartition(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag);
EXTERN Fsm_Fsm_t * GrabCreateAbstractFsm(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag, int independentFlag);
EXTERN mdd_t * GrabComputeInitialStates(Ntk_Network_t *network, array_t *psVars);
EXTERN mdd_t * GrabFsmComputeReachableStates(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *invStatesArray, int verbose);
EXTERN mdd_t * GrabFsmComputeConstrainedReachableStates(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *SORs, int verbose);
EXTERN array_t * GrabFsmComputeSynchronousOnionRings(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, mdd_t *inv_states, int cexType, int verbose);
EXTERN array_t * GrabGetVisibleVarMddIds(Fsm_Fsm_t *absFsm, st_table *absVarTable);
EXTERN array_t * GrabGetInvisibleVarMddIds(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable);
EXTERN int GrabTestRefinementSetSufficient(Ntk_Network_t *network, array_t *SORs, st_table *absVarTable, int verbose);
EXTERN int GrabTestRefinementBnvSetSufficient(Ntk_Network_t *network, st_table *coiBnvTable, array_t *SORs, st_table *absVarTable, st_table *absBnvTable, int verbose);
EXTERN void GrabMinimizeLatchRefinementSet(Ntk_Network_t *network, st_table **absVarTable, st_table **absBnvTable, array_t *newlyAddedLatches, array_t **newlyAddedBnvs, array_t *SORs, int verbose);
EXTERN void GrabMinimizeBnvRefinementSet(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table **absBnvTable, array_t *newlyAddedBnvs, array_t *SORs, int verbose);
EXTERN void GrabNtkClearAllMddIds(Ntk_Network_t *network);
EXTERN void GrabPrintNodeArray(char *caption, array_t *theArray);
EXTERN void GrabPrintMddIdArray(Ntk_Network_t *network, char *caption, array_t *mddIdArray);
EXTERN void GrabPrintNodeList(char *caption, lsList theList);
EXTERN void GrabPrintNodeHashTable(char *caption, st_table *theTable);

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

#endif /* _GRABINT */