forked from vprover/vampire
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lglconst.h
41 lines (31 loc) · 1011 Bytes
/
lglconst.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
#ifndef lglconst_h_INCLUDED
#define lglconst_h_INCLUDED
#include <limits.h>
#define REMOVED INT_MAX
#define NOTALIT ((INT_MAX >> RMSHFT))
#define MAXVAR ((INT_MAX >> RMSHFT) - 2)
#define GLUESHFT 4
#define POW2GLUE (1 << GLUESHFT)
#define MAXGLUE (POW2GLUE - 1)
#define GLUEMASK (POW2GLUE - 1)
#define MAXREDLIDX ((1 << (31 - GLUESHFT)) - 2)
#define MAXIRRLIDX ((1 << (31 - RMSHFT)) - 2)
#define MAXLDFW 31
#define REPMOD 22
#define FUNVAR 12
#define FUNQUADS (1<<(FUNVAR - 6))
#define FALSECNF (1ll<<32)
#define TRUECNF 0ll
#define FLTPRC 32
#define EXPMIN (0x0000 ## 0000)
#define EXPZRO (0x1000 ## 0000)
#define EXPMAX (0x7fff ## ffff)
#define MNTBIT (0x0000 ## 0001 ## 0000 ## 0000 ## ull)
#define MNTMAX (0x0000 ## 0001 ## ffff ## ffff ## ull)
#define FLTMIN (0x0000 ## 0000 ## 0000 ## 0000 ## ll)
#define FLTMAX (0x7fff ## ffff ## ffff ## ffff ## ll)
#define DEFSCOREXP 500
#define LLMAX (0x7fff ## ffff ## ffff ## ffff ## ll)
#define MAXFLTSTR 6
#define MAXPHN 10
#endif