diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index 96b3df3ed..b0f2b932b 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -26,6 +26,7 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_suffix = "seq.s.prefix"; m_accept = "aut.accept"; m_tail = "seq.tail"; + m_slice = "seq.slice"; m_left = "seq.left"; m_right = "seq.right"; m_seq_first = "seq.first"; @@ -159,6 +160,16 @@ bool skolem::is_tail(expr* e, expr*& s, expr*& idx) const { return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true); } +bool skolem::is_slice(expr* e, expr*& s) const { + expr* l = nullptr; + expr* r = nullptr; + return is_slice(e, s, l, r); +} + +bool skolem::is_slice(expr* e, expr*& s, expr*& l, expr*& r) const { + return is_slice(e) && (s = to_app(e)->get_arg(0), l = to_app(e)->get_arg(1), r = to_app(e)->get_arg(2), true); +} + bool skolem::is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z) { if (!is_skolem(m_left, e) && !is_skolem(m_right, e)) return false; diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 4e327f0fa..472cb2503 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -32,6 +32,7 @@ namespace seq { symbol m_prefix, m_suffix; symbol m_tail; + symbol m_slice; symbol m_left, m_right; symbol m_seq_first, m_seq_last; symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t. @@ -87,6 +88,7 @@ namespace seq { expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_right, t, s, offset); } expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); } + expr_ref mk_slice(expr* s, expr* l, expr* r) { return mk(m_slice, s, l, r); } expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); } expr_ref mk_postp(expr* s, expr* i) { return mk(m_postp, s, i); } expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); } @@ -116,6 +118,7 @@ namespace seq { bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); } bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); } bool is_tail(expr* e) const { return is_skolem(m_tail, e); } + bool is_slice(expr* e) const { return is_skolem(m_slice, e); } bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); } bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); } bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); } @@ -154,6 +157,8 @@ namespace seq { bool is_tail(expr* e, expr*& s, expr*& idx) const; bool is_tail_u(expr* e, expr*& s, unsigned& idx) const; bool is_tail(expr* e, expr*& s) const; + bool is_slice(expr* e, expr*& s, expr*& l, expr*& r) const; + bool is_slice(expr* e, expr*& s) const; bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); } bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); } bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); } diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 5e835cda3..92e18b3a5 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1155,6 +1155,37 @@ namespace seq { return true; } + euf::snode* nielsen_graph::get_slice(euf::snode* v, expr* left, expr* right) { + SASSERT(v && v->get_expr() && left && right); + SASSERT(v->is_var()); + + expr_ref new_arg(v->get_expr(), m); + expr_ref new_l(left, m), new_r(right, m); + expr* arg, *l, *r; + std::cout << "Creating slice for " << mk_pp(new_arg, m) << "; " << mk_pp(new_l, m) << "; " << mk_pp(new_r, m) << std::endl; + + if (m_sk.is_slice(new_arg, arg, l, r)) { + new_l = a.mk_add(left, l); + m_rw(new_l); + new_r = a.mk_add(right, r); + m_rw(new_r); + new_arg = arg; + } + expr_ref slice = m_sk.mk_slice(new_arg, new_l, new_r); + std::cout << "Got " << mk_pp(slice, m) << std::endl; + return m_sg.mk(slice); + } + + + euf::snode* nielsen_graph::get_tail(euf::snode* v, expr* cnt, const bool fwd) { + if (fwd) + return get_slice(v, cnt, a.mk_int(0)); + return get_slice(v, a.mk_int(0), cnt); + } + + euf::snode* nielsen_graph::get_tail(euf::snode* v, const unsigned cnt, const bool fwd) { + return get_tail(v, a.mk_int(cnt), fwd); + } simplify_result nielsen_node::simplify_and_init(ptr_vector const& cur_path) { if (m_is_extended) @@ -1680,7 +1711,7 @@ namespace seq { inc_run_idx(); ptr_vector cur_path; // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search - const search_result r = search_dfs(m_root, cur_path); + const search_result r = search_dfs(m_root, cur_path); // the main search loop IF_VERBOSE(1, verbose_stream() << " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes << " max_depth=" << m_stats.m_max_depth << " extensions=" << m_stats.m_num_extensions @@ -1722,8 +1753,7 @@ namespace seq { } nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node, - ptr_vector& cur_path, - const unsigned depth) { + ptr_vector& cur_path, const unsigned depth) { ++m_stats.m_num_dfs_nodes; // std::cout << m_stats.m_num_dfs_nodes << std::endl; @@ -1885,6 +1915,7 @@ namespace seq { // explore children bool any_unknown = false; + bool all_general_conflict = true; for (nielsen_edge *e : node->outgoing()) { cur_path.push_back(e); // Push a solver scope for this edge and assert its side integer @@ -1922,8 +1953,15 @@ namespace seq { cur_path.pop_back(); if (r == search_result::unknown) any_unknown = true; + if (!e->tgt()->is_general_conflict()) + all_general_conflict = false; } + if (all_general_conflict) { + SASSERT(!any_unknown); + // mark it such that we do not have to reconsider it even after a hot-restart + node->set_general_conflict(); + } if (!any_unknown) { node->set_child_conflict(); return search_result::unsat; @@ -2236,7 +2274,8 @@ namespace seq { for (unsigned j = 1; j < i; ++j) { prefix_sn = dir_concat(m_sg, prefix_sn, char_toks[j], fwd); } - euf::snode* replacement = dir_concat(m_sg, prefix_sn, var_node, fwd); + euf::snode* replacement = dir_concat(m_sg, prefix_sn, + get_tail(var_node, compute_length_expr(prefix_sn).get(), fwd), fwd); nielsen_subst s(var_node, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_node), compute_length_expr(prefix_sn))), eq.m_dep); @@ -2304,7 +2343,7 @@ namespace seq { child->apply_subst(m_sg, s1); - euf::snode* replacement = dir_concat(m_sg, char_head, var_head, fwd); + euf::snode* replacement = dir_concat(m_sg, char_head, get_tail(var_head, a.mk_int(1), fwd), fwd); child = mk_child(node); e = mk_edge(node, child, false); const nielsen_subst s2(var_head, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_head), a.mk_int(1))), eq.m_dep); @@ -4249,7 +4288,8 @@ namespace seq { SASSERT(n->m_conflict_external_literal == sat::null_literal); continue; } - SASSERT(n->outgoing().empty()); + // not true anymore since we might have done a hot-restart where we previously created the child: + //SASSERT(n->outgoing().empty()); SASSERT(n->is_currently_conflict()); if (n->m_conflict_external_literal != sat::null_literal) // We know from the outer solver that this literal is assigned true and contradicts node constraint diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 8dc179761..b03a89f42 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -475,7 +475,7 @@ namespace seq { // var may be s_var or s_power; sgraph::subst uses pointer identity matching SASSERT(var->is_var() || var->is_power() || var->is_unit()); SASSERT(!var->is_unit() || repl->is_char_or_unit()); - // SASSERT(!repl->collect_tokens().contains(var)); // for now - maybe we want to drop this later again + SASSERT(!repl->collect_tokens().contains(var)); // for now - maybe we want to drop this later again } // an eliminating substitution does not contain the variable in the replacement @@ -694,6 +694,8 @@ namespace seq { backtrack_reason reason() const { return m_reason; } + void clear_reason() { m_reason = backtrack_reason::unevaluated; } + void set_child_conflict() { SASSERT(m_reason == backtrack_reason::unevaluated); SASSERT(!m_conflict_internal); @@ -1118,6 +1120,12 @@ namespace seq { // stores it in projection_re iff SCC coverage has grown. bool try_extract_partial_projection(euf::snode* root_re, euf::snode*& projection_re); + euf::snode* get_slice(euf::snode* v, expr* left, expr* right); + + euf::snode* get_tail(euf::snode* v, expr* cnt, bool fwd = true); + + euf::snode* get_tail(euf::snode* v, unsigned cnt, bool fwd = true); + // Apply the Parikh image filter to a node: generate modular length // constraints from regex memberships and append them to the node's // constraints. Also performs a lightweight feasibility pre-check; diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 96c0e3013..ac7c2938d 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -387,11 +387,21 @@ namespace seq { return dot_html_escape(os.str()); } + std::string decode_recursive_name(expr* e, ast_manager& m) { + SASSERT(e && is_app(e)); + th_rewriter rw(m); + const skolem sk(m, rw); + expr* arg = e, *l, *r; + while (sk.is_slice(arg, arg, l, r)) { } + if (to_app(arg)->get_num_args() != 0) + return ""; + return dot_html_escape(to_app(arg)->get_decl()->get_name().str()); + } + // Helper: render a snode as an HTML label for DOT output. // Groups consecutive s_char tokens into quoted strings, renders s_var by name, // shows s_power with superscripts, s_unit by its inner expression, // and falls back to mk_pp, HTML-escaped, for other token kinds. - std::string snode_label_html(euf::snode const* n, obj_map& names, uint64_t& next_id, ast_manager& m) { if (!n) return "null"; seq_util seq(m); @@ -437,8 +447,9 @@ namespace seq { if (!e) { result += "#" + std::to_string(tok->id()); } else if (tok->is_var()) { - if (to_app(e)->get_num_args() == 0) { - result += to_app(e)->get_decl()->get_name().str(); + std::string name = decode_recursive_name(e, m); + if (!name.empty()) { + result += name; } else if (names.contains(e)) result += names[e]; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 54d1ec52b..e479f8b3d 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -713,6 +713,11 @@ namespace smt { if (node->is_general_conflict()) // all its children are general conflicts as well - nothing to do continue; + if (node->reason() == seq::backtrack_reason::children_failed) { + SASSERT(!node->is_general_conflict()); + node->clear_reason(); + } + if (node->is_external_conflict()) node->clear_local_conflict();