mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 14:47:51 +00:00
Code Activity

Make dot output a bit more readable

Browse source
This commit is contained in:
CEisenhofer 2026-05-11 19:17:00 +02:00
parent fb6b05aa83
commit d20a27e1df
1 changed files with 33 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/smt/seq/seq_nielsen_pp.cpp
View file

@ -226,7 +226,7 @@ namespace seq {
return "null"; return "null";
} }
static std::string regex_expr_html(expr* e, ast_manager& m, seq_util& seq) { static std::string regex_expr_html(expr* e, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m, seq_util& seq) {
if (!e) if (!e)
return "null"; return "null";
expr* a = nullptr, * b = nullptr; expr* a = nullptr, * b = nullptr;
@ -273,20 +273,27 @@ namespace seq {
if (i > 0) res += " "; if (i > 0) res += " ";
bool needs_parens = seq.re.is_union(ap->get_arg(i)); bool needs_parens = seq.re.is_union(ap->get_arg(i));
if (needs_parens) res += "("; if (needs_parens) res += "(";
res += regex_expr_html(ap->get_arg(i), m, seq); res += regex_expr_html(ap->get_arg(i), names, next_id, m, seq);
if (needs_parens) res += ")"; if (needs_parens) res += ")";
} }
return res; return res;
} }
if (m.is_ite(e)) {
app* ap = to_app(e);
std::string cond = arith_expr_html(ap->get_arg(0), names, next_id, m);
std::string t = regex_expr_html(ap->get_arg(1), names, next_id, m, seq);
std::string f = regex_expr_html(ap->get_arg(2), names, next_id, m, seq);
return cond + " ? (" + t + ") : (" + f + ")";
}
if (seq.re.is_union(e)) { if (seq.re.is_union(e)) {
app* ap = to_app(e); app* ap = to_app(e);
std::string res; std::string res;
if (ap->get_num_args() == 0) if (ap->get_num_args() == 0)
return "&#8709;"; return "&#8709;";
res = regex_expr_html(ap->get_arg(0), m, seq); res = regex_expr_html(ap->get_arg(0), names, next_id, m, seq);
for (unsigned i = 1; i < ap->get_num_args(); ++i) { for (unsigned i = 1; i < ap->get_num_args(); ++i) {
res += " | "; res += " | ";
res += regex_expr_html(ap->get_arg(i), m, seq); res += regex_expr_html(ap->get_arg(i), names, next_id, m, seq);
} }
return res; return res;
} }
@ -297,7 +304,7 @@ namespace seq {
if (i > 0) res += " &amp; "; if (i > 0) res += " &amp; ";
bool needs_parens = seq.re.is_union(ap->get_arg(i)) || seq.re.is_concat(ap->get_arg(i)); bool needs_parens = seq.re.is_union(ap->get_arg(i)) || seq.re.is_concat(ap->get_arg(i));
if (needs_parens) res += "("; if (needs_parens) res += "(";
res += regex_expr_html(ap->get_arg(i), m, seq); res += regex_expr_html(ap->get_arg(i), names, next_id, m, seq);
if (needs_parens) res += ")"; if (needs_parens) res += ")";
} }
return res; return res;
@ -305,21 +312,21 @@ namespace seq {
if (seq.re.is_star(e, a)) { if (seq.re.is_star(e, a)) {
bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a); bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a);
std::string res = needs_parens ? "(" : ""; std::string res = needs_parens ? "(" : "";
res += regex_expr_html(a, m, seq); res += regex_expr_html(a, names, next_id, m, seq);
res += needs_parens ? ")<SUP>*</SUP>" : "<SUP>*</SUP>"; res += needs_parens ? ")<SUP>*</SUP>" : "<SUP>*</SUP>";
return res; return res;
} }
if (seq.re.is_plus(e, a)) { if (seq.re.is_plus(e, a)) {
bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a); bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a);
std::string res = needs_parens ? "(" : ""; std::string res = needs_parens ? "(" : "";
res += regex_expr_html(a, m, seq); res += regex_expr_html(a, names, next_id, m, seq);
res += needs_parens ? ")<SUP>+</SUP>" : "<SUP>+</SUP>"; res += needs_parens ? ")<SUP>+</SUP>" : "<SUP>+</SUP>";
return res; return res;
} }
if (seq.re.is_opt(e, a)) { if (seq.re.is_opt(e, a)) {
bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a); bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a);
std::string res = needs_parens ? "(" : ""; std::string res = needs_parens ? "(" : "";
res += regex_expr_html(a, m, seq); res += regex_expr_html(a, names, next_id, m, seq);
res += needs_parens ? ")?" : "?"; res += needs_parens ? ")?" : "?";
return res; return res;
} }
@ -327,13 +334,11 @@ namespace seq {
bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a); bool needs_parens = seq.re.is_union(a) || seq.re.is_concat(a) || seq.re.is_intersection(a);
std::string res = "~"; std::string res = "~";
res += needs_parens ? "(" : ""; res += needs_parens ? "(" : "";
res += regex_expr_html(a, m, seq); res += regex_expr_html(a, names, next_id, m, seq);
res += needs_parens ? ")" : ""; res += needs_parens ? ")" : "";
return res; return res;
} }
if (seq.re.is_range(e, a, b)) { if (seq.re.is_range(e, a, b)) {
uint64_t next_id = 0;
obj_map<expr, std::string> names;
zstring s1, s2; zstring s1, s2;
std::string c1 = seq.str.is_string(a, s1) ? dot_html_escape(s1.encode()) : arith_expr_html(a, names, next_id, m); std::string c1 = seq.str.is_string(a, s1) ? dot_html_escape(s1.encode()) : arith_expr_html(a, names, next_id, m);
std::string c2 = seq.str.is_string(b, s2) ? dot_html_escape(s2.encode()) : arith_expr_html(b, names, next_id, m); std::string c2 = seq.str.is_string(b, s2) ? dot_html_escape(s2.encode()) : arith_expr_html(b, names, next_id, m);
@ -447,7 +452,7 @@ namespace seq {
result += "</SUP>"; result += "</SUP>";
} }
else if (e && seq.is_re(e)) else if (e && seq.is_re(e))
result += regex_expr_html(e, m, seq); result += regex_expr_html(e, names, next_id, m, seq);
else { else {
std::ostringstream os; std::ostringstream os;
os << mk_pp(e, m); os << mk_pp(e, m);
@ -475,8 +480,6 @@ namespace seq {
bool hasEq = false; bool hasEq = false;
bool hasMem = false; bool hasMem = false;
bool hasRange = false; bool hasRange = false;
bool hasDiseq = false;
bool hasInt = false;
// string equalities // string equalities
for (auto const& eq : m_str_eq) { for (auto const& eq : m_str_eq) {
@ -505,10 +508,24 @@ namespace seq {
out << "<br/>"; out << "<br/>";
} }
// integer constraints // integer constraints
std::vector<std::string> int_constraints(m_constraints.size());
for (auto const& ic : m_constraints) { for (auto const& ic : m_constraints) {
int_constraints.push_back(constraint_html(ic, names, next_id, m));
}
if (!int_constraints.empty()) {
// eliminate duplicates
std::ranges::sort(int_constraints);
unsigned prev = 0;
for (unsigned i = 1; i < int_constraints.size(); i++) {
if (int_constraints[i] != int_constraints[prev])
int_constraints[++prev] = int_constraints[i];
}
int_constraints.resize(prev);
out << "Int:<br/>";
if (!any) { out << "Cnstr:<br/>"; any = true; } if (!any) { out << "Cnstr:<br/>"; any = true; }
if (!hasInt) { out << "Int:<br/>"; hasInt = true; } for (const auto& s : int_constraints) {
out << constraint_html(ic, names, next_id, m) << "<br/>"; out << s << "<br/>";
}
} }
if (!any) if (!any)