diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 9da36b27a..660dcab28 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -364,6 +364,13 @@ namespace recfun { return alloc(def, m(), m_fid, name, n, domain, range, is_generated); } + func_decl *util::find_def_decl(symbol const &name, unsigned n, sort *const *params, sort *range, bool is_generated) { + def d(m_manager, m_fid, name, n, params, range, is_generated); + if (m_plugin->has_def(d.get_decl())) + return d.get_decl(); + return nullptr; + } + void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { expr_ref rhs1(rhs, m()); if (!is_macro) @@ -551,6 +558,7 @@ namespace recfun { } } + expr_ref plugin::redirect_ite(replace& subst, unsigned n, var * const* vars, expr * e) { expr_ref result(e, m()); util u(m()); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index d9fe07dcf..fe241483e 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -211,6 +211,7 @@ namespace recfun { case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); } bool is_defined(func_decl* f) {return has_case_def(f) && !get_def(f).get_cases().empty(); } + func_decl_ref_vector get_rec_funs() { func_decl_ref_vector result(m()); for (auto& kv : m_defs) result.push_back(kv.m_key); @@ -250,7 +251,7 @@ namespace recfun { bool is_num_rounds(expr * e) const { return is_app_of(e, m_fid, OP_NUM_ROUNDS); } bool owns_app(app * e) const { return e->get_family_id() == m_fid; } bool contains_def(expr* e); // expression contains a def - + func_decl *find_def_decl(symbol const &name, unsigned n, sort *const *params, sort *range, bool is_generated); //has_defs(); } diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 5951d953d..ce2070cfd 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -34,7 +34,6 @@ namespace seq { a(m), seq(m), m_sk(m, r), - m_not_contains(m), m_clause(m), m_trail(m) {} @@ -1104,37 +1103,41 @@ namespace seq { VERIFY(seq.str.is_replace_all(r, s, p, t)); recfun::util rec(m); recfun::decl::plugin& plugin = rec.get_plugin(); - recfun_replace replace(m); sort* srt = s->get_sort(); sort* domain[4] = { srt, srt, srt, srt }; - auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true); - func_decl* ra = d.get_def()->get_decl(); - // vars: vs=var(3), vp=var(2), vt=var(1), vr=var(0) - var_ref vs(m.mk_var(3, srt), m); - var_ref vp(m.mk_var(2, srt), m); - var_ref vt(m.mk_var(1, srt), m); - var_ref vr(m.mk_var(0, srt), m); - var* vars[4] = { vs, vp, vt, vr }; - // base case: empty s or empty p -> r = s (no replacements) - expr_ref test1(m.mk_or(seq.str.mk_is_empty(vs), seq.str.mk_is_empty(vp)), m); - expr_ref branch1(m.mk_eq(vr, vs), m); - // match case: prefix(p, s) -> s = p ++ s_tail, r = t ++ r_tail, ra(s_tail, p, t, r_tail) - expr_ref s_tail(m_sk.mk_prefix_inv(vp, vs), m); - expr_ref r_tail(m_sk.mk_prefix_inv(vt, vr), m); - expr* args_match[4] = { s_tail, vp, vt, r_tail }; - expr_ref test2(seq.str.mk_prefix(vp, vs), m); - expr_ref branch2(m.mk_and(m.mk_eq(vs, seq.str.mk_concat(vp, s_tail)), - m.mk_eq(vr, seq.str.mk_concat(vt, r_tail)), - m.mk_app(ra, 4, args_match)), m); - // no-match case: copy first char, ra(s[1:], p, t, r[1:]) - expr_ref s_head(m), s_tail2(m); - m_sk.decompose(vs, s_head, s_tail2); - expr_ref r_tail2(m_sk.mk_tail(vr, a.mk_int(0)), m); - expr* args_skip[4] = { s_tail2, vp, vt, r_tail2 }; - expr_ref branch3(m.mk_and(m.mk_eq(vr, seq.str.mk_concat(s_head, r_tail2)), - m.mk_app(ra, 4, args_skip)), m); - expr_ref body(m.mk_ite(test1, branch1, m.mk_ite(test2, branch2, branch3)), m); - plugin.set_definition(replace, d, false, 4, vars, body); + auto ra = rec.find_def_decl(symbol("ra"), 4, domain, m.mk_bool_sort(), true); + + if (!ra) { + recfun_replace replace(m); + auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true); + ra = d.get_def()->get_decl(); + // vars: vs=var(3), vp=var(2), vt=var(1), vr=var(0) + var_ref vs(m.mk_var(3, srt), m); + var_ref vp(m.mk_var(2, srt), m); + var_ref vt(m.mk_var(1, srt), m); + var_ref vr(m.mk_var(0, srt), m); + var *vars[4] = {vs, vp, vt, vr}; + // base case: empty s or empty p -> r = s (no replacements) + expr_ref test1(m.mk_or(seq.str.mk_is_empty(vs), seq.str.mk_is_empty(vp)), m); + expr_ref branch1(m.mk_eq(vr, vs), m); + // match case: prefix(p, s) -> s = p ++ s_tail, r = t ++ r_tail, ra(s_tail, p, t, r_tail) + expr_ref s_tail(m_sk.mk_prefix_inv(vp, vs), m); + expr_ref r_tail(m_sk.mk_prefix_inv(vt, vr), m); + expr *args_match[4] = {s_tail, vp, vt, r_tail}; + expr_ref test2(seq.str.mk_prefix(vp, vs), m); + expr_ref branch2(m.mk_and(m.mk_eq(vs, seq.str.mk_concat(vp, s_tail)), + m.mk_eq(vr, seq.str.mk_concat(vt, r_tail)), m.mk_app(ra, 4, args_match)), + m); + // no-match case: copy first char, ra(s[1:], p, t, r[1:]) + expr_ref s_head(m), s_tail2(m); + m_sk.decompose(vs, s_head, s_tail2); + expr_ref r_tail2(m_sk.mk_tail(vr, a.mk_int(0)), m); + expr *args_skip[4] = {s_tail2, vp, vt, r_tail2}; + expr_ref branch3(m.mk_and(m.mk_eq(vr, seq.str.mk_concat(s_head, r_tail2)), m.mk_app(ra, 4, args_skip)), m); + expr_ref body(m.mk_ite(test1, branch1, m.mk_ite(test2, branch2, branch3)), m); + TRACE(seq, tout << body << "\n"); + plugin.set_definition(replace, d, false, 4, vars, body); + } expr* args[4] = { s, p, t, r }; expr_ref lit(m.mk_app(ra, 4, args), m); add_clause(lit); @@ -1358,14 +1361,17 @@ namespace seq { auto ca = purify(_a); auto cb = purify(_b); sort* srt = ca->get_sort(); + recfun::util rec(m); + sort *domain[2] = {srt, srt}; + func_decl *not_contains = rec.find_def_decl(symbol("nc"), 2, domain, m.mk_bool_sort(), true); + + if (!not_contains) { - if (!m_not_contains || m_not_contains->get_domain(0) != srt) { - recfun::util rec(m); recfun::decl::plugin& plugin = rec.get_plugin(); recfun_replace rf(m); - sort* domain[2] = { srt, srt }; + auto d = plugin.ensure_def(symbol("nc"), 2, domain, m.mk_bool_sort(), true); - m_not_contains = d.get_def()->get_decl(); + not_contains = d.get_def()->get_decl(); var_ref vs(m.mk_var(1, srt), m); var_ref vp(m.mk_var(0, srt), m); expr_ref len_s(seq.str.mk_length(vs), m); @@ -1376,7 +1382,7 @@ namespace seq { expr_ref pref(seq.str.mk_prefix(vp, vs), m); expr_ref hd(seq.str.mk_unit(seq.str.mk_nth_i(vs, a.mk_int(0))), m); expr_ref decomp(m.mk_eq(vs, seq.str.mk_concat(hd, tail)), m); - expr_ref else_branch(m.mk_and(m.mk_not(pref), m.mk_and(decomp, m.mk_app(m_not_contains.get(), 2, nc_args))), m); + expr_ref else_branch(m.mk_and(m.mk_not(pref), m.mk_and(decomp, m.mk_app(not_contains, 2, nc_args))), m); expr_ref body(m.mk_ite(a.mk_gt(len_p, len_s), m.mk_true(), m.mk_ite(m.mk_eq(len_p, len_s), @@ -1388,7 +1394,7 @@ namespace seq { } expr* app_args[2] = { ca.get(), cb.get() }; - expr_ref nc_app(m.mk_app(m_not_contains.get(), 2, app_args), m); + expr_ref nc_app(m.mk_app(not_contains, 2, app_args), m); expr_ref cnt(e, m); add_clause(cnt, nc_app); } diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 53d448f7d..29fffe00f 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -32,7 +32,6 @@ namespace seq { arith_util a; seq_util seq; skolem m_sk; - func_decl_ref m_not_contains; expr_ref_vector m_clause; expr_ref_vector m_trail; obj_map m_purified; diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index d2dffaf98..d2265532a 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -150,6 +150,7 @@ namespace smt { } void theory_recfun::push(propagation_item* p) { + TRACE(recfun, tout << "push " << p << "\n"); m_propagation_queue.push_back(p); ctx.push_trail(push_back_vector>(m_propagation_queue)); }