Source

z3 / src / math / polynomial / upolynomial_factorization_int.h

Full commit
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    upolynomial_factorization_int.h

Abstract:
    
    (Internal) header file for univariate polynomial factorization.
    This classes are exposed for debugging purposes only.

Author:

    Dejan (t-dejanj) 2011-11-29

Notes:

   [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, 
       46(8-10):1853–1859, 1967.
   [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third 
       edition, 1997.
   [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993.

--*/
#ifndef _UPOLYNOMIAL_FACTORIZATION_INT_H_
#define _UPOLYNOMIAL_FACTORIZATION_INT_H_

#include"upolynomial_factorization.h"

namespace upolynomial {
    // copy p from some manager to zp_p in Z_p[x]
    inline void to_zp_manager(zp_manager & zp_upm, numeral_vector & p) {
        zp_numeral_manager & zp_nm(zp_upm.m());
        for (unsigned i = 0; i < p.size(); ++ i) {
            zp_nm.p_normalize(p[i]);
        }
        zp_upm.trim(p);
    }

    // copy p from some manager to zp_p in Z_p[x]
    inline void to_zp_manager(zp_manager & zp_upm, numeral_vector const & p, numeral_vector & zp_p) {
        zp_numeral_manager & zp_nm(zp_upm.m());
        zp_upm.reset(zp_p);
        for (unsigned i = 0; i < p.size(); ++ i) {
            numeral p_i; // no need to delete, we keep it pushed in zp_p
            zp_nm.set(p_i, p[i]);
            zp_p.push_back(p_i);
        }
        zp_upm.trim(zp_p);
    }

    /**
       \brief Contains all possible degrees of a factorization of a polynomial.
       If 
         p = p1^{k_1} * ... * pn^{k_n} with p_i of degree d_i
       then it is represents numbers of the for \sum a_i*d_i, where a_i <= k_i. Two numbers always in the set are
       deg(p) and 0. 

    */
    class factorization_degree_set {
    
        // the set itself, a (m_max_degree)-binary number
        bit_vector m_set;
        
    public:

        factorization_degree_set() { }

        factorization_degree_set(zp_factors const & factors)
        {
            zp_manager & upm = factors.upm();
            // the set contains only {0}
            m_set.push_back(true);
            for (unsigned i = 0; i < factors.distinct_factors(); ++ i) {
                unsigned degree = upm.degree(factors[i]);
                unsigned multiplicity = factors.get_degree(i);                
                for (unsigned k = 0; k < multiplicity; ++ k) {
                    bit_vector tmp(m_set);
                    m_set.shift_right(degree);
                    m_set |= tmp;
                }
            }
            SASSERT(in_set(0) && in_set(factors.get_degree()));
        }

        unsigned max_degree() const { return m_set.size() - 1; }

        void swap(factorization_degree_set & other) {
            m_set.swap(other.m_set);
        }

        bool is_trivial() const { 
            // check if set = {0, n}
            for (int i = 1; i < (int) m_set.size() - 1; ++ i) {
                if (m_set.get(i)) return false;
            }
            return true;
        }

        void remove(unsigned k) {
            m_set.set(k, false);
        }

        bool in_set(unsigned k) const { 
            return m_set.get(k);
        }

        void intersect(const factorization_degree_set& other) {
            m_set &= other.m_set;
        }

        void display(std::ostream & out) const {
            out << "[0";
            for (unsigned i = 1; i <= max_degree(); ++ i) {
                if (in_set(i)) {
                    out << ", " << i;
                }
            }
            out << "] represented by " << m_set;
        }
    };

    /**
       \brief A to iterate through all combinations of factors. This is only needed for the factorization, and we 
       always iterate through the 
    */
    template <typename factors_type>
    class factorization_combination_iterator_base {

    protected:


        // total size of available factors
        int                    m_total_size;
        // maximal size of the selection
        int                    m_max_size;
        // the factors to select from
        factors_type const   & m_factors;
        // which factors are enabled
        svector<bool>          m_enabled;
        // the size of the current selection
        int                    m_current_size;
        // the current selection: indices at positions < m_current_size, other values are maxed out
        svector<int>           m_current;
        
        /**
           Assuming a valid selection m_current[0], ..., m_current[position], try to find the next option for
           m_current[position], i.e. the first bigger one that's enabled.
        */
        int find(int position, int upper_bound) {
            int current = m_current[position] + 1;
            while (current < upper_bound && !m_enabled[current]) {
                current ++;
            }
            if (current == upper_bound) {
                return -1;
            } else {
                return current;
            }
        }

    public:

        factorization_combination_iterator_base(factors_type const & factors)
        : m_total_size(factors.distinct_factors()), 
          m_max_size(factors.distinct_factors()/2), 
          m_factors(factors)
        {    
            SASSERT(factors.total_factors() > 1);
            SASSERT(factors.total_factors() == factors.distinct_factors());
            // enable all to start with
            m_enabled.resize(m_factors.distinct_factors(), true);
            // max out the m_current so that it always fits
            m_current.resize(m_factors.distinct_factors()+1, m_factors.distinct_factors());
            m_current_size = 0;
        }

        /**
           \brief Returns the factors we are enumerating through.
        */
        factors_type const & get_factors() const { 
            return m_factors; 
        }

        /**
           \brief Computes the next combination of factors and returns true if it exists. If remove current is true
           it will eliminate the current selected elements from any future selection.
        */
        bool next(bool remove_current) {
            
            int max_upper_bound = m_factors.distinct_factors();
            
            do {

                // the index we are currently trying to fix
                int current_i = m_current_size - 1;
                // the value we found as plausable (-1 we didn't find anything)
                int current_value = -1;

                if (remove_current) {
                    SASSERT(m_current_size > 0);
                    // disable the elements of the current selection from ever appearing again
                    for (current_i = m_current_size - 1; current_i > 0; -- current_i) {
                        SASSERT(m_enabled[m_current[current_i]]);
                        m_enabled[m_current[current_i]] = false;
                        m_current[current_i] = max_upper_bound;
                    }
                    // the last one
                    SASSERT(m_enabled[m_current[0]]);
                    m_enabled[m_current[0]] = false;
                    // not removing current anymore
                    remove_current = false;
                    // out max size is also going down
                    m_total_size -= m_current_size;
                    m_max_size = m_total_size/2;
                } 
            
                // we go back to the first one that can be increased (if removing current go all the way)
                while (current_i >= 0) {
                    current_value = find(current_i, m_current[current_i + 1]);
                    if (current_value >= 0) {
                        // found one
                        m_current[current_i] = current_value;
                        break;
                    } else {
                        // go back some more
                        current_i --;
                    }
                }
            
                do {
                        
                    if (current_value == -1) {
                        // we couldn't find any options, we have to increse size and start from the first one of that size
                        if (m_current_size >= m_max_size) {
                            return false;
                        } else {     
                            m_current_size ++;
                            m_current[0] = -1;
                            current_i = 0;
                            current_value = find(current_i, max_upper_bound);
                            // if we didn't find any, we are done
                            if (current_value == -1) {
                                return false;
                            } else {
                                m_current[current_i] = current_value;
                            }
                        }
                    } 

                    // ok we have a new selection for the current one
                    for (current_i ++; current_i < m_current_size; ++ current_i) {
                        // start from the previous one
                        m_current[current_i] = m_current[current_i-1];
                        current_value = find(current_i, max_upper_bound);
                        if (current_value == -1) {
                            // screwed, didn't find the next one, this means we need to increase the size
                            m_current[0] = -1;
                            break;
                        } else {
                            m_current[current_i] = current_value;
                        }
                    }
                        
                } while (current_value == -1);
                    
            } while (filter_current());
            
            // found the next one, hurray
            return true;
        }

        /**
           \brief A function that returns true if the current combination should be ignored.
        */
        virtual bool filter_current() const = 0;

        /**
           \brief Returns the size of the current selection (cardinality)
        */
        unsigned left_size() const {
            return m_current_size;
        }

        /**
           \brief Returns the size of the rest of the current selection (cardinality)
        */
        unsigned right_size() const {
            return m_total_size - m_current_size;
        }

        void display(std::ostream& out) const {            
            out << "[ ";
            for (unsigned i = 0; i < m_current.size(); ++ i) {
                out << m_current[i] << " ";
            }          
            out << "] from [ ";
            for (unsigned i = 0; i < m_factors.distinct_factors(); ++ i) {
                if (m_enabled[i]) {
                    out << i << " ";
                }
            }                      
            out << "]" << std::endl;
        }


    };

    class ufactorization_combination_iterator : public factorization_combination_iterator_base<zp_factors> {
    
        // the degree sets to choose from
        factorization_degree_set const & m_degree_set;

    public:
        
        ufactorization_combination_iterator(zp_factors const & factors, factorization_degree_set const & degree_set)
        : factorization_combination_iterator_base<zp_factors>(factors),
          m_degree_set(degree_set) 
        {}

        /**
           \brief Filter the ones not in the degree set.
        */
        bool filter_current() const {
            
            // select only the ones that have degrees in the degree set
            if (!m_degree_set.in_set(current_degree())) {
                return true;
            }            
            return false;
        }

        /** 
           \brief Returns the degree of the current selection.
        */
        unsigned current_degree() const {
            unsigned degree = 0;
            zp_manager & upm = m_factors.pm();
            for (unsigned i = 0; i < left_size(); ++ i) {
                degree += upm.degree(m_factors[m_current[i]]);
            }
            return degree;
        }        

        void left(numeral_vector & out) const {
            SASSERT(m_current_size > 0);
            zp_manager & upm = m_factors.upm();
            upm.set(m_factors[m_current[0]].size(), m_factors[m_current[0]].c_ptr(), out);
            for (int i = 1; i < m_current_size; ++ i) {
                upm.mul(out.size(), out.c_ptr(), m_factors[m_current[i]].size(), m_factors[m_current[i]].c_ptr(), out);
            }
        }

        void get_left_tail_coeff(numeral const & m, numeral & out) {
            zp_numeral_manager &  nm = m_factors.upm().m();
            nm.set(out, m);
            for (int i = 0; i < m_current_size; ++ i) {
                nm.mul(out, m_factors[m_current[i]][0], out);
            }
        }

        void get_right_tail_coeff(numeral const & m, numeral & out) {
            zp_numeral_manager &  nm = m_factors.upm().m();
            nm.set(out, m);

            unsigned current = 0;
            unsigned selection_i = 0;

            // selection is ordered, so we just take the ones in between that are not disable
            while (current <  m_factors.distinct_factors()) {
                if (!m_enabled[current]) {
                    // by skipping the disabled we never skip a selected one
                    current ++;
                } else {   
                    if (selection_i >= m_current.size() || (int) current < m_current[selection_i]) {
                        SASSERT(m_factors.get_degree(current) == 1);
                        nm.mul(out, m_factors[current][0], out);
                        current ++;
                    } else {
                        current ++;
                        selection_i ++;
                    }
                }
            }
        }

        void right(numeral_vector & out) const {
            SASSERT(m_current_size > 0);
            zp_manager & upm = m_factors.upm();
            upm.reset(out);

            unsigned current = 0;
            unsigned selection_i = 0;

            // selection is ordered, so we just take the ones in between that are not disable
            while (current <  m_factors.distinct_factors()) {
                if (!m_enabled[current]) {
                    // by skipping the disabled we never skip a selected one
                    current ++;
                } else {   
                    if (selection_i >= m_current.size() || (int) current < m_current[selection_i]) {
                        SASSERT(m_factors.get_degree(current) == 1);
                        if (out.size() == 0) {
                            upm.set(m_factors[current].size(), m_factors[current].c_ptr(), out);
                        } else {
                            upm.mul(out.size(), out.c_ptr(), m_factors[current].size(), m_factors[current].c_ptr(), out);
                        }
                        current ++;
                    } else {
                        current ++;
                        selection_i ++;
                    }
                }
            }
        }
    };
};

#endif