mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

A bit more "dot" improvements

Browse source
This commit is contained in:
CEisenhofer 2026-05-11 19:22:45 +02:00
parent d20a27e1df
commit 55ea1929e9
1 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -147,6 +147,18 @@ namespace seq {
}
app* a = to_app(e);
expr* x, * y;
if (m.is_or(e)) {
app* ap = to_app(e);
std::string res;
res = arith_expr_html(ap->get_arg(0), names, next_id, m);
for (unsigned i = 1; i < ap->get_num_args(); ++i) {
res += " || ";
res += arith_expr_html(ap->get_arg(i), names, next_id, m);
}
return res;
}
if (m.is_not(e, x))
return "!(" + arith_expr_html(x, names, next_id, m) + ")";
if (arith.is_le(e, x, y)) {
return arith_expr_html(x, names, next_id, m) + " &lt; " + arith_expr_html(y, names, next_id, m);
}
@ -521,8 +533,8 @@ namespace seq {
int_constraints[++prev] = int_constraints[i];
}
int_constraints.resize(prev);
out << "Int:<br/>";
if (!any) { out << "Cnstr:<br/>"; any = true; }
out << "Int:<br/>";
for (const auto& s : int_constraints) {
out << s << "<br/>";
}