1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 int_gcd_test.h 7 8 Abstract: 9 10 Gcd_Test heuristic 11 12 gcd test 13 5*x + 3*y + 6*z = 5 14 suppose x is fixed at 2. 15 so we have 10 + 3(y + 2z) = 5 16 5 = -3(y + 2z) 17 this is unsolvable because 5/3 is not an integer. 18 so we create a lemma that rules out this condition. 19 20 21 Author: 22 Nikolaj Bjorner (nbjorner) 23 Lev Nachmanson (levnach) 24 25 Revision History: 26 --*/ 27 #pragma once 28 29 #include "math/lp/lia_move.h" 30 31 namespace lp { 32 class int_solver; 33 class lar_solver; 34 class int_gcd_test { 35 36 struct parity { 37 mpq m_offset; 38 mpq m_modulo; 39 const row_strip<mpq>* m_row = nullptr; parityparity40 parity(mpq const& p, mpq const& m, row_strip<mpq> const& r): 41 m_offset(p), 42 m_modulo(m), 43 m_row(&r) 44 {} 45 }; 46 class int_solver& lia; 47 class lar_solver& lra; 48 unsigned m_next_gcd = 0; 49 unsigned m_delay = 0; 50 mpq m_consts; 51 mpq m_least_coeff; 52 mpq m_lcm_den; 53 unsigned_vector m_inserted_vars; 54 vector<vector<parity>> m_parities; 55 unsigned_vector m_visited; 56 unsigned m_visited_ts = 0; 57 is_visited(unsigned i)58 bool is_visited(unsigned i) { return m_visited.get(i, 0) == m_visited_ts; } mark_visited(unsigned i)59 void mark_visited(unsigned i) { m_visited.setx(i, m_visited_ts, 0); } 60 61 void reset_test(); 62 bool insert_parity(unsigned j, row_strip<mpq> const& r, mpq const& parity, mpq const& modulo); 63 64 bool gcd_test(); 65 bool gcd_test_for_row(const static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i); 66 bool ext_gcd_test(const row_strip<mpq> & row); 67 void fill_explanation_from_fixed_columns(const row_strip<mpq> & row); 68 void add_to_explanation_from_fixed_or_boxed_column(unsigned j); 69 bool accumulate_parity(const row_strip<mpq> & row, unsigned least_coeff_index); 70 public: 71 int_gcd_test(int_solver& lia); 72 lia_move operator()(); 73 bool should_apply(); 74 }; 75 } 76