Chernikova level functions

The following functions represent the core of operations in Polylib. They are used in the conversion process and work with localy defined types like the saturation matrix. Their declaration is static so they are accessible to all the functions declared in the file Polyhedron.c but not in any other functions.

struct SatMatrix

: the saturation matrix is defined to be an integer (int type) matrix.

static SatMatrix * BuildSat

(Matrix *Mat, Matrix *Ray, unsigned NbConstraints, unsigned NbMaxRays): build a saturation matrix from constraint matrix 'Mat' and a ray matrix 'Ray'.

void errormsg1

(char *f , char *msgname, char *msg): errormsg1 is an external function which is usually supplied by the calling program.

static SatMatrix * SMAlloc

(int rows, int cols): allocate memory space for a saturation matrix.

static void SMFree

(SatMatrix *matrix): free the memory space occupied by a saturation matrix.

static void SMPrint

(SatMatrix *matrix): print the contents of a saturation matrix.

static void SatVector_OR

(int *p1, int *p2, int *p3, unsigned length): compute the bitwise OR of two saturation matrices.

static void Combine

(Value *p1, Value *p2, Value *p3, int pos, unsigned length): compute the linear combination of two vectors 'p1' and 'p2'.

static SatMatrix * TransformSat

(Matrix *Mat, Matrix *Ray, SatMatrix *Sat): return the transpose of the saturation matrix 'Sat'.

static void RaySort

(Matrix *Ray, SatMatrix *Sat, int NbBid, int NbRay, int *equal_bound, int *sup_bound, unsigned RowSize1, unsigned RowSize2, unsigned bx, unsigned jx): sort the rays (Ray, Sat) into three tiers as used in the Chernikova function.

static int Chernikova

(Matrix *Mat, Matrix *Ray, SatMatrix *Sat, unsigned NbBid, unsigned NbMaxRays, unsigned FirstConstraint, unsigned dual): compute the dual of matrix 'Mat' and place it in matrix 'Ray'.

int Gauss

(Matrix *Mat, int NbEq, int Dimension): compute a minimal system of equations using Gausian elimination method.

static Polyhedron * Remove_Redundants

(Matrix *Mat, Matrix *Ray, SatMatrix *Sat, unsigned *Filter): compute a polyhedron composed of 'Mat' as constraint matrix and 'Ray' as ray matrix after reductions.

static void SimplifyEqualities

(Polyhedron *Pol1, Polyhedron *Pol2, unsigned *Filter): eliminate equations of 'Pol1' using equations of 'Pol2'.

static int SimplifyConstraints

(Polyhedron *Pol1, Polyhedron *Pol2, unsigned *Filter, unsigned NbMaxRays): return 0 if the intersection of two polyhedra is empty, otherwise return 1.