1 /*++ 2 Copyright (c) 2014 Microsoft Corporation 3 4 Module Name: 5 6 simplex.h 7 8 Abstract: 9 10 Multi-precision simplex tableau. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2014-01-15 15 16 Notes: 17 18 --*/ 19 20 #include "math/simplex/simplex.h" 21 #include "math/simplex/sparse_matrix_def.h" 22 #include "math/simplex/simplex_def.h" 23 #include "util/rational.h" 24 #include "util/inf_rational.h" 25 26 namespace simplex { 27 template class simplex<mpz_ext>; 28 template class simplex<mpq_ext>; 29 30 static void refine_delta(rational& delta, inf_rational const& l, inf_rational const& u) { 31 if (l.get_rational() < u.get_rational() && l.get_infinitesimal() > u.get_infinitesimal()) { 32 rational new_delta = (u.get_rational() - l.get_rational()) / (l.get_infinitesimal() - u.get_infinitesimal()); 33 if (new_delta < delta) { 34 delta = new_delta; 35 } 36 } 37 } 38 39 40 void ensure_rational_solution(simplex<mpq_ext>& S) { 41 rational delta(1); 42 for (unsigned i = 0; i < S.get_num_vars(); ++i) { 43 auto const& _value = S.get_value(i); 44 inf_rational value(rational(_value.first), rational(_value.second)); 45 if (S.lower_valid(i)) { 46 auto const& _bound = S.get_lower(i); 47 inf_rational bound(rational(_bound.first), rational(_bound.second)); 48 refine_delta(delta, bound, value); 49 } 50 if (S.upper_valid(i)) { 51 auto const& _bound = S.get_upper(i); 52 inf_rational bound(rational(_bound.first), rational(_bound.second)); 53 refine_delta(delta, value, bound); 54 } 55 } 56 unsynch_mpq_inf_manager inf_mgr; 57 scoped_mpq_inf q(inf_mgr); 58 for (unsigned i = 0; i < S.get_num_vars(); ++i) { 59 auto const& _value = S.get_value(i); 60 rational inf(_value.second); 61 if (!inf.is_zero()) { 62 rational fin = rational(_value.first) + inf * delta; 63 inf = 0; 64 inf_mgr.set(q, fin.to_mpq(), inf.to_mpq()); 65 S.set_value(i, q); 66 } 67 } 68 } 69 }; 70