1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     int_cube.cpp
7 
8 Abstract:
9 
10     Cube finder
11 
12 Author:
13     Lev Nachmanson (levnach)
14     Nikolaj Bjorner (nbjorner)
15 
16 Revision History:
17 --*/
18 
19 #include "math/lp/int_solver.h"
20 #include "math/lp/lar_solver.h"
21 #include "math/lp/int_cube.h"
22 
23 namespace lp {
24 
int_cube(int_solver & lia)25     int_cube::int_cube(int_solver& lia):lia(lia), lra(lia.lra) {}
26 
operator ()()27     lia_move int_cube::operator()() {
28         lia.settings().stats().m_cube_calls++;
29         TRACE("cube",
30               for (unsigned j = 0; j < lra.number_of_vars(); j++)
31                   lia.display_column(tout, j);
32               tout << lra.constraints();
33               );
34 
35         lra.push();
36         if (!tighten_terms_for_cube()) {
37             lra.pop();
38             lra.set_status(lp_status::OPTIMAL);
39             return lia_move::undef;
40         }
41 
42         lp_status st = lra.find_feasible_solution();
43         if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
44             TRACE("cube", tout << "cannot find a feasible solution";);
45             lra.pop();
46             lra.move_non_basic_columns_to_bounds(false);
47             // it can happen that we found an integer solution here
48             return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
49         }
50         lra.pop();
51         lra.round_to_integer_solution();
52         lra.set_status(lp_status::FEASIBLE);
53         lp_assert(lia.settings().get_cancel_flag() || lia.is_feasible());
54         TRACE("cube", tout << "success";);
55         lia.settings().stats().m_cube_success++;
56         return lia_move::sat;
57     }
58 
tighten_term_for_cube(unsigned i)59     bool int_cube::tighten_term_for_cube(unsigned i) {
60         if (!lra.term_is_used_as_row(i))
61             return true;
62         const lar_term* t = lra.terms()[i];
63         impq delta = get_cube_delta_for_term(*t);
64         TRACE("cube", lra.print_term_as_indices(*t, tout); tout << ", delta = " << delta;);
65         if (is_zero(delta))
66             return true;
67         return lra.tighten_term_bounds_by_delta(tv::term(i), delta);
68     }
69 
tighten_terms_for_cube()70     bool int_cube::tighten_terms_for_cube() {
71         for (unsigned i = 0; i < lra.terms().size(); i++)
72             if (!tighten_term_for_cube(i)) {
73                 TRACE("cube", tout << "cannot tighten";);
74                 return false;
75             }
76         return true;
77     }
78 
find_feasible_solution()79     void int_cube::find_feasible_solution() {
80         lra.find_feasible_solution();
81         lp_assert(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status());
82     }
83 
get_cube_delta_for_term(const lar_term & t) const84     impq int_cube::get_cube_delta_for_term(const lar_term& t) const {
85         if (t.size() == 2) {
86             bool seen_minus = false;
87             bool seen_plus = false;
88             for(const auto & p : t) {
89                 if (!lia.column_is_int(p.column()))
90                     goto usual_delta;
91                 const mpq & c = p.coeff();
92                 if (c == one_of_type<mpq>()) {
93                     seen_plus = true;
94                 } else if (c == -one_of_type<mpq>()) {
95                     seen_minus = true;
96                 } else {
97                     goto usual_delta;
98                 }
99             }
100             if (seen_minus && seen_plus)
101                 return zero_of_type<impq>();
102             return impq(0, 1);
103         }
104     usual_delta:
105         mpq delta = zero_of_type<mpq>();
106         for (const auto & p : t)
107             if (lia.column_is_int(p.column()))
108                 delta += abs(p.coeff());
109 
110         delta *= mpq(1, 2);
111         return impq(delta);
112     }
113 
114 }
115