1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     z3_logger.h
7 
8 Abstract:
9 
10     Goodies for log generation
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2011-09-22
15 
16 Notes:
17 
18 --*/
19 #include<iostream>
20 #include "util/symbol.h"
ll_escapedll_escaped21 struct ll_escaped { char const * m_str; ll_escaped(char const * str):m_str(str) {} };
22 static std::ostream & operator<<(std::ostream & out, ll_escaped const & d);
23 
R()24 static void __declspec(noinline) R()  { *g_z3_log << "R\n"; g_z3_log->flush(); }
P(void * obj)25 static void __declspec(noinline) P(void * obj)  { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); }
I(int64_t i)26 static void __declspec(noinline) I(int64_t i)   { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); }
U(uint64_t u)27 static void __declspec(noinline) U(uint64_t u)   { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); }
D(double d)28 static void __declspec(noinline) D(double d)   { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); }
S(Z3_string str)29 static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); }
Sy(Z3_symbol sym)30 static void __declspec(noinline) Sy(Z3_symbol sym) {
31     symbol s = symbol::c_api_ext2symbol(sym);
32     if (s.is_null()) {
33         *g_z3_log << "N\n";
34     }
35     else if (s.is_numerical()) {
36         *g_z3_log << "# " << s.get_num() << "\n";
37     }
38     else {
39         *g_z3_log << "$ |" << ll_escaped(s.bare_str()) << "|\n";
40     }
41     g_z3_log->flush();
42 }
Ap(unsigned sz)43 static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); }
Au(unsigned sz)44 static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); }
Ai(unsigned sz)45 static void __declspec(noinline) Ai(unsigned sz) { *g_z3_log << "i " << sz << "\n"; g_z3_log->flush(); }
Asy(unsigned sz)46 static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); }
C(unsigned id)47 static void __declspec(noinline) C(unsigned id)   { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); }
_Z3_append_log(char const * msg)48 void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); }
49 
50 static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
51     char const * s = d.m_str;
52     while (*s) {
53         unsigned char c = *s;
54         if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') ||
55             c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' ||
56             c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' ||
57             c == '<' || c == '>') {
58             out << c;
59         }
60         else {
61             unsigned char str[4] = {'0', '0', '0', 0};
62             str[2] = '0' + (c % 10);
63             c /= 10;
64             str[1] = '0' + (c % 10);
65             c /= 10;
66             str[0] = '0' + c;
67             out << '\\' << str;
68         }
69         s++;
70     }
71     return out;
72 }
73