From 035ea95faac740b0afe4da76d6c84d0554f8babb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Apr 2026 11:41:49 -0700 Subject: [PATCH] add pp methods Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 8 ++++++-- src/smt/seq/seq_nielsen.h | 39 +++++++++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+), 2 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ed073bf0c..a507e3acc 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1085,6 +1085,9 @@ namespace seq { euf::snode* deriv = fwd ? sg.brzozowski_deriv(mem.m_regex, tok) : reverse_brzozowski_deriv(sg, mem.m_regex, tok); + TRACE(seq, tout << mk_pp(mem.m_str->get_expr(), m) + << " in " << mk_pp(mem.m_regex->get_expr(), m) + << " d: " << mk_pp(deriv->get_expr(), m) << "\n"); if (!deriv) break; if (deriv->is_fail()) { @@ -1128,6 +1131,7 @@ namespace seq { auto next = sg.mk(d); if (next->is_fail()) { + TRACE(seq, tout << "empty regex" << mk_pp(mem.m_regex->get_expr(), m) << " d: " << d << "\n"); set_general_conflict(); set_conflict(backtrack_reason::regex, mem.m_dep); return simplify_result::conflict; @@ -1142,6 +1146,7 @@ namespace seq { // check for regex memberships that are immediately infeasible for (str_mem& mem : m_str_mem) { if (mem.is_contradiction()) { + TRACE(seq, tout << "contradiction " << mem_pp(m, mem) << "\n"); set_general_conflict(); set_conflict(backtrack_reason::regex, mem.m_dep); return simplify_result::conflict; @@ -4253,8 +4258,6 @@ namespace seq { u_map, dep_tracker>> var_regexes; for (auto const& mem : node.str_mems()) { - if (!mem.m_str || !mem.m_regex) - continue; if (!mem.is_primitive()) continue; euf::snode* const first = mem.m_str->first(); @@ -4270,6 +4273,7 @@ namespace seq { continue; lbool result = m_seq_regex->check_intersection_emptiness(regexes.first, 5000); if (result == l_true) { + TRACE(seq, tout << "empty intersection\n"); // Intersection is empty — infeasible dep = regexes.second; return false; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index e14ab1960..37c9ce88c 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -316,6 +316,24 @@ 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. @@ -364,6 +382,16 @@ namespace seq { bool contains_var(euf::snode* var) const; }; + struct eq_pp { + str_eq const &eq; + ast_manager &m; + eq_pp(str_eq const &e, ast_manager &m) : eq(e), m(m) {} + }; + + inline std::ostream &operator<<(std::ostream &out, eq_pp const &p) { + return out << mk_pp(p.eq.m_lhs->get_expr(), p.m) << " == " << mk_pp(p.eq.m_rhs->get_expr(), p.m) << "\n"; + } + // regex membership constraint: str in regex // mirrors ZIPT's StrMem struct str_mem { @@ -392,6 +420,15 @@ namespace seq { bool contains_var(euf::snode* var) const; }; + struct mem_pp { + ast_manager &m; + str_mem const& mem; + mem_pp(ast_manager &m, str_mem const&mem) : m(m), mem(mem) {} + }; + inline std::ostream &operator<<(std::ostream &out, mem_pp const &p) { + return out << mk_pp(p.mem.m_str->get_expr(), p.m) << " in " << mk_pp(p.mem.m_regex->get_expr(), p.m) << "\n"; + } + // string variable substitution: var -> replacement // (can be used as well to substitute arbitrary nodes - like powers) // mirrors ZIPT's Subst @@ -629,6 +666,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"); m_reason = r; m_conflict_internal = confl; m_conflict_external_literal = sat::null_literal; @@ -637,6 +675,7 @@ namespace seq { void set_external_conflict(sat::literal lit, dep_tracker confl) { if (m_reason != backtrack_reason::unevaluated) return; + TRACE(seq, tout << "external conflict " << lit << "\n"); m_reason = backtrack_reason::external; m_conflict_external_literal = ~lit; m_conflict_internal = confl;