z3-src 503.2.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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    api_log.cpp

Abstract:
    API for creating logs

Author:

    Leonardo de Moura (leonardo) 2012-02-29.

Revision History:

--*/
#include<fstream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/z3_logger.h"
#include "util/util.h"
#include "util/z3_version.h"
#include "util/mutex.h"

static std::ostream * g_z3_log = nullptr;
atomic<bool> g_z3_log_enabled;

#ifdef Z3_LOG_SYNC
static mutex g_log_mux;
#define SCOPED_LOCK() lock_guard lock(g_log_mux)
#else
#define SCOPED_LOCK() {}
#endif

// functions called from api_log_macros.*
void SetR(const void * obj) {
    *g_z3_log << "= " << obj << '\n';
}

void SetO(void * obj, unsigned pos) {
    *g_z3_log << "* " << obj << ' ' << pos << '\n';
}

void SetAO(void * obj, unsigned pos, unsigned idx) {
    *g_z3_log << "@ " << obj << ' ' << pos << ' ' << idx << '\n';
}

namespace {
struct ll_escaped { char const * m_str; };
std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
    char const * s = d.m_str;
    while (*s) {
        unsigned char c = *s;
        if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') ||
            c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' ||
            c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' ||
            c == '<' || c == '>') {
            out << c;
        }
        else {
            unsigned char str[4] = {'0', '0', '0', 0};
            str[2] = '0' + (c % 10);
            c /= 10;
            str[1] = '0' + (c % 10);
            c /= 10;
            str[0] = '0' + c;
            out << '\\' << str;
        }
        s++;
    }
    return out;
}
}

void R()              { *g_z3_log << 'R' << std::endl; }
void P(void * obj)    { *g_z3_log << "P " << obj <<std::endl; }
void I(int64_t i)     { *g_z3_log << "I " << i << std::endl; }
void U(uint64_t u)    { *g_z3_log << "U " << u << std::endl; }
void D(double d)      { *g_z3_log << "D " << d << std::endl; }
void S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped{str} << '"' << std::endl; }
void Sy(Z3_symbol sym) {
    symbol s = symbol::c_api_ext2symbol(sym);
    if (s.is_null()) {
        *g_z3_log << 'N';
    }
    else if (s.is_numerical()) {
        *g_z3_log << "# " << s.get_num();
    }
    else {
        *g_z3_log << "$ |" << ll_escaped{s.str().c_str()} << '|';
    }
    *g_z3_log << std::endl;
}
void Ap(unsigned sz)  { *g_z3_log << "p " << sz << std::endl; }
void Au(unsigned sz)  { *g_z3_log << "u " << sz << std::endl; }
void Ai(unsigned sz)  { *g_z3_log << "i " << sz << std::endl; }
void Asy(unsigned sz) { *g_z3_log << "s " << sz << std::endl; }
void C(unsigned id)   { *g_z3_log << "C " << id << std::endl; }
static void _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped{msg} << '"' << std::endl; }

void ctx_enable_logging() {
    SCOPED_LOCK();
    if (g_z3_log != nullptr)
        g_z3_log_enabled = true;
}

static void Z3_close_log_unsafe(void) {
    if (g_z3_log != nullptr) {
        g_z3_log_enabled = false;
        dealloc(g_z3_log);
        g_z3_log = nullptr;
    }
}

extern "C" {
    bool Z3_API Z3_open_log(Z3_string filename) {
        bool res;

        SCOPED_LOCK();
        Z3_close_log_unsafe();

        g_z3_log = alloc(std::ofstream, filename);
        if (g_z3_log->bad() || g_z3_log->fail()) {
            dealloc(g_z3_log);
            g_z3_log = nullptr;
            res = false;
        }
        else {
            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << '"' << std::endl;
            res = true;
        }

        g_z3_log_enabled = res;
        return res;
    }

    void Z3_API Z3_append_log(Z3_string str) {
        if (!g_z3_log_enabled)
            return;
        SCOPED_LOCK();
        if (g_z3_log != nullptr)
            _Z3_append_log(static_cast<char const *>(str));
    }

    void Z3_API Z3_close_log(void) {
        SCOPED_LOCK();
        Z3_close_log_unsafe();
    }
}