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