1 /*-----------------------------------------------------------------------
2
3 File : clb_defines.h
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Basic definition useful (very nearly) everywhere.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Sat Jul 5 02:28:25 MET DST 1997
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #ifndef CLB_DEFINES
25
26 #define CLB_DEFINES
27
28 #include <assert.h>
29 #include <stdio.h>
30 #include <string.h>
31 #include <errno.h>
32 #include <sys/param.h>
33 #include <unistd.h>
34 #include <stddef.h>
35 #include <stdlib.h>
36 #include <math.h>
37 #include <stdbool.h>
38
39 /*---------------------------------------------------------------------*/
40 /* Data type declarations */
41 /*---------------------------------------------------------------------*/
42
43 /* Trick the stupid type concept for polymorphic indices (hashes,
44 trees) with int/pointer type. */
45
46 typedef union int_or_p
47 {
48 long i_val;
49 void *p_val;
50 }IntOrP;
51
52 #ifdef CONSTANT_MEM_ESTIMATE
53 #define INTORP_MEM 4
54 #define LONG_MEM 4
55 #else
56 #define INTORP_MEM sizeof(IntOrP)
57 #define LONG_MEM sizeof(long)
58 #endif
59
60 /* Generic cleanup function for pseudo-objects - the function has to
61 know how to get rid of the passed data. */
62
63 typedef void (*GenericExitFun)(void* data);
64
65 /* Type of a comparison function for <stdlib>'s qsort */
66
67 typedef int (*ComparisonFunctionType)(const void*, const void*);
68
69 /*---------------------------------------------------------------------*/
70 /* Exported Functions and Variables */
71 /*---------------------------------------------------------------------*/
72
73 #undef MAX
74 #define MAX(x,y) ({ __typeof__ (x) _x = (x);\
75 __typeof__ (y) _y = (y);\
76 _x > _y ? _x : _y; })
77
78 #undef MIN
79 #define MIN(x,y) ({ __typeof__ (x) _x = (x);\
80 __typeof__ (y) _y = (y);\
81 _x < _y ? _x : _y; })
82
83 #define CMP(x,y) ({ __typeof__ (x) _x = (x);\
84 __typeof__ (y) _y = (y);\
85 (_x > _y) - (_x < _y); })
86
87 #undef ABS
88 #define ABS(x) ((x)>0?(x):-(x))
89
90 #undef XOR
91 #define XOR(x,y) (!(x)!=!(y))
92
93 #undef EQUIV
94 #define EQUIV(x,y) (!(x)==!(y))
95
96 #undef SWAP
97 #define SWAP(x,y) do{ __typeof__ (x) tmp =(x); (x)=(y); (y)=(tmp);}while(0)
98
99
100 #define LIKELY(x) __builtin_expect(!!(x), 1)
101 #define UNLIKELY(x) __builtin_expect(!!(x), 0)
102
103 #define UNUSED(x) (void)(x)
104
105 #define KILO 1024
106 #define MEGA (1024*1024)
107
108
109 /* Convenience function */
110 static __inline__ size_t WriteStr(int fd, const char* msg);
111
112
113 #ifdef PRINT_TSTP_STATUS
114 #define TSTPOUT(file,msg) fprintf(file, "# SZS status %s\n", msg)
115 #define TSTPOUTFD(fd,msg) do{\
116 WriteStr(fd, "# SZS status ");\
117 WriteStr(fd, msg);\
118 WriteStr(fd, "\n");\
119 }while(0)
120 #else
121 #define TSTPOUT(file,msg)
122 #define TSTPOUTFD(fd,msg)
123 #endif
124
125
126 #if __GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)
127 #define GCC_DIAGNOSTIC_POP _Pragma("GCC diagnostic pop")
128 #define GCC_DIAGNOSTIC_PUSH _Pragma("GCC diagnostic push")
129 #else
130 #define GCC_DIAGNOSTIC_POP
131 #define GCC_DIAGNOSTIC_PUSH
132 #endif
133
134 /*-----------------------------------------------------------------------
135 //
136 // Function: WriteStr()
137 //
138 // Computes the length of msg and writes msg to the file descriptor.
139 // WriteStr is used for output instead of the print functions in low
140 // memory situations since the later may try to allocate memory which
141 // is likely to fail. WriteStr is defined as a function instead of a
142 // macro to silence warnings in case the return value of write is
143 // unused. The function write may be defined with warn_unused_result
144 // in the system header files.
145 //
146 // Global Variables: -
147 //
148 // Side Effects : Output
149 //
150 /----------------------------------------------------------------------*/
151
WriteStr(int fd,const char * msg)152 static __inline__ size_t WriteStr(int fd, const char* msg){
153 return write(fd, msg, strlen(msg));
154 }
155
156
157 #endif
158
159 /*---------------------------------------------------------------------*/
160 /* End of File */
161 /*---------------------------------------------------------------------*/
162