z3-src 501.0.1

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    trace.h

Abstract:

    Trace message support.

Author:

    Leonardo de Moura (leonardo) 2006-09-13.

Revision History:

--*/

#pragma once

#include<fstream>
#include<string_view>
#include "trace_tags.h"

#ifdef SINGLE_THREAD
# define is_threaded() false
#else
bool is_threaded();
#endif

#ifdef SINGLE_THREAD
#define LOCK_CODE(CODE) CODE;
#define THREAD_LOCK(CODE) CODE

#else
void verbose_lock();
void verbose_unlock();

#define LOCK_CODE(CODE)                                         \
    {                                                           \
        verbose_lock();                                         \
        CODE;                                                   \
        verbose_unlock();                                       \
    }

#define THREAD_LOCK(CODE) if (is_threaded()) { LOCK_CODE(CODE); } else { CODE; }

#endif



#ifdef _TRACE
extern std::ofstream tout; 
#define TRACE_CODE(CODE) { CODE } ((void) 0 )

void enable_trace(std::string_view tag);
void enable_all_trace(bool flag);
void disable_trace(std::string_view tag);
bool is_trace_enabled(TraceTag tag);
void close_trace();
void open_trace();

#else
#define TRACE_CODE(CODE) ((void) 0)

static inline void enable_trace(std::string_view tag) {}
static inline void enable_all_trace(bool flag) {}
static inline void disable_trace(std::string_view tag) {}
static inline bool is_trace_enabled(TraceTag tag) { return false; }
static inline void close_trace() {}
static inline void open_trace() {}
static inline void finalize_trace() {}
#endif

#define TRACEH(TAG)  tout << "-------- [" << tracetag_to_string(TraceTag::TAG) << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"
#define TRACEEND tout << "------------------------------------------------\n"
#define TRACEBODY(TAG, CODE) TRACEH(TAG); CODE; TRACEEND; tout.flush()
#define STRACEBODY(CODE) CODE; tout.flush()

#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TraceTag::TAG)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })
#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TraceTag::TAG)) { THREAD_LOCK(STRACEBODY(CODE)); })
#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TraceTag::TAG) && (COND)) { THREAD_LOCK(STRACEBODY(CODE)); })
#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TraceTag::TAG) && (COND)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); })