mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

work on Gomory cut

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-18 13:47:18 -07:00
parent ca3ce964ce
commit b940b7873b
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/util/lp/gomory.cpp
View file

@ -190,12 +190,13 @@ class gomory::imp {
void dump_row_coefficients(std::ostream & out) const { void dump_row_coefficients(std::ostream & out) const {
for (const auto& p : m_row) { for (const auto& p : m_row) {
dump_coeff(out, p); if (!column_is_fixed(p.var()))
dump_coeff(out, p);
} }
} }
void dump_the_row(std::ostream& out) const { void dump_the_row(std::ostream& out) const {
out << "; the row\n"; out << "; the row, excluding fixed vars\n";
out << "(assert ( = ( + "; out << "(assert ( = ( + ";
dump_row_coefficients(out); dump_row_coefficients(out);
out << ") 0))\n"; out << ") 0))\n";
@ -204,6 +205,7 @@ class gomory::imp {
void dump_declarations(std::ostream& out) const { void dump_declarations(std::ostream& out) const {
// for a column j the var name is vj // for a column j the var name is vj
for (const auto & p : m_row) { for (const auto & p : m_row) {
if (column_is_fixed(p.var())) continue;
out << "(declare-fun " << var_name(p.var()) << " () " out << "(declare-fun " << var_name(p.var()) << " () "
<< (is_int(p.var())? "Int" : "Real") << ")\n"; << (is_int(p.var())? "Int" : "Real") << ")\n";
} }
@ -217,8 +219,9 @@ class gomory::imp {
} }
void dump_explanations(std::ostream& out) const { void dump_explanations(std::ostream& out) const {
for (const auto & p : m_row) { for (const auto & p : m_row) {
unsigned j = p.var(); unsigned j = p.var();
if (column_is_fixed(j)) continue;
if (j == m_inf_col) { if (j == m_inf_col) {
continue; continue;
} }