ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros
profile.hpp File Reference
#include "global.h"
Include dependency graph for profile.hpp:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define NON_CADICAL_QUIET_PROFILE_CODE(CODE)
 
#define START(P)
 
#define STOP(P)
 
#define PROFILE_ACTIVE(P)
 
#define START_SIMPLIFIER(S, M)
 
#define STOP_SIMPLIFIER(S, M)
 
#define START_INNER_WALK()
 
#define STOP_INNER_WALK()
 
#define START_OUTER_WALK()
 
#define STOP_OUTER_WALK()
 

Macro Definition Documentation

◆ NON_CADICAL_QUIET_PROFILE_CODE

#define NON_CADICAL_QUIET_PROFILE_CODE ( CODE)

Definition at line 142 of file profile.hpp.

◆ PROFILE_ACTIVE

#define PROFILE_ACTIVE ( P)
Value:
((internal->profiles.P.level <= internal->opts.profile) && \
(internal->profiles.P.active))

Definition at line 166 of file profile.hpp.

166#define PROFILE_ACTIVE(P) \
167 ((internal->profiles.P.level <= internal->opts.profile) && \
168 (internal->profiles.P.active))

◆ START

#define START ( P)
Value:
do { \
NON_CADICAL_QUIET_PROFILE_CODE ( \
if (internal->profiles.P.level <= internal->opts.profile) \
internal->start_profiling (internal->profiles.P, \
internal->time ());) \
} while (0)

Definition at line 150 of file profile.hpp.

150#define START(P) \
151 do { \
152 NON_CADICAL_QUIET_PROFILE_CODE ( \
153 if (internal->profiles.P.level <= internal->opts.profile) \
154 internal->start_profiling (internal->profiles.P, \
155 internal->time ());) \
156 } while (0)

◆ START_INNER_WALK

#define START_INNER_WALK ( )
Value:
do { \
require_mode (SEARCH); \
CADICAL_assert (!preprocessing); \
NON_CADICAL_QUIET_PROFILE_CODE ( \
const double N = time (); const int L = internal->opts.profile; \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.walk.level <= L) \
internal->start_profiling (internal->profiles.walk, N);) \
set_mode (WALK); \
} while (0)

Definition at line 222 of file profile.hpp.

222#define START_INNER_WALK() \
223 do { \
224 require_mode (SEARCH); \
225 CADICAL_assert (!preprocessing); \
226 NON_CADICAL_QUIET_PROFILE_CODE ( \
227 const double N = time (); const int L = internal->opts.profile; \
228 if (stable && internal->profiles.stable.level <= L) \
229 internal->stop_profiling (internal->profiles.stable, N); \
230 if (!stable && internal->profiles.unstable.level <= L) \
231 internal->stop_profiling (internal->profiles.unstable, N); \
232 if (internal->profiles.walk.level <= L) \
233 internal->start_profiling (internal->profiles.walk, N);) \
234 set_mode (WALK); \
235 } while (0)

◆ START_OUTER_WALK

#define START_OUTER_WALK ( )
Value:
do { \
require_mode (SEARCH); \
CADICAL_assert (!preprocessing); \
NON_CADICAL_QUIET_PROFILE_CODE (START (walk);) \
set_mode (WALK); \
} while (0)
START
#define START(P)
Definition profile.hpp:150

Definition at line 259 of file profile.hpp.

259#define START_OUTER_WALK() \
260 do { \
261 require_mode (SEARCH); \
262 CADICAL_assert (!preprocessing); \
263 NON_CADICAL_QUIET_PROFILE_CODE (START (walk);) \
264 set_mode (WALK); \
265 } while (0)

◆ START_SIMPLIFIER

#define START_SIMPLIFIER ( S,
M )
Value:
do { \
NON_CADICAL_QUIET_PROFILE_CODE (const double N = time (); \
const int L = internal->opts.profile;) \
if (!preprocessing && !lookingahead) { \
NON_CADICAL_QUIET_PROFILE_CODE ( \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.search.level <= L) \
internal->stop_profiling (internal->profiles.search, N);) \
reset_mode (SEARCH); \
} \
NON_CADICAL_QUIET_PROFILE_CODE ( \
if (internal->profiles.simplify.level <= L) \
internal->start_profiling (internal->profiles.simplify, N); \
if (internal->profiles.S.level <= L) \
internal->start_profiling (internal->profiles.S, N);) \
set_mode (SIMPLIFY); \
set_mode (M); \
} while (0)
M
word M(word f1, word f2, int n)
Definition kitPerm.c:240
if
if(last==0)
Definition sparse_int.h:34

Definition at line 172 of file profile.hpp.

