mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

print bounded terms for better efficiency

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-21 10:42:39 -04:00
parent 13da6a02a6
commit 6eed885379
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/opt/opt_context.cpp
View file

@ -967,12 +967,12 @@ namespace opt {
tout << "Convert minimization " << orig_term << "\n"; tout << "Convert minimization " << orig_term << "\n";
tout << "to maxsat: " << term << "\n"; tout << "to maxsat: " << term << "\n";
for (unsigned i = 0; i < weights.size(); ++i) { 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"; tout << "offset: " << offset << "\n";
); );
std::ostringstream out; std::ostringstream out;
out << orig_term << ':' << index; out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
id = symbol(out.str()); id = symbol(out.str());
return true; return true;
} }
@ -995,7 +995,7 @@ namespace opt {
} }
neg = true; neg = true;
std::ostringstream out; std::ostringstream out;
out << orig_term << ':' << index; out << mk_bounded_pp(orig_term, m) << ':' << index;
id = symbol(out.str()); id = symbol(out.str());
return true; return true;
} }
@ -1014,7 +1014,7 @@ namespace opt {
} }
neg = is_max; neg = is_max;
std::ostringstream out; std::ostringstream out;
out << orig_term << ':' << index; out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
id = symbol(out.str()); id = symbol(out.str());
return true; return true;
} }