From 8c67c238833c4dde873f444ec1317443a14a65ed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Apr 2023 16:14:33 -0700 Subject: [PATCH] update print to elide overly long sets of intervals --- src/math/polysat/viable.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 85c8510a7..9052014a2 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -2075,11 +2075,15 @@ namespace { out << e->side_cond << " "; else out << e->side_cond.size() << " side-conditions "; - if (e->src.size() <= 5) - for (const auto& src : e->src) - out << src << "; "; - else - out << e->src.size() << " sources"; + unsigned count = 0; + for (const auto& src : e->src) { + ++count; + out << src << "; "; + if (count > 10) { + out << " ..."; + break; + } + } return out; } @@ -2087,9 +2091,15 @@ namespace { if (!e) return out; entry const* first = e; + unsigned count = 0; do { display_one(out, v, e) << delimiter; e = e->next(); + ++count; + if (count > 10) { + out << " ..."; + break; + } } while (e != first); return out;