1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_ast_map.cpp
7 
8 Abstract:
9     API for creating AST maps
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-03-09.
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_ast_map.h"
23 #include "api/api_ast_vector.h"
24 #include "ast/ast_smt2_pp.h"
25 #include "util/dec_ref_util.h"
26 
~Z3_ast_map_ref()27 Z3_ast_map_ref::~Z3_ast_map_ref() {
28     dec_ref_key_values(m, m_map);
29 }
30 
31 extern "C" {
32 
Z3_mk_ast_map(Z3_context c)33     Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c) {
34         Z3_TRY;
35         LOG_Z3_mk_ast_map(c);
36         RESET_ERROR_CODE();
37         Z3_ast_map_ref * m = alloc(Z3_ast_map_ref, *mk_c(c), mk_c(c)->m());
38         mk_c(c)->save_object(m);
39         Z3_ast_map r       = of_ast_map(m);
40         RETURN_Z3(r);
41         Z3_CATCH_RETURN(nullptr);
42     }
43 
Z3_ast_map_inc_ref(Z3_context c,Z3_ast_map m)44     void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m) {
45         Z3_TRY;
46         LOG_Z3_ast_map_inc_ref(c, m);
47         RESET_ERROR_CODE();
48         to_ast_map(m)->inc_ref();
49         Z3_CATCH;
50     }
51 
Z3_ast_map_dec_ref(Z3_context c,Z3_ast_map m)52     void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m) {
53         Z3_TRY;
54         LOG_Z3_ast_map_dec_ref(c, m);
55         RESET_ERROR_CODE();
56         to_ast_map(m)->dec_ref();
57         Z3_CATCH;
58     }
59 
Z3_ast_map_contains(Z3_context c,Z3_ast_map m,Z3_ast k)60     bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k) {
61         Z3_TRY;
62         LOG_Z3_ast_map_contains(c, m, k);
63         RESET_ERROR_CODE();
64         return to_ast_map_ref(m).contains(to_ast(k));
65         Z3_CATCH_RETURN(false);
66     }
67 
Z3_ast_map_find(Z3_context c,Z3_ast_map m,Z3_ast k)68     Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k) {
69         Z3_TRY;
70         LOG_Z3_ast_map_find(c, m, k);
71         RESET_ERROR_CODE();
72         obj_map<ast, ast*>::obj_map_entry * entry = to_ast_map_ref(m).find_core(to_ast(k));
73         if (entry == nullptr) {
74             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
75             RETURN_Z3(nullptr);
76         }
77         else {
78             ast * r = entry->get_data().m_value;
79             RETURN_Z3(of_ast(r));
80         }
81         Z3_CATCH_RETURN(nullptr);
82     }
83 
Z3_ast_map_insert(Z3_context c,Z3_ast_map m,Z3_ast k,Z3_ast v)84     void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v) {
85         Z3_TRY;
86         LOG_Z3_ast_map_insert(c, m, k, v);
87         RESET_ERROR_CODE();
88         ast_manager & mng = to_ast_map(m)->m;
89         auto& value = to_ast_map_ref(m).insert_if_not_there(to_ast(k), 0);
90         if (!value) {
91             // new entry
92             mng.inc_ref(to_ast(k));
93             mng.inc_ref(to_ast(v));
94             value = to_ast(v);
95         }
96         else {
97             // replacing entry
98             mng.inc_ref(to_ast(v));
99             mng.dec_ref(value);
100             value = to_ast(v);
101         }
102         Z3_CATCH;
103     }
104 
Z3_ast_map_reset(Z3_context c,Z3_ast_map m)105     void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m) {
106         Z3_TRY;
107         LOG_Z3_ast_map_reset(c, m);
108         RESET_ERROR_CODE();
109         dec_ref_key_values(to_ast_map(m)->m, to_ast_map_ref(m));
110         SASSERT(to_ast_map_ref(m).empty());
111         Z3_CATCH;
112     }
113 
Z3_ast_map_erase(Z3_context c,Z3_ast_map m,Z3_ast k)114     void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k) {
115         Z3_TRY;
116         LOG_Z3_ast_map_erase(c, m, k);
117         RESET_ERROR_CODE();
118         ast * v = nullptr;
119         if (to_ast_map_ref(m).find(to_ast(k), v)) {
120             to_ast_map_ref(m).erase(to_ast(k));
121             ast_manager & mng = to_ast_map(m)->m;
122             mng.dec_ref(to_ast(k));
123             mng.dec_ref(v);
124         }
125         Z3_CATCH;
126     }
127 
Z3_ast_map_size(Z3_context c,Z3_ast_map m)128     unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m) {
129         Z3_TRY;
130         LOG_Z3_ast_map_size(c, m);
131         RESET_ERROR_CODE();
132         return to_ast_map_ref(m).size();
133         Z3_CATCH_RETURN(0);
134     }
135 
Z3_ast_map_keys(Z3_context c,Z3_ast_map m)136     Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m) {
137         Z3_TRY;
138         LOG_Z3_ast_map_keys(c, m);
139         RESET_ERROR_CODE();
140         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), to_ast_map(m)->m);
141         mk_c(c)->save_object(v);
142         obj_map<ast, ast*>::iterator it  = to_ast_map_ref(m).begin();
143         obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();
144         for (; it != end; ++it) {
145             v->m_ast_vector.push_back(it->m_key);
146         }
147         Z3_ast_vector r       = of_ast_vector(v);
148         RETURN_Z3(r);
149         Z3_CATCH_RETURN(nullptr);
150     }
151 
Z3_ast_map_to_string(Z3_context c,Z3_ast_map m)152     Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m) {
153         Z3_TRY;
154         LOG_Z3_ast_map_to_string(c, m);
155         RESET_ERROR_CODE();
156         std::ostringstream buffer;
157         ast_manager & mng = to_ast_map(m)->m;
158         buffer << "(ast-map";
159         obj_map<ast, ast*>::iterator it  = to_ast_map_ref(m).begin();
160         obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();
161         for (; it != end; ++it) {
162             buffer << "\n  (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n   " << mk_ismt2_pp(it->m_value, mng, 3) << ")";
163         }
164         buffer << ")";
165         return mk_c(c)->mk_external_string(buffer.str());
166         Z3_CATCH_RETURN(nullptr);
167     }
168 
169 };
170