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