mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

expose operator kinds for internal functions using their sequence variants. Issue #1051

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-01 09:32:17 -07:00
parent 1fa60f4893
commit fda59f5a24
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_ast.cpp
View file

@ -1124,6 +1124,20 @@ extern "C" {
case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET;
case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;