1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_stats.cpp 7 8 Abstract: 9 API for browsing statistics 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-03-07. 14 15 Revision History: 16 17 --*/ 18 #include<iostream> 19 #include "api/z3.h" 20 #include "api/api_log_macros.h" 21 #include "api/api_context.h" 22 #include "api/api_stats.h" 23 24 extern "C" { 25 Z3_stats_to_string(Z3_context c,Z3_stats s)26 Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s) { 27 Z3_TRY; 28 LOG_Z3_stats_to_string(c, s); 29 RESET_ERROR_CODE(); 30 std::ostringstream buffer; 31 to_stats_ref(s).display_smt2(buffer); 32 std::string result = buffer.str(); 33 // Hack for removing the trailing '\n' 34 result = buffer.str(); 35 SASSERT(result.size() > 0); 36 result.resize(result.size()-1); 37 return mk_c(c)->mk_external_string(std::move(result)); 38 Z3_CATCH_RETURN(""); 39 } 40 Z3_stats_inc_ref(Z3_context c,Z3_stats s)41 void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s) { 42 Z3_TRY; 43 LOG_Z3_stats_inc_ref(c, s); 44 RESET_ERROR_CODE(); 45 to_stats(s)->inc_ref(); 46 Z3_CATCH; 47 } 48 Z3_stats_dec_ref(Z3_context c,Z3_stats s)49 void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s) { 50 Z3_TRY; 51 LOG_Z3_stats_dec_ref(c, s); 52 RESET_ERROR_CODE(); 53 to_stats(s)->dec_ref(); 54 Z3_CATCH; 55 } 56 Z3_stats_size(Z3_context c,Z3_stats s)57 unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s) { 58 Z3_TRY; 59 LOG_Z3_stats_size(c, s); 60 RESET_ERROR_CODE(); 61 return to_stats_ref(s).size(); 62 Z3_CATCH_RETURN(0); 63 } 64 Z3_stats_get_key(Z3_context c,Z3_stats s,unsigned idx)65 Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx) { 66 Z3_TRY; 67 LOG_Z3_stats_get_key(c, s, idx); 68 RESET_ERROR_CODE(); 69 if (idx >= to_stats_ref(s).size()) { 70 SET_ERROR_CODE(Z3_IOB, nullptr); 71 return ""; 72 } 73 return to_stats_ref(s).get_key(idx); 74 Z3_CATCH_RETURN(""); 75 } 76 Z3_stats_is_uint(Z3_context c,Z3_stats s,unsigned idx)77 bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx) { 78 Z3_TRY; 79 LOG_Z3_stats_is_uint(c, s, idx); 80 RESET_ERROR_CODE(); 81 if (idx >= to_stats_ref(s).size()) { 82 SET_ERROR_CODE(Z3_IOB, nullptr); 83 return false; 84 } 85 return to_stats_ref(s).is_uint(idx); 86 Z3_CATCH_RETURN(0); 87 } 88 Z3_stats_is_double(Z3_context c,Z3_stats s,unsigned idx)89 bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx) { 90 Z3_TRY; 91 LOG_Z3_stats_is_double(c, s, idx); 92 RESET_ERROR_CODE(); 93 if (idx >= to_stats_ref(s).size()) { 94 SET_ERROR_CODE(Z3_IOB, nullptr); 95 return false; 96 } 97 return !to_stats_ref(s).is_uint(idx); 98 Z3_CATCH_RETURN(false); 99 } 100 Z3_stats_get_uint_value(Z3_context c,Z3_stats s,unsigned idx)101 unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx) { 102 Z3_TRY; 103 LOG_Z3_stats_get_uint_value(c, s, idx); 104 RESET_ERROR_CODE(); 105 if (idx >= to_stats_ref(s).size()) { 106 SET_ERROR_CODE(Z3_IOB, nullptr); 107 return 0; 108 } 109 if (!to_stats_ref(s).is_uint(idx)) { 110 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 111 return 0; 112 } 113 return to_stats_ref(s).get_uint_value(idx); 114 Z3_CATCH_RETURN(0); 115 } 116 Z3_stats_get_double_value(Z3_context c,Z3_stats s,unsigned idx)117 double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx) { 118 Z3_TRY; 119 LOG_Z3_stats_get_double_value(c, s, idx); 120 RESET_ERROR_CODE(); 121 if (idx >= to_stats_ref(s).size()) { 122 SET_ERROR_CODE(Z3_IOB, nullptr); 123 return 0.0; 124 } 125 if (to_stats_ref(s).is_uint(idx)) { 126 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 127 return 0.0; 128 } 129 return to_stats_ref(s).get_double_value(idx); 130 Z3_CATCH_RETURN(0.0); 131 } 132 Z3_get_estimated_alloc_size(void)133 uint64_t Z3_API Z3_get_estimated_alloc_size(void) { 134 return memory::get_allocation_size(); 135 } 136 137 }; 138