From a32fabf5ee59cdcfa1d23cc19b8b5b9258ce6c96 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Jun 2020 12:13:39 -0700 Subject: [PATCH 01/11] fix #4403 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 11 +++++++++-- src/opt/optsmt.cpp | 5 ++++- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8423bb1b9..d86893199 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -367,6 +367,7 @@ namespace opt { void context::fix_model(model_ref& mdl) { if (mdl && !m_model_fixed.contains(mdl.get())) { TRACE("opt", m_fm->display(tout << "fix-model\n"); + tout << *mdl << "\n"; if (m_model_converter) m_model_converter->display(tout);); (*m_fm)(mdl); apply(m_model_converter, mdl); @@ -482,6 +483,7 @@ namespace opt { lbool context::execute_box() { if (m_box_index < m_box_models.size()) { m_model = m_box_models[m_box_index]; + CTRACE("opt", m_model, tout << *m_model << "\n";); ++m_box_index; return l_true; } @@ -505,12 +507,15 @@ namespace opt { m_box_models.push_back(m_model.get()); } else { - m_box_models.push_back(m_optsmt.get_model(j)); + model* mdl = m_optsmt.get_model(j); + if (!mdl) mdl = m_model.get(); + m_box_models.push_back(mdl); ++j; } } if (r == l_true && !m_box_models.empty()) { m_model = m_box_models[0]; + CTRACE("opt", m_model, tout << *m_model << "\n";); } return r; } @@ -787,6 +792,7 @@ namespace opt { void context::normalize(expr_ref_vector const& asms) { expr_ref_vector fmls(m); + m_model_converter = nullptr; to_fmls(fmls); simplify_fmls(fmls, asms); from_fmls(fmls); @@ -1248,7 +1254,7 @@ namespace opt { case O_MAXSMT: { maxsmt& ms = *m_maxsmts.find(obj.m_id); for (unsigned j = 0; j < obj.m_terms.size(); ++j) { - ms.add(obj.m_terms[j].get(), obj.m_weights[j]); + ms.add(obj.m_terms.get(j), obj.m_weights[j]); } break; } @@ -1468,6 +1474,7 @@ namespace opt { void context::clear_state() { m_pareto = nullptr; m_box_index = UINT_MAX; + m_box_models.reset(); m_model.reset(); m_model_fixed.reset(); m_core.reset(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 8dff3f924..c8c254179 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -469,6 +469,7 @@ namespace opt { return l_true; } + void optsmt::setup(opt_solver& solver) { m_s = &solver; solver.reset_objectives(); @@ -577,7 +578,9 @@ namespace opt { m_upper.reset(); m_objs.reset(); m_vars.reset(); - m_model.reset(); + m_model.reset(); + m_best_model = nullptr; + m_models.reset(); m_lower_fmls.reset(); m_s = nullptr; } From 4dbf7b183d9f0cb3cacb93f29b3d47607d98b09d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Jun 2020 13:51:05 -0700 Subject: [PATCH 02/11] inline conditions with derivative computation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 202 ++++++++++++++++++++---------- src/ast/rewriter/seq_rewriter.h | 9 ++ 2 files changed, 145 insertions(+), 66 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 61824f615..132d2de3c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2304,7 +2304,110 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { Symbolic derivative: seq -> regex -> regex seq should be single char */ + br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { + result = mk_derivative(ele, r); + // TBD: we may even declare BR_DONE here and potentially miss some simplifications + return re().is_derivative(result) ? BR_DONE : BR_REWRITE_FULL; +} + +expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) { + expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, ele, r), m()); + if (!result) { + result = mk_derivative_rec(ele, r); + m_op_cache.insert(OP_RE_DERIVATIVE, ele, r, result); + } + return result; +} + +expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) { + return mk_der_op(OP_RE_UNION, r1, r2); +} + +expr_ref seq_rewriter::mk_der_inter(expr* r1, expr* r2) { + return mk_der_op(OP_RE_INTERSECT, r1, r2); +} + +expr_ref seq_rewriter::mk_der_concat(expr* r1, expr* r2) { + return mk_der_op(OP_RE_CONCAT, r1, r2); +} + +expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) { + expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr; + expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr; + expr_ref result(m()); + if (m().is_ite(a, ca, a1, a2)) { + if (m().is_ite(b, cb, b1, b2)) { + if (ca == cb) { + expr_ref r1 = mk_der_op(k, a1, b1); + expr_ref r2 = mk_der_op(k, a2, b2); + result = m().mk_ite(ca, r1, r2); + return result; + } + else if (ca->get_id() < cb->get_id()) { + expr_ref r1 = mk_der_op(k, a, b1); + expr_ref r2 = mk_der_op(k, a, b2); + result = m().mk_ite(cb, r1, r2); + return result; + } + } + expr_ref r1 = mk_der_op(k, a1, b); + expr_ref r2 = mk_der_op(k, a2, b); + result = m().mk_ite(ca, r1, r2); + return result; + } + if (m().is_ite(b, cb, b1, b2)) { + expr_ref r1 = mk_der_op(k, a, b1); + expr_ref r2 = mk_der_op(k, a, b2); + result = m().mk_ite(cb, r1, r2); + return result; + } + switch (k) { + case OP_RE_INTERSECT: + if (BR_FAILED == mk_re_inter(a, b, result)) + result = re().mk_inter(a, b); + break; + case OP_RE_UNION: + if (BR_FAILED == mk_re_union(a, b, result)) + result = re().mk_union(a, b); + break; + case OP_RE_CONCAT: + if (BR_FAILED == mk_re_concat(a, b, result)) + result = re().mk_concat(a, b); + break; + default: + UNREACHABLE(); + break; + } + return result; +} + +expr_ref seq_rewriter::mk_der_op(decl_kind k, expr* a, expr* b) { + expr_ref _a(a, m()), _b(b, m()); + expr_ref result(m_op_cache.find(k, a, b), m()); + if (!result) { + result = mk_der_op_rec(k, a, b); + m_op_cache.insert(k, a, b, result); + } + return result; +} + +expr_ref seq_rewriter::mk_der_compl(expr* r) { + expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr), m()); + if (!result) { + expr* c = nullptr, * r1 = nullptr, * r2 = nullptr; + if (m().is_ite(r, c, r1, r2)) { + result = m().mk_ite(c, mk_der_compl(r1), mk_der_compl(r2)); + } + else if (BR_FAILED == mk_re_complement(r, result)) + result = re().mk_complement(r); + } + m_op_cache.insert(OP_RE_COMPLEMENT, r, nullptr, result); + return result; +} + +expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { + expr_ref result(m()); sort* seq_sort = nullptr, *ele_sort = nullptr; VERIFY(m_util.is_re(r, seq_sort)); VERIFY(m_util.is_seq(seq_sort, ele_sort)); @@ -2313,110 +2416,77 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { unsigned lo = 0, hi = 0; if (re().is_concat(r, r1, r2)) { expr_ref is_n = is_nullable(r1); - expr_ref dr1(re().mk_derivative(ele, r1), m()); - expr_ref dr2(re().mk_derivative(ele, r2), m()); - result = re().mk_concat(dr1, r2); + expr_ref dr1 = mk_derivative(ele, r1); + result = mk_der_concat(dr1, r2); if (m().is_false(is_n)) { - return BR_REWRITE2; - } - else if (m().is_true(is_n)) { - result = re().mk_union(result, dr2); - return BR_REWRITE3; - } - else { - result = re().mk_union(result, re_and(is_n, dr2)); - return BR_REWRITE3; + return result; } + expr_ref dr2 = mk_derivative(ele, r2); + return mk_der_union(result, re_and(is_n, dr2)); } else if (re().is_star(r, r1)) { - result = re().mk_concat(re().mk_derivative(ele, r1), r); - return BR_REWRITE2; + return mk_der_concat(mk_derivative(ele, r1), r); } else if (re().is_plus(r, r1)) { - result = re().mk_derivative(ele, re().mk_star(r1)); - return BR_REWRITE1; + expr_ref star(re().mk_star(r1), m()); + return mk_derivative(ele, star); } else if (re().is_union(r, r1, r2)) { - result = re().mk_union( - re().mk_derivative(ele, r1), - re().mk_derivative(ele, r2) - ); - return BR_REWRITE2; + return mk_der_union(mk_derivative(ele, r1), mk_derivative(ele, r2)); } else if (re().is_intersection(r, r1, r2)) { - result = re().mk_inter( - re().mk_derivative(ele, r1), - re().mk_derivative(ele, r2) - ); - return BR_REWRITE2; + return mk_der_inter(mk_derivative(ele, r1), mk_derivative(ele, r2)); } else if (re().is_diff(r, r1, r2)) { - result = re().mk_diff( - re().mk_derivative(ele, r1), - re().mk_derivative(ele, r2) - ); - return BR_REWRITE2; + return mk_der_inter(mk_derivative(ele, r1), mk_der_compl(mk_derivative(ele, r2))); } else if (m().is_ite(r, p, r1, r2)) { - result = m().mk_ite( - p, - re().mk_derivative(ele, r1), - re().mk_derivative(ele, r2) - ); - return BR_REWRITE2; + // there is no BDD normalization here + result = m().mk_ite(p, mk_derivative(ele, r1), mk_derivative(ele, r2)); + return result; } else if (re().is_opt(r, r1)) { - result = re().mk_derivative(ele, r1); - return BR_REWRITE1; + return mk_derivative(ele, r1); } else if (re().is_complement(r, r1)) { - result = re().mk_complement(re().mk_derivative(ele, r1)); - return BR_REWRITE2; + return mk_der_compl(mk_derivative(ele, r1)); } else if (re().is_loop(r, r1, lo)) { if (lo > 0) { lo--; } - result = re().mk_concat( - re().mk_derivative(ele, r1), - re().mk_loop(r1, lo) - ); - return BR_REWRITE2; + return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo)); } else if (re().is_loop(r, r1, lo, hi)) { if (hi == 0) { result = re().mk_empty(m().get_sort(r)); - return BR_DONE; + return result; } hi--; if (lo > 0) { lo--; } - result = re().mk_concat( - re().mk_derivative(ele, r1), - re().mk_loop(r1, lo, hi) - ); - return BR_REWRITE2; + return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo, hi)); } else if (re().is_full_seq(r) || re().is_empty(r)) { result = r; - return BR_DONE; + return result; } else if (re().is_to_re(r, r1)) { // r1 is a string here (not a regexp) expr_ref hd(m()), tl(m()); if (get_head_tail(r1, hd, tl)) { // head must be equal; if so, derivative is tail - result = re_and(m().mk_eq(ele, hd),re().mk_to_re(tl)); - return BR_REWRITE2; + result = re_and(m().mk_eq(ele, hd), re().mk_to_re(tl)); + return result; } else if (str().is_empty(r1)) { result = re().mk_empty(m().get_sort(r)); - return BR_DONE; + return result; } else { - return BR_FAILED; + return expr_ref(re().mk_derivative(ele, r), m()); } } else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) { @@ -2429,14 +2499,14 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { m().mk_eq(ele, tl), re().mk_reverse(re().mk_to_re(hd)) ); - return BR_REWRITE3; + return result; } else if (str().is_empty(r2)) { result = re().mk_empty(m().get_sort(r)); - return BR_DONE; + return result; } else { - return BR_FAILED; + return expr_ref(re().mk_derivative(ele, r), m()); } } else if (re().is_range(r, r1, r2)) { @@ -2448,34 +2518,34 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { r2 = m_util.mk_char(s2[0]); result = m().mk_and(m_util.mk_le(r1, ele), m_util.mk_le(ele, r2)); result = re_predicate(result, seq_sort); - return BR_REWRITE3; + return result; } else { result = re().mk_empty(m().get_sort(r)); - return BR_DONE; + return result; } } expr* e1 = nullptr, *e2 = nullptr; if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) { result = m().mk_and(m_util.mk_le(e1, ele), m_util.mk_le(ele, e2)); result = re_predicate(result, seq_sort); - return BR_REWRITE2; + return result; } } else if (re().is_full_char(r)) { result = re().mk_to_re(str().mk_empty(seq_sort)); - return BR_DONE; + return result; } else if (re().is_of_pred(r, p)) { array_util array(m()); expr* args[2] = { p, ele }; result = array.mk_select(2, args); result = re_predicate(result, seq_sort); - return BR_REWRITE2; + return result; } // stuck cases: re().is_derivative, variable, ... // and re().is_reverse if the reverse is not applied to a string - return BR_FAILED; + return expr_ref(re().mk_derivative(ele, r), m()); } /* diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 873f88581..5f5f36feb 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -180,6 +180,15 @@ class seq_rewriter { expr_ref re_predicate(expr* cond, sort* seq_sort); expr_ref mk_seq_concat(expr* a, expr* b); + expr_ref mk_der_op(decl_kind k, expr* a, expr* b); + expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b); + expr_ref mk_der_concat(expr* a, expr* b); + expr_ref mk_der_union(expr* a, expr* b); + expr_ref mk_der_inter(expr* a, expr* b); + expr_ref mk_der_compl(expr* a); + expr_ref mk_derivative(expr* ele, expr* r); + expr_ref mk_derivative_rec(expr* ele, expr* r); + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_seq_length(expr* a, expr_ref& result); From 1b9fcc7098d79160cad1cb59bd05b8e527957b54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Jun 2020 17:28:48 -0700 Subject: [PATCH 03/11] integrate ite-normalized derivatives Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 174 ++++-------------------------- src/ast/rewriter/seq_rewriter.h | 12 +-- src/smt/seq_regex.cpp | 103 +++++++++--------- src/smt/seq_regex.h | 9 +- 4 files changed, 86 insertions(+), 212 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 132d2de3c..26021f9b6 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2336,30 +2336,33 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) { expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr; expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr; expr_ref result(m()); + auto mk_ite = [&](expr* c, expr* a, expr* b) { + return (a == b) ? a : m().mk_ite(c, a, b); + }; if (m().is_ite(a, ca, a1, a2)) { if (m().is_ite(b, cb, b1, b2)) { if (ca == cb) { expr_ref r1 = mk_der_op(k, a1, b1); expr_ref r2 = mk_der_op(k, a2, b2); - result = m().mk_ite(ca, r1, r2); + result = mk_ite(ca, r1, r2); return result; } else if (ca->get_id() < cb->get_id()) { expr_ref r1 = mk_der_op(k, a, b1); expr_ref r2 = mk_der_op(k, a, b2); - result = m().mk_ite(cb, r1, r2); + result = mk_ite(cb, r1, r2); return result; } } expr_ref r1 = mk_der_op(k, a1, b); expr_ref r2 = mk_der_op(k, a2, b); - result = m().mk_ite(ca, r1, r2); + result = mk_ite(ca, r1, r2); return result; } if (m().is_ite(b, cb, b1, b2)) { expr_ref r1 = mk_der_op(k, a, b1); expr_ref r2 = mk_der_op(k, a, b2); - result = m().mk_ite(cb, r1, r2); + result = mk_ite(cb, r1, r2); return result; } switch (k) { @@ -2413,6 +2416,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { VERIFY(m_util.is_seq(seq_sort, ele_sort)); SASSERT(ele_sort == m().get_sort(ele)); expr* r1 = nullptr, *r2 = nullptr, *p = nullptr; + auto mk_empty = [&]() { return expr_ref(re().mk_empty(m().get_sort(r)), m()); }; unsigned lo = 0, hi = 0; if (re().is_concat(r, r1, r2)) { expr_ref is_n = is_nullable(r1); @@ -2422,7 +2426,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } expr_ref dr2 = mk_derivative(ele, r2); - return mk_der_union(result, re_and(is_n, dr2)); + is_n = re_predicate(is_n, seq_sort); + return mk_der_union(result, mk_der_concat(is_n, dr2)); } else if (re().is_star(r, r1)) { return mk_der_concat(mk_derivative(ele, r1), r); @@ -2459,8 +2464,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } else if (re().is_loop(r, r1, lo, hi)) { if (hi == 0) { - result = re().mk_empty(m().get_sort(r)); - return result; + return mk_empty(); } hi--; if (lo > 0) { @@ -2470,20 +2474,17 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } else if (re().is_full_seq(r) || re().is_empty(r)) { - result = r; - return result; + return expr_ref(r, m()); } else if (re().is_to_re(r, r1)) { // r1 is a string here (not a regexp) expr_ref hd(m()), tl(m()); if (get_head_tail(r1, hd, tl)) { // head must be equal; if so, derivative is tail - result = re_and(m().mk_eq(ele, hd), re().mk_to_re(tl)); - return result; + return re_and(m().mk_eq(ele, hd), re().mk_to_re(tl)); } else if (str().is_empty(r1)) { - result = re().mk_empty(m().get_sort(r)); - return result; + return mk_empty(); } else { return expr_ref(re().mk_derivative(ele, r), m()); @@ -2495,15 +2496,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // This is analagous to the previous is_to_re case. expr_ref hd(m()), tl(m()); if (get_head_tail_reversed(r2, hd, tl)) { - result = re_and( - m().mk_eq(ele, tl), - re().mk_reverse(re().mk_to_re(hd)) - ); - return result; + return re_and(m().mk_eq(ele, tl), re().mk_reverse(re().mk_to_re(hd))); } else if (str().is_empty(r2)) { - result = re().mk_empty(m().get_sort(r)); - return result; + return mk_empty(); } else { return expr_ref(re().mk_derivative(ele, r), m()); @@ -2516,32 +2512,27 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { if (s1.length() == 1 && s2.length() == 1) { r1 = m_util.mk_char(s1[0]); r2 = m_util.mk_char(s2[0]); - result = m().mk_and(m_util.mk_le(r1, ele), m_util.mk_le(ele, r2)); - result = re_predicate(result, seq_sort); - return result; + return mk_der_inter(re_predicate(m_util.mk_le(r1, ele), seq_sort), + re_predicate(m_util.mk_le(ele, r2), seq_sort)); } else { - result = re().mk_empty(m().get_sort(r)); - return result; + return mk_empty(); } } expr* e1 = nullptr, *e2 = nullptr; if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) { - result = m().mk_and(m_util.mk_le(e1, ele), m_util.mk_le(ele, e2)); - result = re_predicate(result, seq_sort); - return result; + return mk_der_inter(re_predicate(m_util.mk_le(e1, ele), seq_sort), + re_predicate(m_util.mk_le(ele, e2), seq_sort)); } } else if (re().is_full_char(r)) { - result = re().mk_to_re(str().mk_empty(seq_sort)); - return result; + return expr_ref(re().mk_to_re(str().mk_empty(seq_sort)), m()); } else if (re().is_of_pred(r, p)) { array_util array(m()); expr* args[2] = { p, ele }; result = array.mk_select(2, args); - result = re_predicate(result, seq_sort); - return result; + return re_predicate(result, seq_sort); } // stuck cases: re().is_derivative, variable, ... // and re().is_reverse if the reverse is not applied to a string @@ -3196,7 +3187,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { else intersect(0, ch-1, ranges); } - // TBD: case for negation of range (not (and (<= lo e) (<= e hi))) else { all_ranges = false; break; @@ -3237,124 +3227,6 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { } } -void seq_rewriter::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) { - expr_ref cond(m()), th(m()), el(m()); - if (has_cofactor(r, cond, th, el)) { - conds.push_back(cond); - get_cofactors(th, conds, result); - conds.pop_back(); - conds.push_back(mk_not(m(), cond)); - get_cofactors(el, conds, result); - conds.pop_back(); - } - else { - cond = mk_and(conds); - result.push_back(cond, r); - } -} - -bool seq_rewriter::has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el) { - if (m().is_ite(r)) { - cond = to_app(r)->get_arg(0); - th = to_app(r)->get_arg(1); - el = to_app(r)->get_arg(2); - return true; - } - expr_ref_vector trail(m()), args_th(m()), args_el(m()); - expr* c = nullptr, *tt = nullptr, *ee = nullptr; - cond = nullptr; - obj_map cache_th, cache_el; - expr_mark no_cofactor, visited; - ptr_vector todo; - todo.push_back(r); - while (!todo.empty()) { - expr* e = todo.back(); - if (visited.is_marked(e) || !is_app(e)) { - todo.pop_back(); - continue; - } - app* a = to_app(e); - if (m().is_ite(e, c, tt, ee)) { - if (!cond) { - cond = c; - cache_th.insert(a, tt); - cache_el.insert(a, ee); - } - else if (cond == c) { - cache_th.insert(a, tt); - cache_el.insert(a, ee); - } - else { - no_cofactor.mark(a); - } - visited.mark(e, true); - todo.pop_back(); - continue; - } - - if (a->get_family_id() != u().get_family_id()) { - visited.mark(e, true); - no_cofactor.mark(e, true); - todo.pop_back(); - continue; - } - switch (a->get_decl_kind()) { - case OP_RE_CONCAT: - case OP_RE_UNION: - case OP_RE_INTERSECT: - case OP_RE_COMPLEMENT: - break; - case OP_RE_STAR: - case OP_RE_LOOP: - default: - visited.mark(e, true); - no_cofactor.mark(e, true); - continue; - } - args_th.reset(); - args_el.reset(); - bool has_cof = false; - for (expr* arg : *a) { - if (no_cofactor.is_marked(arg)) { - args_th.push_back(arg); - args_el.push_back(arg); - } - else if (cache_th.contains(arg)) { - args_th.push_back(cache_th[arg]); - args_el.push_back(cache_el[arg]); - has_cof = true; - } - else { - todo.push_back(arg); - } - } - if (args_th.size() == a->get_num_args()) { - if (has_cof) { - th = mk_app(a->get_decl(), args_th); - el = mk_app(a->get_decl(), args_el); - trail.push_back(th); - trail.push_back(el); - cache_th.insert(a, th); - cache_el.insert(a, el); - } - else { - no_cofactor.mark(a, true); - } - visited.mark(e, true); - todo.pop_back(); - } - } - SASSERT(cond == !no_cofactor.is_marked(r)); - if (cond) { - th = cache_th[r]; - el = cache_el[r]; - return true; - } - else { - return false; - } -} - br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) { expr* r1, *r2, *r3, *r4; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5f5f36feb..6b7b06653 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -273,12 +273,13 @@ class seq_rewriter { class seq_util::str& str() { return u().str; } class seq_util::str const& str() const { return u().str; } - void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result); + expr_ref is_nullable_rec(expr* r); void intersect(unsigned lo, unsigned hi, svector>& ranges); public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) { + m_util(m), m_autil(m), m_re2aut(m), m_op_cache(m), m_es(m), + m_lhs(m), m_rhs(m), m_coalesce_chars(true) { } ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } @@ -320,14 +321,7 @@ public: void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs); expr_ref is_nullable(expr* r); - expr_ref is_nullable_rec(expr* r); - bool has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el); - - void get_cofactors(expr* r, expr_ref_pair_vector& result) { - expr_ref_vector conds(m()); - get_cofactors(r, conds, result); - } // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 4ca6cdbf7..f08cc2a6c 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -148,32 +148,6 @@ namespace smt { m_to_propagate.push_back(lit); } - - // s in R[if(p,R1,R2)] & p => s in R[R1] - // s in R[if(p,R1,R2)] & ~p => s in R[R2] - - bool seq_regex::unfold_cofactors(expr_ref& r, literal_vector& conds) { - expr_ref cond(m), tt(m), el(m); - while (seq_rw().has_cofactor(r, cond, tt, el)) { - rewrite(cond); - literal lcond = th.mk_literal(cond); - switch (ctx.get_assignment(lcond)) { - case l_true: - conds.push_back(~lcond); - r = tt; - break; - case l_false: - conds.push_back(lcond); - r = el; - break; - case l_undef: - ctx.mark_as_relevant(lcond); - return false; - } - rewrite(r); - } - return true; - } /** * Propagate the atom (accept s i r) @@ -198,19 +172,14 @@ namespace smt { TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); - if (block_unfolding(lit, idx)) - return true; - - literal_vector conds; - conds.push_back(~lit); - if (!unfold_cofactors(d, conds)) - return false; - - if (re().is_empty(d)) { - th.add_axiom(conds); + if (re().is_empty(r)) { + th.add_axiom(~lit); return true; } + if (block_unfolding(lit, idx)) + return true; + // s in R & len(s) <= i => nullable(R) literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); switch (ctx.get_assignment(len_s_le_i)) { @@ -218,11 +187,9 @@ namespace smt { ctx.mark_as_relevant(len_s_le_i); return false; case l_true: - is_nullable = seq_rw().is_nullable(d); + is_nullable = seq_rw().is_nullable(r); rewrite(is_nullable); - conds.push_back(~len_s_le_i); - conds.push_back(th.mk_literal(is_nullable)); - th.add_axiom(conds); + th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable)); return true; case l_false: break; @@ -230,14 +197,38 @@ namespace smt { // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds expr_ref head = th.mk_nth(s, i); - d = re().mk_derivative(head, r); + d = re().mk_derivative(m.mk_var(0, m.get_sort(head)), r); rewrite(d); - literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d)); + literal_vector conds; + conds.push_back(~lit); conds.push_back(len_s_le_i); - conds.push_back(acc_next); - th.add_axiom(conds); - + expr* cond = nullptr, *tt = nullptr, *el = nullptr; + var_subst subst(m); + expr_ref_vector sub(m); + sub.push_back(head); + // s in R[if(p,R1,R2)] & p => s in R[R1] + // s in R[if(p,R1,R2)] & ~p => s in R[R2] + while (m.is_ite(d, cond, tt, el)) { + literal lcond = th.mk_literal(subst(cond, sub)); + switch (ctx.get_assignment(lcond)) { + case l_true: + conds.push_back(~lcond); + d = tt; + break; + case l_false: + conds.push_back(lcond); + d = el; + break; + case l_undef: + ctx.mark_as_relevant(lcond); + return false; + } + } + // at this point there should be no free variables as the ites are at top-level. + if (!re().is_empty(d)) + conds.push_back(th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d))); + th.add_axiom(conds); TRACE("seq", tout << "unfold " << head << "\n" << mk_pp(r, m) << "\n";); return true; } @@ -358,7 +349,7 @@ namespace smt { if (null_lit != false_literal) lits.push_back(null_lit); expr_ref_pair_vector cofactors(m); - seq_rw().get_cofactors(d, cofactors); + get_cofactors(d, cofactors); for (auto const& p : cofactors) { if (is_member(p.second, u)) continue; @@ -375,6 +366,21 @@ namespace smt { th.add_axiom(lits); } + void seq_regex::get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result) { + expr* cond = nullptr, *th = nullptr, *el = nullptr; + if (m.is_ite(r, cond, th, el)) { + conds.push_back(cond); + get_cofactors(th, conds, result); + conds.pop_back(); + conds.push_back(mk_not(m, cond)); + get_cofactors(el, conds, result); + conds.pop_back(); + } + else { + cond = mk_and(conds); + result.push_back(cond, r); + } + } /* is_empty(r, u) => ~is_nullable(r) @@ -398,10 +404,7 @@ namespace smt { rewrite(d); literal_vector lits; expr_ref_pair_vector cofactors(m); - seq_rw().get_cofactors(d, cofactors); - - // is_empty(r, u) => forall hd . cond => is_empty(r1, u union r) - + get_cofactors(d, cofactors); for (auto const& p : cofactors) { if (is_member(p.second, u)) continue; diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index ebcbc53b1..02fe1555a 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -63,12 +63,17 @@ namespace smt { expr_ref unroll_non_empty(expr* r, expr_mark& seen, unsigned depth); - bool unfold_cofactors(expr_ref& r, literal_vector& conds); - bool is_member(expr* r, expr* u); expr_ref symmetric_diff(expr* r1, expr* r2); + void get_cofactors(expr* r, expr_ref_vector& conds, expr_ref_pair_vector& result); + + void get_cofactors(expr* r, expr_ref_pair_vector& result) { + expr_ref_vector conds(m); + get_cofactors(r, conds, result); + } + public: seq_regex(theory_seq& th); From 65b6ccd6511ac3ef74bb62d994206d2a948e82cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2020 11:32:43 -0700 Subject: [PATCH 04/11] add nullable propagation instead of waiting for length assignment Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 91 ++++++++++++++++++++++++++++++++----------- src/smt/seq_regex.h | 4 ++ 2 files changed, 72 insertions(+), 23 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index f08cc2a6c..1b866eda4 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -116,11 +116,9 @@ namespace smt { if (coallesce_in_re(lit)) return; -#if 1 - // Enable/disable to test effect if (is_string_equality(lit)) return; -#endif + // // TBD s in R => R != {} // non-emptiness enforcement could instead of here, @@ -156,6 +154,8 @@ namespace smt { * * (accept s i r[if(c,r1,r2)]) & c => (accept s i r[r1]) * (accept s i r[if(c,r1,r2)]) & ~c => (accept s i r[r2]) + * (accept s i r) & nullable(r) => len(s) >= i + * (accept s i r) & ~nullable(r) => len(s) >= i + 1 * (accept s i r) & len(s) <= i => nullable(r) * (accept s i r) & len(s) > i => (accept s (+ i 1) D(nth(s,i), r)) */ @@ -167,8 +167,6 @@ namespace smt { expr* e = ctx.bool_var2expr(lit.var()); unsigned idx = 0; VERIFY(sk().is_accept(e, s, i, idx, r)); - expr_ref is_nullable(m), d(r, m); - TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); @@ -180,29 +178,55 @@ namespace smt { if (block_unfolding(lit, idx)) return true; - // s in R & len(s) <= i => nullable(R) - literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); - switch (ctx.get_assignment(len_s_le_i)) { - case l_undef: - ctx.mark_as_relevant(len_s_le_i); - return false; - case l_true: - is_nullable = seq_rw().is_nullable(r); - rewrite(is_nullable); - th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable)); - return true; - case l_false: - break; - } + propagate_nullable(lit, e, s, idx, r); + return propagate_derivative(lit, e, s, i, idx, r); + } + + /** + Implement the two axioms as propagations: + + (accept s i r) => len(s) >= i + (accept s i r) & ~nullable(r) => len(s) >= i + 1 + */ + + void seq_regex::propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r) { + expr_ref is_nullable = seq_rw().is_nullable(r); + rewrite(is_nullable); + literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); + literal len_s_ge_i = th.m_ax.mk_ge(th.mk_len(s), idx); + if (m.is_true(is_nullable)) { + th.propagate_lit(nullptr, 1,&lit, len_s_ge_i); + } + else if (m.is_false(is_nullable)) { + th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1)); + } + else { + switch (ctx.get_assignment(len_s_le_i)) { + case l_undef: + th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable)); + break; + case l_true: { + literal lits[2] = { lit, len_s_le_i }; + th.propagate_lit(nullptr, 2, lits, th.mk_literal(is_nullable)); + break; + } + case l_false: + break; + } + th.propagate_lit(nullptr, 1, &lit, len_s_ge_i); + } + } + + bool seq_regex::propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r) { // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds + expr_ref d(m); expr_ref head = th.mk_nth(s, i); d = re().mk_derivative(m.mk_var(0, m.get_sort(head)), r); rewrite(d); - literal_vector conds; conds.push_back(~lit); - conds.push_back(len_s_le_i); + conds.push_back(th.m_ax.mk_le(th.mk_len(s), idx)); expr* cond = nullptr, *tt = nullptr, *el = nullptr; var_subst subst(m); expr_ref_vector sub(m); @@ -220,9 +244,30 @@ namespace smt { conds.push_back(lcond); d = el; break; - case l_undef: + case l_undef: ctx.mark_as_relevant(lcond); return false; +#if 0 + if (re().is_empty(tt)) { + literal_vector ensure_false(conds); + ensure_false.push_back(~lcond); + th.add_axiom(ensure_false); + conds.push_back(lcond); + d = el; + } + else if (re().is_empty(el)) { + literal_vector ensure_true(conds); + ensure_true.push_back(lcond); + th.add_axiom(ensure_true); + conds.push_back(~lcond); + d = tt; + } + else { + ctx.mark_as_relevant(lcond); + return false; + } + break; +#endif } } // at this point there should be no free variables as the ites are at top-level. @@ -252,7 +297,7 @@ namespace smt { */ bool seq_regex::coallesce_in_re(literal lit) { // initially disable this - return false; + // return false; expr* s = nullptr, *r = nullptr; expr* e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 02fe1555a..71bcd160d 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -59,6 +59,10 @@ namespace smt { bool block_unfolding(literal lit, unsigned i); + void propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r); + + bool propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r); + expr_ref mk_first(expr* r); expr_ref unroll_non_empty(expr* r, expr_mark& seen, unsigned depth); From ccea27de350a153441755979fac98ac96a6d2ba1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2020 12:11:04 -0700 Subject: [PATCH 05/11] add nullable propagation instead of waiting for length assignment Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 1b866eda4..c9dcb7181 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -193,7 +193,6 @@ namespace smt { void seq_regex::propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r) { expr_ref is_nullable = seq_rw().is_nullable(r); rewrite(is_nullable); - literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); literal len_s_ge_i = th.m_ax.mk_ge(th.mk_len(s), idx); if (m.is_true(is_nullable)) { th.propagate_lit(nullptr, 1,&lit, len_s_ge_i); @@ -202,6 +201,7 @@ namespace smt { th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1)); } else { + literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx); switch (ctx.get_assignment(len_s_le_i)) { case l_undef: th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable)); @@ -245,9 +245,10 @@ namespace smt { d = el; break; case l_undef: +#if 1 ctx.mark_as_relevant(lcond); return false; -#if 0 +#else if (re().is_empty(tt)) { literal_vector ensure_false(conds); ensure_false.push_back(~lcond); @@ -296,8 +297,6 @@ namespace smt { * within the same Regex. */ bool seq_regex::coallesce_in_re(literal lit) { - // initially disable this - // return false; expr* s = nullptr, *r = nullptr; expr* e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); @@ -305,6 +304,7 @@ namespace smt { literal_vector lits; for (unsigned i = 0; i < m_s_in_re.size(); ++i) { auto const& entry = m_s_in_re[i]; + std::cout << "CHECK " << i << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n"; enode* n1 = th.ensure_enode(entry.m_s); enode* n2 = th.ensure_enode(s); if (!entry.m_active) @@ -316,7 +316,7 @@ namespace smt { th.m_trail_stack.push(vector_value_trail(m_s_in_re, i)); m_s_in_re[i].m_active = false; - IF_VERBOSE(11, verbose_stream() << "intersect " << regex << " " << + IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " << mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";); regex = re().mk_inter(entry.m_re, regex); rewrite(regex); From ba1ca336376341d4a3c86843cbb6df0cb22bb541 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2020 12:54:44 -0700 Subject: [PATCH 06/11] normalization of union/intersection Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 89 ++++++++++++++++++++++++++++++- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/rewriter/th_rewriter.cpp | 2 +- src/smt/seq_regex.cpp | 5 +- 4 files changed, 91 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 26021f9b6..9246cb390 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -416,6 +416,9 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args, return mk_bool_app_helper(true, n, args, result); case OP_OR: return mk_bool_app_helper(false, n, args, result); + case OP_EQ: + SASSERT(n == 2); + // return mk_eq_helper(args[0], args[1], result); default: return BR_FAILED; } @@ -492,7 +495,27 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const* } } - result = is_and ? m().mk_and(new_args.size(), new_args.c_ptr()) : m().mk_or(new_args.size(), new_args.c_ptr()); + result = is_and ? m().mk_and(new_args) : m().mk_or(new_args); + return BR_REWRITE_FULL; +} + +br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) { + expr* sa = nullptr, *ra = nullptr, *sb = nullptr, *rb = nullptr; + if (str().is_in_re(b)) + std::swap(a, b); + if (!str().is_in_re(a, sa, ra)) + return BR_FAILED; + bool is_not = m().is_not(b, b); + if (!str().is_in_re(b, sb, rb)) + return BR_FAILED; + if (sa != sb) + return BR_FAILED; + // sa in ra = sb in rb; + // sa in (ra n rb) u (C(ra) n C(rb)) + if (is_not) + rb = re().mk_complement(rb); + expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb))); + result = re().mk_in_re(sa, r); return BR_REWRITE_FULL; } @@ -2870,6 +2893,35 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { result = b; return BR_DONE; } + expr* ac = nullptr, *bc = nullptr; + expr* a1 = nullptr, *a2 = nullptr; + expr* b1 = nullptr, *b2 = nullptr; + // ensure union is right-associative + // and swap-sort entries + if (re().is_union(a, a1, a2)) { + result = re().mk_union(a1, re().mk_union(a2, b)); + return BR_REWRITE2; + } + auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; + auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; + if (re().is_union(b, b1, b2)) { + if (a == b1) { + result = b; + return BR_DONE; + } + if (re().is_complement(a, ac) && b1 == ac) { + result = mk_full(); + return BR_DONE; + } + if (re().is_complement(b1, bc) && a == bc) { + result = mk_full(); + return BR_DONE; + } + if (get_id(a) > get_id(b1)) { + result = re().mk_union(b1, re().mk_union(a, b2)); + return BR_REWRITE2; + } + } return BR_FAILED; } @@ -2891,6 +2943,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { result = re().mk_empty(m().get_sort(a)); return BR_DONE; } + if (re().is_complement(a, e1)) { + result = e1; + return BR_DONE; + } return BR_FAILED; } @@ -2923,9 +2979,38 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { return BR_DONE; } expr* ac = nullptr, *bc = nullptr; + expr* a1 = nullptr, *a2 = nullptr; + expr* b1 = nullptr, *b2 = nullptr; + + // ensure intersection is right-associative + // and swap-sort entries + if (re().is_intersection(a, a1, a2)) { + result = re().mk_inter(a1, re().mk_inter(a2, b)); + return BR_REWRITE2; + } + auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); }; + auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; + if (re().is_intersection(b, b1, b2)) { + if (a == b1) { + result = b; + return BR_DONE; + } + if (re().is_complement(a, ac) && b1 == ac) { + result = mk_empty(); + return BR_DONE; + } + if (re().is_complement(b1, bc) && a == bc) { + result = mk_empty(); + return BR_DONE; + } + if (get_id(a) > get_id(b1)) { + result = re().mk_inter(b1, re().mk_inter(a, b2)); + return BR_REWRITE2; + } + } if ((re().is_complement(a, ac) && ac == b) || (re().is_complement(b, bc) && bc == a)) { - result = re().mk_empty(m().get_sort(a)); + result = mk_empty(); return BR_DONE; } if (re().is_to_re(b)) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 6b7b06653..8464b2fd4 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -238,6 +238,7 @@ class seq_rewriter { bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result); br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result); + br_status mk_eq_helper(expr* a, expr* b, expr_ref& result); bool cannot_contain_prefix(expr* a, expr* b); bool cannot_contain_suffix(expr* a, expr* b); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 6ba8bc481..340c76805 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -203,7 +203,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (st != BR_FAILED) return st; } - if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) { + if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) { st = m_seq_rw.mk_bool_app(f, num, args, result); if (st != BR_FAILED) return st; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index c9dcb7181..b6c438546 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -304,11 +304,10 @@ namespace smt { literal_vector lits; for (unsigned i = 0; i < m_s_in_re.size(); ++i) { auto const& entry = m_s_in_re[i]; - std::cout << "CHECK " << i << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n"; - enode* n1 = th.ensure_enode(entry.m_s); - enode* n2 = th.ensure_enode(s); if (!entry.m_active) continue; + enode* n1 = th.ensure_enode(entry.m_s); + enode* n2 = th.ensure_enode(s); if (n1->get_root() != n2->get_root()) continue; if (entry.m_re == regex) From 1809ee510775e5cbc9db7495b329af1882450982 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 7 Jun 2020 15:50:53 +0100 Subject: [PATCH 07/11] fix regression in FPA internalization --- src/smt/theory_fpa.cpp | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index d3793b707..21cce643a 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -436,7 +436,8 @@ namespace smt { ctx.internalize(term->get_args(), term->get_num_args(), false); - enode * e = ctx.mk_enode(term, false, false, true); + enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : + ctx.mk_enode(term, false, false, true); if (!is_attached_to_var(e)) { attach_new_th_var(e); @@ -503,16 +504,14 @@ namespace smt { fpa_util & fu = m_fpa_util; - expr_ref xe(m), ye(m); - xe = e_x->get_owner(); - ye = e_y->get_owner(); + expr * xe = e_x->get_owner(); + expr * ye = e_y->get_owner(); if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye)) return; - expr_ref xc(m), yc(m); - xc = convert(xe); - yc = convert(ye); + expr_ref xc = convert(xe); + expr_ref yc = convert(ye); TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl << "yc = " << mk_ismt2_pp(yc, m) << std::endl;); @@ -546,16 +545,14 @@ namespace smt { fpa_util & fu = m_fpa_util; - expr_ref xe(m), ye(m); - xe = e_x->get_owner(); - ye = e_y->get_owner(); + expr * xe = e_x->get_owner(); + expr * ye = e_y->get_owner(); if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye)) return; - expr_ref xc(m), yc(m); - xc = convert(xe); - yc = convert(ye); + expr_ref xc = convert(xe); + expr_ref yc = convert(ye); expr_ref c(m); From 30a3618ebf4c4025cdd82b2de81b9435c31c1f7a Mon Sep 17 00:00:00 2001 From: FabianWolff Date: Sun, 7 Jun 2020 21:27:54 +0200 Subject: [PATCH 08/11] Fix build failure on riscv64 (#4506) --- CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ae3bce9a..7cf4eec58 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -315,6 +315,7 @@ endif() ################################################################################ # Threading support ################################################################################ +set(THREADS_PREFER_PTHREAD_FLAG TRUE) find_package(Threads) list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) From cfed69caae6884b53fe57d4880913afafae69b10 Mon Sep 17 00:00:00 2001 From: FabianWolff Date: Sun, 7 Jun 2020 21:28:39 +0200 Subject: [PATCH 09/11] Remove __DATE__ to make the build more reproducible (#4505) --- src/api/api_log.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 942448a7f..e740a21c3 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -54,7 +54,7 @@ extern "C" { res = false; } else { - *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; + *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n"; g_z3_log->flush(); g_z3_log_enabled = true; } From d2a12f6db59c6489767764e2873a848725d6db7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jun 2020 12:52:09 -0700 Subject: [PATCH 10/11] tuning Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 112 ++++++++++++++++++++++++------ src/ast/rewriter/seq_rewriter.h | 3 + src/smt/seq_regex.cpp | 6 ++ 3 files changed, 101 insertions(+), 20 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 9246cb390..f7518f919 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2758,7 +2758,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { return BR_REWRITE_FULL; } -#if 0 if (get_re_head_tail(b, hd, tl)) { SASSERT(re().min_length(hd) == re().max_length(hd)); expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m()); @@ -2779,7 +2778,6 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)); return BR_REWRITE_FULL; } -#endif if (false && rewrite_contains_pattern(a, b, result)) return BR_REWRITE_FULL; @@ -2859,6 +2857,50 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { } return BR_FAILED; } + +bool seq_rewriter::are_complements(expr* r1, expr* r2) const { + expr* r = nullptr; + if (re().is_complement(r1, r) && r == r2) + return true; + if (re().is_complement(r2, r) && r == r1) + return true; + return false; +} + +/* + * basic subset checker. + */ +bool seq_rewriter::is_subset(expr* r1, expr* r2) const { + // return false; + expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr; + expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr; + if (re().is_complement(r1, ra1) && + re().is_complement(r2, rb1)) { + return is_subset(rb1, ra1); + } + auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) { + return re().is_concat(r, a, b) && re().is_concat(b, b, c); + }; + while (true) { + if (r1 == r2) + return true; + if (re().is_full_seq(r2)) + return true; + if (is_concat(r1, ra1, ra2, ra3) && + is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) { + r1 = ra3; + r2 = rb3; + continue; + } + if (re().is_concat(r1, ra1, ra2) && + re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) { + r1 = ra2; + continue; + } + return false; + } +} + /* (a + a) = a (a + eps) = a @@ -2893,7 +2935,12 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { result = b; return BR_DONE; } - expr* ac = nullptr, *bc = nullptr; + auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; + if (are_complements(a, b)) { + result = mk_full(); + return BR_DONE; + } + expr* a1 = nullptr, *a2 = nullptr; expr* b1 = nullptr, *b2 = nullptr; // ensure union is right-associative @@ -2902,18 +2949,17 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { result = re().mk_union(a1, re().mk_union(a2, b)); return BR_REWRITE2; } - auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); }; auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; if (re().is_union(b, b1, b2)) { - if (a == b1) { + if (is_subset(a, b1)) { result = b; return BR_DONE; } - if (re().is_complement(a, ac) && b1 == ac) { - result = mk_full(); - return BR_DONE; + if (is_subset(b1, a)) { + result = re().mk_union(a, b2); + return BR_REWRITE1; } - if (re().is_complement(b1, bc) && a == bc) { + if (are_complements(a, b1)) { result = mk_full(); return BR_DONE; } @@ -2922,6 +2968,20 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { return BR_REWRITE2; } } + else { + if (get_id(a) > get_id(b)) { + result = re().mk_union(b, a); + return BR_DONE; + } + if (is_subset(a, b)) { + result = b; + return BR_DONE; + } + if (is_subset(b, a)) { + result = a; + return BR_DONE; + } + } return BR_FAILED; } @@ -2978,7 +3038,11 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { result = a; return BR_DONE; } - expr* ac = nullptr, *bc = nullptr; + auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); }; + if (are_complements(a, b)) { + result = mk_empty(); + return BR_DONE; + } expr* a1 = nullptr, *a2 = nullptr; expr* b1 = nullptr, *b2 = nullptr; @@ -2988,18 +3052,17 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { result = re().mk_inter(a1, re().mk_inter(a2, b)); return BR_REWRITE2; } - auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); }; auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; if (re().is_intersection(b, b1, b2)) { - if (a == b1) { + if (is_subset(b1, a)) { result = b; return BR_DONE; } - if (re().is_complement(a, ac) && b1 == ac) { - result = mk_empty(); - return BR_DONE; + if (is_subset(a, b1)) { + result = re().mk_inter(a, b2); + return BR_REWRITE1; } - if (re().is_complement(b1, bc) && a == bc) { + if (are_complements(a, b1)) { result = mk_empty(); return BR_DONE; } @@ -3008,10 +3071,19 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { return BR_REWRITE2; } } - if ((re().is_complement(a, ac) && ac == b) || - (re().is_complement(b, bc) && bc == a)) { - result = mk_empty(); - return BR_DONE; + else { + if (get_id(a) > get_id(b)) { + result = re().mk_inter(b, a); + return BR_DONE; + } + if (is_subset(a, b)) { + result = a; + return BR_DONE; + } + if (is_subset(b, a)) { + result = b; + return BR_DONE; + } } if (re().is_to_re(b)) std::swap(a, b); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 8464b2fd4..541a08f9f 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -189,6 +189,9 @@ class seq_rewriter { expr_ref mk_derivative(expr* ele, expr* r); expr_ref mk_derivative_rec(expr* ele, expr* r); + bool are_complements(expr* r1, expr* r2) const; + bool is_subset(expr* r1, expr* r2) const; + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_seq_length(expr* a, expr_ref& result); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b6c438546..2a8c2e3a4 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -223,7 +223,12 @@ namespace smt { expr_ref d(m); expr_ref head = th.mk_nth(s, i); d = re().mk_derivative(m.mk_var(0, m.get_sort(head)), r); + // timer tm; rewrite(d); + // std::cout << d->get_id() << " " << tm.get_seconds() << "\n"; + // if (tm.get_seconds() > 1) + // std::cout << d << "\n"; + // std::cout.flush(); literal_vector conds; conds.push_back(~lit); conds.push_back(th.m_ax.mk_le(th.mk_len(s), idx)); @@ -297,6 +302,7 @@ namespace smt { * within the same Regex. */ bool seq_regex::coallesce_in_re(literal lit) { + return false; expr* s = nullptr, *r = nullptr; expr* e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); From 5f9973d8c4b1cbd86dadb58da8425d5e2acfc1a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jun 2020 16:28:53 -0700 Subject: [PATCH 11/11] fix #4508 Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 2905d334c..ee74e90a2 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -330,7 +330,7 @@ namespace sat { m_stats.m_num_conflicts++; TRACE("ba", display(tout, c, true); ); if (!validate_conflict(c)) { - display(std::cout, c, true); + IF_VERBOSE(0, display(verbose_stream(), c, true)); UNREACHABLE(); } SASSERT(validate_conflict(c)); @@ -2941,6 +2941,8 @@ namespace sat { void ba_solver::pre_simplify() { VERIFY(s().at_base_lvl()); + if (s().inconsistent()) + return; m_constraint_removed = false; xor_finder xf(s()); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]); @@ -2983,6 +2985,8 @@ namespace sat { void ba_solver::simplify() { if (!s().at_base_lvl()) s().pop_to_base_level(); + if (s().inconsistent()) + return; unsigned trail_sz, count = 0; do { trail_sz = s().init_trail_size();