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