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