mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

pretty printing for lp

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-06 11:34:28 +02:00
parent ef284cca5d
commit 16452fec43
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/column_namer.h
View file

@ -53,7 +53,7 @@ public:
if (val == -numeric_traits<T>::one()) if (val == -numeric_traits<T>::one())
out << " - "; out << " - ";
else if (val != numeric_traits<T>::one()) else if (val != numeric_traits<T>::one())
out << val; out << val << "*";
out << get_variable_name(it.second); out << get_variable_name(it.second);
} }

2
src/math/lp/lp_utils.h
View file

@ -118,7 +118,7 @@ std::ostream& print_linear_combination_customized(const vector<std::pair<T, unsi
} }
} }
if (val != 1) { if (val != 1) {
out << T_to_string(val); out << T_to_string(val) << "*";
} }
out << var_str(it.second); out << var_str(it.second);
} }