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