1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3 
4 Module Name:
5 
6     api_seq.cpp
7 
8 Abstract:
9 
10     API for sequences and regular expressions.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2016-01-02.
15 
16 Revision History:
17 
18 --*/
19 #include "api/z3.h"
20 #include "api/api_log_macros.h"
21 #include "api/api_context.h"
22 #include "api/api_util.h"
23 #include "ast/ast_pp.h"
24 
25 extern "C" {
26 
Z3_mk_seq_sort(Z3_context c,Z3_sort domain)27     Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort domain) {
28         Z3_TRY;
29         LOG_Z3_mk_seq_sort(c, domain);
30         RESET_ERROR_CODE();
31         sort * ty =  mk_c(c)->sutil().str.mk_seq(to_sort(domain));
32         mk_c(c)->save_ast_trail(ty);
33         RETURN_Z3(of_sort(ty));
34         Z3_CATCH_RETURN(nullptr);
35     }
36 
Z3_mk_re_sort(Z3_context c,Z3_sort domain)37     Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) {
38         Z3_TRY;
39         LOG_Z3_mk_re_sort(c, domain);
40         RESET_ERROR_CODE();
41         sort * ty =  mk_c(c)->sutil().re.mk_re(to_sort(domain));
42         mk_c(c)->save_ast_trail(ty);
43         RETURN_Z3(of_sort(ty));
44         Z3_CATCH_RETURN(nullptr);
45     }
46 
Z3_mk_string(Z3_context c,Z3_string str)47     Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) {
48         Z3_TRY;
49         LOG_Z3_mk_string(c, str);
50         RESET_ERROR_CODE();
51         zstring s(str);
52         app* a = mk_c(c)->sutil().str.mk_string(s);
53         mk_c(c)->save_ast_trail(a);
54         RETURN_Z3(of_ast(a));
55         Z3_CATCH_RETURN(nullptr);
56     }
57 
58 
Z3_mk_lstring(Z3_context c,unsigned sz,Z3_string str)59     Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned sz, Z3_string str) {
60         Z3_TRY;
61         LOG_Z3_mk_string(c, str);
62         RESET_ERROR_CODE();
63         unsigned_vector chs;
64         for (unsigned i = 0; i < sz; ++i) chs.push_back(str[i]);
65         zstring s(sz, chs.c_ptr());
66         app* a = mk_c(c)->sutil().str.mk_string(s);
67         mk_c(c)->save_ast_trail(a);
68         RETURN_Z3(of_ast(a));
69         Z3_CATCH_RETURN(nullptr);
70     }
71 
Z3_mk_string_sort(Z3_context c)72     Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) {
73         Z3_TRY;
74         LOG_Z3_mk_string_sort(c);
75         RESET_ERROR_CODE();
76         sort* ty = mk_c(c)->sutil().str.mk_string_sort();
77         mk_c(c)->save_ast_trail(ty);
78         RETURN_Z3(of_sort(ty));
79         Z3_CATCH_RETURN(nullptr);
80     }
81 
Z3_is_seq_sort(Z3_context c,Z3_sort s)82     bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
83         Z3_TRY;
84         LOG_Z3_is_seq_sort(c, s);
85         RESET_ERROR_CODE();
86         return mk_c(c)->sutil().is_seq(to_sort(s));
87         Z3_CATCH_RETURN(false);
88     }
89 
Z3_is_re_sort(Z3_context c,Z3_sort s)90     bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) {
91         Z3_TRY;
92         LOG_Z3_is_re_sort(c, s);
93         RESET_ERROR_CODE();
94         return mk_c(c)->sutil().is_re(to_sort(s));
95         Z3_CATCH_RETURN(false);
96     }
97 
Z3_get_seq_sort_basis(Z3_context c,Z3_sort s)98     Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s) {
99         Z3_TRY;
100         LOG_Z3_get_seq_sort_basis(c, s);
101         RESET_ERROR_CODE();
102         sort* r = nullptr;
103         if (!mk_c(c)->sutil().is_seq(to_sort(s), r)) {
104             SET_ERROR_CODE(Z3_INVALID_ARG, "expected sequence sort");
105             RETURN_Z3(nullptr);
106         }
107         RETURN_Z3(of_sort(r));
108         Z3_CATCH_RETURN(nullptr);
109     }
110 
Z3_get_re_sort_basis(Z3_context c,Z3_sort s)111     Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s) {
112         Z3_TRY;
113         LOG_Z3_get_re_sort_basis(c, s);
114         RESET_ERROR_CODE();
115         sort* r = nullptr;
116         if (!mk_c(c)->sutil().is_re(to_sort(s), r)) {
117             SET_ERROR_CODE(Z3_INVALID_ARG, "expected regex sort");
118             RETURN_Z3(nullptr);
119         }
120         RETURN_Z3(of_sort(r));
121         Z3_CATCH_RETURN(nullptr);
122     }
123 
Z3_is_string_sort(Z3_context c,Z3_sort s)124     bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
125         Z3_TRY;
126         LOG_Z3_is_string_sort(c, s);
127         RESET_ERROR_CODE();
128         return mk_c(c)->sutil().is_string(to_sort(s));
129         Z3_CATCH_RETURN(false);
130     }
131 
Z3_is_string(Z3_context c,Z3_ast s)132     bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) {
133         Z3_TRY;
134         LOG_Z3_is_string(c, s);
135         RESET_ERROR_CODE();
136         return mk_c(c)->sutil().str.is_string(to_expr(s));
137         Z3_CATCH_RETURN(false);
138     }
139 
Z3_get_string(Z3_context c,Z3_ast s)140     Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s) {
141         Z3_TRY;
142         LOG_Z3_get_string(c, s);
143         RESET_ERROR_CODE();
144         zstring str;
145         if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
146             SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
147             return "";
148         }
149         return mk_c(c)->mk_external_string(str.encode());
150         Z3_CATCH_RETURN("");
151     }
152 
Z3_get_lstring(Z3_context c,Z3_ast s,unsigned * length)153     Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) {
154         Z3_TRY;
155         LOG_Z3_get_lstring(c, s, length);
156         RESET_ERROR_CODE();
157         zstring str;
158         if (!length) {
159             SET_ERROR_CODE(Z3_INVALID_ARG, "length argument is null");
160             return "";
161         }
162         if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
163             SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
164             return "";
165         }
166         auto& buffer = mk_c(c)->m_char_buffer;
167         buffer.reset();
168         svector<char> buff;
169         for (unsigned i = 0; i < str.length(); ++i) {
170             unsigned ch = str[i];
171             if (ch >= 256) {
172                 buff.reset();
173                 buffer.push_back('\\');
174                 buffer.push_back('\\');  // possibly replace by native non-escaped version?
175                 buffer.push_back('u');
176                 buffer.push_back('{');
177                 while (ch > 0) {
178                     buff.push_back('0' + (ch & 0xF));
179                     ch /= 16;
180                 }
181                 for (unsigned j = buff.size(); j-- > 0; ) {
182                     buffer.push_back(buff[j]);
183                 }
184                 buffer.push_back('}');
185             }
186             else {
187                 buffer.push_back((char)ch);
188             }
189         }
190         *length = buffer.size();
191         return buffer.c_ptr();
192         Z3_CATCH_RETURN("");
193     }
194 
195 #define MK_SORTED(NAME, FN )                                    \
196     Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) {               \
197     Z3_TRY;                                                     \
198     LOG_ ## NAME(c, s);                                         \
199     RESET_ERROR_CODE();                                         \
200     app* a = FN(to_sort(s));                                    \
201     mk_c(c)->save_ast_trail(a);                                 \
202     RETURN_Z3(of_ast(a));                                       \
203     Z3_CATCH_RETURN(0);                                         \
204     }
205 
206     MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty);
207 
208     MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP);
209     MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP);
210     MK_BINARY(Z3_mk_seq_prefix, mk_c(c)->get_seq_fid(), OP_SEQ_PREFIX, SKIP);
211     MK_BINARY(Z3_mk_seq_suffix, mk_c(c)->get_seq_fid(), OP_SEQ_SUFFIX, SKIP);
212     MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP);
213     MK_BINARY(Z3_mk_str_lt, mk_c(c)->get_seq_fid(), OP_STRING_LT, SKIP);
214     MK_BINARY(Z3_mk_str_le, mk_c(c)->get_seq_fid(), OP_STRING_LE, SKIP);
215 
216     MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
217     MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
218     MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
219     MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_NTH, SKIP);
220     MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);
221     MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP);
222     MK_BINARY(Z3_mk_seq_last_index, mk_c(c)->get_seq_fid(), OP_SEQ_LAST_INDEX, SKIP);
223     MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
224     MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
225 
226     MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
227     MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP);
228 
229 
Z3_mk_re_loop(Z3_context c,Z3_ast r,unsigned lo,unsigned hi)230     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
231         Z3_TRY;
232         LOG_Z3_mk_re_loop(c, r, lo, hi);
233         RESET_ERROR_CODE();
234         app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi);
235         mk_c(c)->save_ast_trail(a);
236         RETURN_Z3(of_ast(a));
237         Z3_CATCH_RETURN(nullptr);
238     }
239 
240     MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);
241     MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
242     MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
243     MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_COMPLEMENT, SKIP);
244     MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
245     MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP);
246     MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
247     MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP);
248 
249     MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty);
250     MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
251 
252 
253 
254 };
255