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

pin expressions

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-16 19:41:32 -08:00
parent 6cc9aa3562
commit 4e82a9af5f
1 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_rewriter.cpp
View file

@ -3326,8 +3326,9 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond)
} }
expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
VERIFY(m_util.is_re(r1)); expr_ref _r1(r1, m), _r2(r2, m);
VERIFY(m_util.is_re(r2)); ASSERT(m_util.is_re(r1));
ASSERT(m_util.is_re(r2));
expr_ref result(m()); expr_ref result(m());
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); }; std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); }; std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); };
@ -3345,8 +3346,9 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
} }
expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
VERIFY(m_util.is_re(r1)); expr_ref _r1(r1, m), _r2(r2, m);
VERIFY(m_util.is_re(r2)); ASSERT(m_util.is_re(r1));
ASSERT(m_util.is_re(r2));
expr_ref result(m()); expr_ref result(m());
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); };
@ -3380,7 +3382,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
expr_ref_vector prefix(m()); expr_ref_vector prefix(m());
expr* a, * ar, * ar1, * b, * br, * br1; expr* a, * ar, * ar1, * b, * br, * br1;
VERIFY(m_util.is_re(r1, seq_sort)); VERIFY(m_util.is_re(r1, seq_sort));
VERIFY(m_util.is_re(r2)); ASSERT(m_util.is_re(r2));
SASSERT(r2->get_sort() == r1->get_sort()); SASSERT(r2->get_sort() == r1->get_sort());
// Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1 // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1
auto compare = [&](expr* x, expr* y) { auto compare = [&](expr* x, expr* y) {
@ -3393,7 +3395,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); xid = (re().is_complement(x, z) ? z->get_id() : x->get_id());
yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); yid = (re().is_complement(y, z) ? z->get_id() : y->get_id());
VERIFY(xid != yid); ASSERT(xid != yid);
return (xid < yid ? -1 : 1); return (xid < yid ? -1 : 1);
}; };
auto composeresult = [&](expr* suffix) { auto composeresult = [&](expr* suffix) {
@ -3942,7 +3944,7 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) {
*/ */
expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) { expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) {
STRACE("seq_verbose", tout << "mk_der_cond: " STRACE("seq_verbose", tout << "mk_der_cond: "
<< mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;); << mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;);
sort *ele_sort = nullptr; sort *ele_sort = nullptr;
VERIFY(u().is_seq(seq_sort, ele_sort)); VERIFY(u().is_seq(seq_sort, ele_sort));
SASSERT(ele_sort == ele->get_sort()); SASSERT(ele_sort == ele->get_sort());