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

  FileName    [grab.h]

  PackageName [grab]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [Abstraction refinement for large scale invariant checking.]

  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 _GRAB
#define _GRAB

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "vm.h"
#include "ntk.h"

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


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


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


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


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


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

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

EXTERN void Grab_Init(void);
EXTERN void Grab_End(void);
EXTERN void Grab_NetworkCheckInvariants(Ntk_Network_t *network, array_t *InvariantFormulaArray, char *refineAlgorithm, int fineGrainFlag, int refineMinFlag, int useArdcFlag, int cexType, int verbosity, int dbgLevel, int printInputs, FILE *debugFile, int useMore, char *driverName);

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

#endif /* _GRAB */