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_escaped21struct 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()24static void __declspec(noinline) R() { *g_z3_log << "R\n"; g_z3_log->flush(); } P(void * obj)25static void __declspec(noinline) P(void * obj) { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); } I(int64_t i)26static void __declspec(noinline) I(int64_t i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } U(uint64_t u)27static void __declspec(noinline) U(uint64_t u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } D(double d)28static void __declspec(noinline) D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } S(Z3_string str)29static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } Sy(Z3_symbol sym)30static 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)43static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); } Au(unsigned sz)44static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); } Ai(unsigned sz)45static void __declspec(noinline) Ai(unsigned sz) { *g_z3_log << "i " << sz << "\n"; g_z3_log->flush(); } Asy(unsigned sz)46static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); } C(unsigned id)47static void __declspec(noinline) C(unsigned id) { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); } _Z3_append_log(char const * msg)48void __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