mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
change lar_terms to use column indices
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c2e5cd78c8
commit
d702f48f9e
|
@ -50,8 +50,7 @@ namespace lp {
|
|||
m_constraints_for_explanation.push_back(ci);
|
||||
|
||||
for (const auto &p : *t) {
|
||||
auto tv = lia.lra.column2tv(p.column());
|
||||
m_var_register.add_var(tv.id(), true); // hnf only deals with integral variables for now
|
||||
m_var_register.add_var(p.column().index(), true); // hnf only deals with integral variables for now
|
||||
mpq t = abs(ceil(p.coeff()));
|
||||
if (t > m_abs_max)
|
||||
m_abs_max = t;
|
||||
|
|
|
@ -187,7 +187,7 @@ struct gomory_test {
|
|||
void print_term(lar_term & t, std::ostream & out) {
|
||||
vector<std::pair<mpq, unsigned>> row;
|
||||
for (auto p : t)
|
||||
row.push_back(std::make_pair(p.coeff(), p.var().index()));
|
||||
row.push_back(std::make_pair(p.coeff(), p.column().index()));
|
||||
print_row(out, row);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue