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

add _re.unroll internal operator to seq_decl_plugin

Browse source
This commit is contained in:
Murphy Berzish 2017-02-23 20:57:19 -05:00
parent e744d0f271
commit 0ebd93c8b5
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/seq_decl_plugin.h
View file

@ -79,6 +79,7 @@ enum seq_op_kind {
_OP_REGEXP_EMPTY,
_OP_REGEXP_FULL,
_OP_SEQ_SKOLEM,
_OP_RE_UNROLL,
LAST_SEQ_OP
};
@ -334,6 +335,7 @@ public:
MATCH_UNARY(is_opt);
bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
bool is_loop(expr const* n, expr*& body, unsigned& lo);
bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
};
str str;
re re;