mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-10 09:15:47 +00:00
Code Activity

theory_str api: concat, length

Browse source
This commit is contained in:
Murphy Berzish 2016-10-20 12:25:52 -04:00
parent ce53b36864
commit d57c92f69e
2 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_str.cpp
View file

@ -77,4 +77,7 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
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);
}; };

13
src/api/z3_api.h
View file

@ -3200,6 +3200,19 @@ extern "C" {
*/ */
Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str); Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str);
/**
\brief Create a string concatenation term.
def_API('Z3_mk_str_concat', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_str_concat(Z3_context c, Z3_ast s1, Z3_ast s2);
/**
\brief Create a string length term. (Integer representation)
def_API('Z3_mk_str_length', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_str_length(Z3_context c, Z3_ast s);
/*@}*/ /*@}*/
/** @name Sequences and regular expressions */ /** @name Sequences and regular expressions */