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

Merge pull request #922 from mtrberzi/regex-unroll

Browse source 
add _re.unroll internal operator to seq_decl_plugin
This commit is contained in:
Nikolaj Bjorner 2017-02-27 18:37:37 -08:00 committed by GitHub
parent f8a3a46d44 0ebd93c8b5
commit 4792229c2b
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/seq_decl_plugin.cpp
View file

@ -473,6 +473,7 @@ void seq_decl_plugin::init() {
sort* str2TintT[3] = { strT, strT, intT }; sort* str2TintT[3] = { strT, strT, intT };
sort* seqAintT[2] = { seqA, intT }; sort* seqAintT[2] = { seqA, intT };
sort* seq3A[3] = { seqA, seqA, seqA }; sort* seq3A[3] = { seqA, seqA, seqA };
sort* reTintT[2] = { reT, intT };
m_sigs.resize(LAST_SEQ_OP); m_sigs.resize(LAST_SEQ_OP);
// TBD: have (par ..) construct and load parameterized signature from premable. // TBD: have (par ..) construct and load parameterized signature from premable.
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA);
@ -516,6 +517,7 @@ void seq_decl_plugin::init() {
m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, 0, reT); m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, 0, reT);
m_sigs[_OP_REGEXP_FULL] = alloc(psig, m, "re.allchar", 0, 0, 0, reT); m_sigs[_OP_REGEXP_FULL] = alloc(psig, m, "re.allchar", 0, 0, 0, reT);
m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
m_sigs[_OP_RE_UNROLL] = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT);
} }
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
@ -672,6 +674,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
} }
case _OP_RE_UNROLL:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case OP_STRING_CONST: case OP_STRING_CONST:
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {

2
src/ast/seq_decl_plugin.h
View file

@ -79,6 +79,7 @@ enum seq_op_kind {
_OP_REGEXP_EMPTY, _OP_REGEXP_EMPTY,
_OP_REGEXP_FULL, _OP_REGEXP_FULL,
_OP_SEQ_SKOLEM, _OP_SEQ_SKOLEM,
_OP_RE_UNROLL,
LAST_SEQ_OP LAST_SEQ_OP
}; };
@ -334,6 +335,7 @@ public:
MATCH_UNARY(is_opt); 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, unsigned& hi);
bool is_loop(expr const* n, expr*& body, unsigned& lo); 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; str str;
re re; re re;