mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

add pp methods

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-13 11:41:49 -07:00
parent 9155ce85bb
commit 035ea95faa
2 changed files with 45 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/seq/seq_nielsen.cpp
View file

@ -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<std::pair<ptr_vector<euf::snode>, 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;

39
src/smt/seq/seq_nielsen.h
View file

@ -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 << "<tbd reason>";
}
}
// 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;