From 53cc320efab1ae214542612457a8b6a2436e46fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Apr 2026 00:29:58 -0700 Subject: [PATCH] deps Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 15 +++++++-------- src/smt/seq/seq_nielsen.h | 4 ++-- src/smt/seq/seq_nielsen_pp.cpp | 2 +- src/smt/seq/seq_regex.cpp | 23 +++++++++++------------ 4 files changed, 21 insertions(+), 23 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 8a003109d..95b65086e 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -43,7 +43,7 @@ NSB review: namespace seq { - void deps_to_lits(dep_tracker const &deps, svector &eqs, svector &lits) { + void deps_to_lits(dep_tracker deps, svector &eqs, svector &lits) { vector vs; dep_manager::s_linearize(deps, vs); for (dep_source const &d : vs) { @@ -4159,8 +4159,7 @@ namespace seq { // Concrete character → to_re(unit(c)) expr* te = tok->get_expr(); SASSERT(te); - expr_ref tre(m_seq.re.mk_to_re(te), m); - tok_re = m_sg.mk(tre); + tok_re = m_sg.mk(m_seq.re.mk_to_re(te)); } else if (tok->is_var()) { // Variable → intersection of primitive regex constraints, or Σ* @@ -4173,6 +4172,8 @@ namespace seq { expr_ref all_re(m_seq.re.mk_full_seq(m_seq.re.mk_re(str_sort)), m); tok_re = m_sg.mk(all_re); } + TRACE(seq, tout << "intersection-collection\n" << mk_pp(tok->get_expr(), m) + << "\n" << mk_pp(tok_re->get_expr(), m) << "\n"); } else if (tok->is_unit()) { // Symbolic char — try to get char_range @@ -4182,8 +4183,6 @@ namespace seq { // Build union of re.range for each interval euf::snode* range_re = nullptr; for (auto const& r : cs.first.ranges()) { - expr_ref lo(m_seq.mk_char(r.m_lo), m); - expr_ref hi(m_seq.mk_char(r.m_hi - 1), m); expr_ref rng(m_seq.re.mk_range( m_seq.str.mk_string(zstring(r.m_lo)), m_seq.str.mk_string(zstring(r.m_hi - 1))), m); @@ -4221,8 +4220,7 @@ namespace seq { expr* ae = approx->get_expr(); expr* te = tok_re->get_expr(); SASSERT(ae && te); - expr_ref cat(m_seq.re.mk_concat(ae, te), m); - approx = m_sg.mk(cat); + approx = m_sg.mk(m_seq.re.mk_concat(ae, te)); } } @@ -4240,7 +4238,8 @@ namespace seq { // TODO: Minimize the conflict here 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(m, mem) << "\n"); + << " <= " << mk_pp(ae, m) << "\n" << mem_pp(m, mem) << "\n"; + display(tout, &node) << "\n"); return result == l_true; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 7d0085caf..42fa8a075 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -352,7 +352,7 @@ namespace seq { using dep_tracker = dep_manager::dependency*; // partition dep_source leaves from deps into enode pairs and sat literals. - void deps_to_lits(dep_tracker const& deps, + void deps_to_lits(dep_tracker deps, svector& eqs, svector& lits); @@ -831,7 +831,7 @@ namespace seq { mutable dep_manager m_dep_mgr; - std::ostream &display(std::ostream &out, nielsen_node* n) const; + std::ostream &display(std::ostream &out, nielsen_node const* n) const; public: // Construct with a caller-supplied solver. Ownership is NOT transferred; diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index c04fd7588..231b14f65 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -25,7 +25,7 @@ Author: namespace seq { - std::ostream& nielsen_graph::display(std::ostream& out, nielsen_node* n) const { + std::ostream& nielsen_graph::display(std::ostream& out, nielsen_node const* n) const { out << " node[" << n->id() << "]"; if (n == m_root) out << " (root)"; diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 556c36cb9..4c03d3f3b 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -148,15 +148,12 @@ namespace seq { } void seq_regex::set_self_stabilizing(euf::snode* regex) { - if (!regex) - return; - m_self_stabilizing.insert(regex->id()); + if (regex) + m_self_stabilizing.insert(regex->id()); } bool seq_regex::is_self_stabilizing(euf::snode* regex) const { - if (!regex) - return false; - return m_self_stabilizing.contains(regex->id()); + return regex && m_self_stabilizing.contains(regex->id()); } // ----------------------------------------------------------------------- @@ -502,6 +499,8 @@ namespace seq { // BFS regex emptiness check // ----------------------------------------------------------------------- + // NSB review: we have similar functionality in seq_rewriter::some_seq_in_re + // currently both these versions only relly work for strings not general sequences lbool seq_regex::is_empty_bfs(euf::snode* re, unsigned max_states) { if (!re) return l_undef; @@ -603,8 +602,7 @@ namespace seq { expr* r1 = result->get_expr(); expr* r2 = regexes[i]->get_expr(); SASSERT(r1 && r2); - expr_ref inter(seq.re.mk_inter(r1, r2), mgr); - result = m_sg.mk(inter); + result = m_sg.mk(seq.re.mk_inter(r1, r2)); SASSERT(result); } @@ -662,18 +660,19 @@ namespace seq { SASSERT(var); seq_util& seq = m_sg.get_seq_util(); - ast_manager& mgr = m_sg.get_manager(); + ast_manager& m = m_sg.get_manager(); euf::snode* result = nullptr; for (auto const& mem : node.str_mems()) { - SASSERT(mem.m_str && mem.m_regex); // Primitive constraint: str is a single variable if (!mem.is_primitive()) continue; - euf::snode* first = mem.m_str->first(); + euf::snode *first = mem.m_str->first(); + // NSB review: why is this "first" and not mem.m_str? SASSERT(first); if (first != var) continue; + TRACE(seq, tout << mk_pp(first->get_expr(), m) << " " << mem_pp(m, mem) << " dep: " << mem.m_dep << "\n"); if (!result) { result = mem.m_regex; @@ -683,7 +682,7 @@ namespace seq { expr* r1 = result->get_expr(); expr* r2 = mem.m_regex->get_expr(); if (r1 && r2) { - expr_ref inter(seq.re.mk_inter(r1, r2), mgr); + expr_ref inter(seq.re.mk_inter(r1, r2), m); result = m_sg.mk(inter); dep = dep_mgr.mk_join(dep, mem.m_dep); }