Skip to content

Commit

Permalink
Renamed "matrix_t" and related functions, adding prefix "pk_".
Browse files Browse the repository at this point in the history 
Patch contributed by Michele Spotti.

This renaming is needed to avoid a name clash with (version 3 of)
the FLINT library, which is a required dependency when enabling PPLite.
Note: name clash is caused by functions matrix_clear and matrix_equal.
  • Loading branch information
@ezaffanella
ezaffanella committed Apr 11, 2024
1 parent 457a854 commit 7c43da1
Show file tree
Hide file tree
Showing 28 changed files with 438 additions and 438 deletions.
4 changes: 2 additions & 2 deletions newpolka/pk.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ typedef enum pk_status_t {

struct pk_t {
/* private data: do not use directly ! */
struct matrix_t* C;
struct matrix_t* F;
struct pk_matrix_t* C;
struct pk_matrix_t* F;
struct satmat_t* satC;
struct satmat_t* satF;
size_t intdim;
Expand Down
54 changes: 27 additions & 27 deletions newpolka/pk_approximate.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ static
void poly_set_save_C(pk_t* po, pk_t* pa)
{
if (po != pa){
po->F = pa->F ? matrix_copy(pa->F) : NULL;
po->F = pa->F ? pk_matrix_copy(pa->F) : NULL;
po->satC = pa->satC ? satmat_copy(pa->satC) : NULL;
po->satF = pa->satF ? satmat_copy(pa->satF) : NULL;
po->status = pa->status;
Expand All @@ -49,18 +49,18 @@ bool poly_approximate_n1(ap_manager_t* man, pk_t* po, pk_t* pa, int algorithm)
return false;
}
if (po!=pa){
po->C = matrix_copy(pa->C);
po->C = pk_matrix_copy(pa->C);
}
change = matrix_normalize_constraint_int(pk,po->C,po->intdim,po->realdim);
change = pk_matrix_normalize_constraint_int(pk,po->C,po->intdim,po->realdim);
if (change){
{
/* Add positivity and strictness that may not be implied any more */
size_t nbrows = po->C->nbrows;
matrix_resize_rows_lazy(po->C,nbrows+pk->dec-1);
matrix_fill_constraint_top(pk,po->C,nbrows);
pk_matrix_resize_rows_lazy(po->C,nbrows+pk->dec-1);
pk_matrix_fill_constraint_top(pk,po->C,nbrows);
}
if (po==pa){
if (po->F){ matrix_free(po->F); po->F = NULL; }
if (po->F){ pk_matrix_free(po->F); po->F = NULL; }
if (po->satC){ satmat_free(po->satC); po->satC = NULL; }
if (po->satF){ satmat_free(po->satF); po->satF = NULL; }
}
Expand All @@ -81,7 +81,7 @@ bool poly_approximate_n1(ap_manager_t* man, pk_t* po, pk_t* pa, int algorithm)
pk->max_coeff_size, if pk->max_coeff_size > 0 */
/* ---------------------------------------------------------------------- */
static
bool matrix_approximate_constraint_1(pk_internal_t* pk, matrix_t* C)
bool pk_matrix_approximate_constraint_1(pk_internal_t* pk, pk_matrix_t* C)
{
size_t i,j;
bool change,removed;
Expand All @@ -95,7 +95,7 @@ bool matrix_approximate_constraint_1(pk_internal_t* pk, matrix_t* C)
change = true;
removed = true;
C->nbrows--;
matrix_exch_rows(C,i,C->nbrows);
pk_matrix_exch_rows(C,i,C->nbrows);
break;
}
}
Expand All @@ -105,8 +105,8 @@ bool matrix_approximate_constraint_1(pk_internal_t* pk, matrix_t* C)
if (change){
/* Add positivity and strictness that may not be implied any more */
size_t nbrows = C->nbrows;
matrix_resize_rows_lazy(C,nbrows+pk->dec-1);
matrix_fill_constraint_top(pk,C,nbrows);
pk_matrix_resize_rows_lazy(C,nbrows+pk->dec-1);
pk_matrix_fill_constraint_top(pk,C,nbrows);
C->_sorted = false;
}
return change;
Expand All @@ -123,12 +123,12 @@ bool poly_approximate_1(ap_manager_t* man, pk_t* po, pk_t* pa)
return false;
}
if (po!=pa){
po->C = matrix_copy(pa->C);
po->C = pk_matrix_copy(pa->C);
}
change = matrix_approximate_constraint_1(pk,po->C);
change = pk_matrix_approximate_constraint_1(pk,po->C);
if (change){
if (po==pa){
if (po->F){ matrix_free(po->F); po->F = NULL; }
if (po->F){ pk_matrix_free(po->F); po->F = NULL; }
if (po->satC){ satmat_free(po->satC); po->satC = NULL; }
if (po->satF){ satmat_free(po->satF); po->satF = NULL; }
}
Expand Down Expand Up @@ -190,10 +190,10 @@ void poly_approximate_123(ap_manager_t* man, pk_t* po, int algorithm)
itv_init(itv);
if (algorithm>=2){ /* Add interval constraints */
nbrows2 = 2*dim;
matrix_resize_rows_lazy(pa->C, nbrows + nbrows2);
pk_matrix_resize_rows_lazy(pa->C, nbrows + nbrows2);
pa->C->_sorted = false;
for (i=0; i<dim;i++){
matrix_bound_dimension(pk,itv,i,po->F);
pk_matrix_bound_dimension(pk,itv,i,po->F);
if (!bound_infty(itv->inf)){
vector_set_dim_bound(pk,
pa->C->p[nbrows],
Expand All @@ -219,11 +219,11 @@ void poly_approximate_123(ap_manager_t* man, pk_t* po, int algorithm)
for (i=0; i<dim;i++){
numint_set_int(pk->poly_numintp[pk->dec+i],1);
nbrows2 = 4*(dim-i-1);
matrix_resize_rows_lazy(pa->C, nbrows + nbrows2);
pk_matrix_resize_rows_lazy(pa->C, nbrows + nbrows2);
for (j=i+1; j<dim;j++){
for (sgny=-1; sgny<=1; sgny += 2){
numint_set_int(pk->poly_numintp[pk->dec+j],sgny);
matrix_bound_vector(pk,itv,pk->poly_numintp,po->F);
pk_matrix_bound_vector(pk,itv,pk->poly_numintp,po->F);
if (!bound_infty(itv->inf)){
vector_set_linexpr_bound(pk,
pa->C->p[nbrows], pk->poly_numintp,
Expand Down Expand Up @@ -258,7 +258,7 @@ void poly_approximate_123(ap_manager_t* man, pk_t* po, int algorithm)
/* ---------------------------------------------------------------------- */

static
bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t* F,
bool pk_matrix_approximate_constraint_1x(pk_internal_t* pk, pk_matrix_t* C, pk_matrix_t* F,
bool outerfallback, bool combine)
{
size_t i,j,size,nbrows,nbrows2;
Expand Down Expand Up @@ -304,7 +304,7 @@ bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t*
/* C. Compute new constant coefficient */
numint_set_int(vec[0],1);
numint_set_int(vec[polka_cst],0);
matrix_bound_vector(pk,itv,vec,F);
pk_matrix_bound_vector(pk,itv,vec,F);
finite = !bound_infty(itv->inf);
if (finite){
/* D. We round the constant to an integer and keep the constraint */
Expand All @@ -319,8 +319,8 @@ bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t*
} else {
/* we remove the vector */
removed = true;
matrix_exch_rows(C,i,nbrows-1);
matrix_exch_rows(C,nbrows-1,nbrows2-1);
pk_matrix_exch_rows(C,i,nbrows-1);
pk_matrix_exch_rows(C,nbrows-1,nbrows2-1);
nbrows--; nbrows2--;
}
if (combine || (!finite && outerfallback)){
Expand All @@ -336,7 +336,7 @@ bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t*
/* G. Compute new constant coefficient */
numint_set_int(vec[0],1);
numint_set_int(vec[polka_cst],0);
matrix_bound_vector(pk,itv,vec,F);
pk_matrix_bound_vector(pk,itv,vec,F);
finite = !bound_infty(itv->inf);
if (finite){
/* E. We round the constant to an integer and keep the constraint */
Expand All @@ -348,7 +348,7 @@ bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t*
if (false){ printf("before norm 2: "); vector_print(vec,C->nbcolumns); }
vector_normalize(pk,vec,C->nbcolumns);
if (false){ printf("after norm 2: "); vector_print(vec,C->nbcolumns); }
if (nbrows2>=C->_maxrows) matrix_resize_rows(C,(C->_maxrows*3+1)/2);
if (nbrows2>=C->_maxrows) pk_matrix_resize_rows(C,(C->_maxrows*3+1)/2);
vector_copy(C->p[nbrows2],vec,C->nbcolumns);
nbrows2++;
}
Expand All @@ -361,8 +361,8 @@ bool matrix_approximate_constraint_1x(pk_internal_t* pk, matrix_t* C, matrix_t*
C->nbrows = nbrows2;
/* Add positivity and strictness that may not be implied any more */
size_t nbrows = C->nbrows;
matrix_resize_rows_lazy(C,nbrows+pk->dec-1);
matrix_fill_constraint_top(pk,C,nbrows);
pk_matrix_resize_rows_lazy(C,nbrows+pk->dec-1);
pk_matrix_fill_constraint_top(pk,C,nbrows);
C->_sorted = false;
}
itv_clear(itv);
Expand All @@ -385,9 +385,9 @@ void poly_approximate_1x(ap_manager_t* man, pk_t* po, bool outerfallback, bool c
return;
}
assert(po->C && po->F);
change = matrix_approximate_constraint_1x(pk, po->C, po->F, outerfallback,combine);
change = pk_matrix_approximate_constraint_1x(pk, po->C, po->F, outerfallback,combine);
if (change){
if (po->F) matrix_free(po->F);
if (po->F) pk_matrix_free(po->F);
if (po->satC) satmat_free(po->satC);
if (po->satF) satmat_free(po->satF);
po->F = NULL;
Expand Down
56 changes: 28 additions & 28 deletions newpolka/pk_assign.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,28 +37,28 @@

/* Hypothesis:
- either nmat is a matrix allocated with _matrix_alloc_int,
- either nmat is a matrix allocated with _pk_matrix_alloc_int,
and his coefficients are not initialized,
- or nmat==mat
*/
static
matrix_t* matrix_assign_variable(pk_internal_t* pk,
pk_matrix_t* pk_matrix_assign_variable(pk_internal_t* pk,
bool destructive,
matrix_t* mat,
pk_matrix_t* mat,
ap_dim_t dim, numint_t* tab)
{
size_t i,j,var;
bool den;
matrix_t* nmat;
pk_matrix_t* nmat;

var = pk->dec + dim;
den = numint_cmp_int(tab[0],1)>0;

nmat =
destructive ?
mat :
_matrix_alloc_int(mat->nbrows,mat->nbcolumns,false);
_pk_matrix_alloc_int(mat->nbrows,mat->nbcolumns,false);

nmat->_sorted = false;

Expand Down Expand Up @@ -97,7 +97,7 @@ matrix_t* matrix_assign_variable(pk_internal_t* pk,
else
numint_set(nmat->p[i][var],pk->matrix_prod);

matrix_normalize_row(pk,nmat,i);
pk_matrix_normalize_row(pk,nmat,i);
}
return nmat;
}
Expand All @@ -108,27 +108,27 @@ matrix_t* matrix_assign_variable(pk_internal_t* pk,

/* Hypothesis:
- either nmat is a matrix allocated with _matrix_alloc_int,
- either nmat is a matrix allocated with _pk_matrix_alloc_int,
and his coefficients are not initialized,
- or nmat==mat
*/
static
matrix_t* matrix_substitute_variable(pk_internal_t* pk,
pk_matrix_t* pk_matrix_substitute_variable(pk_internal_t* pk,
bool destructive,
matrix_t* mat,
pk_matrix_t* mat,
ap_dim_t dim, numint_t* tab)
{
size_t i,j,var;
bool den;
matrix_t* nmat;
pk_matrix_t* nmat;

var = pk->dec + dim;
den = numint_cmp_int(tab[0],1)>0;
nmat =
destructive ?
mat :
_matrix_alloc_int(mat->nbrows,mat->nbcolumns,false);
_pk_matrix_alloc_int(mat->nbrows,mat->nbcolumns,false);

nmat->_sorted = false;

Expand Down Expand Up @@ -171,7 +171,7 @@ matrix_t* matrix_substitute_variable(pk_internal_t* pk,
/* var column */
numint_mul(nmat->p[i][var],nmat->p[i][var],tab[var]);
}
matrix_normalize_row(pk,nmat,i);
pk_matrix_normalize_row(pk,nmat,i);
}
else {
/* No substitution */
Expand Down Expand Up @@ -223,14 +223,14 @@ void pk_asssub_isort(ap_dim_t* tdim, numint_t** tvec, size_t size)
/* Assignement by an array of equations */
/* ---------------------------------------------------------------------- */
static
matrix_t* matrix_assign_variables(pk_internal_t* pk,
matrix_t* mat,
pk_matrix_t* pk_matrix_assign_variables(pk_internal_t* pk,
pk_matrix_t* mat,
ap_dim_t* tdim,
numint_t** tvec,
size_t size)
{
size_t i,j,eindex;
matrix_t* nmat = _matrix_alloc_int(mat->nbrows, mat->nbcolumns,false);
pk_matrix_t* nmat = _pk_matrix_alloc_int(mat->nbrows, mat->nbcolumns,false);
numint_t den;

/* Computing common denominator */
Expand Down Expand Up @@ -303,7 +303,7 @@ matrix_t* matrix_assign_variables(pk_internal_t* pk,
}
numint_clear(den);
for (i=0; i<mat->nbrows; i++){
matrix_normalize_row(pk,nmat,i);
pk_matrix_normalize_row(pk,nmat,i);
}

return nmat;
Expand All @@ -314,14 +314,14 @@ matrix_t* matrix_assign_variables(pk_internal_t* pk,
/* ---------------------------------------------------------------------- */

static
matrix_t* matrix_substitute_variables(pk_internal_t* pk,
matrix_t* mat,
pk_matrix_t* pk_matrix_substitute_variables(pk_internal_t* pk,
pk_matrix_t* mat,
ap_dim_t* tdim,
numint_t** tvec,
size_t size)
{
size_t i,j,eindex;
matrix_t* nmat = matrix_alloc(mat->nbrows, mat->nbcolumns,false);
pk_matrix_t* nmat = pk_matrix_alloc(mat->nbrows, mat->nbcolumns,false);
numint_t den;

/* Computing common denominator */
Expand Down Expand Up @@ -394,7 +394,7 @@ matrix_t* matrix_substitute_variables(pk_internal_t* pk,
}
numint_clear(den);
for (i=0; i<mat->nbrows; i++){
matrix_normalize_row(pk,nmat,i);
pk_matrix_normalize_row(pk,nmat,i);
}

return nmat;
Expand Down Expand Up @@ -457,7 +457,7 @@ pk_t* poly_asssub_linexpr_array_det(bool assign,
ap_dim_t* tdim2;
numint_t** tvec;
size_t nbcols;
matrix_t* mat;
pk_matrix_t* mat;
pk_t* po;
pk_internal_t* pk = (pk_internal_t*)man->internal;

Expand Down Expand Up @@ -499,8 +499,8 @@ pk_t* poly_asssub_linexpr_array_det(bool assign,
/* Perform the operation */
mat =
assign ?
matrix_assign_variables(pk, pa->F, tdim2, tvec, size) :
matrix_substitute_variables(pk, pa->F, tdim2, tvec, size);
pk_matrix_assign_variables(pk, pa->F, tdim2, tvec, size) :
pk_matrix_substitute_variables(pk, pa->F, tdim2, tvec, size);
/* Free allocated stuff */
for (i=0; i<size; i++){
vector_free(tvec[i],nbcols);
Expand Down Expand Up @@ -792,15 +792,15 @@ pk_t* poly_asssub_linexpr_det(bool assign,
/* If side-effect, free everything but generators */
if (po->satC){ satmat_free(po->satC); po->satC = NULL; }
if (po->satF){ satmat_free(po->satF); po->satF = NULL; }
if (po->C){ matrix_free(po->C); po->C = NULL; }
if (po->C){ pk_matrix_free(po->C); po->C = NULL; }
}
}
if (pa->F){
/* Perform assignements on generators */
po->F =
assign ?
matrix_assign_variable(pk, destructive, pa->F, dim, pk->poly_numintp) :
matrix_substitute_variable(pk, destructive, pa->F, dim, pk->poly_numintp);
pk_matrix_assign_variable(pk, destructive, pa->F, dim, pk->poly_numintp) :
pk_matrix_substitute_variable(pk, destructive, pa->F, dim, pk->poly_numintp);
}
if (sgn && pa->C){ /* Expression is invertible and we have constraints */
/* Invert the expression in pk->poly_numintp2 */
Expand All @@ -811,8 +811,8 @@ pk_t* poly_asssub_linexpr_det(bool assign,
/* Perform susbtitution on constraints */
po->C =
assign ?
matrix_substitute_variable(pk,destructive,pa->C, dim, pk->poly_numintp2) :
matrix_assign_variable(pk,destructive,pa->C, dim, pk->poly_numintp2);
pk_matrix_substitute_variable(pk,destructive,pa->C, dim, pk->poly_numintp2) :
pk_matrix_assign_variable(pk,destructive,pa->C, dim, pk->poly_numintp2);
}
if (po->C && po->F){
po->nbeq = pa->nbeq;
Expand Down
Loading

0 comments on commit 7c43da1

Please sign in to comment.