From 0aafa8b7ce3adb82125d72c10370151e35a2fd18 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Feb 2019 15:52:42 +0100
Subject: [PATCH] optimize binary output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_drat.cpp | 19 ++++++++++++-------
src/sat/sat_simplifier.cpp | 1 -
2 files changed, 12 insertions(+), 8 deletions(-)
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index c0799c061..f8e04a583 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -120,22 +120,27 @@ namespace sat {
case status::deleted: ch = 'd'; break;
default: UNREACHABLE(); break;
}
- (*m_bout) << ch;
+ char buffer[10000];
+ int len = 0;
+ buffer[len++] = ch;
for (unsigned i = 0; i < n; ++i) {
literal lit = c[i];
unsigned v = 2 * lit.var() + (lit.sign() ? 1 : 0);
do {
- ch = static_cast<unsigned char>(v & ((1 << 7) - 1));
+ ch = static_cast<unsigned char>(v & 255);
v >>= 7;
- if (v) ch |= (1 << 7);
- //std::cout << std::hex << ((unsigned char)ch) << std::dec << " ";
- (*m_bout) << ch;
+ if (v) ch |= 128;
+ buffer[len++] = ch;
+ if (len == sizeof(buffer)) {
+ m_bout->write(buffer, len);
+ len = 0;
+ }
}
while (v);
}
- ch = 0;
- (*m_bout) << ch;
+ buffer[len++] = 0;
+ m_bout->write(buffer, len);
}
bool drat::is_cleaned(clause& c) const {
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index f536dda03..58dab0ff5 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1222,7 +1222,6 @@ namespace sat {
RI literals.
*/
void minimize_covered_clause(unsigned idx) {
- literal _blocked = m_covered_clause[idx];
for (literal l : m_tautology) VERIFY(s.is_marked(l));
for (literal l : m_covered_clause) s.unmark_visited(l);
for (literal l : m_tautology) s.mark_visited(l);