1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * MATRIX REPRESENTATION FOR LINEAR ARITHMETIC SOLVER
21 */
22
23 /*
24 * A matrix is represented as an array of rows
25 * - row i is a sparse representation of (a_i1, ..., a_in)
26 * (where only the non-zero elements are stored)
27 * - for each column j, we keep track of all the rows where
28 * a_ij is non-zero in a column vector
29 *
30 * Equivalently, each row can be seen as a linear equation
31 * a_i1 x_1 + ... + a_in x_n == 0
32 * where x_1, ... , x_n are n variables corresponding to the columns.
33 *
34 * Each row is an array of triples (col_idx, c_ptr, a)
35 * - if col_idx < 0, the triple is not used. A list of free elements
36 * is maintained. Links are stored in the c_ptr field.
37 * - if col_idx >= 0, then it's the index k of a variable x_k
38 * the triple represents a * x_k and c_ptr is an index in the array
39 * column[k].
40 *
41 * Each column is an array of pairs (row_idx, r_ptr)
42 * - if row_idx < 0, the pair is not used. It's stored in a free list
43 * with links stored in r_ptr.
44 * - if row_idx >= 0, then it's the index of a row i and r_ptr is
45 * an index in the array row[i].
46 *
47 * For a non-zero element a_ij in row i, column j, there are two
48 * indices i_ptr and j_ptr such that
49 * - row[i][i_ptr] = (j, j_ptr, a_ij)
50 * - col[j][j_ptr] = (i, i_ptr)
51 *
52 * Column index 0 = const_idx is used to represent constants in the equations:
53 * a_1 x_1 + ... + a_n x_n + b = 0, where b is a rational constant, is represented as
54 * b.x_0 + a_1.x_1 + ... + a_n x_n = 0. The value of x_0 should always be one (i.e., it
55 * should be a fixed variable with lower bound and upper bound both equal to 1).
56 *
57 * Initially, the matrix is not a tableau. Rows can be added arbitrarily, and there are
58 * no basic variables. The matrix can be converted to a tableau using the
59 * tableau_construction functions. This assigns a basic variable to every row.
60 * Then the matrix is in the form
61 *
62 * y_1 + a_11 x_1 + ... + a_1n x_n = 0
63 * ...
64 * y_p + a_p1 x_1 + ... + a_pn x_n = 0
65 *
66 * where y_1, ..., y_p are basic variables. It is possible to add a new row to the
67 * tableau provided the row is of the form y_t + a_t1 x_1 + ... + a_tn x_n = 0
68 * - the basic variable y_t must be a fresh variable, not occurring in any other row.
69 * - the existing basic variables y_1, ..., y_p must not occur in the new row.
70 */
71
72 #ifndef __MATRICES_H
73 #define __MATRICES_H
74
75 #include <stdint.h>
76 #include <stdbool.h>
77
78 #include "terms/polynomials.h"
79 #include "terms/rationals.h"
80 #include "utils/bitvectors.h"
81 #include "utils/generic_heap.h"
82 #include "utils/object_stores.h"
83
84
85 /*
86 * Row and column element
87 */
88 typedef struct row_elem_s {
89 int32_t c_idx; // column index
90 int32_t c_ptr; // pointer into column[c_idx]
91 rational_t coeff;
92 } row_elem_t;
93
94 typedef struct col_elem_s {
95 int32_t r_idx; // row index
96 int32_t r_ptr; // index into row[r_idx]
97 } col_elem_t;
98
99
100 /*
101 * Row descriptor:
102 * - the initialized elements are in row->data[0 ... size-1]
103 * - capacity = size of the array data
104 * - nelems = number of elements (non-zero coefficients)
105 * - free = start of the free list
106 */
107 typedef struct row_s {
108 uint32_t nelems;
109 uint32_t size;
110 uint32_t capacity;
111 int32_t free;
112 row_elem_t data[0]; // real size is equal to capacity
113 } row_t;
114
115
116 /*
117 * Column descriptor: same thing
118 */
119 typedef struct column_s {
120 uint32_t nelems;
121 uint32_t size;
122 uint32_t capacity;
123 int32_t free;
124 col_elem_t data[0]; // the real size is equal to capacity
125 } column_t;
126
127
128
129 /*
130 * Matrix
131 * - two arrays: one for rows, one for columns
132 * - base_var[i] = the basic variable of row i or -1 if basic variables
133 * have not been computed
134 * - base_row[v] = row where v is basic variable or -1 if v is non-basic
135 *
136 * Index array:
137 * - index is an auxiliary array used for building a row r
138 * - for a column j, index[j] is the index of a row_element in r
139 * whose c_idx is j (or -1 if r does not contain j)
140 * (if k = index[j] then r->data[k].c_idx == j)
141 * - outside row operations, index[j] must be -1 for all j
142 *
143 * Mark bitvector:
144 * - one bit per row: 1 means the row is marked, 0 means it's not marked.
145 * - this is used by external code to construct sets of rows (e.g., for propagation)
146 *
147 * Constant array: built on demand
148 * - constant: for each row i, constant[i] = index of the
149 * constant in row i. If constant[i] = k >= 0, then row[i][k] is
150 * <b, x_0, ..>. If constant[i] = -1, then there's no constant in row i.
151 *
152 */
153 typedef struct matrix_s {
154 uint32_t nrows; // number of rows
155 uint32_t ncolumns; // number of columns
156 uint32_t row_cap; // size of the arrays row and basic_var
157 uint32_t column_cap; // size of the column array
158 row_t **row;
159 column_t **column;
160 int32_t *base_var;
161 int32_t *base_row;
162
163 // auxiliary data structures
164 int32_t *index;
165 rational_t factor; // pivot coefficient
166
167 // marks
168 byte_t *marks;
169
170 // optional components
171 int32_t *constant; // maps rows to constant
172 } matrix_t;
173
174
175 /*
176 * Default and maximal size (i.e., max capacity) of a row or column
177 */
178 #define DEF_MATRIX_ROW_SIZE 10
179 #define MAX_MATRIX_ROW_SIZE ((uint32_t)((UINT32_MAX-sizeof(row_t))/sizeof(row_elem_t)))
180
181 #define DEF_MATRIX_COL_SIZE 10
182 #define MAX_MATRIX_COL_SIZE ((uint32_t)((UINT32_MAX-sizeof(column_t))/sizeof(col_elem_t)))
183
184
185 /*
186 * Threshold that triggers a reduction of basic columns
187 * - if variable x is made basic and column[x] has capacity >= MATRIX_SHRINK_THRESHOLD
188 * then column[x] is reduced to a column of default capacity (i.e., DEF_MATRIX_COL_SIZE)
189 * (because column[x] needs to contain only one element).
190 */
191 #define MATRIX_SHRINK_COLUMN_THRESHOLD 100
192
193
194 /*
195 * Default and maximal number of rows/columns in a matrix
196 * - we set the max to UINT32_MAX/8 == UINT32_MAX/sizeof(pointer on 64bit machines)
197 * - this should help make the behavior consistent on 32/64 bit architectures
198 */
199 #define DEF_MATRIX_NUM_ROWS 100
200 #define MAX_MATRIX_NUM_ROWS (UINT32_MAX/8)
201
202 #define DEF_MATRIX_NUM_COLUMNS 100
203 #define MAX_MATRIX_NUM_COLUMNS (UINT32_MAX/8)
204
205
206
207
208 /*
209 * GAUSSIAN ELIMINATION
210 */
211
212 /*
213 * Gaussian elimination constructs a triangular matrix
214 * a_11 x_1 + a_12 x_2 + ..... + a_1n x_n == 0
215 * a_22 x_2 + ..... + a_2n x_n == 0
216 * ....
217 * a_kk xk + ... + a_kn x_n == 0
218 * with a_11=1, ..., a_kk = 1
219 *
220 * We may need this to construct models. We store the
221 * triangular matrix in two arrays: each row is represented
222 * as a polynomial + we keep a base_var array that gives
223 * the diagonal variable for each row
224 */
225 typedef struct elim_matrix_s {
226 uint32_t nrows;
227 uint32_t capacity;
228 polynomial_t **row;
229 int32_t *base_var;
230 } elim_matrix_t;
231
232
233 #define DEF_ELIM_MATRIX_NUM_ROWS 10
234 #define MAX_ELIM_MATRIX_NUM_ROWS (UINT32_MAX/8)
235
236
237 /*
238 * Fixed variables: during Gaussian elimination,
239 * all variables that occur in a row x == 0 or x + a == 0
240 * (where a is a constant) are eliminated.
241 * The corresponding variables and their values are stored in
242 * a resizable array. Each element of the array is a pair <var, rational>
243 */
244 typedef struct fvar_rec_s {
245 int32_t var;
246 rational_t value;
247 } fvar_rec_t;
248
249 typedef struct fvar_vector_s {
250 uint32_t nvars; // number of fixed variables
251 uint32_t size; // size of the array
252 fvar_rec_t *fvar;
253 } fvar_vector_t;
254
255 #define DEF_FVAR_VECTOR_SIZE 10
256 #define MAX_FVAR_VECTOR_SIZE (UINT32_MAX/sizeof(fvar_rec_t))
257
258
259 /*
260 * Markowitz's heuristic:
261 * - Gaussian elimination selects a pivot a_ij/=0 in row i, column j
262 * - to keep the matrix sparse after pivoting, the heuristic picks
263 * a_ij for which (r_count[i] - 1) * (c_count[j] - 1) is minimal
264 * where r_count[i] = number of non-zero coefficients in row i
265 * c_count[j] = number of non-zero coefficients in column j
266 *
267 * To implement this, we keep for a record for each row i:
268 * - the best column j in that row + the index k of the corresponding element
269 * - the score (r_count[i] - 1) * (c_count[j] - 1)
270 */
271
272 /*
273 * Record for each row r
274 * - row[r]->data[r_ptr].c_idx = best column
275 */
276 typedef struct row_record_s row_record_t;
277
278 struct row_record_s {
279 uint32_t score; // (r_count[r_idx] - 1) * (c_count[c_idx] - 1)
280 uint32_t c_idx; // best column
281 uint32_t r_ptr; // element index
282 };
283
284
285 /*
286 * Pivot selection data:
287 * - row_rec[r] = record for row r or NULL is r is not considered for elimination
288 * - elim_flag = bitvector: elim_flag[x] = 1 if x is to be eliminated, 0 otherwise
289 * - heap = all rows with non-NULL record in increasing score order
290 * - store = object store to allocate row_records
291 */
292 typedef struct markowitz_s {
293 uint32_t nrows;
294 uint32_t ncolumns;
295 row_record_t **row_rec;
296 byte_t *elim_flag;
297 generic_heap_t heap;
298 object_store_t store;
299 } markowitz_t;
300
301
302 // parameter for object-store: number of records per block
303 #define MARKOWITZ_RECORDS_PER_BLOCK 330
304
305
306
307 /*
308 * GENERIC MATRICES
309 */
310
311 /*
312 * Initialize a matrix of initial capacity = n rows, m columns
313 * - if n == 0, then DEF_MATRIX_NUM_ROWS is used,
314 * - if m == 0, then DEF_MATRIX_NUM_COLUMNS is used
315 * - nrows and ncolumns are both 0
316 */
317 extern void init_matrix(matrix_t *matrix, uint32_t n, uint32_t m);
318
319 /*
320 * Delete matrix: free all memory it uses
321 */
322 extern void delete_matrix(matrix_t *matrix);
323
324 /*
325 * Reset the matrix: to the empty matrix (nrows = ncolumns = 0)
326 */
327 extern void reset_matrix(matrix_t *matrix);
328
329 /*
330 * Make a copy of matrix1 into matrix
331 * - this copies the rows and columns
332 * - row_idx, base_var, base_row are set to NULL
333 */
334 extern void copy_matrix(matrix_t *matrix, matrix_t *matrix1);
335
336
337
338 /*
339 * ROW AND COLUMN ADDITION
340 */
341
342 /*
343 * Add one column to matrix
344 * - the new column vector is initialized to NULL (empty column)
345 * - its index is the current number of columns
346 */
347 extern void matrix_add_column(matrix_t *matrix);
348
349 /*
350 * Add m columns to matrix
351 * - if p = number of columns before the call, then the new columns
352 * are given ids p to p + m - 1
353 */
354 extern void matrix_add_columns(matrix_t *matrix, uint32_t m);
355
356
357 /*
358 * The two following functions can add arbitrary rows to the matrix,
359 * without assigning basic variables to the new row. They cannot be
360 * used if the matrix is in tableau form.
361 */
362
363 /*
364 * Add a new row of the form p == 0
365 * - p is stored as an array of monomials a[0] ... a[n-1]
366 * - the variables a[0].var ... a[n-1].var must all be existing columns
367 * It should be OK for p to be zero, but that should be avoided since it
368 * adds an empty row to the matrix.
369 */
370 extern void matrix_add_row(matrix_t *matrix, monomial_t *a, uint32_t n);
371
372 /*
373 * Add a new row of the form x - p == 0
374 * - p is stored as an array of monomials a[0] ... a[n-1]
375 * - x must not occur in p
376 * - x and a[0].var, ..., a[n-1].var must be existing columns
377 */
378 extern void matrix_add_eq(matrix_t *matrix, int32_t x, monomial_t *a, uint32_t n);
379
380
381 /*
382 * Add a new row of the form x - p == 0 and make x the basic variable in the new row
383 * - the matrix must be in tableau form
384 * - p is stored as an array of monomials a[0] ... a[n-1]
385 * - x must be a fresh variable not occurring in any row of the tableau
386 * - x and the existing basic variables must not occur in p
387 * - x and a[0].var, ..., a[n-1].var must be existing columns
388 */
389 extern void matrix_add_tableau_eq(matrix_t *matrix, int32_t x, monomial_t *a, uint32_t n);
390
391
392
393 /*
394 * REMOVE ROWS AND COLUMNS
395 */
396
397 /*
398 * Reduce the matrix to dimension n x m
399 * - n = number of rows to keep
400 * - m = number of columns to keep
401 */
402 extern void matrix_shrink(matrix_t *matrix, uint32_t n, uint32_t m);
403
404
405 /*
406 * ACCESS TO MATRIX COMPONENTS
407 */
408
409 /*
410 * Get row i of the matrix
411 */
matrix_row(matrix_t * matrix,uint32_t i)412 static inline row_t *matrix_row(matrix_t *matrix, uint32_t i) {
413 assert(i < matrix->nrows);
414 return matrix->row[i];
415 }
416
417 /*
418 * Get column x of the matrix (this may be NULL)
419 */
matrix_column(matrix_t * matrix,int32_t x)420 static inline column_t *matrix_column(matrix_t *matrix, int32_t x) {
421 assert(0 <= x && x < matrix->ncolumns);
422 return matrix->column[x];
423 }
424
425 /*
426 * Get the basic variable in row i
427 * - return -1 = null_thvar if there's no basic variable
428 */
matrix_basic_var(matrix_t * matrix,uint32_t i)429 static inline int32_t matrix_basic_var(matrix_t *matrix, uint32_t i) {
430 assert(i < matrix->nrows);
431 return matrix->base_var[i];
432 }
433
434 /*
435 * Get the row where variable x is basic
436 * - return -1 if x is not basic
437 */
matrix_basic_row(matrix_t * matrix,int32_t x)438 static inline int32_t matrix_basic_row(matrix_t *matrix, int32_t x) {
439 assert(0 <= x && x < matrix->ncolumns);
440 return matrix->base_row[x];
441 }
442
443 /*
444 * Check whether x is basic
445 */
matrix_is_basic_var(matrix_t * matrix,int32_t x)446 static inline bool matrix_is_basic_var(matrix_t *matrix, int32_t x) {
447 return matrix_basic_row(matrix, x) >= 0;
448 }
449
matrix_is_nonbasic_var(matrix_t * matrix,int32_t x)450 static inline bool matrix_is_nonbasic_var(matrix_t *matrix, int32_t x) {
451 return matrix_basic_row(matrix, x) < 0;
452 }
453
454
455 /*
456 * Number of non-zero coefficients in row i
457 */
matrix_row_count(matrix_t * matrix,uint32_t i)458 static inline uint32_t matrix_row_count(matrix_t *matrix, uint32_t i) {
459 assert(i < matrix->nrows);
460 return matrix->row[i]->nelems;
461 }
462
463
464 /*
465 * Number of non-zero coefficients in column x
466 */
matrix_column_count(matrix_t * matrix,int32_t x)467 static inline uint32_t matrix_column_count(matrix_t *matrix, int32_t x) {
468 assert(0 <= x && x < matrix->ncolumns);
469 return matrix->column[x] == NULL ? 0 : matrix->column[x]->nelems;
470 }
471
472
473
474 /*
475 * Coefficient of element k in row r
476 */
matrix_coeff(matrix_t * matrix,uint32_t r,uint32_t k)477 static inline rational_t *matrix_coeff(matrix_t *matrix, uint32_t r, uint32_t k) {
478 assert(r < matrix->nrows && k < matrix->row[r]->size && matrix->row[r]->data[k].c_idx >= 0);
479 return &matrix->row[r]->data[k].coeff;
480 }
481
482
483
484 /*
485 * MARKS
486 */
487
488 /*
489 * Set or clear mark on row r
490 */
matrix_mark_row(matrix_t * matrix,uint32_t r)491 static inline void matrix_mark_row(matrix_t *matrix, uint32_t r) {
492 assert(r < matrix->nrows);
493 set_bit(matrix->marks, r);
494 }
495
matrix_unmark_row(matrix_t * matrix,uint32_t r)496 static inline void matrix_unmark_row(matrix_t *matrix, uint32_t r) {
497 assert(r < matrix->nrows);
498 clr_bit(matrix->marks, r);
499 }
500
501
502 /*
503 * Check whether row r is marked
504 */
matrix_row_is_marked(matrix_t * matrix,uint32_t r)505 static inline bool matrix_row_is_marked(matrix_t *matrix, uint32_t r) {
506 assert(r < matrix->nrows);
507 return tst_bit(matrix->marks, r);
508 }
509
matrix_row_is_unmarked(matrix_t * matrix,uint32_t r)510 static inline bool matrix_row_is_unmarked(matrix_t *matrix, uint32_t r) {
511 return ! matrix_row_is_marked(matrix, r);
512 }
513
514
515
516 /*
517 * ELIMINATION OF FIXED VARIABLES
518 */
519
520 /*
521 * The process is
522 * 1) build the const_idx vector
523 * 2) call eliminate_fixed variable for every fixed variable x
524 * 3) call cleanup_constants
525 * - no rows or columns should be added during this process
526 */
527
528 /*
529 * Allocate and initialize the constant array
530 */
531 extern void matrix_collect_constants(matrix_t *matrix);
532
533 /*
534 * Remove a fixed variable x (i.e., apply the substitution x := a)
535 * - a must be a rational (not an extended rational)
536 * - if row i contains variable x with coefficient b, then we add
537 * b * a to the constant of that row
538 */
539 extern void matrix_eliminate_fixed_variable(matrix_t *matrix, int32_t x, rational_t *a);
540
541 /*
542 * Cleanup the constants: remove all constant elements with coeff == 0
543 * - then delete the constant vector
544 */
545 extern void matrix_cleanup_constants(matrix_t *matrix);
546
547
548
549
550 /*
551 * PIVOTING
552 */
553
554 /*
555 * Given a row r and k = index of a row element in r (such that r[k] = <a, x, ..>
556 * - divide all coefficients in row r by a so that the coefficient of x is 1
557 */
558 extern void matrix_scale_row(row_t *r, uint32_t k);
559
560 /*
561 * Eliminate a variable from row r:
562 * - r = index of the row where variable elimination is done
563 * - k = index in that row of an element a.x where x is the variable to eliminate
564 * (i.e., matrix->row[r]->data[k] is (x, .., a) and a is non-zero
565 * - row0 = a row where x has coefficient 1 (it must be distinct from row[r])
566 *
567 * The function subtract a * row0 from row[r] to eliminate x.
568 */
569 extern void matrix_submul_row(matrix_t *matrix, uint32_t r, uint32_t k, row_t *row0);
570
571 /*
572 * Pivoting: make a variable x basic in row r0
573 * - r0 = row index
574 * - k = element index in row r0 that identifies x:
575 * k must be the index of a valid element, such that
576 * matrix->row[r0]->data[k] is a triple (x, j, a) where
577 * x is a variable index (x >= 0)
578 * a is a non-zero rational
579 * Important: x must not be equal to const_idx (i.e., 0)
580 */
581 extern void matrix_pivot(matrix_t *matrix, uint32_t r0, uint32_t k);
582
583
584
585
586 /*
587 * ELIMINATION MATRICES
588 */
589
590 /*
591 * Initialize an elimination matrix.
592 * - the initial row_capacity is 0
593 * - number of rows = 0 too
594 */
595 extern void init_elim_matrix(elim_matrix_t *matrix);
596
597 /*
598 * Delete an elimination matrix
599 * - also delete all the polynomials it contains
600 */
601 extern void delete_elim_matrix(elim_matrix_t *matrix);
602
603 /*
604 * Reset to an empty elimination matrix
605 * - also delete all polynomials
606 */
607 extern void reset_elim_matrix(elim_matrix_t *matrix);
608
609
610 /*
611 * Get row number i
612 */
elim_matrix_row(elim_matrix_t * matrix,uint32_t i)613 static inline polynomial_t *elim_matrix_row(elim_matrix_t *matrix, uint32_t i) {
614 assert(i < matrix->nrows);
615 return matrix->row[i];
616 }
617
618 /*
619 * Get diagonal variable for row i
620 */
elim_matrix_base_var(elim_matrix_t * matrix,uint32_t i)621 static inline int32_t elim_matrix_base_var(elim_matrix_t *matrix, uint32_t i) {
622 assert(i < matrix->nrows);
623 return matrix->base_var[i];
624 }
625
626
627
628 /*
629 * FIXED VARIABLE VECTOR
630 */
631
632 /*
633 * Initialize a vector to store fixed variables
634 * - initial size is 0
635 */
636 extern void init_fvar_vector(fvar_vector_t *v);
637
638 /*
639 * Clear all rationals then delete the vector
640 */
641 extern void delete_fvar_vector(fvar_vector_t *v);
642
643 /*
644 * Reset to the empty vector
645 */
646 extern void reset_fvar_vector(fvar_vector_t *v);
647
648
649
650 /*
651 * MATRIX SIMPLIFICATION AND TABLEAU CONSTRUCTION
652 */
653
654 /*
655 * The simplifications rely on Gaussian elimination to attempt to
656 * remove variables. Empty rows that occur during Gaussian elimination
657 * are removed. Also, if a simple row a.x + b == 0 or a.x == 0 is
658 * created, then x is eliminated and stored in the fixed-variable
659 * vector.
660 *
661 * Parameters:
662 * - matrix = input matrix
663 * - elim_candidates = array of variables that may be eliminated
664 * n = size of that array. There must not be duplicates in the array.
665 * - i_flag = bitvector that indicates which variables are integer:
666 * i_flag[x] = 1 means x is an integer variable,
667 * i_flag[x] = 0 means x is not an integer variable
668 * - elim = elimination matrix where the eliminated rows will be stored
669 * (if elim is NULL nothing is stored)
670 * - fvars = vectors to record the eliminated fixed variables
671 *
672 * The result is stored in matrix, elim, and fvars:
673 * - matrix = the simplified matrix
674 * - fvars = rows of the form x == b where x is eliminated and b is a rational constant
675 * - elim (if non-NULL) = other eliminated rows/triangular matrix
676 *
677 * NOTE: the variable assignments in fvars may be inconsistent
678 * - there can be two types of inconsistencies:
679 * (x == 0) where x = const_idx = 1 if a row a == 0 is generated with a!=0
680 * (x == b) where x is an integer variable and b is not an integer
681 * - the caller must check for this
682 */
683 extern void simplify_matrix(matrix_t *matrix, int32_t *elim_candidates, uint32_t n,
684 byte_t *i_flag, elim_matrix_t *elim, fvar_vector_t *fvars);
685
686
687
688
689 /*
690 * Simple tableau construction
691 * - scan all rows
692 * - if a row is of the form a.x == 0 or a.x + b == 0,
693 * record the corresponding assignment (x == 0 or x == -b/a) in fvars
694 * and remove the row
695 * - otherwise, pick the variable with smallest column count and make it basic variable
696 *
697 * There can be inconsistent assignments in fvars (cf. simplify_matrix)
698 */
699 extern void simple_tableau_construction(matrix_t *matrix, fvar_vector_t *fvars);
700
701
702 /*
703 * Tableau construction using the Markowitz heuristic
704 * - process the rows in the order defined by the Markowitz heuristic
705 * - eliminate rows of the from a.x == 0 or a.x + b == 0
706 * and record the corresponding variable assignment in fvars
707 *
708 * There can be inconsistent assignments in fvars (cf. note in simplify_matrix)
709 */
710 extern void markowitz_tableau_construction(matrix_t *matrix, fvar_vector_t *fvars);
711
712
713
714
715 #ifndef NDEBUG
716
717 /*
718 * SUPPORT FOR DEBUGGING
719 */
720
721 /*
722 * Check internal consistency of matrix m:
723 * - check whether the base_var and base_row are consistent
724 * - check whether row and columns are consistent
725 */
726 extern bool good_matrix(matrix_t *matrix);
727
728 #endif
729
730
731
732
733 #endif /* __MATRICES_H */
734