diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index fc6531144b..37fa9c5707 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -28,6 +28,8 @@ namespace euf { m(m), m_seq(m), m_rewriter(m), + m_th_rewriter(m), + m_sk(m, m_th_rewriter), m_egraph(eg), m_str_sort(m_seq.str.mk_string_sort(), m), m_pin(m) { @@ -305,7 +307,7 @@ namespace euf { } } - static const unsigned HASH_BASE = 31; + static constexpr unsigned HASH_BASE = 31; // Compute a 2x2 polynomial hash matrix for associativity-respecting hashing. // Unsigned overflow is intentional and well-defined (mod 2^32). @@ -333,7 +335,20 @@ namespace euf { else { // leaf/token: [[HASH_BASE, value], [0, 1]] // +1 avoids zero hash values; wraps safely on unsigned overflow - unsigned v = n->get_expr() ? n->get_expr()->get_id() + 1 : n->id() + 1; + // for slices it is the same as its parent + expr* e = n->get_expr(); + SASSERT(e); + unsigned v; + if (m_sk.is_slice(e)) { + do { + // get root variable + e = to_app(e)->get_arg(0); + } while (m_sk.is_slice(e)); + v = e->get_id(); + } + else + v = e->get_id() + 1; + n->m_hash_matrix[0][0] = HASH_BASE; n->m_hash_matrix[0][1] = v; n->m_hash_matrix[1][0] = 0; diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h index 1687883249..4e80bef6cd 100644 --- a/src/ast/euf/euf_sgraph.h +++ b/src/ast/euf/euf_sgraph.h @@ -83,6 +83,8 @@ namespace euf { ast_manager& m; seq_util m_seq; seq_rewriter m_rewriter; + th_rewriter m_th_rewriter; + seq::skolem m_sk; egraph& m_egraph; region m_region; snode_vector m_nodes; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 106f1a8f64..22c26f8a6b 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2124,13 +2124,14 @@ namespace seq { return reason_is_string_only(n->m_reason); } - std::vector nielsen_graph::compute_node_signature(nielsen_node const* n) const { + 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()) + 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); } @@ -2139,9 +2140,10 @@ namespace seq { // string disequalities { std::vector> v; - for (auto const& d : n->str_deqs()) + for (auto const& d : n->str_deqs()) { v.emplace_back(d.m_lhs->id(), d.m_rhs->id()); - std::sort(v.begin(), v.end()); + } + 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); } } @@ -2154,9 +2156,13 @@ namespace seq { static_cast(mm.m_kind), mm.m_root ? mm.m_root->id() : UINT_MAX, mm.m_nu, mm.m_discharged ? 1u : 0u }); - std::sort(v.begin(), v.end()); + std::ranges::sort(v); sig.push_back(static_cast(v.size())); - for (auto const& a : v) for (unsigned x : a) sig.push_back(x); + for (auto const& a : v) { + for (unsigned x : a) { + sig.push_back(x); + } + } } sig.push_back(UINT_MAX); // character-range constraints (per symbolic unit) @@ -2165,22 +2171,38 @@ namespace seq { 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); } + 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); } + 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) { + dep_tracker nielsen_graph::node_all_deps(nielsen_node const* n) const { dep_tracker d = nullptr; - for (auto const& e : n->str_eqs()) d = m_dep_mgr.mk_join(d, e.m_dep); - for (auto const& q : n->str_deqs()) d = m_dep_mgr.mk_join(d, q.m_dep); - for (auto const& mm : n->str_mems()) d = m_dep_mgr.mk_join(d, mm.m_dep); - for (auto const& [uid, cr] : n->char_ranges()) d = m_dep_mgr.mk_join(d, cr.second); + for (auto const& e : n->str_eqs()) { + d = m_dep_mgr.mk_join(d, e.m_dep); + } + for (auto const& q : n->str_deqs()) { + d = m_dep_mgr.mk_join(d, q.m_dep); + } + for (auto const& mm : n->str_mems()) { + d = m_dep_mgr.mk_join(d, mm.m_dep); + } + for (auto const& [uid, cr] : n->char_ranges()) { + d = m_dep_mgr.mk_join(d, cr.second); + } return d; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 95d3276da5..8b62a81cba 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1066,9 +1066,9 @@ namespace seq { // 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. - std::vector compute_node_signature(nielsen_node const* n) const; + 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); + dep_tracker node_all_deps(nielsen_node const* n) const; // True iff the node's UNSAT depends only on string/regex constraints. bool node_unsat_string_only(nielsen_node const* n) const;