172#define START_SIMPLIFIER(S, M) \
173 do { \
174 NON_CADICAL_QUIET_PROFILE_CODE (const double N = time (); \
175 const int L = internal->opts.profile;) \
176 if (!preprocessing && !lookingahead) { \
177 NON_CADICAL_QUIET_PROFILE_CODE ( \
178 if (stable && internal->profiles.stable.level <= L) \
179 internal->stop_profiling (internal->profiles.stable, N); \
180 if (!stable && internal->profiles.unstable.level <= L) \
181 internal->stop_profiling (internal->profiles.unstable, N); \
182 if (internal->profiles.search.level <= L) \
183 internal->stop_profiling (internal->profiles.search, N);) \
184 reset_mode (SEARCH); \
185 } \
186 NON_CADICAL_QUIET_PROFILE_CODE ( \
187 if (internal->profiles.simplify.level <= L) \
188 internal->start_profiling (internal->profiles.simplify, N); \
189 if (internal->profiles.S.level <= L) \
190 internal->start_profiling (internal->profiles.S, N);) \
191 set_mode (SIMPLIFY); \
192 set_mode (M); \
193 } while (0)

◆ STOP

#define STOP ( P)
Value:
do { \
NON_CADICAL_QUIET_PROFILE_CODE ( \
if (internal->profiles.P.level <= internal->opts.profile) \
internal->stop_profiling (internal->profiles.P, \
internal->time ());) \
} while (0)

Definition at line 158 of file profile.hpp.

158#define STOP(P) \
159 do { \
160 NON_CADICAL_QUIET_PROFILE_CODE ( \
161 if (internal->profiles.P.level <= internal->opts.profile) \
162 internal->stop_profiling (internal->profiles.P, \
163 internal->time ());) \
164 } while (0)

◆ STOP_INNER_WALK

#define STOP_INNER_WALK ( )
Value:
do { \
require_mode (SEARCH); \
CADICAL_assert (!preprocessing); \
reset_mode (WALK); \
NON_CADICAL_QUIET_PROFILE_CODE ( \
const double N = time (); const int L = internal->opts.profile; \
if (internal->profiles.walk.level <= L) \
internal->stop_profiling (internal->profiles.walk, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N); \
internal->profiles.walk.started = (N);) \
} while (0)

Definition at line 240 of file profile.hpp.

240#define STOP_INNER_WALK() \
241 do { \
242 require_mode (SEARCH); \
243 CADICAL_assert (!preprocessing); \
244 reset_mode (WALK); \
245 NON_CADICAL_QUIET_PROFILE_CODE ( \
246 const double N = time (); const int L = internal->opts.profile; \
247 if (internal->profiles.walk.level <= L) \
248 internal->stop_profiling (internal->profiles.walk, N); \
249 if (stable && internal->profiles.stable.level <= L) \
250 internal->start_profiling (internal->profiles.stable, N); \
251 if (!stable && internal->profiles.unstable.level <= L) \
252 internal->start_profiling (internal->profiles.unstable, N); \
253 internal->profiles.walk.started = (N);) \
254 } while (0)

◆ STOP_OUTER_WALK

#define STOP_OUTER_WALK ( )
Value:
do { \
require_mode (SEARCH); \
CADICAL_assert (!preprocessing); \
reset_mode (WALK); \
NON_CADICAL_QUIET_PROFILE_CODE (STOP (walk);) \
} while (0)
STOP
#define STOP(P)
Definition profile.hpp:158

Definition at line 270 of file profile.hpp.

270#define STOP_OUTER_WALK() \
271 do { \
272 require_mode (SEARCH); \
273 CADICAL_assert (!preprocessing); \
274 reset_mode (WALK); \
275 NON_CADICAL_QUIET_PROFILE_CODE (STOP (walk);) \
276 } while (0)

◆ STOP_SIMPLIFIER

#define STOP_SIMPLIFIER ( S,
M )
Value:
do { \
NON_CADICAL_QUIET_PROFILE_CODE ( \
const double N = time (); const int L = internal->opts.profile; \
if (internal->profiles.S.level <= L) \
internal->stop_profiling (internal->profiles.S, N); \
if (internal->profiles.simplify.level <= L) \
internal->stop_profiling (internal->profiles.simplify, N);) \
reset_mode (M); \
reset_mode (SIMPLIFY); \
if (!preprocessing && !lookingahead) { \
NON_CADICAL_QUIET_PROFILE_CODE ( \
if (internal->profiles.search.level <= L) \
internal->start_profiling (internal->profiles.search, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N);) \
set_mode (SEARCH); \
} \
} while (0)

Definition at line 197 of file profile.hpp.

197#define STOP_SIMPLIFIER(S, M) \
198 do { \
199 NON_CADICAL_QUIET_PROFILE_CODE ( \
200 const double N = time (); const int L = internal->opts.profile; \
201 if (internal->profiles.S.level <= L) \
202 internal->stop_profiling (internal->profiles.S, N); \
203 if (internal->profiles.simplify.level <= L) \
204 internal->stop_profiling (internal->profiles.simplify, N);) \
205 reset_mode (M); \
206 reset_mode (SIMPLIFY); \
207 if (!preprocessing && !lookingahead) { \
208 NON_CADICAL_QUIET_PROFILE_CODE ( \
209 if (internal->profiles.search.level <= L) \
210 internal->start_profiling (internal->profiles.search, N); \
211 if (stable && internal->profiles.stable.level <= L) \
212 internal->start_profiling (internal->profiles.stable, N); \
213 if (!stable && internal->profiles.unstable.level <= L) \
214 internal->start_profiling (internal->profiles.unstable, N);) \
215 set_mode (SEARCH); \
216 } \
217 } while (0)