From 6eed885379370a1ec1912cef7e08b9504e37116b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Oct 2021 10:42:39 -0400 Subject: [PATCH] print bounded terms for better efficiency --- src/opt/opt_context.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e78da961b..a8c0d5144 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -967,12 +967,12 @@ namespace opt { tout << "Convert minimization " << orig_term << "\n"; tout << "to maxsat: " << term << "\n"; for (unsigned i = 0; i < weights.size(); ++i) { - tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n"; + tout << mk_pp(terms.get(i), m) << ": " << weights[i] << "\n"; } tout << "offset: " << offset << "\n"; ); std::ostringstream out; - out << orig_term << ':' << index; + out << mk_bounded_pp(orig_term, m, 2) << ':' << index; id = symbol(out.str()); return true; } @@ -995,7 +995,7 @@ namespace opt { } neg = true; std::ostringstream out; - out << orig_term << ':' << index; + out << mk_bounded_pp(orig_term, m) << ':' << index; id = symbol(out.str()); return true; } @@ -1014,7 +1014,7 @@ namespace opt { } neg = is_max; std::ostringstream out; - out << orig_term << ':' << index; + out << mk_bounded_pp(orig_term, m, 2) << ':' << index; id = symbol(out.str()); return true; }