mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

add rewrites for #2575

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-20 02:16:22 -07:00
parent 78ed71b8de
commit 12034df11a
3 changed files with 70 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.h
View file

@ -366,6 +366,8 @@ public:
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
app* mk_loop(expr* r, unsigned lo);
app* mk_loop(expr* r, unsigned lo, unsigned hi);
app* mk_loop(expr* r, expr* lo);
app* mk_loop(expr* r, expr* lo, expr* hi);
app* mk_full_char(sort* s);
app* mk_full_seq(sort* s);
app* mk_empty(sort* s);
@ -394,6 +396,8 @@ 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_loop(expr const* n, expr*& body, expr*& lo, expr*& hi);
bool is_loop(expr const* n, expr*& body, expr*& lo);
bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
};
str str;