From 05dfa5509a0263f48a29e33bf2ebc24a9590b472 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 20 Oct 2016 15:36:54 -0400 Subject: [PATCH] theory_str high-level and regex API --- src/api/api_str.cpp | 78 +++++++++++++++++++++++++++++++++++++++++ src/api/z3_api.h | 84 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 162 insertions(+) diff --git a/src/api/api_str.cpp b/src/api/api_str.cpp index e28c6a501..1a1debb5b 100644 --- a/src/api/api_str.cpp +++ b/src/api/api_str.cpp @@ -79,5 +79,83 @@ extern "C" { MK_BINARY(Z3_mk_str_concat, mk_c(c)->get_str_fid(), OP_STRCAT, SKIP); MK_UNARY(Z3_mk_str_length, mk_c(c)->get_str_fid(), OP_STRLEN, SKIP); + MK_BINARY(Z3_mk_str_at, mk_c(c)->get_str_fid(), OP_STR_CHARAT, SKIP); + // translate prefixof/suffixof to StartsWith/EndsWith + // TODO string standardization might just remove StartsWith/EndsWith in future + Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full) { + LOG_Z3_mk_str_prefixof(c, pre, full); + Z3_TRY; + RESET_ERROR_CODE(); + expr * args[2] = { to_expr(full), to_expr(pre) }; // reverse args + ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_STARTSWITH, 0, 0, 2, args); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_str_suffixof(Z3_context c, Z3_ast suf, Z3_ast full) { + LOG_Z3_mk_str_suffixof(c, suf, full); + Z3_TRY; + RESET_ERROR_CODE(); + expr * args[2] = { to_expr(full), to_expr(suf) }; // reverse args + ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_ENDSWITH, 0, 0, 2, args); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + MK_BINARY(Z3_mk_str_contains, mk_c(c)->get_str_fid(), OP_STR_CONTAINS, SKIP); + MK_TERNARY(Z3_mk_str_indexof, mk_c(c)->get_str_fid(), OP_STR_INDEXOF, SKIP); + MK_TERNARY(Z3_mk_str_substr, mk_c(c)->get_str_fid(), OP_STR_SUBSTR, SKIP); + MK_TERNARY(Z3_mk_str_replace, mk_c(c)->get_str_fid(), OP_STR_REPLACE, SKIP); + + Z3_ast Z3_API Z3_mk_str_to_regex(Z3_context c, Z3_string str) { + LOG_Z3_mk_str_to_regex(c, str); + Z3_TRY; + RESET_ERROR_CODE(); + std::string s(str); + app * a = mk_c(c)->strutil().mk_string(str); + mk_c(c)->save_ast_trail(a); + + expr * args[1] = { to_expr(a) }; + ast * re = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_STR2REGEX, 0, 0, 1, args); + mk_c(c)->save_ast_trail(re); + check_sorts(c, re); + RETURN_Z3(of_ast(re)); + Z3_CATCH_RETURN(0); + } + + MK_BINARY(Z3_mk_str_in_regex, mk_c(c)->get_str_fid(), OP_RE_REGEXIN, SKIP); + MK_BINARY(Z3_mk_regex_concat, mk_c(c)->get_str_fid(), OP_RE_REGEXCONCAT, SKIP); + MK_BINARY(Z3_mk_regex_union, mk_c(c)->get_str_fid(), OP_RE_REGEXUNION, SKIP); + MK_UNARY(Z3_mk_regex_star, mk_c(c)->get_str_fid(), OP_RE_REGEXSTAR, SKIP); + MK_UNARY(Z3_mk_regex_plus, mk_c(c)->get_str_fid(), OP_RE_REGEXPLUS, SKIP); + + Z3_ast Z3_API Z3_mk_regex_range(Z3_context c, Z3_string start, Z3_string end) { + LOG_Z3_mk_regex_range(c, start, end); + Z3_TRY; + RESET_ERROR_CODE(); + + std::string cStart(start); + std::string cEnd(end); + if(cStart.length() != 1 || cEnd.length() != 1) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + + app * a1 = mk_c(c)->strutil().mk_string(cStart); + mk_c(c)->save_ast_trail(a1); + app * a2 = mk_c(c)->strutil().mk_string(cEnd); + mk_c(c)->save_ast_trail(a2); + + expr * args[2] = { to_expr(a1), to_expr(a2) }; + ast * range = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_REGEXCHARRANGE, 0, 0, 2, args); + mk_c(c)->save_ast_trail(range); + check_sorts(c, range); + RETURN_Z3(of_ast(range)); + + Z3_CATCH_RETURN(0); + } }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index c938678d6..7494bcb17 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3212,6 +3212,90 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_str_length(Z3_context c, Z3_ast s); + /** + \brief Create 'character at index' term. + def_API('Z3_mk_str_at', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_at(Z3_context c, Z3_ast s, Z3_ast idx); + + /** + \brief Create 'str.prefixof' term. + def_API('Z3_mk_str_prefixof', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full); + + /** + \brief Create 'str.suffixof' term. + def_API('Z3_mk_str_suffixof', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_suffixof(Z3_context c, Z3_ast suf, Z3_ast full); + + /** + \brief Create 'str.contains' term. + def_API('Z3_mk_str_contains', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_contains(Z3_context c, Z3_ast needle, Z3_ast haystack); + + /** + \brief Create 'str.indexof' term. + def_API('Z3_mk_str_indexof', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_indexof(Z3_context c, Z3_ast haystack, Z3_ast needle, Z3_ast start); + + /** + \brief Create 'str.substr' term. + def_API('Z3_mk_str_substr', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_substr(Z3_context c, Z3_ast s, Z3_ast start, Z3_ast count); + + /** + \brief Create 'str.replace' term. + def_API('Z3_mk_str_replace', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_replace(Z3_context c, Z3_ast base, Z3_ast target, Z3_ast replacement); + + + /** + \brief Create a regular expression that matches the given string constant. + def_API('Z3_mk_str_to_regex', AST, (_in(CONTEXT), _in(STRING))) + */ + Z3_ast Z3_API Z3_mk_str_to_regex(Z3_context c, Z3_string str); + + /** + \brief Create a regular expression membership predicate. + def_API('Z3_mk_str_in_regex', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_in_regex(Z3_context c, Z3_ast str, Z3_ast regex); + + /** + \brief Create a regex concatenation term. + def_API('Z3_mk_regex_concat', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_regex_concat(Z3_context c, Z3_ast r1, Z3_ast r2); + + /** + \brief Create a regex union term. + def_API('Z3_mk_regex_union', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_regex_union(Z3_context c, Z3_ast r1, Z3_ast r2); + + /** + \brief Create a regex Kleene star term. + def_API('Z3_mk_regex_star', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_regex_star(Z3_context c, Z3_ast r); + + /** + \brief Create a regex plus term. + def_API('Z3_mk_regex_plus', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_regex_plus(Z3_context c, Z3_ast r); + + /** + \brief Create a regex character range term. + def_API('Z3_mk_regex_range', AST, (_in(CONTEXT), _in(STRING), _in(STRING))) + */ + Z3_ast Z3_API Z3_mk_regex_range(Z3_context c, Z3_string start, Z3_string end); /*@}*/