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