From 6f1eafaa5c39de31b9b13845b50593c85a04a641 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 29 Jun 2026 16:52:16 +0200 Subject: [PATCH] Better caching/hashing First try for reintroducting subsumption --- src/ast/euf/euf_snode.h | 30 +++ src/smt/seq/seq_nielsen.cpp | 372 +++++++++++++++++++++------------ src/smt/seq/seq_nielsen.h | 250 ++++++++++++++++------ src/smt/seq/seq_nielsen_pp.cpp | 2 +- src/smt/seq/seq_regex.cpp | 59 +----- src/smt/seq/seq_regex.h | 17 +- src/smt/seq/seq_state.h | 12 +- src/smt/theory_nseq.cpp | 27 ++- src/test/seq_nielsen.cpp | 68 ------ 9 files changed, 486 insertions(+), 351 deletions(-) diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index e1a05d175b..b19d285f2c 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -123,6 +123,36 @@ namespace euf { return arg(0); } + // equal modulo slicing + bool similar(const snode* str, ast_manager& m) const { + if (m_length != str->m_length) + return false; + auto it1 = begin(); + auto it2 = str->begin(); + for (; it1 != end() && it2 != str->end(); it1++, it2++) { + if ((*it1)->kind() != (*it2)->kind()) + return false; + if ((*it1)->is_var()) { + expr* e1 = (*it1)->get_expr(); + expr* e2 = (*it2)->get_expr(); + th_rewriter th(m); + seq::skolem sk(m, th); + while (sk.is_slice(e1)) { + e1 = to_app(e1)->get_arg(0); + } + while (sk.is_slice(e2)) { + e2 = to_app(e2)->get_arg(0); + } + if (e1 != e2) + return false; + continue; + } + if (*it1 != *it2) + return false; + } + return true; + } + // Iterator over the leaf tokens of this snode, modulo concatenation // (analogous to first()/last()/at()): an s_concat tree is flattened to // its leaf tokens in left-to-right order, empty nodes are skipped, and diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 22c26f8a6b..326366a484 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -363,12 +363,11 @@ namespace seq { SASSERT(m_constraints.size() == parent.m_constraints.size()); } - void nielsen_node::add_str_eq(str_eq& eq) { + void nielsen_node::add_str_eq(const str_eq& eq) { SASSERT(eq.m_lhs != nullptr); SASSERT(eq.m_rhs != nullptr); if (eq.is_trivial()) return; - eq.sort(); // check if root node contains this equation already if (std::ranges::any_of(str_eqs(), [&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; })) @@ -377,10 +376,9 @@ namespace seq { m_str_eq.push_back(eq); } - void nielsen_node::add_str_deq(str_deq& deq) { + void nielsen_node::add_str_deq(const str_deq& deq) { SASSERT(deq.m_lhs != nullptr); SASSERT(deq.m_rhs != nullptr); - deq.sort(); // check if root node contains this equation already if (std::ranges::any_of(str_deqs(), [&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; })) @@ -507,6 +505,59 @@ namespace seq { } } + unsigned nielsen_node::canonize_and_compute_node_hash() { + unsigned hash = 457260179; + std::sort(str_eqs().begin(), str_eqs().end()); + for (auto const& e : str_eqs()) { + hash += 433867097 * e.hash(); + } + std::sort(str_deqs().begin(), str_deqs().end()); + for (auto const& e : str_deqs()) { + hash += 982048589 * e.hash(); + } + std::sort(str_mems().begin(), str_mems().end()); + for (auto const& e : str_mems()) { + hash += 736051237 * e.hash(); + } + + for (auto const& [uid, cr] : char_ranges()) { + // not sorted; computation needs to be commutative + for (auto const& rg : cr.first.ranges()) { + hash += 473672767 * (750753749 * rg.m_lo + rg.m_hi) + uid; + } + } + return hash; + } + + bool nielsen_node::is_node_sibling(nielsen_node const* n) { + if (n->str_eqs().size() != str_eqs().size()) + return false; + if (n->str_deqs().size() != str_deqs().size()) + return false; + if (n->str_mems().size() != str_mems().size()) + return false; + if (n->char_ranges().size() != char_ranges().size()) + return false; + for (unsigned i = 0; i < str_eqs().size(); i++) { + if (str_eqs()[i] != n->str_eqs()[i]) + return false; + } + for (unsigned i = 0; i < str_deqs().size(); i++) { + if (str_deqs()[i] != n->str_deqs()[i]) + return false; + } + for (unsigned i = 0; i < str_mems().size(); i++) { + if (str_mems()[i] != n->str_mems()[i]) + return false; + } + for (unsigned i = 0; i < char_ranges().size(); i++) { + // TODO: Check once more + if (char_ranges()[i] != n->char_ranges()[i]) + return false; + } + return true; + } + void nielsen_node::add_char_range(euf::snode const* sym_char, char_set const& range, dep_tracker dep) { if (sym_char->is_char()) { // for a concrete character just check if it matches @@ -558,8 +609,8 @@ namespace seq { // ----------------------------------------------- nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver) : - m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_sk(m, m_rw), - m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)), + m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m), + m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)), m_partial_dfa_pin(sg.get_manager()) { } @@ -619,38 +670,37 @@ namespace seq { void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode *l, smt::enode *r) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); - str_eq eq(lhs, rhs, dep); + str_eq eq(m, lhs, rhs, dep); m_root->add_str_eq(eq); } void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const { const dep_tracker dep = m_dep_mgr.mk_leaf(l); - str_deq deq(lhs, rhs, dep); + str_deq deq(m, lhs, rhs, dep); m_root->add_str_deq(deq); } void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal l) const { const dep_tracker dep = m_dep_mgr.mk_leaf(l); - m_root->add_str_mem(str_mem(str, regex, dep)); + m_root->add_str_mem(str_mem(m, str, regex, dep)); } // test-friendly overloads (no external dependency tracking) void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); - str_eq eq(lhs, rhs, dep); - eq.sort(); + const str_eq eq(m, lhs, rhs, dep); m_root->add_str_eq(eq); } void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); - str_deq deq(lhs, rhs, dep); + const str_deq deq(m, lhs, rhs, dep); m_root->add_str_deq(deq); } void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) const { const dep_tracker dep = nullptr; - str_mem mem(str, regex, dep); + const str_mem mem(m, str, regex, dep); m_root->add_str_mem(mem); } @@ -678,6 +728,7 @@ namespace seq { m_projection_extract_idx = 0; m_explored_automaton.reset(); m_unsat_node_cache.clear(); + m_siblings.clear(); m_num_cache_hits = 0; m_eager_active = false; m_eager_leaf = nullptr; @@ -1616,7 +1667,7 @@ namespace seq { euf::snode const* deriv = fwd ? sg.brzozowski_deriv(mem.m_regex, tok) : reverse_brzozowski_deriv(sg, mem.m_regex, tok); - TRACE(seq, tout << mem_pp(mem, m) << " d: " << spp(deriv, m) << "\n"); + TRACE(seq, tout << mem_pp(mem) << " d: " << spp(deriv, m) << "\n"); if (!deriv) break; if (deriv->is_fail()) { @@ -1721,7 +1772,7 @@ namespace seq { // check for regex memberships that are immediately infeasible for (str_mem& mem : m_str_mem) { if (mem.is_contradiction(this)) { - TRACE(seq, tout << "contradiction " << mem_pp(mem, m) << "\n"); + TRACE(seq, tout << "contradiction " << mem_pp(mem) << "\n"); set_general_conflict(); set_conflict(backtrack_reason::regex, mem.m_dep); return simplify_result::conflict; @@ -1949,6 +2000,9 @@ namespace seq { if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth) break; ptr_vector cur_path; + // The active-path index is per-traversal; clear it so a sat-aborted + // previous iteration cannot leave stale ancestors behind. + m_siblings.clear(); // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search SASSERT(!m_root->is_currently_conflict()); const search_result r = search_dfs(m_root, cur_path); // the main search loop @@ -2014,7 +2068,7 @@ namespace seq { dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); lhs = eager_rewrite(lhs, dep); rhs = eager_rewrite(rhs, dep); - str_eq eq(lhs, rhs, dep); + str_eq eq(m, lhs, rhs, dep); eq.sort(); m_eager_leaf->add_str_eq(eq); } @@ -2024,7 +2078,7 @@ namespace seq { dep_tracker dep = m_dep_mgr.mk_leaf(lit); lhs = eager_rewrite(lhs, dep); rhs = eager_rewrite(rhs, dep); - str_deq deq(lhs, rhs, dep); + str_deq deq(m, lhs, rhs, dep); m_eager_leaf->add_str_deq(deq); } @@ -2033,7 +2087,7 @@ namespace seq { dep_tracker dep = m_dep_mgr.mk_leaf(lit); str = eager_rewrite(str, dep); regex = eager_rewrite(regex, dep); - m_eager_leaf->add_str_mem(str_mem(str, regex, dep)); + m_eager_leaf->add_str_mem(str_mem(m, str, regex, dep)); } // Drive the deterministic chain from the current leaf to a fixpoint. Each step @@ -2044,7 +2098,7 @@ namespace seq { nielsen_graph::search_result nielsen_graph::eager_close() { SASSERT(m_eager_active && m_eager_leaf); ++m_stats.m_num_eager_calls; - ptr_vector empty_path; + const ptr_vector empty_path; // Rigid defined ops (str.replace_all, …) must never be Nielsen-substituted; // a rigid term is inherited down the whole chain, so a single check on the @@ -2111,6 +2165,12 @@ namespace seq { case backtrack_reason::regex_widening: case backtrack_reason::symbol_clash: case backtrack_reason::character_range: + // a sibling (subsumption / loop-cut) conflict depends only on the node's + // string signature: a cut equates two nodes by their string constraints, + // and a sibling closure is reached only when every leaf below is itself a + // string-only conflict or a cut. (Whether the closure is *cacheable* is a + // separate, stronger question handled via the lowlink in search_dfs.) + case backtrack_reason::sibling: return true; default: // arithmetic, parikh_image, external, children_failed, unevaluated @@ -2124,71 +2184,6 @@ namespace seq { return reason_is_string_only(n->m_reason); } - std::vector nielsen_graph::compute_node_signature(nielsen_node const* n) { - std::vector sig; - // string equalities (order-independent) - { - std::vector> v; - for (auto const& e : n->str_eqs()) { - v.emplace_back(e.m_lhs->id(), e.m_rhs->id()); - } - std::sort(v.begin(), v.end()); - sig.push_back(static_cast(v.size())); - for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); } - } - sig.push_back(UINT_MAX); // section separator - // string disequalities - { - std::vector> v; - for (auto const& d : n->str_deqs()) { - v.emplace_back(d.m_lhs->id(), d.m_rhs->id()); - } - std::ranges::sort(v); - sig.push_back(static_cast(v.size())); - for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); } - } - sig.push_back(UINT_MAX); - // regex memberships incl. view/guard metadata - { - std::vector> v; - for (auto const& mm : n->str_mems()) - v.push_back({ mm.m_str->id(), mm.m_regex->id(), - static_cast(mm.m_kind), - mm.m_root ? mm.m_root->id() : UINT_MAX, - mm.m_nu, mm.m_discharged ? 1u : 0u }); - std::ranges::sort(v); - sig.push_back(static_cast(v.size())); - for (auto const& a : v) { - for (unsigned x : a) { - sig.push_back(x); - } - } - } - sig.push_back(UINT_MAX); - // character-range constraints (per symbolic unit) - { - std::vector> v; - for (auto const& [uid, cr] : n->char_ranges()) { - std::vector entry; - entry.push_back(uid); - for (auto const& rg : cr.first.ranges()) { - entry.push_back(rg.m_lo); - entry.push_back(rg.m_hi); - } - v.push_back(std::move(entry)); - } - std::sort(v.begin(), v.end()); - sig.push_back(static_cast(v.size())); - for (auto const& e : v) { - sig.push_back(static_cast(e.size())); - for (unsigned x : e) { - sig.push_back(x); - } - } - } - return sig; - } - dep_tracker nielsen_graph::node_all_deps(nielsen_node const* n) const { dep_tracker d = nullptr; for (auto const& e : n->str_eqs()) { @@ -2217,6 +2212,11 @@ namespace seq { SASSERT(depth <= cur_path.size()); m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth); + // structural depth of this node on the current DFS path (counts ALL edges, + // unlike `depth` which discounts progress edges). Used by the subsumption + // rule to identify and compare ancestors. + node->m_dfs_path_pos = cur_path.size(); + if (node->is_general_conflict()) { ++m_stats.m_num_simplify_conflict; return search_result::unsat; @@ -2262,9 +2262,8 @@ namespace seq { // constraints — so we prune without re-exploring its subtree. We derive // the conflict from this node's own constraint deps (a sound over-approx). { - const std::vector sig = compute_node_signature(node); - if (m_unsat_node_cache.contains(sig)) { - node->set_conflict(backtrack_reason::regex, node_all_deps(node)); + if (m_unsat_node_cache.contains(node)) { + node->set_conflict(backtrack_reason::sibling, node_all_deps(node)); node->set_general_conflict(); node->m_unsat_cacheable = true; ++m_stats.m_num_simplify_conflict; @@ -2324,7 +2323,8 @@ namespace seq { node->set_conflict(backtrack_reason::regex, dep); // string-only conflict (empty intersection) → memoize. node->m_unsat_cacheable = true; - m_unsat_node_cache.insert(compute_node_signature(node)); + node->canonize_and_compute_final_node_hash(); + m_unsat_node_cache.insert(node); return search_result::unsat; } assert_node_side_constraints(node); @@ -2334,6 +2334,7 @@ namespace seq { ++m_stats.m_num_simplify_conflict; return search_result::unsat; } + node->canonize_and_compute_final_node_hash(); m_sat_node = node; m_sat_path = cur_path; return search_result::sat; @@ -2342,6 +2343,34 @@ namespace seq { if (node->is_currently_conflict()) return search_result::unsat; + // ------------------------------------------------------------------- + // Subsumption rule (Nielsen loop-cut). + // If this node has the SAME string constraints as a node further up the + // current DFS path (an ancestor "sibling"), then every continuation from + // here is already being explored from that ancestor. We must NOT report a + // conflict: the arithmetic side-constraints accumulated along the two paths + // differ, so a model may exist here that does not at the ancestor. Instead + // we CUT — return unsat provisionally and remember (in m_subtree_lowlink) + // the structural depth of the ancestor we defer to. A cut only hardens + // into a genuine conflict at an enclosing node whose entire subtree closes + // with string-only conflicts and self-contained cuts (see the epilogue). + // ------------------------------------------------------------------- + node->canonize_and_compute_final_node_hash(); + { + auto it = m_siblings.find(node); + if (it != m_siblings.end() && !it->second.empty()) { + nielsen_node* anc = it->second.back(); // deepest sibling still on the path + SASSERT(anc != node); + // deps are a sound over-approximation (the node's own constraint + // sources); only used if a children_failed ancestor recurses here. + node->set_conflict(backtrack_reason::sibling, node_all_deps(node)); + node->m_subtree_lowlink = anc->m_dfs_path_pos; // escape level + node->m_subtree_has_cut = true; + ++m_stats.m_num_sibling_cut; + return search_result::unsat; + } + } + // depth bound check if (depth >= m_depth_bound) return search_result::unknown; @@ -2370,9 +2399,18 @@ namespace seq { ++m_stats.m_num_extensions; } + // Register this node on the active path so descendants can detect a loop + // back to it (the subsumption cut above). The hash/signature is already + // computed (cut check) so the structural key is stable. Popped after the + // child loop. A bucket holds at most one on-path node per signature + // (a second equal node on the path would have been cut before reaching here). + m_siblings[node].push_back(node); + // explore children bool any_unknown = false; bool all_general_conflict = true; + bool subtree_has_cut = false; // a sibling loop-cut occurred below + unsigned min_child_lowlink = UINT_MAX; // min depth any sibling cut below escapes to for (nielsen_edge *e : node->outgoing()) { cur_path.push_back(e); // Push a solver scope for this edge and assert its side integer @@ -2397,25 +2435,39 @@ namespace seq { m_length_solver.pop(1); if (r == search_result::sat) + // m_siblings entry is left dangling; it is cleared at the start of + // the next iteration (and the whole search returns sat now anyway). return search_result::sat; cur_path.pop_back(); if (r == search_result::unknown) any_unknown = true; + else { // unsat: fold the child's lowlink (cut escape level) into ours + min_child_lowlink = std::min(min_child_lowlink, e->tgt()->m_subtree_lowlink); + subtree_has_cut |= e->tgt()->m_subtree_has_cut; + } if (!e->tgt()->is_general_conflict()) all_general_conflict = false; } + // leave the active path (mirrors the push above) + SASSERT(!m_siblings[node].empty() && m_siblings[node].back() == node); + m_siblings[node].pop_back(); + 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(); } + node->m_subtree_has_cut = subtree_has_cut; if (!any_unknown) { - node->set_child_conflict(); - // Memoize this internal UNSAT iff its whole subtree closed for - // string/regex-only reasons (no child relied on arithmetic / Parikh / - // external context). Then a same-signature node found via any other - // path is pruned by the lookup above. + // The subtree closed. Record our lowlink and decide how strong a + // conflict we may claim. self_contained == no sibling cut below + // escapes above this node, i.e. every loop is internal to our subtree. + node->m_subtree_lowlink = min_child_lowlink; + const bool self_contained = (min_child_lowlink >= node->m_dfs_path_pos); + + // string-only closure: every leaf below is a string-only conflict or a + // sibling cut (cuts count as string-only, see reason_is_string_only). bool all_string_only = true; for (nielsen_edge* e : node->outgoing()) { if (!node_unsat_string_only(e->tgt())) { @@ -2423,9 +2475,40 @@ namespace seq { break; } } - node->m_unsat_cacheable = all_string_only; - if (all_string_only) - m_unsat_node_cache.insert(compute_node_signature(node)); + + // Soundness of the subsumption rule: a loop-cut defers to an ancestor + // whose arithmetic side-constraints differ from this path's, so a cut is + // only a valid UNSAT witness when the WHOLE closure is string-only. If a + // cut coexists with an arithmetic / Parikh / external conflict, the cut + // may be hiding a model feasible under this node's distinct side + // constraints — we cannot conclude UNSAT. Report unknown (the node is + // left unmarked and re-explored at a larger depth bound). + if (subtree_has_cut && !all_string_only) + return search_result::unknown; + + if (all_string_only) { + // Subsumption rule: this node is a string-only conflict. Internal + // (has children) closures carry no own deps — collect_conflict_deps + // recurses through them to the genuine conflict / cut leaves below. + node->set_conflict(backtrack_reason::sibling, nullptr); + ++m_stats.m_num_sibling_closure; + if (self_contained) { + // No cut escapes this subtree: the unsat is a property of the + // node's string signature alone. Make it sticky (survives + // hot-restart) and memoize it in the transposition table. + node->set_general_conflict(); + node->m_unsat_cacheable = true; + m_unsat_node_cache.insert(node); + } + else + // Conditional on an ancestor above us; valid for this path only. + node->m_unsat_cacheable = false; + } + else { + // a child relied on arithmetic / Parikh / external context. + node->set_child_conflict(); + node->m_unsat_cacheable = false; + } return search_result::unsat; } return search_result::unknown; @@ -2522,7 +2605,7 @@ namespace seq { child->apply_subst(m_sg, subst); if (!lhs_rest->is_empty() || !rhs_rest->is_empty()) - eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep)); + eqs.push_back(str_eq(m, lhs_rest, rhs_rest, eq.m_dep)); return true; } else @@ -2557,7 +2640,7 @@ namespace seq { child->apply_subst(m_sg, subst); if (!lhs_rest->is_empty() || !rhs_rest->is_empty()) - eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep)); + eqs.push_back(str_eq(m, lhs_rest, rhs_rest, eq.m_dep)); return true; } else @@ -2841,30 +2924,46 @@ namespace seq { e->add_subst(s); child->apply_subst(m_sg, s); } - // child 2: y → ε (progress) + // child 2: y → ε && |x| > 0 (progress) { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, "nielsen var =r", true); const nielsen_subst s(rhead, m_sg.mk_empty_seq(rhead->get_sort()), eq.m_dep); e->add_subst(s); + e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep)); child->apply_subst(m_sg, s); } - // child 3: x → y·x (no progress) + // child 3: x → y && |x| > 0 (progress) { - euf::snode const* replacement = dir_concat(m_sg, rhead, get_tail(lhead, compute_length_expr(rhead).get(), fwd), fwd); + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "nielsen var =", true); + const nielsen_subst s(lhead, rhead, eq.m_dep); + e->add_subst(s); + e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep)); + child->apply_subst(m_sg, s); + } + // child 4: x → y·x && |x| > 0 && |y| > 0 (no progress) + { + auto* tail = get_tail(lhead, compute_length_expr(rhead).get(), fwd); + euf::snode const* replacement = dir_concat(m_sg, rhead, tail, fwd); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, "nielsen var >", false); const nielsen_subst s(lhead, replacement, eq.m_dep); e->add_subst(s); + e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(rhead), a.mk_int(0)), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(tail), a.mk_int(0)), eq.m_dep)); child->apply_subst(m_sg, s); } - // child 4: y → x·y (no progress) + // child 5: y → x·y && |x| > 0 && |y| > 0 (no progress) { - euf::snode const* replacement = dir_concat(m_sg, lhead, get_tail(rhead, compute_length_expr(lhead).get(), fwd), fwd); + auto* tail = get_tail(rhead, compute_length_expr(lhead).get(), fwd); + euf::snode const* replacement = dir_concat(m_sg, lhead, tail, fwd); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, "nielsen var <", false); const nielsen_subst s(rhead, replacement, eq.m_dep); e->add_subst(s); + e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(tail), a.mk_int(0)), eq.m_dep)); child->apply_subst(m_sg, s); } return true; @@ -2939,9 +3038,9 @@ namespace seq { bool rhs_has_symbolic = token_has_variable_length(rhs_toks[0]); int const_diff = 0; if (!lhs_has_symbolic) - const_diff += (int)token_const_length(lhs_toks[0]); + const_diff += token_const_length(lhs_toks[0]); if (!rhs_has_symbolic) - const_diff -= (int)token_const_length(rhs_toks[0]); + const_diff -= token_const_length(rhs_toks[0]); bool seen_variable = lhs_has_symbolic || rhs_has_symbolic; @@ -3055,17 +3154,13 @@ namespace seq { for (unsigned eq_idx = 0; eq_idx < node->str_eqs().size(); ++eq_idx) { str_eq const& eq = node->str_eqs()[eq_idx]; SASSERT(eq.well_formed()); - if (eq.is_trivial()) - continue; - // EqSplit only applies to regex-free equations. - if (!eq.m_lhs->is_regex_free() || !eq.m_rhs->is_regex_free()) - continue; + SASSERT(!eq.is_trivial()); euf::snode_vector lhs_toks, rhs_toks; eq.m_lhs->collect_tokens(lhs_toks); eq.m_rhs->collect_tokens(rhs_toks); - if (lhs_toks.empty() || rhs_toks.empty()) - continue; + SASSERT(!lhs_toks.empty()); + SASSERT(!rhs_toks.empty()); unsigned split_lhs = 0, split_rhs = 0; int padding = 0; @@ -3114,8 +3209,8 @@ namespace seq { auto& eqs = child->str_eqs(); eqs[eq_idx] = eqs.back(); eqs.pop_back(); - eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_dep)); - eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_dep)); + eqs.push_back(str_eq(m, eq1_lhs, eq1_rhs, eq.m_dep)); + eqs.push_back(str_eq(m, eq2_lhs, eq2_rhs, eq.m_dep)); // Int constraints on the edge. // 1) len(pad) = |padding| (if padding variable was created) @@ -3342,7 +3437,7 @@ namespace seq { bool& fwd) { for (str_mem const& mem : node->str_mems()) { if (mem.is_trivial(node)) { - std::cout << "Trivial mem: " << mem_pp(mem, node->graph().get_manager()) << std::endl; + std::cout << "Trivial mem: " << mem_pp(mem) << std::endl; } SASSERT(mem.well_formed() && !mem.is_trivial(node)); @@ -3806,10 +3901,10 @@ namespace seq { child->m_str_mem[mi].m_str = dir_drop(m_sg, child->m_str_mem[mi].m_str, 1, true); // x' ∈ stab(R, Q_ν) (stabilizer view, F = {R}, current state = R) - child->add_str_mem(str_mem::mk_view(xp, R, R, nu, mem.m_dep)); + child->add_str_mem(str_mem::mk_view(m, xp, R, R, nu, mem.m_dep)); // noloop(x'', R, Q_ν) (cycle guard, two-mode monitor, state = R) - child->add_str_mem(str_mem::mk_guard(xpp, R, R, nu, mem.m_dep)); + child->add_str_mem(str_mem::mk_guard(m, xpp, R, R, nu, mem.m_dep)); TRACE(seq, tout << "cycle_decomp: x=" << mk_pp(x->get_expr(), m) << " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n"); @@ -3982,8 +4077,8 @@ namespace seq { } } - child->add_str_mem(str_mem(head, m_p, m_dep)); - child->add_str_mem(str_mem(tail, m_q, m_dep)); + child->add_str_mem(str_mem(m, head, m_p, m_dep)); + child->add_str_mem(str_mem(m, tail, m_q, m_dep)); } return true; } @@ -4269,12 +4364,12 @@ namespace seq { // (1) u1·x = v1 and u2 = x·v2 // (2) u1 = v1·x and x·u2 = v2 if (branch == 0) { - child_eqs.push_back(str_eq(m_sg.mk_concat(u1, x), v1, eq.m_dep)); - child_eqs.push_back(str_eq(u2, m_sg.mk_concat(x, v2), eq.m_dep)); + child_eqs.push_back(str_eq(m, m_sg.mk_concat(u1, x), v1, eq.m_dep)); + child_eqs.push_back(str_eq(m, u2, m_sg.mk_concat(x, v2), eq.m_dep)); } else { - child_eqs.push_back(str_eq(u1, m_sg.mk_concat(v1, x), eq.m_dep)); - child_eqs.push_back(str_eq(m_sg.mk_concat(x, u2), v2, eq.m_dep)); + child_eqs.push_back(str_eq(m, u1, m_sg.mk_concat(v1, x), eq.m_dep)); + child_eqs.push_back(str_eq(m, m_sg.mk_concat(x, u2), v2, eq.m_dep)); } } return true; @@ -4683,7 +4778,6 @@ namespace seq { const expr_ref u_len(compute_length_expr(u), m); const expr_ref v_len(compute_length_expr(v), m); expr_ref len_eq(m.mk_eq(u_len, v_len), m); - str_eq eq_uv(u, v, first.m_dep); sort *char_sort = nullptr; VERIFY(seq().is_seq(u->get_sort(), char_sort)); euf::snode const* a = m_sg.mk(seq().str.mk_unit(m_sk.mk("diseq.a", u->get_expr(), v->get_expr(), char_sort).get())); @@ -4695,8 +4789,8 @@ namespace seq { const expr_ref vp_len(compute_length_expr(vp), m); euf::snode const* wau = dir_concat(m_sg, dir_concat(m_sg, w, a, true), up, true); euf::snode const* wbv = dir_concat(m_sg, dir_concat(m_sg, w, b, true), vp, true); - str_eq u_eq(u, wau, first.m_dep); - str_eq v_eq(v, wbv, first.m_dep); + str_eq u_eq(m, u, wau, first.m_dep); + str_eq v_eq(m, v, wbv, first.m_dep); // Branch 1: |u| < |v| { @@ -4740,9 +4834,17 @@ namespace seq { while (!to_visit.empty()) { nielsen_node const* n = to_visit.back(); to_visit.pop_back(); - if (n->reason() == backtrack_reason::children_failed) { - SASSERT(n->m_conflict_external_literal == sat::null_literal); - SASSERT(!n->m_conflict_internal); + // Recurse through internal closures: children_failed nodes, and sibling + // (subsumption) closures that have children. The latter carry no own + // deps (m_conflict_internal == null) — their justification is the union + // of the genuine conflict / cut leaves below them, gathered by recursing + // (sound: collecting from all leaves never under-approximates). A sibling + // LEAF (a loop cut, or a transposition-cache hit; no children) instead + // contributes its own node_all_deps recorded in m_conflict_internal. + const bool recurse = + n->reason() == backtrack_reason::children_failed || + (n->reason() == backtrack_reason::sibling && !n->outgoing().empty()); + if (recurse) { for (unsigned i = n->outgoing().size(); i > 0; i--) { nielsen_edge const* e = n->outgoing()[i - 1]; to_visit.push_back(e->tgt()); @@ -4794,13 +4896,17 @@ namespace seq { if (n->is_power()) { const expr_ref base = compute_length_expr(n->arg0()); - return expr_ref(a.mk_mul(base.get(), n->arg(1)->get_expr()), m); + expr_ref res(m); + m_a_rw.mk_mul(base.get(), n->arg(1)->get_expr(), res); + return res; } if (n->is_concat()) { const expr_ref left = compute_length_expr(n->arg0()); const expr_ref right = compute_length_expr(n->arg(1)); - return expr_ref(a.mk_add(left, right), m); + expr_ref res(m); + m_a_rw.mk_add(left, right, res); + return res; } //euf::snode const* length_term = nullptr; @@ -5221,7 +5327,7 @@ namespace seq { // TODO: Minimize the conflict here const lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000); TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m) - << " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem, m) << "\n"; + << " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem) << "\n"; display(tout, &node) << "\n"); return result == l_true; } @@ -5452,6 +5558,8 @@ namespace seq { st.update("nseq mod axiomatized disequalities", m_stats.m_ax_diseq); st.update("nseq unsat-cache size", (unsigned) m_unsat_node_cache.size()); st.update("nseq unsat-cache hits", m_num_cache_hits); + st.update("nseq sibling cuts", m_stats.m_num_sibling_cut); + st.update("nseq sibling closures", m_stats.m_num_sibling_closure); } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 8b62a81cba..d5e890fa44 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -39,7 +39,9 @@ Author: #include "ast/ast.h" #include "ast/seq_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "ast/euf/euf_mam.h" #include "ast/euf/euf_sgraph.h" +#include "ast/rewriter/arith_rewriter.h" #include "model/model.h" #include "util/lbool.h" #include "util/dependency.h" @@ -48,7 +50,7 @@ Author: #include "util/rational.h" #include "util/uint_set.h" #include "util/vector.h" -#include +#include #include #include @@ -85,9 +87,9 @@ namespace seq { extended, symbol_clash, parikh_image, - subsumption, // not used; retained for enum completeness arithmetic, regex, + sibling, regex_widening, character_range, smt, @@ -95,24 +97,6 @@ namespace seq { children_failed, }; - inline std::ostream& operator<<(std::ostream& out, backtrack_reason r) { - switch (r) { - case backtrack_reason::unevaluated: return out << "unevaluated"; - case backtrack_reason::extended: return out << "extended"; - case backtrack_reason::symbol_clash: return out << "symbol_clash"; - case backtrack_reason::parikh_image: return out << "parikh_image"; - case backtrack_reason::subsumption: return out << "subsumption"; - case backtrack_reason::arithmetic: return out << "arithmetic"; - case backtrack_reason::regex: return out << "regex"; - case backtrack_reason::regex_widening: return out << "regex_widening"; - case backtrack_reason::character_range: return out << "char range"; - case backtrack_reason::children_failed: return out << "children_failed"; - case backtrack_reason::external: return out << "external"; - case backtrack_reason::smt: return out << "smt"; - default: return out << ""; - } - } - // source of a dependency: identifies an input constraint by kind and index. // kind::eq means a string equality, kind::mem means a regex membership. // index is the 0-based position in the input eq or mem list respectively. @@ -194,17 +178,36 @@ namespace seq { // string equality constraint: lhs = rhs // mirrors ZIPT's StrEq (both sides are regex-free snode trees) struct str_eq { + ast_manager& m; euf::snode const* m_lhs; // assumed to be non-null euf::snode const* m_rhs; // assumed to be non-null dep_tracker m_dep; - str_eq(euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep): - m_lhs(lhs), m_rhs(rhs), m_dep(dep) { + str_eq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep): + m(m), m_lhs(lhs), m_rhs(rhs), m_dep(dep) { SASSERT(well_formed()); + sort(); } - bool operator==(str_eq const& other) const { - return m_lhs == other.m_lhs && m_rhs == other.m_rhs; + str_eq& operator=(const str_eq & other) { + m_lhs = other.m_lhs; + m_rhs = other.m_rhs; + m_dep = other.m_dep; + return *this; + } + + bool operator==(const str_eq& other) const { + return m_lhs->similar(other.m_lhs, m) && m_rhs->similar(other.m_rhs, m); + } + + bool operator<(const str_eq& other) const { + if (m_lhs != other.m_lhs) + return m_lhs < other.m_lhs; + return m_rhs < other.m_rhs; + } + + unsigned hash() const { + return 586947209 * m_lhs->assoc_hash() + m_rhs->assoc_hash(); } // sort so that lhs <= rhs by snode id @@ -224,29 +227,47 @@ namespace seq { struct eq_pp { str_eq const &eq; - ast_manager &m; - eq_pp(str_eq const &e, ast_manager &m) : eq(e), m(m) {} + eq_pp(str_eq const &e) : eq(e) {} }; inline std::ostream &operator<<(std::ostream &out, eq_pp const &p) { - return out << snode_label_html(p.eq.m_lhs, p.m, false) + return out << snode_label_html(p.eq.m_lhs, p.eq.m, false) << " == " - << snode_label_html(p.eq.m_rhs, p.m, false); + << snode_label_html(p.eq.m_rhs, p.eq.m, false); } // string disequality constraint: lhs != rhs struct str_deq { + ast_manager& m; euf::snode const* m_lhs; // assumed to be non-null euf::snode const* m_rhs; // assumed to be non-null dep_tracker m_dep; - str_deq(euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep): - m_lhs(lhs), m_rhs(rhs), m_dep(dep) { + str_deq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep): + m(m), m_lhs(lhs), m_rhs(rhs), m_dep(dep) { SASSERT(well_formed()); + sort(); } - bool operator==(str_deq const& other) const { - return m_lhs == other.m_lhs && m_rhs == other.m_rhs; + str_deq& operator=(const str_deq & other) { + m_lhs = other.m_lhs; + m_rhs = other.m_rhs; + m_dep = other.m_dep; + return *this; + } + + bool operator==(const str_deq& other) const { + return m_lhs->similar(other.m_lhs, m) && m_rhs->similar(other.m_rhs, m); + } + + bool operator<(const str_deq& other) const { + if (m_lhs != other.m_lhs) + return m_lhs < other.m_lhs; + return m_rhs < other.m_rhs; + } + + unsigned hash() const { + return 891170543 * m_lhs->assoc_hash() + m_rhs->assoc_hash(); } void sort() { @@ -267,14 +288,13 @@ namespace seq { struct deq_pp { str_deq const &deq; - ast_manager &m; - deq_pp(str_deq const &e, ast_manager &m) : deq(e), m(m) {} + deq_pp(str_deq const &e) : deq(e) {} }; inline std::ostream &operator<<(std::ostream &out, deq_pp const &p) { - return out << snode_label_html(p.deq.m_lhs, p.m, false) + return out << snode_label_html(p.deq.m_lhs, p.deq.m, false) << " != " - << snode_label_html(p.deq.m_rhs, p.m, false); + << snode_label_html(p.deq.m_rhs, p.deq.m, false); } // kind of a regex membership constraint (paper Section 3.3, "views"): @@ -290,6 +310,7 @@ namespace seq { // regex membership constraint: str in regex // mirrors ZIPT's StrMem struct str_mem { + ast_manager& m; euf::snode const* m_str; // assumed to be non-null euf::snode const* m_regex; // assumed to be non-null (plain regex = current run state) dep_tracker m_dep; @@ -300,20 +321,31 @@ namespace seq { unsigned m_nu = 0; // ν: snapshot index identifying Q bool m_discharged = false; // guard monitor: false=watch, true=discharged - str_mem(euf::snode const* str, euf::snode const* regex, dep_tracker const& dep): - m_str(str), m_regex(regex), m_dep(dep) {} + str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, dep_tracker const& dep): + m(m), m_str(str), m_regex(regex), m_dep(dep) {} + + str_mem& operator=(const str_mem& other) { + m_str = other.m_str; + m_regex = other.m_regex; + m_dep = other.m_dep; + m_kind = other.m_kind; + m_root = other.m_root; + m_nu = other.m_nu; + m_discharged = other.m_discharged; + return *this; + } // factory for a stabilizer view str ∈_{Q_ν,{root}} root (m_regex=state) - static str_mem mk_view(euf::snode const* str, euf::snode const* state, + static str_mem mk_view(ast_manager& m, euf::snode const* str, euf::snode const* state, euf::snode const* root, unsigned nu, dep_tracker const& dep) { - str_mem r(str, state, dep); + str_mem r(m, str, state, dep); r.m_kind = mem_kind::stab_view; r.m_root = root; r.m_nu = nu; return r; } // factory for a cycle guard noloop(str, root, Q_ν) (m_regex=state) - static str_mem mk_guard(euf::snode const* str, euf::snode const* state, + static str_mem mk_guard(ast_manager& m, euf::snode const* str, euf::snode const* state, euf::snode const* root, unsigned nu, dep_tracker const& dep) { - str_mem r(str, state, dep); + str_mem r(m, str, state, dep); r.m_kind = mem_kind::no_loop; r.m_root = root; r.m_nu = nu; return r; } @@ -322,12 +354,22 @@ namespace seq { bool is_view() const { return m_kind == mem_kind::stab_view; } bool is_guard() const { return m_kind == mem_kind::no_loop; } - bool operator==(str_mem const& other) const { - return m_str == other.m_str && m_regex == other.m_regex + bool operator==(const str_mem& other) const { + return m_str->similar(other.m_str, m) && m_regex == other.m_regex && m_kind == other.m_kind && m_root == other.m_root && m_nu == other.m_nu && m_discharged == other.m_discharged; } + bool operator<(const str_mem& other) const { + if (m_str != other.m_str) + return m_str < other.m_str; + return m_regex < other.m_regex; + } + + unsigned hash() const { + return 381416603 * m_str->assoc_hash() + m_regex->assoc_hash(); + } + // check if the constraint has the form x in R with x a single variable bool is_primitive() const; @@ -347,14 +389,13 @@ namespace seq { struct mem_pp { str_mem const& mem; - ast_manager &m; - mem_pp(str_mem const& mem, ast_manager& m) : mem(mem), m(m) {} + mem_pp(str_mem const& mem) : mem(mem) {} }; inline std::ostream &operator<<(std::ostream &out, mem_pp const &p) { return out - << snode_label_html(p.mem.m_str, p.m, false) + << snode_label_html(p.mem.m_str, p.mem.m, false) << " in " - << snode_label_html(p.mem.m_regex, p.m, false); + << snode_label_html(p.mem.m_regex, p.mem.m, false); } // string variable substitution: var -> replacement @@ -399,6 +440,7 @@ namespace seq { dep_tracker dep; // tracks which input constraints contributed static expr_ref simplify(expr* f, ast_manager& m) { + //arith_rewriter th(m); //th_rewriter th(m); expr_ref fml(f, m); //th(fml); @@ -514,6 +556,30 @@ namespace seq { backtrack_reason m_reason = backtrack_reason::unevaluated; bool m_is_progress = false; bool m_node_len_constraints_generated = false; // true after generate_node_length_constraints runs + + unsigned m_hash = 0; // 0 ... unset + + nielsen_node* m_parent = this; + + // DFS bookkeeping for the subsumption (loop-cut) rule. + // m_dfs_path_pos: structural depth (= cur_path.size()) of this node while + // it is on the active DFS path; read by a descendant that + // loops back to it as a sibling. + // m_subtree_lowlink: minimum structural depth that this node's UNSAT closure + // escapes to via sibling cuts below it (Tarjan-style + // lowlink). UINT_MAX means "no cut escapes" — the unsat + // is self-contained. Only meaningful when the node's last + // result was unsat. + unsigned m_dfs_path_pos = 0; + unsigned m_subtree_lowlink = UINT_MAX; + // m_subtree_has_cut: a sibling loop-cut occurred somewhere in this node's + // closed subtree. A cut defers to an ancestor whose ARITHMETIC side + // constraints differ, so it is only a valid UNSAT witness inside a closure + // that uses string-only reasons throughout. When a cut coexists with a + // non-string-only (arithmetic / external) conflict the subtree result is + // NOT a sound UNSAT — search_dfs reports unknown instead. + bool m_subtree_has_cut = false; + // true once this node has been proven UNSAT for reasons that depend only // on its string/regex constraints (not on arithmetic / Parikh / external // context). Such an unsat is a property of the node's string signature @@ -543,10 +609,10 @@ namespace seq { vector const& str_mems() const { return m_str_mem; } vector& str_mems() { return m_str_mem; } - void add_str_eq(str_eq& eq); - void add_str_deq(str_deq& deq); - void add_str_mem(str_mem const& mem); - void add_constraint(constraint const &ic); + void add_str_eq(const str_eq& eq); + void add_str_deq(const str_deq& deq); + void add_str_mem(const str_mem& mem); + void add_constraint(const constraint &ic); vector const& constraints() const { return m_constraints; } vector& constraints() { return m_constraints; } @@ -578,6 +644,11 @@ namespace seq { nielsen_edge* parent_edge() const { return m_parent_edge; } void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; } + // returns 0 if hash is unknown + unsigned hash() const { + return m_hash; + } + // status bool is_general_conflict() const { return m_is_general_conflict; } void set_general_conflict() { @@ -592,6 +663,9 @@ namespace seq { bool is_currently_conflict() const { return is_general_conflict() || m_conflict_external_literal != sat::null_literal || + // a sibling (loop-cut / subsumption) conflict counts even when the + // node was never extended (a cut leaf has no children). + reason() == backtrack_reason::sibling || (reason() != backtrack_reason::unevaluated && m_is_extended); } @@ -617,7 +691,7 @@ namespace seq { if (m_conflict_internal != nullptr && m_conflict_external_literal == sat::null_literal) return; // We prefer internal conflicts (we need it as a justification for general conflicts) - TRACE(seq, tout << "internal conflict " << r << "\n"); + TRACE(seq, tout << "internal conflict " << (unsigned)r << "\n"); m_reason = r; m_conflict_internal = confl; m_conflict_external_literal = sat::null_literal; @@ -640,6 +714,22 @@ namespace seq { // apply a substitution to all constraints void apply_subst(euf::sgraph& sg, nielsen_subst const& s); + // Transposition table helpers (node memoization of string-only UNSAT). + // after computing the signature we should not change the node anymore + // the hash disregards length constraints on purpose for subsumption checks + unsigned canonize_and_compute_node_hash(); + + unsigned canonize_and_compute_final_node_hash() { + if (m_hash) + return m_hash; + m_hash = canonize_and_compute_node_hash(); + return m_hash; + } + + // check if two nodes are equivalent modulo side-constraints + // (actually subset checks would be better but we currently do not track this) + bool is_node_sibling(nielsen_node const* n); + // simplify all constraints at this node and initialize status. // Uses cur_path for LP solver queries during deterministic power cancellation. // Returns proceed, conflict, satisfied, or restart. @@ -679,6 +769,22 @@ namespace seq { // Length bounds are queried from the arithmetic subsolver when needed. }; + struct nielsen_node_hash { + // outputs the hash without side-constraints + unsigned operator()(nielsen_node* n) const { + const unsigned h = n->hash(); + if (h == 0) + return n->canonize_and_compute_node_hash(); + return h; + } + }; + + struct nielsen_node_eq { + unsigned operator()(nielsen_node* n1, nielsen_node* n2) const { + return n1->is_node_sibling(n2); + } + }; + // search statistics collected during Nielsen graph solving struct nielsen_stats { unsigned m_num_solve_calls = 0; @@ -712,6 +818,9 @@ namespace seq { unsigned m_mod_var_num_unwinding_eq = 0; unsigned m_mod_var_num_unwinding_mem = 0; unsigned m_ax_diseq = 0; + // subsumption rule + unsigned m_num_sibling_cut = 0; // loop-cut leaves (deferred to an ancestor) + unsigned m_num_sibling_closure = 0; // subtrees closed as string-only sibling conflicts void reset() { memset(this, 0, sizeof(nielsen_stats)); } }; @@ -750,7 +859,7 @@ namespace seq { struct partial_dfa_edge_key_hash { size_t operator()(partial_dfa_edge_key const& k) const { - size_t h = static_cast(k.m_src); + size_t h = k.m_src; h = (h * 1315423911u) ^ static_cast(k.m_label + 0x9e3779b9u); h = (h * 2654435761u) ^ static_cast(k.m_dst + 0x85ebca6bu); return h; @@ -762,6 +871,7 @@ namespace seq { seq_util& m_seq; euf::sgraph& m_sg; th_rewriter m_rw; + arith_rewriter m_a_rw; skolem m_sk; ptr_vector m_nodes; ptr_vector m_edges; @@ -835,12 +945,19 @@ namespace seq { // see ensure_automaton_explored). uint_set m_explored_automaton; + // Active-path index for the subsumption rule, keyed structurally (nodes + // with identical string constraints share a bucket). While a node is on + // the DFS path it is pushed onto its bucket and popped on leaving, so a + // non-empty bucket for the current node holds exactly the ancestor(s) it + // is a sibling of — i.e. a loop back up the Nielsen tree. + std::unordered_map, nielsen_node_hash, nielsen_node_eq> m_siblings; + // Transposition table: structural signatures of nodes already proven // UNSAT for string/regex-only reasons. A node whose signature is present // is unsatisfiable regardless of how it was reached, so the DFS can prune // it without re-exploring its subtree (turns the search tree into the // finite DAG the termination proof bounds). See compute_node_signature. - std::set> m_unsat_node_cache; + std::unordered_set m_unsat_node_cache; unsigned m_num_cache_hits = 0; // Incremental eager-closure chain state (see eager_begin / eager_close). @@ -1062,11 +1179,6 @@ namespace seq { search_result search_dfs(nielsen_node *node, ptr_vector& path, unsigned depth = 0); - // Transposition table helpers (node memoization of string-only UNSAT). - // Canonical structural signature of a node (string equalities, - // disequalities, memberships incl. view/guard metadata, char ranges). - // Two nodes with equal signatures have identical string constraints. - static std::vector compute_node_signature(nielsen_node const* n); // Union of all constraint deps of a node (sound over-approx conflict). dep_tracker node_all_deps(nielsen_node const* n) const; // True iff the node's UNSAT depends only on string/regex constraints. @@ -1356,3 +1468,21 @@ namespace seq { }; } + +template <> struct std::hash { + unsigned operator()(seq::str_eq& eq) const noexcept { + return eq.hash(); + } +}; + +template <> struct std::hash { + unsigned operator()(seq::str_deq& deq) const noexcept { + return deq.hash(); + } +}; + +template <> struct std::hash { + unsigned operator()(seq::str_mem& mem) const noexcept { + return mem.hash(); + } +}; \ No newline at end of file diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 4448774058..798703382a 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -597,9 +597,9 @@ namespace seq { case backtrack_reason::extended: return "Extended"; case backtrack_reason::symbol_clash: return "Symbol Clash"; case backtrack_reason::parikh_image: return "Parikh Image"; - case backtrack_reason::subsumption: return "Subsumption"; case backtrack_reason::arithmetic: return "Arithmetic"; case backtrack_reason::regex: return "Regex"; + case backtrack_reason::sibling: return "Sibling"; case backtrack_reason::regex_widening: return "RegexWidening"; case backtrack_reason::character_range: return "Character Range"; case backtrack_reason::smt: return "SMT"; diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 1572d70fa0..61d5e88a35 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -625,7 +625,7 @@ namespace seq { SASSERT(first); if (first != var) continue; - TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem, m) << "\n"); + TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem) << "\n"); if (!result) { result = mem.m_regex; @@ -644,14 +644,6 @@ namespace seq { return result; } - // ----------------------------------------------------------------------- - // Cycle detection - // ----------------------------------------------------------------------- - - bool seq_regex::detect_cycle(seq::str_mem const& mem) const { - return extract_cycle(mem) != nullptr; - } - // ----------------------------------------------------------------------- // Ground prefix consumption // ----------------------------------------------------------------------- @@ -784,55 +776,6 @@ namespace seq { return true; } - // ----------------------------------------------------------------------- - // History recording - // ----------------------------------------------------------------------- - - seq::str_mem seq_regex::record_history(seq::str_mem const& mem, euf::snode const* history_re) { - - return str_mem(mem.m_str, mem.m_regex, mem.m_dep); - } - - // ----------------------------------------------------------------------- - // Cycle detection - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::extract_cycle(seq::str_mem const& mem) const { -#if 0 - // Walk the history chain looking for a repeated regex. - // A cycle exists when the current regex matches a regex in the history. - if (!mem.m_regex || !mem.m_history) - return nullptr; - - euf::snode const* current = mem.m_regex; - euf::snode const* hist = mem.m_history; - - // Walk the history chain up to a bounded depth. - // The history is structured as a chain of regex snapshots connected - // via the sgraph's regex-concat: each level's arg(0) is a snapshot - // and arg(1) is the tail. A leaf (non-concat) is a terminal entry. - unsigned bound = 1000; - while (hist && bound-- > 0) { - euf::snode const* entry = hist; - euf::snode const* tail = nullptr; - - // If the history node is a regex concat, decompose it: - // arg(0) is the regex snapshot, arg(1) is the rest of the chain - if (hist->is_concat() && seq.re.is_concat(hist->get_expr())) { - entry = hist->arg(0); - tail = hist->arg(1); - } - - // Check pointer equality (fast, covers normalized regexes) - if (entry == current) - return entry; - - hist = tail; - } -#endif - return nullptr; - } - // ----------------------------------------------------------------------- // Stabilizer from cycle // ----------------------------------------------------------------------- diff --git a/src/smt/seq/seq_regex.h b/src/smt/seq/seq_regex.h index 7728481e30..45b911d8b7 100644 --- a/src/smt/seq/seq_regex.h +++ b/src/smt/seq/seq_regex.h @@ -251,7 +251,7 @@ namespace seq { if (deriv) propagate_self_stabilizing(parent_re, deriv); euf::snode const* new_str = m_sg.drop_first(mem.m_str); - return str_mem(new_str, deriv, mem.m_dep); + return str_mem(mem.m, new_str, deriv, mem.m_dep); } // ----------------------------------------------------------------- @@ -321,21 +321,6 @@ namespace seq { // Cycle detection and stabilizers // ----------------------------------------------------------------- - // record current regex in the derivation history of a str_mem. - // the history tracks a chain of (regex, id) pairs for cycle detection. - // returns the updated str_mem. - str_mem record_history(str_mem const& mem, euf::snode const* history_re); - - // check if the derivation history of mem contains a cycle, i.e., - // the same regex id appears twice in the history chain. - // if found, returns the cycle entry point regex; nullptr otherwise. - euf::snode const* extract_cycle(str_mem const& mem) const; - - // check if the derivation history exhibits a cycle. - // returns true when the current regex matches a previously seen regex - // in the history chain. used to trigger stabilizer introduction. - bool detect_cycle(str_mem const& mem) const; - // compute a Kleene star stabilizer from a cycle. // given the regex at the cycle point and the current regex, // builds r* that over-approximates any number of cycle iterations. diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h index 21962e6086..649ce645f7 100644 --- a/src/smt/seq/seq_state.h +++ b/src/smt/seq/seq_state.h @@ -29,20 +29,20 @@ namespace smt { struct tracked_str_eq : seq::str_eq { enode *m_l, *m_r; - tracked_str_eq(euf::snode const* lhs, euf::snode const* rhs, enode* l, enode* r, seq::dep_tracker const &dep) - : str_eq(lhs, rhs, dep), m_l(l), m_r(r) {} + tracked_str_eq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, enode* l, enode* r, seq::dep_tracker const &dep) + : str_eq(m, lhs, rhs, dep), m_l(l), m_r(r) {} }; struct tracked_str_deq : seq::str_deq { sat::literal lit; - tracked_str_deq(euf::snode const* lhs, euf::snode const* rhs, const sat::literal lit, seq::dep_tracker const &dep) - : str_deq(lhs, rhs, dep), lit(lit) {} + tracked_str_deq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, const sat::literal lit, seq::dep_tracker const &dep) + : str_deq(m, lhs, rhs, dep), lit(lit) {} }; struct tracked_str_mem : seq::str_mem { sat::literal lit; - tracked_str_mem(euf::snode const* str, euf::snode const* regex, const sat::literal lit, seq::dep_tracker const &dep) - : str_mem(str, regex, dep), lit(lit) {} + tracked_str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, const sat::literal lit, seq::dep_tracker const &dep) + : str_mem(m, str, regex, dep), lit(lit) {} }; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 117e7cf48d..2a8af4f2da 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -222,9 +222,8 @@ namespace smt { return; euf::snode const* s1 = get_snode(e1); euf::snode const* s2 = get_snode(e2); - seq::dep_tracker dep = nullptr; ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); + m_prop_queue.push_back(eq_item(m, s1, s2, get_enode(v1), get_enode(v2), nullptr)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; ++m_eager_dirty; @@ -269,10 +268,9 @@ namespace smt { else { euf::snode const* s1 = get_snode(e1); euf::snode const* s2 = get_snode(e2); - const seq::dep_tracker dep = nullptr; ctx.push_trail(restore_vector(m_prop_queue)); const expr_ref eq_expr(m.mk_eq(e1, e2), m); - m_prop_queue.push_back(deq_item(s1, s2, ~ctx.get_literal(eq_expr), dep)); + m_prop_queue.push_back(deq_item(m, s1, s2, ~ctx.get_literal(eq_expr), nullptr)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; ++m_eager_dirty; @@ -296,10 +294,9 @@ namespace smt { if (m_seq.str.is_in_re(e, s, re)) { euf::snode const* sn_str = get_snode(s); euf::snode const* sn_re = get_snode(re); - const seq::dep_tracker dep = nullptr; if (is_true) { ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep)); + m_prop_queue.push_back(mem_item(m, sn_str, sn_re, lit, nullptr)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; ++m_eager_dirty; @@ -311,7 +308,7 @@ namespace smt { const expr_ref re_compl(m_seq.re.mk_complement(re), m); euf::snode const* sn_re_compl = get_snode(re_compl.get()); ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep)); + m_prop_queue.push_back(mem_item(m, sn_str, sn_re_compl, lit, nullptr)); m_last_constraint_added = ctx.get_scope_level(); m_can_hot_restart = false; ++m_eager_dirty; @@ -973,6 +970,16 @@ namespace smt { SASSERT(!node->is_general_conflict()); node->clear_reason(); } + else if (node->reason() == seq::backtrack_reason::sibling) { + // A non-general sibling conflict (a loop cut, or a closure + // that escaped to an ancestor) is valid only for the path it + // was found on; the changed external context may now admit a + // model. Clear it (and its recorded deps) for re-exploration. + // Self-contained sibling closures are general and were skipped + // above. + SASSERT(!node->is_general_conflict()); + node->clear_local_conflict(); + } if (node->is_external_conflict()) node->clear_local_conflict(); @@ -1291,11 +1298,11 @@ namespace smt { std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl; unsigned idx = 0; for (auto& eq : m_nielsen.root()->str_eqs()) { - std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq, m) << "\n"; + std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq) << "\n"; } idx = 0; for (auto& mem : m_nielsen.root()->str_mems()) { - std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem, m) << "\n"; + std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem) << "\n"; } std::flush(std::cout); #endif @@ -2033,7 +2040,7 @@ namespace smt { literal_vector dep_lits; for (unsigned idx : mem_indices) { - std::cout << seq::mem_pp(mems[idx], m) << std::endl; + std::cout << seq::mem_pp(mems[idx]) << std::endl; seq::deps_to_lits(m_nielsen.dep_mgr(), mems[idx].m_dep, eqs, dep_lits); } diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index 6b82bd0d98..2a03328e5a 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -2194,72 +2194,6 @@ static void test_explain_conflict_mixed_eq_mem() { ng.test_aux_explain_conflict(eqs, mem_literals); } -// test subsumption pruning during solve: a node whose constraint set -// is a superset of a known-unsat node is pruned -static void test_subsumption_pruning_unsat() { - std::cout << "test_subsumption_pruning_unsat\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - - dummy_simple_solver solver; - seq::context_solver_i context_solver; - seq::nielsen_graph ng(sg, solver, context_solver); - euf::snode const* a = sg.mk_char('A'); - euf::snode const* b = sg.mk_char('B'); - - // A = B is an immediate conflict (symbol clash). - // Any branch that inherits this equation should be pruned. - ng.add_str_eq(a, b); - const auto result = ng.solve(); - SASSERT(result == seq::nielsen_graph::search_result::unsat); - - // root should have conflict set - SASSERT(ng.root()->is_general_conflict()); -} - -// test that subsumption sets backtrack_reason::subsumption -static void test_subsumption_reason_set() { - std::cout << "test_subsumption_reason_set\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - - dummy_simple_solver solver; - seq::context_solver_i context_solver; - seq::nielsen_graph ng(sg, solver, context_solver); - euf::snode const* x = sg.mk_var(symbol("x"), sg.get_str_sort()); - euf::snode const* y = sg.mk_var(symbol("y"), sg.get_str_sort()); - euf::snode const* a = sg.mk_char('A'); - euf::snode const* b = sg.mk_char('B'); - - // x·A = y·B: after Nielsen splitting, children will have A=B - // which is unsat. The subsumption pruning may fire on sibling - // branches that inherit the same conflict. - euf::snode const* xa = sg.mk_concat(x, a); - euf::snode const* yb = sg.mk_concat(y, b); - ng.add_str_eq(xa, yb); - - const auto result = ng.solve(); - SASSERT(result == seq::nielsen_graph::search_result::unsat); - - // check that at least one node has subsumption reason - bool found_subsumption = false; - for (const seq::nielsen_node* nd : ng.nodes()) { - if (nd->reason() == seq::backtrack_reason::subsumption) { - found_subsumption = true; - SASSERT(nd->is_general_conflict()); - break; - } - } - // subsumption may or may not fire depending on search order; - // the important thing is the solve result is correct. - // If it does fire, the reason must be subsumption. - (void)found_subsumption; -} - // test generate_length_constraints: basic equation x . y = A . B static void test_length_constraints_basic() { std::cout << "test_length_constraints_basic\n"; @@ -3971,8 +3905,6 @@ void tst_seq_nielsen() { test_var_nielsen_substitution_types(); test_explain_conflict_mem_only(); test_explain_conflict_mixed_eq_mem(); - test_subsumption_pruning_unsat(); - test_subsumption_reason_set(); test_length_constraints_basic(); test_length_constraints_trivial_skip(); test_length_constraints_empty();