From 22507281cf25d79911fc796e1c3d6bf3e4c8edb0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Apr 2016 12:23:46 -0700 Subject: [PATCH] fix model generation in opt Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 60 +++++++++++++++++----------- src/test/model_based_opt.cpp | 8 ++++ 2 files changed, 44 insertions(+), 24 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 77e552da9..abc93a0b9 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -142,49 +142,61 @@ namespace opt { for (unsigned i = bound_trail.size(); i > 0; ) { --i; unsigned x = bound_vars[i]; - row const& r = m_rows[bound_trail[i]]; + row& r = m_rows[bound_trail[i]]; rational val = r.m_coeff; + rational x_val; rational x_coeff; vector const& vars = r.m_vars; for (unsigned j = 0; j < vars.size(); ++j) { var const& v = vars[j]; - if (x = v.m_id) { + if (x == v.m_id) { x_coeff = v.m_coeff; } else { val += m_var2value[v.m_id]*v.m_coeff; } } + TRACE("opt", display(tout << "v" << x << " val: " << val + << " coeff_x: " << x_coeff << " val_x: " << m_var2value[x] << " ", r); ); SASSERT(!x_coeff.is_zero()); - val /= -x_coeff; - // Adjust epsilon to be s - if (!val.is_zero() && (eps.is_zero() || eps > abs(val))) { - eps = abs(val)/rational(2); - } - if (!r.m_value.is_zero() && (eps.is_zero() || eps > abs(r.m_value))) { - eps = abs(r.m_value)/rational(2); - } + x_val = -val/x_coeff; // // // ax + t < 0 // <=> x < -t/a // <=> x := -t/a - epsilon // - if (x_coeff.is_pos() && r.m_type == t_lt) { - val -= eps; + if (r.m_type == t_lt) { + // Adjust epsilon to be + if (!x_val.is_zero() && (eps.is_zero() || eps >= abs(x_val))) { + eps = abs(x_val)/rational(2); + } + if (!r.m_value.is_zero() && (eps.is_zero() || eps >= abs(r.m_value))) { + eps = abs(r.m_value)/rational(2); + } + + SASSERT(!eps.is_zero()); + if (x_coeff.is_pos()) { + x_val -= eps; + } + // + // -ax + t < 0 + // <=> -ax < -t + // <=> -x < -t/a + // <=> x > t/a + // <=> x := t/a + epsilon + // + else if (x_coeff.is_neg()) { + x_val += eps; + } } - // - // -ax + t < 0 - // <=> -ax < -t - // <=> -x < -t/a - // <=> x > t/a - // <=> x := t/a + epsilon - // - else if (x_coeff.is_neg() && r.m_type == t_lt) { - val += eps; - } - m_var2value[x] = val; - } + m_var2value[x] = x_val; + r.m_value = (x_val * x_coeff) + val; + + TRACE("opt", display(tout << "v" << x << " val: " << val << " coeff_x: " + << x_coeff << " val_x: " << m_var2value[x] << " ", r); ); + SASSERT(invariant(bound_trail[i], r)); + } } bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, unsigned_vector& other, bool is_pos) { diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index ad1ff1a85..94ac81222 100644 --- a/src/test/model_based_opt.cpp +++ b/src/test/model_based_opt.cpp @@ -36,6 +36,10 @@ static void test1() { opt::inf_eps value = mbo.maximize(); std::cout << value << "\n"; + std::cout << "x: " << mbo.get_value(x) << "\n"; + std::cout << "y: " << mbo.get_value(y) << "\n"; + std::cout << "z: " << mbo.get_value(z) << "\n"; + std::cout << "u: " << mbo.get_value(u) << "\n"; } // test with lower bounds @@ -105,6 +109,10 @@ static void test4() { opt::inf_eps value = mbo.maximize(); std::cout << value << "\n"; + std::cout << "x: " << mbo.get_value(x) << "\n"; + std::cout << "y: " << mbo.get_value(y) << "\n"; + std::cout << "z: " << mbo.get_value(z) << "\n"; + std::cout << "u: " << mbo.get_value(u) << "\n"; } // test with mix of upper and lower bounds