mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
04ac5f03f7
commit
78f4513441
|
@ -108,7 +108,7 @@ public:
|
|||
void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix, const mpq& sign) {
|
||||
auto & row = m_data[adjust_row(i)];
|
||||
lp_assert(row_is_initialized_correctly(row));
|
||||
for (const auto & p : c) {
|
||||
for (lp::lar_term::ival p : c) {
|
||||
unsigned j = adjust_column(column_fix(p.column().index()));
|
||||
row[j] = sign * p.coeff();
|
||||
}
|
||||
|
|
|
@ -85,7 +85,7 @@ namespace lp {
|
|||
if (t.size() == 2) {
|
||||
bool seen_minus = false;
|
||||
bool seen_plus = false;
|
||||
for(const auto & p : t) {
|
||||
for(lar_term::ival p : t) {
|
||||
if (!lia.column_is_int(p.column()))
|
||||
goto usual_delta;
|
||||
const mpq & c = p.coeff();
|
||||
|
|
|
@ -271,7 +271,7 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream&
|
|||
|
||||
bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
|
||||
rational b(0); // the bound
|
||||
for (const auto& p : t) {
|
||||
for (lp::lar_term::ival p : t) {
|
||||
rational pb;
|
||||
if (explain_coeff_upper_bound(p, pb, e)) {
|
||||
b += pb;
|
||||
|
|
Loading…
Reference in a new issue