Improved non-verbose ezSAT::printDIMACS() format

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index dccc00555aae8a89a4c966a4d12fe0ec8c9a96a3..577625259f3049fd27fc16c00db1a6c5f3ad82a9 100644 (file)
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -1131,10 +1131,15 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
        int maxClauseLen = 0;
        for (auto &clause : cnfClauses)
                maxClauseLen = std::max(int(clause.size()), maxClauseLen);
+       if (!verbose)
+               maxClauseLen = std::min(maxClauseLen, 3);
        for (auto &clause : cnfClauses) {
                for (auto idx : clause)
                        fprintf(f, " %*d", digits, idx);
-               fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+               if (maxClauseLen >= int(clause.size()))
+                       fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+               else
+                       fprintf(f, " %*d\n", digits, 0);
        }
 }