mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

theory_str high-level and regex API

Browse source
This commit is contained in:
Murphy Berzish 2016-10-20 15:36:54 -04:00
parent d57c92f69e
commit 05dfa5509a
2 changed files with 162 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
src/api/api_str.cpp
View file

@ -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);
}
};

84
src/api/z3_api.h
View file

@ -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);
/*@}*/