summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-18 09:25:41 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-18 09:25:41 +0100
commit61a2bf57b43eff81f177f1280574dff22885ad86 (patch)
tree20095be6daa1f068b5dda1b6d61afcc343046e3f
parent13051e6acf6c1fd506a49d258c3d99c1334c78cc (diff)
Improved non-verbose ezSAT::printDIMACS() format
-rw-r--r--libs/ezsat/ezsat.cc7
1 files changed, 6 insertions, 1 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index dccc0055..57762525 100644
--- 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);
}
}