1 | /**CHeaderFile***************************************************************** |
---|
2 | |
---|
3 | FileName [grab.h] |
---|
4 | |
---|
5 | PackageName [grab] |
---|
6 | |
---|
7 | Synopsis [Abstraction refinement for large scale invariant checking.] |
---|
8 | |
---|
9 | Description [Abstraction refinement for large scale invariant checking.] |
---|
10 | |
---|
11 | Author [Chao Wang.] |
---|
12 | |
---|
13 | Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All |
---|
14 | rights reserved. |
---|
15 | |
---|
16 | Permission is hereby granted, without written agreement and without license |
---|
17 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
18 | documentation for any purpose, provided that the above copyright notice and |
---|
19 | the following two paragraphs appear in all copies of this software. |
---|
20 | ] |
---|
21 | |
---|
22 | ******************************************************************************/ |
---|
23 | |
---|
24 | #ifndef _GRAB |
---|
25 | #define _GRAB |
---|
26 | |
---|
27 | /*---------------------------------------------------------------------------*/ |
---|
28 | /* Nested includes */ |
---|
29 | /*---------------------------------------------------------------------------*/ |
---|
30 | #include "vm.h" |
---|
31 | #include "ntk.h" |
---|
32 | |
---|
33 | /*---------------------------------------------------------------------------*/ |
---|
34 | /* Constant declarations */ |
---|
35 | /*---------------------------------------------------------------------------*/ |
---|
36 | |
---|
37 | |
---|
38 | /*---------------------------------------------------------------------------*/ |
---|
39 | /* Structure declarations */ |
---|
40 | /*---------------------------------------------------------------------------*/ |
---|
41 | |
---|
42 | |
---|
43 | /*---------------------------------------------------------------------------*/ |
---|
44 | /* Type declarations */ |
---|
45 | /*---------------------------------------------------------------------------*/ |
---|
46 | |
---|
47 | |
---|
48 | /*---------------------------------------------------------------------------*/ |
---|
49 | /* Variable declarations */ |
---|
50 | /*---------------------------------------------------------------------------*/ |
---|
51 | |
---|
52 | |
---|
53 | /*---------------------------------------------------------------------------*/ |
---|
54 | /* Macro declarations */ |
---|
55 | /*---------------------------------------------------------------------------*/ |
---|
56 | |
---|
57 | |
---|
58 | /**AutomaticStart*************************************************************/ |
---|
59 | |
---|
60 | /*---------------------------------------------------------------------------*/ |
---|
61 | /* Function prototypes */ |
---|
62 | /*---------------------------------------------------------------------------*/ |
---|
63 | |
---|
64 | EXTERN void Grab_Init(void); |
---|
65 | EXTERN void Grab_End(void); |
---|
66 | 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); |
---|
67 | |
---|
68 | /**AutomaticEnd***************************************************************/ |
---|
69 | |
---|
70 | #endif /* _GRAB */ |
---|