diff --git a/configure b/configure index 9e0b590..043526d 100755 --- a/configure +++ b/configure @@ -429,6 +429,35 @@ else has_ppl=0 fi +get_pplite_version() +{ + echo_n "getting PPLite version: " + rm -f tmp.cc tmp + echo "#include " > tmp.cc + echo "#include " >> tmp.cc + echo "int main() {" >> tmp.cc + echo " std::cout << PPLITE_PACKAGE_VERSION << std::endl;" >> tmp.cc + echo "}" >> tmp.cc + r=1 + if test "x$pplite_prefix" != "x" + then + $cxx $cxxflags $deps -I$pplite_prefix/include -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 + else + $cxx $cxxflags $deps -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 + fi + if test $r -eq 0 -o ! -f tmp + then + r=0 + pplite_version="not found" + else + r=1 + pplite_version=`./tmp` + fi + echo $pplite_version + rm -f tmp.cc tmp + return $r +} + if test $has_cxx -eq 1 -a $has_pplite -eq 1 then # check for flint @@ -450,6 +479,17 @@ then if test $? -eq 0; then has_pplite=0; fi pplite_prefix="$prefix" fi + # check if pplite version is 0.11 + if test $has_pplite -eq 1 + then + get_pplite_version + if test "x$pplite_version" != "x0.11" + then + have_pplite_0_11_cxxflags= + else + have_pplite_0_11_cxxflags=-DHAVE_PPLITE_0_11 + fi + fi else has_pplite=0 fi @@ -610,7 +650,7 @@ detected configuration: optional C++ support $has_cxx optional Java support $has_java ($java_version) optional PPL support $has_ppl - optional PPLite support $has_pplite + optional PPLite support $has_pplite ($pplite_version) optional GLPK support $has_glpk optional debug libraries $has_debug @@ -685,8 +725,8 @@ CXXFLAGS = -U__STRICT_ANSI__ -DNDEBUG -O3 $cxxflags CXXFLAGS_DEBUG = -U__STRICT_ANSI__ -UNDEBUG -O0 -g $cxxflags # The PPLite wrapper requires using the C++11 language standard -PPLITE_CXXFLAGS = -std=c++11 -DNDEBUG -O3 $cxxflags -PPLITE_CXXFLAGS_DEBUG = -std=c++11 -UNDEBUG -O0 -g $cxxflags +PPLITE_CXXFLAGS = -std=c++11 -DNDEBUG -O3 $have_pplite_0_11_cxxflags $cxxflags +PPLITE_CXXFLAGS_DEBUG = -std=c++11 -UNDEBUG -O0 -g $have_pplite_0_11_cxxflags $cxxflags EXT_DLL = $ext_dll diff --git a/newpolka/pk.h b/newpolka/pk.h index 44e028b..8e9df77 100644 --- a/newpolka/pk.h +++ b/newpolka/pk.h @@ -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; diff --git a/newpolka/pk_approximate.c b/newpolka/pk_approximate.c index 228416b..8fe5ff4 100644 --- a/newpolka/pk_approximate.c +++ b/newpolka/pk_approximate.c @@ -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; @@ -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; } } @@ -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; @@ -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; } } @@ -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; @@ -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; } } @@ -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; iF); + pk_matrix_bound_dimension(pk,itv,i,po->F); if (!bound_infty(itv->inf)){ vector_set_dim_bound(pk, pa->C->p[nbrows], @@ -219,11 +219,11 @@ void poly_approximate_123(ap_manager_t* man, pk_t* po, int algorithm) for (i=0; ipoly_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; jpoly_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, @@ -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; @@ -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 */ @@ -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)){ @@ -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 */ @@ -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++; } @@ -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); @@ -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; diff --git a/newpolka/pk_assign.c b/newpolka/pk_assign.c index 09e77bd..d5ab720 100644 --- a/newpolka/pk_assign.c +++ b/newpolka/pk_assign.c @@ -37,20 +37,20 @@ /* 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; @@ -58,7 +58,7 @@ matrix_t* matrix_assign_variable(pk_internal_t* pk, nmat = destructive ? mat : - _matrix_alloc_int(mat->nbrows,mat->nbcolumns,false); + _pk_matrix_alloc_int(mat->nbrows,mat->nbcolumns,false); nmat->_sorted = false; @@ -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; } @@ -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; @@ -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 */ @@ -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 */ @@ -303,7 +303,7 @@ matrix_t* matrix_assign_variables(pk_internal_t* pk, } numint_clear(den); for (i=0; inbrows; i++){ - matrix_normalize_row(pk,nmat,i); + pk_matrix_normalize_row(pk,nmat,i); } return nmat; @@ -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 */ @@ -394,7 +394,7 @@ matrix_t* matrix_substitute_variables(pk_internal_t* pk, } numint_clear(den); for (i=0; inbrows; i++){ - matrix_normalize_row(pk,nmat,i); + pk_matrix_normalize_row(pk,nmat,i); } return nmat; @@ -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; @@ -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; isatC){ 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 */ @@ -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; diff --git a/newpolka/pk_cherni.c b/newpolka/pk_cherni.c index b90ab73..06974b3 100644 --- a/newpolka/pk_cherni.c +++ b/newpolka/pk_cherni.c @@ -27,7 +27,7 @@ bool cherni_checksatmat(pk_internal_t* pk, bool con_to_ray, - matrix_t* C, matrix_t* F, satmat_t* satC) + pk_matrix_t* C, pk_matrix_t* F, satmat_t* satC) { int s1,s2; size_t i; @@ -44,8 +44,8 @@ bool cherni_checksatmat(pk_internal_t* pk, if (s1<0 || (s1!=0 && s2==0) || (s1==0 && s2!=0)){ printf("cherni_checksatmat con_to_ray=%d: ray %lu, con %lu\n", con_to_ray,(unsigned long)i,(unsigned long)j.index); - printf("Constraints\n"); matrix_print(C); - printf("Frames\n"); matrix_print(F); + printf("Constraints\n"); pk_matrix_print(C); + printf("Frames\n"); pk_matrix_print(F); satmat_print(satC); return false; } @@ -58,19 +58,19 @@ bool cherni_checksatmat(pk_internal_t* pk, bool cherni_checksat(pk_internal_t* pk, bool con_to_ray, - matrix_t* C, size_t nbequations, - matrix_t* F, size_t nblines, + pk_matrix_t* C, size_t nbequations, + pk_matrix_t* F, size_t nblines, satmat_t* satC) { size_t i,k,nb,rank; bitindex_t j; - matrix_t* mat; + pk_matrix_t* mat; bool res = true; const size_t nbcols = C->nbcolumns; /* saturation des rayons */ - mat = matrix_alloc(C->nbrows,nbcols,false); + mat = pk_matrix_alloc(C->nbrows,nbcols,false); for (i=0; inbrows; i++){ nb = 0; for (j = bitindex_init(0); j.index < C->nbrows; bitindex_inc(&j)){ @@ -90,10 +90,10 @@ bool cherni_checksat(pk_internal_t* pk, res = false; } } - matrix_free(mat); + pk_matrix_free(mat); /* saturation des contraintes */ - mat = matrix_alloc(F->nbrows,nbcols,false); + mat = pk_matrix_alloc(F->nbrows,nbcols,false); for (j = bitindex_init(0); j.index < C->nbrows; bitindex_inc(&j)){ nb = 0; for (i=0; inbrows; i++){ @@ -112,11 +112,11 @@ bool cherni_checksat(pk_internal_t* pk, res = false; } } - matrix_free(mat); + pk_matrix_free(mat); if (res==false){ - printf("Constraints\n"); matrix_print(C); - printf("Frames\n"); matrix_print(F); + printf("Constraints\n"); pk_matrix_print(C); + printf("Frames\n"); pk_matrix_print(F); satmat_print(satC); } return res; @@ -126,13 +126,13 @@ bool cherni_checksat(pk_internal_t* pk, /* II. Conversion algorithm */ /* ********************************************************************** */ -void cherni_resize(matrix_t* mat, satmat_t* sat) +void cherni_resize(pk_matrix_t* mat, satmat_t* sat) { assert(mat->nbrows==sat->nbrows); size_t nbrows = mat->nbrows; size_t currentsize = mat->_maxrows >= sat->_maxrows ? mat->_maxrows : sat->_maxrows; size_t addsize = currentsize < 20 ? 10 : currentsize / 2; - matrix_resize_rows(mat, currentsize+addsize); + pk_matrix_resize_rows(mat, currentsize+addsize); satmat_resize_rows(sat, currentsize+addsize); mat->nbrows = sat->nbrows = nbrows; return; @@ -165,8 +165,8 @@ Throw exception. */ size_t cherni_conversion(pk_internal_t* pk, - matrix_t* con, size_t start, - matrix_t* ray, satmat_t* satc, size_t nbline) + pk_matrix_t* con, size_t start, + pk_matrix_t* ray, satmat_t* satc, size_t nbline) { size_t i,j,l,w; int is_inequality; @@ -217,11 +217,11 @@ size_t cherni_conversion(pk_internal_t* pk, /* remove it of lines and put it at index nbline */ nbline--; if (index_non_zero != nbline) - matrix_exch_rows(ray,index_non_zero,nbline); + pk_matrix_exch_rows(ray,index_non_zero,nbline); /* compute new lineality space */ for (i=index_non_zero; ip[i][0]) != 0){ - matrix_combine_rows(pk,ray,i,nbline,i,0); + pk_matrix_combine_rows(pk,ray,i,nbline,i,0); if (pk->exn) goto cherni_conversion_exit0; } @@ -233,7 +233,7 @@ size_t cherni_conversion(pk_internal_t* pk, /* compute the new pointed cone */ for (i=nbline+1; ip[i][0])){ - matrix_combine_rows(pk,ray,i,nbline,i,0); + pk_matrix_combine_rows(pk,ray,i,nbline,i,0); if (pk->exn) goto cherni_conversion_exit0; } @@ -245,7 +245,7 @@ size_t cherni_conversion(pk_internal_t* pk, } else { /* one remove the ray */ nbrows --; ray->nbrows --; satc->nbrows--; - matrix_exch_rows(ray, nbline, nbrows); + pk_matrix_exch_rows(ray, nbline, nbrows); satmat_exch_rows(satc, nbline, nbrows); } @@ -271,13 +271,13 @@ size_t cherni_conversion(pk_internal_t* pk, while (inf_bound>sup_bound) { int s = numint_sgn(ray->p[sup_bound][0]); if (s==0){ - matrix_exch_rows(ray, sup_bound, equal_bound); + pk_matrix_exch_rows(ray, sup_bound, equal_bound); satmat_exch_rows(satc, sup_bound, equal_bound); equal_bound++; sup_bound++; } else if (s<0) { inf_bound--; - matrix_exch_rows(ray, sup_bound, inf_bound); + pk_matrix_exch_rows(ray, sup_bound, inf_bound); satmat_exch_rows(satc, sup_bound, inf_bound); } else { sup_bound++; @@ -286,7 +286,7 @@ size_t cherni_conversion(pk_internal_t* pk, if (is_inequality && sup_bound == nbrows){ /* all rays satisfy the constraint:redundancy */ con->nbrows--; - matrix_exch_rows(con, k.index, con->nbrows); + pk_matrix_exch_rows(con, k.index, con->nbrows); } else { if (sup_bound==nbline){ /* no ray satisfies the constraint */ @@ -332,12 +332,12 @@ size_t cherni_conversion(pk_internal_t* pk, pk->exn = AP_EXC_OUT_OF_SPACE; goto cherni_conversion_exit0; } - if (nbrows>=matrix_get_maxrows(ray) || nbrows>=satc->_maxrows){ + if (nbrows>=pk_matrix_get_maxrows(ray) || nbrows>=satc->_maxrows){ /* resize output matrices */ cherni_resize(ray,satc); } /* Compute the new ray and put it at end */ - matrix_combine_rows(pk,ray,j,i,nbrows,0); + pk_matrix_combine_rows(pk,ray,j,i,nbrows,0); if (pk->exn) goto cherni_conversion_exit0; /* New row in saturation matrix */ for (w=0; w<=k.word; w++){ @@ -365,7 +365,7 @@ size_t cherni_conversion(pk_internal_t* pk, i = nbrows; while ((jbound)) { i--; - matrix_exch_rows(ray,i,j); + pk_matrix_exch_rows(ray,i,j); satmat_exch_rows(satc,i,j); j++; } @@ -411,7 +411,7 @@ of an equation, in this case the left-most non-zero one. */ size_t cherni_gauss(pk_internal_t* pk, - matrix_t* con, size_t nbeq) + pk_matrix_t* con, size_t nbeq) { size_t i,j,k; numint_t** p = con->p; @@ -425,7 +425,7 @@ size_t cherni_gauss(pk_internal_t* pk, } if (irank) { /* put it in rank */ - matrix_exch_rows(con,i,rank); + pk_matrix_exch_rows(con,i,rank); } if (s<0) { /* normalize with positive coefficient */ for (k=1; knbcolumns; k++) @@ -434,7 +434,7 @@ size_t cherni_gauss(pk_internal_t* pk, numint_set_int(p[rank][0],0); for (k=i+1; kcherni_intp[rank] = j; rank++; @@ -452,7 +452,7 @@ size_t cherni_gauss(pk_internal_t* pk, gauss. */ -void cherni_backsubstitute(pk_internal_t* pk, matrix_t* con, size_t rank) +void cherni_backsubstitute(pk_internal_t* pk, pk_matrix_t* con, size_t rank) { size_t i,j; int k; @@ -461,7 +461,7 @@ void cherni_backsubstitute(pk_internal_t* pk, matrix_t* con, size_t rank) j = pk->cherni_intp[k]; for (i=0; inbrows; i++) { if (i != (size_t)k && numint_sgn(con->p[i][j])) - matrix_combine_rows(pk,con,i,(size_t)k,i,j); + pk_matrix_combine_rows(pk,con,i,(size_t)k,i,j); } } } @@ -484,7 +484,7 @@ Throw exception. */ int cherni_simplify(pk_internal_t* pk, - matrix_t* con, matrix_t* ray, satmat_t* satf, size_t nbline) + pk_matrix_t* con, pk_matrix_t* ray, satmat_t* satf, size_t nbline) { size_t i,j; long int nb,nbj; @@ -522,7 +522,7 @@ int cherni_simplify(pk_internal_t* pk, if (is_equality){ /* we have an equality */ numint_set_int(con->p[i][0],0); - matrix_exch_rows(con, i,nbeq); + pk_matrix_exch_rows(con, i,nbeq); satmat_exch_rows(satf,i,nbeq); nbeq++; } @@ -548,7 +548,7 @@ int cherni_simplify(pk_internal_t* pk, j = rank; while( j < nbeq && i > nbeq ) { i--; - matrix_exch_rows(con, j,i); + pk_matrix_exch_rows(con, j,i); satmat_exch_rows(satf,j,i); j++; } @@ -561,7 +561,7 @@ int cherni_simplify(pk_internal_t* pk, int_set_numint(&nb, con->p[i][0]); if (nb < (long int)(nbcols-nbeq-2)){ /* redundant constraint */ nbcons--; - matrix_exch_rows(con, i,nbcons); + pk_matrix_exch_rows(con, i,nbcons); satmat_exch_rows(satf,i,nbcons); } else @@ -599,7 +599,7 @@ int cherni_simplify(pk_internal_t* pk, if (is_equality){ /* yes: we can remove j */ nbcons--; - matrix_exch_rows(con, j,nbcons); + pk_matrix_exch_rows(con, j,nbcons); satmat_exch_rows(satf,j,nbcons); } else @@ -610,7 +610,7 @@ int cherni_simplify(pk_internal_t* pk, } if (redundant){ nbcons--; - matrix_exch_rows(con, i,nbcons); + pk_matrix_exch_rows(con, i,nbcons); satmat_exch_rows(satf,i,nbcons); } else @@ -663,17 +663,17 @@ void cherni_minimize(pk_internal_t* pk, { size_t i; bool special; - matrix_t* C; - matrix_t* F; + pk_matrix_t* C; + pk_matrix_t* F; satmat_t* satC; C = po->C; - assert(matrix_is_sorted(C) && + assert(pk_matrix_is_sorted(C) && po->F==NULL && po->satC==NULL && po->satF==NULL); /* initialization of F and sat */ - F = matrix_alloc(CHERNI_FACTOR*uint_max(C->nbrows, C->nbcolumns-1), + F = pk_matrix_alloc(CHERNI_FACTOR*uint_max(C->nbrows, C->nbcolumns-1), C->nbcolumns,false); satC = satmat_alloc(F->nbrows, bitindex_size(C->nbrows)); F->nbrows = satC->nbrows = C->nbcolumns-1; @@ -686,7 +686,7 @@ void cherni_minimize(pk_internal_t* pk, if (pk->exn){ /* out of space, overflow */ - matrix_free(F); + pk_matrix_free(F); satmat_free(satC); po->nbeq = po->nbline = 0; } @@ -708,8 +708,8 @@ void cherni_minimize(pk_internal_t* pk, } if (special){ /* this means we have an empty polyhedron */ - matrix_free(C); - matrix_free(F); + pk_matrix_free(C); + pk_matrix_free(F); satmat_free(satC); po->C = 0; po->nbeq = po->nbline = 0; @@ -721,7 +721,7 @@ void cherni_minimize(pk_internal_t* pk, satmat_free(satC); po->nbeq = cherni_simplify(pk,C,F,po->satF,po->nbline); if (F->_maxrows > 3*F->nbrows/2){ - matrix_resize_rows(F,F->nbrows); + pk_matrix_resize_rows(F,F->nbrows); satmat_resize_cols(po->satF,bitindex_size(F->nbrows)); } } @@ -743,8 +743,8 @@ void cherni_add_and_minimize(pk_internal_t* pk, { size_t i; bool special; - matrix_t* C; - matrix_t* F; + pk_matrix_t* C; + pk_matrix_t* F; satmat_t* satC; size_t nbrows,nbcols; @@ -772,7 +772,7 @@ void cherni_add_and_minimize(pk_internal_t* pk, C,start,F,satC,po->nbline); if (pk->exn){ /* out of space, overflow */ - matrix_free(F); + pk_matrix_free(F); satmat_free(satC); po->F = 0; po->satC = po->satF = 0; @@ -794,8 +794,8 @@ void cherni_add_and_minimize(pk_internal_t* pk, } } if (special){ /* this means we have an empty polyhedron */ - matrix_free(C); - matrix_free(F); + pk_matrix_free(C); + pk_matrix_free(F); satmat_free(satC); po->C = po->F = 0; po->satC = 0; @@ -808,7 +808,7 @@ void cherni_add_and_minimize(pk_internal_t* pk, po->satC = NULL; po->nbeq = cherni_simplify(pk,C,F,po->satF,po->nbline); if (F->_maxrows > 3*F->nbrows/2){ - matrix_resize_rows(F,F->nbrows); + pk_matrix_resize_rows(F,F->nbrows); satmat_resize_cols(po->satF,bitindex_size(F->nbrows)); } } @@ -823,7 +823,7 @@ void cherni_add_and_minimize(pk_internal_t* pk, void cherni_buildsatline(pk_internal_t* pk, - matrix_t* con, numint_t* tab, + pk_matrix_t* con, numint_t* tab, bitstring_t* satline) { bitindex_t jx = bitindex_init(0); @@ -849,8 +849,8 @@ void cherni_buildsatline(pk_internal_t* pk, bool cherni_minimizeeps(pk_internal_t* pk, pk_t* po) { bool is_minimaleps,change,removed; - matrix_t* C; - matrix_t* F; + pk_matrix_t* C; + pk_matrix_t* F; satmat_t* satF; size_t i,j,w,Fnbrows,satFnbcols; bitindex_t k; @@ -935,7 +935,7 @@ bool cherni_minimizeeps(pk_internal_t* pk, pk_t* po) is_minimaleps = false; /* one remove the constraint */ C->nbrows--; satF->nbrows--; - matrix_exch_rows(C, i, C->nbrows); + pk_matrix_exch_rows(C, i, C->nbrows); satmat_exch_rows(satF, i, C->nbrows); } else { @@ -952,7 +952,7 @@ bool cherni_minimizeeps(pk_internal_t* pk, pk_t* po) else { po->status &= pk_status_conseps | pk_status_consgauss; po->status |= pk_status_minimaleps; - matrix_free(po->F); po->F = NULL; + pk_matrix_free(po->F); po->F = NULL; satmat_free(po->satF); po->satF = NULL; if (po->satC){ satmat_free(po->satC); po->satC = NULL; } /* Re-add positivity constraint (note: we are sure there is one free row */ @@ -965,9 +965,9 @@ bool cherni_minimizeeps(pk_internal_t* pk, pk_t* po) change = true; } if (!(po->status & pk_status_conseps)){ - bool change2 = matrix_normalize_constraint(pk,po->C,po->intdim,po->realdim); + bool change2 = pk_matrix_normalize_constraint(pk,po->C,po->intdim,po->realdim); if (change2){ - 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; } } diff --git a/newpolka/pk_cherni.h b/newpolka/pk_cherni.h index c74afd4..7dae191 100644 --- a/newpolka/pk_cherni.h +++ b/newpolka/pk_cherni.h @@ -31,15 +31,15 @@ extern "C" { /* ********************************************************************** */ bool cherni_checksatmat(pk_internal_t* pk, bool con_to_ray, - matrix_t* C, matrix_t* F, + pk_matrix_t* C, pk_matrix_t* F, satmat_t* satC); /* Recompute the saturation matrix of C and F and checks the equality with satC. */ bool cherni_checksat(pk_internal_t* pk, bool con_to_ray, - matrix_t* C, size_t nbequations, - matrix_t* F, size_t nblines, + pk_matrix_t* C, size_t nbequations, + pk_matrix_t* F, size_t nblines, satmat_t* satC); /* Check the saturation numbers of constraints and rays. */ @@ -48,8 +48,8 @@ bool cherni_checksat(pk_internal_t* pk, /* ********************************************************************** */ size_t cherni_conversion(pk_internal_t* pk, - matrix_t* con, size_t start, - matrix_t* ray, satmat_t* satc, size_t nbline); + pk_matrix_t* con, size_t start, + pk_matrix_t* ray, satmat_t* satc, size_t nbline); /* Compute the dual form of con. @@ -70,7 +70,7 @@ size_t cherni_conversion(pk_internal_t* pk, The result is given by ray, sat and the returned number of lines. */ -size_t cherni_gauss(pk_internal_t* pk, matrix_t* con, size_t nbeq); +size_t cherni_gauss(pk_internal_t* pk, pk_matrix_t* con, size_t nbeq); /* The function finds a minimal system for equalities, and returns the rank *r* of this system, equations of which are numbered from 0 to *r-1*. Redundant @@ -79,7 +79,7 @@ size_t cherni_gauss(pk_internal_t* pk, matrix_t* con, size_t nbeq); coefficent of an equation, in this case the left-most non-zero one. */ -void cherni_backsubstitute(pk_internal_t* pk, matrix_t* con, size_t rank); +void cherni_backsubstitute(pk_internal_t* pk, pk_matrix_t* con, size_t rank); /* This function backsubstitute the coefficients according to the system of equations and the array pk->cherni_intp properly set by @@ -87,7 +87,7 @@ void cherni_backsubstitute(pk_internal_t* pk, matrix_t* con, size_t rank); */ int cherni_simplify(pk_internal_t* pk, - matrix_t* con, matrix_t* ray, + pk_matrix_t* con, pk_matrix_t* ray, satmat_t* satf, const size_t nbline); /* We suppose that we just obtained ray and satc from con @@ -109,7 +109,7 @@ void cherni_add_and_minimize(pk_internal_t* pk, size_t start); /* Misc */ void cherni_buildsatline(pk_internal_t* pk, - matrix_t* con, numint_t* tab, + pk_matrix_t* con, numint_t* tab, bitstring_t* satline); /* Library is supposed to be in strict mode (pk->strict==true), polyhedron is diff --git a/newpolka/pk_closure.c b/newpolka/pk_closure.c index d97fc98..720c441 100644 --- a/newpolka/pk_closure.c +++ b/newpolka/pk_closure.c @@ -20,7 +20,7 @@ pk_t* pk_closure(ap_manager_t* man, bool destructive, pk_t* pa) { - matrix_t* C; + pk_matrix_t* C; bool change,positivity; size_t i; pk_t* po; @@ -45,7 +45,7 @@ pk_t* pk_closure(ap_manager_t* man, bool destructive, pk_t* pa) return po; } if (!destructive){ - po->C = matrix_copy(pa->C); + po->C = pk_matrix_copy(pa->C); } C = po->C; @@ -71,7 +71,7 @@ pk_t* pk_closure(ap_manager_t* man, bool destructive, pk_t* pa) size_t nbrows; /* we should add it */ nbrows = C->nbrows; - matrix_resize_rows_lazy(C,C->nbrows+1); + pk_matrix_resize_rows_lazy(C,C->nbrows+1); q = C->p[nbrows]; numint_set_int(q[0],1); numint_set_int(q[polka_cst],1); @@ -80,7 +80,7 @@ pk_t* pk_closure(ap_manager_t* man, bool destructive, pk_t* pa) } C->_sorted = false; if (destructive){ - 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; diff --git a/newpolka/pk_constructor.c b/newpolka/pk_constructor.c index e0a64ce..36f4fa7 100644 --- a/newpolka/pk_constructor.c +++ b/newpolka/pk_constructor.c @@ -32,8 +32,8 @@ void poly_set_bottom(pk_internal_t* pk, pk_t* po) { - if (po->C) matrix_free(po->C); - if (po->F) matrix_free(po->F); + if (po->C) pk_matrix_free(po->C); + if (po->F) pk_matrix_free(po->F); if (po->satC) satmat_free(po->satC); if (po->satF) satmat_free(po->satF); po->C = po->F = NULL; @@ -61,7 +61,7 @@ pk_t* pk_bottom(ap_manager_t* man, size_t intdim, size_t realdim) /* Universe polyhedron */ /* ====================================================================== */ -void matrix_fill_constraint_top(pk_internal_t* pk, matrix_t* C, size_t start) +void pk_matrix_fill_constraint_top(pk_internal_t* pk, pk_matrix_t* C, size_t start) { if (pk->strict){ /* constraints epsilon and xi-epsilon*/ @@ -86,8 +86,8 @@ void poly_set_top(pk_internal_t* pk, pk_t* po) size_t i; size_t dim; - if (po->C) matrix_free(po->C); - if (po->F) matrix_free(po->F); + if (po->C) pk_matrix_free(po->C); + if (po->F) pk_matrix_free(po->F); if (po->satC) satmat_free(po->satC); if (po->satF) satmat_free(po->satF); @@ -100,8 +100,8 @@ void poly_set_top(pk_internal_t* pk, pk_t* po) dim = po->intdim + po->realdim; - po->C = matrix_alloc(pk->dec-1, pk->dec+dim,true); - po->F = matrix_alloc(pk->dec+dim-1,pk->dec+dim,true); + po->C = pk_matrix_alloc(pk->dec-1, pk->dec+dim,true); + po->F = pk_matrix_alloc(pk->dec+dim-1,pk->dec+dim,true); /* We have to ensure that the matrices are really sorted */ po->satC = satmat_alloc(pk->dec+dim-1,bitindex_size(pk->dec-1)); po->satF = 0; @@ -109,7 +109,7 @@ void poly_set_top(pk_internal_t* pk, pk_t* po) po->nbline = dim; /* constraints */ - matrix_fill_constraint_top(pk,po->C,0); + pk_matrix_fill_constraint_top(pk,po->C,0); /* generators */ /* lines $x_i$ */ @@ -156,8 +156,8 @@ pk_t* pk_top(ap_manager_t* man, size_t intdim, size_t realdim) /* The matrix is supposed to be big enough */ static -int matrix_fill_constraint_box(pk_internal_t* pk, - matrix_t* C, size_t start, +int pk_matrix_fill_constraint_box(pk_internal_t* pk, + pk_matrix_t* C, size_t start, ap_interval_t** box, size_t intdim, size_t realdim, bool integer) @@ -224,13 +224,13 @@ pk_t* pk_of_box(ap_manager_t* man, po->status = pk_status_conseps; dim = intdim + realdim; - po->C = matrix_alloc(pk->dec-1 + 2*dim, pk->dec + dim, false); + po->C = pk_matrix_alloc(pk->dec-1 + 2*dim, pk->dec + dim, false); /* constraints */ - matrix_fill_constraint_top(pk,po->C,0); - k = matrix_fill_constraint_box(pk,po->C,pk->dec-1,array,intdim,realdim,true); + pk_matrix_fill_constraint_top(pk,po->C,0); + k = pk_matrix_fill_constraint_box(pk,po->C,pk->dec-1,array,intdim,realdim,true); if (k==-1){ - matrix_free(po->C); + pk_matrix_free(po->C); po->C = NULL; return po; } diff --git a/newpolka/pk_constructor.h b/newpolka/pk_constructor.h index 0824f7f..85cbbb0 100644 --- a/newpolka/pk_constructor.h +++ b/newpolka/pk_constructor.h @@ -23,7 +23,7 @@ extern "C" { /* Fill the first (pk->dec-1) rows of the matrix with the constraints of the universe polyhedron */ -void matrix_fill_constraint_top(pk_internal_t* pk, matrix_t* C, size_t start); +void pk_matrix_fill_constraint_top(pk_internal_t* pk, pk_matrix_t* C, size_t start); /* Assign with GMP semantics the given polyhedron with the empty (resp. universe) polyhedron, of same dimensions */ diff --git a/newpolka/pk_expandfold.c b/newpolka/pk_expandfold.c index 1be0bfb..5fd3e74 100644 --- a/newpolka/pk_expandfold.c +++ b/newpolka/pk_expandfold.c @@ -33,9 +33,9 @@ dimensions, with dimsup new dimensions inserted just before offset. */ static -matrix_t* matrix_expand(pk_internal_t* pk, +pk_matrix_t* pk_matrix_expand(pk_internal_t* pk, bool destructive, - matrix_t* C, + pk_matrix_t* C, ap_dim_t dim, size_t offset, size_t dimsup) @@ -44,10 +44,10 @@ matrix_t* matrix_expand(pk_internal_t* pk, size_t i,j,row,col,nb; size_t nbrows, nbcols; numint_t** p; - matrix_t* nC; + pk_matrix_t* nC; if (dimsup==0){ - return destructive ? C : matrix_copy(C); + return destructive ? C : pk_matrix_copy(C); } nbrows = C->nbrows; nbcols = C->nbcolumns; @@ -64,9 +64,9 @@ matrix_t* matrix_expand(pk_internal_t* pk, for (i=0;idim[i]=offset; } - nC = matrix_add_dimensions(pk,destructive,C,dimchange); + nC = pk_matrix_add_dimensions(pk,destructive,C,dimchange); ap_dimchange_free(dimchange); - matrix_resize_rows(nC,nbrows+nb*dimsup); + pk_matrix_resize_rows(nC,nbrows+nb*dimsup); if (nb==0) return nC; @@ -153,13 +153,13 @@ pk_t* pk_expand(ap_manager_t* man, } /* Prepare resulting matrix */ if (destructive){ - if (po->F){ matrix_free(po->F); po->F = NULL; } + if (po->F){ pk_matrix_free(po->F); po->F = NULL; } if (po->satF){ satmat_free(po->satF); po->satF = NULL; } if (po->satC){ satmat_free(po->satC); po->satC = NULL; } po->nbeq = po->nbline = 0; po->status &= ~pk_status_consgauss & ~pk_status_gengauss & ~pk_status_minimaleps; } - po->C = matrix_expand(pk, destructive, pa->C, + po->C = pk_matrix_expand(pk, destructive, pa->C, dim, (dim + dimsup < po->intdim ? po->intdim-dimsup : @@ -194,25 +194,25 @@ pk_t* pk_expand(ap_manager_t* man, /* the array tdim is assumed to be sorted */ static -matrix_t* matrix_fold(pk_internal_t* pk, +pk_matrix_t* pk_matrix_fold(pk_internal_t* pk, bool destructive, - matrix_t* F, + pk_matrix_t* F, ap_dim_t* tdim, size_t size) { - matrix_t* nF; + pk_matrix_t* nF; size_t i,j,row,col; size_t nbrows, nbcols, dimsup; ap_dimchange_t* dimchange; dimsup = size-1; if (dimsup==0){ - return destructive ? F : matrix_copy(F); + return destructive ? F : pk_matrix_copy(F); } nbrows = F->nbrows; nbcols = F->nbcolumns; col = pk->dec + tdim[0]; - nF = matrix_alloc( size*nbrows, + nF = pk_matrix_alloc( size*nbrows, nbcols - dimsup, false ); dimchange = ap_dimchange_alloc(0,dimsup); @@ -240,7 +240,7 @@ matrix_t* matrix_fold(pk_internal_t* pk, nF->nbrows = row; nF->_sorted = false; if (destructive){ - matrix_free(F); + pk_matrix_free(F); } ap_dimchange_free(dimchange); return nF; @@ -294,14 +294,14 @@ pk_t* pk_fold(ap_manager_t* man, /* Prepare resulting matrix */ if (destructive){ - if (po->C){ matrix_free(po->C); po->C = NULL; } + if (po->C){ pk_matrix_free(po->C); po->C = NULL; } if (po->satF){ satmat_free(po->satF); po->satF = NULL; } if (po->satC){ satmat_free(po->satC); po->satC = NULL; } po->nbeq = po->nbline = 0; po->status &= ~pk_status_consgauss & ~pk_status_gengauss & ~pk_status_minimaleps; } - po->F = matrix_fold(pk, destructive, pa->F, + po->F = pk_matrix_fold(pk, destructive, pa->F, tdim, size); /* Minimize the result */ if (pk->funopt->algorithm>0){ diff --git a/newpolka/pk_extract.c b/newpolka/pk_extract.c index 2ff00fe..c8e4245 100644 --- a/newpolka/pk_extract.c +++ b/newpolka/pk_extract.c @@ -21,10 +21,10 @@ /* Bounding the value of a dimension in a matrix of generators. */ -void matrix_bound_dimension(pk_internal_t* pk, +void pk_matrix_bound_dimension(pk_internal_t* pk, itv_t itv, ap_dim_t dim, - matrix_t* F) + pk_matrix_t* F) { size_t i, index; int sgn; @@ -74,8 +74,8 @@ void matrix_bound_dimension(pk_internal_t* pk, } } -itv_t* matrix_to_box(pk_internal_t* pk, - matrix_t* F) +itv_t* pk_matrix_to_box(pk_internal_t* pk, + pk_matrix_t* F) { size_t i,dim; itv_t* res; @@ -85,7 +85,7 @@ itv_t* matrix_to_box(pk_internal_t* pk, dim = F->nbcolumns - pk->dec; res = itv_array_alloc(dim); for (i=0;inbcolumns. */ -void matrix_bound_vector(pk_internal_t* pk, +void pk_matrix_bound_vector(pk_internal_t* pk, itv_t itv, numint_t* vec, - matrix_t* F) + pk_matrix_t* F) { size_t i; int sgn; @@ -201,10 +201,10 @@ void vector_bound_itv_linexpr(pk_internal_t* pk, matrix of generators. */ static -void matrix_bound_itv_linexpr(pk_internal_t* pk, +void pk_matrix_bound_itv_linexpr(pk_internal_t* pk, itv_t itv, itv_linexpr_t* linexpr, - matrix_t* F) + pk_matrix_t* F) { size_t i; int sgn; @@ -287,7 +287,7 @@ ap_interval_t* pk_bound_dimension(ap_manager_t* man, } itv_init(itv); - matrix_bound_dimension(pk,itv,dim,po->F); + pk_matrix_bound_dimension(pk,itv,dim,po->F); ap_interval_set_itv(pk->itv,interval, itv); itv_clear(itv); man->result.flag_exact = man->result.flag_best = @@ -334,7 +334,7 @@ ap_interval_t* pk_bound_linexpr(ap_manager_t* man, &pk->poly_itv_linexpr, expr); itv_init(itv); - matrix_bound_itv_linexpr(pk,itv,&pk->poly_itv_linexpr,po->F); + pk_matrix_bound_itv_linexpr(pk,itv,&pk->poly_itv_linexpr,po->F); ap_interval_set_itv(pk->itv,interval,itv); itv_clear(itv); @@ -373,11 +373,11 @@ ap_interval_t* pk_bound_texpr(ap_manager_t* man, man->result.flag_exact = man->result.flag_best = true; return interval; } - env = matrix_to_box(pk,po->F); + env = pk_matrix_to_box(pk,po->F); itv_intlinearize_ap_texpr0(pk->itv,&pk->poly_itv_linexpr, expr,env,po->intdim); itv_init(itv1); itv_init(itv2); - matrix_bound_itv_linexpr(pk,itv1,&pk->poly_itv_linexpr,po->F); + pk_matrix_bound_itv_linexpr(pk,itv1,&pk->poly_itv_linexpr,po->F); itv_eval_ap_texpr0(pk->itv,itv2,expr,env); itv_meet(pk->itv,itv1,itv1,itv2); ap_interval_set_itv(pk->itv,interval,itv1); @@ -397,7 +397,7 @@ ap_lincons0_array_t pk_to_lincons_array(ap_manager_t* man, pk_t* po) { ap_lincons0_array_t array; - matrix_t* C; + pk_matrix_t* C; size_t i,k; pk_internal_t* pk = pk_init_from_manager(man,AP_FUNID_TO_LINCONS_ARRAY); @@ -469,7 +469,7 @@ ap_interval_t** pk_to_box(ap_manager_t* man, } } else { - titv = matrix_to_box(pk,po->F); + titv = pk_matrix_to_box(pk,po->F); for (i=0; iitv,interval[i],titv[i]); } @@ -490,7 +490,7 @@ ap_generator0_array_t pk_to_generator_array(ap_manager_t* man, pk_t* po) { ap_generator0_array_t array; - matrix_t* F; + pk_matrix_t* F; size_t i,k; pk_internal_t* pk = pk_init_from_manager(man,AP_FUNID_TO_GENERATOR_ARRAY); diff --git a/newpolka/pk_extract.h b/newpolka/pk_extract.h index a89aa41..4a4ab98 100644 --- a/newpolka/pk_extract.h +++ b/newpolka/pk_extract.h @@ -19,24 +19,24 @@ extern "C" { #endif /* Bounding by a itv box a matrix of generators. */ -itv_t* matrix_to_box(pk_internal_t* pk, matrix_t* F); +itv_t* pk_matrix_to_box(pk_internal_t* pk, pk_matrix_t* F); /* Bounding the value of a dimension in a matrix of generators. mode == 1: sup bound mode == -1: inf bound */ -void matrix_bound_dimension(pk_internal_t* pk, +void pk_matrix_bound_dimension(pk_internal_t* pk, itv_t itv, ap_dim_t dim, - matrix_t* F); + pk_matrix_t* F); /* Bounding the value of a linear expression (vector) in a matrix of generators. vec is supposed to be of size F->nbcolumns. */ -void matrix_bound_vector(pk_internal_t* pk, +void pk_matrix_bound_vector(pk_internal_t* pk, itv_t itv, numint_t* vec, - matrix_t* F); + pk_matrix_t* F); #ifdef __cplusplus } diff --git a/newpolka/pk_internal.c b/newpolka/pk_internal.c index b1e4cec..843215f 100644 --- a/newpolka/pk_internal.c +++ b/newpolka/pk_internal.c @@ -56,7 +56,7 @@ void pk_internal_init(pk_internal_t* pk, size_t maxdims) pk->poly_dimp2 = malloc(pk->maxdims*sizeof(ap_dim_t)); pk->poly_fold_dimp = malloc(pk->maxdims*sizeof(ap_dim_t)); /* pk->poly_bitstringp = bitstring_alloc(bitindex_size(pk->maxrows)); */ - pk->poly_matspecial = matrix_alloc(1,pk->maxcols,true); + pk->poly_matspecial = pk_matrix_alloc(1,pk->maxcols,true); numint_init(pk->poly_prod); } @@ -130,7 +130,7 @@ void pk_internal_clear(pk_internal_t* pk) /* if (pk->poly_bitstringp) bitstring_free(pk->poly_bitstringp); pk->poly_bitstringp = 0; */ - if (pk->poly_matspecial) matrix_free(pk->poly_matspecial); + if (pk->poly_matspecial) pk_matrix_free(pk->poly_matspecial); pk->poly_matspecial = 0; numint_clear(pk->poly_prod); diff --git a/newpolka/pk_internal.h b/newpolka/pk_internal.h index 554c256..119f004 100644 --- a/newpolka/pk_internal.h +++ b/newpolka/pk_internal.h @@ -68,7 +68,7 @@ struct pk_internal_t { ap_dim_t* poly_dimp; /* of size maxdims */ ap_dim_t* poly_dimp2; /* of size maxdims */ ap_dim_t* poly_fold_dimp; /* of size maxdims */ - struct matrix_t* poly_matspecial; + struct pk_matrix_t* poly_matspecial; numint_t poly_prod; }; diff --git a/newpolka/pk_matrix.c b/newpolka/pk_matrix.c index a3e6d8a..9a371b8 100644 --- a/newpolka/pk_matrix.c +++ b/newpolka/pk_matrix.c @@ -21,13 +21,13 @@ /* Internal allocation function: the elements are not initialized. mr is the maximum number of rows, and nc the number of columns. By default, nbrows is initialized to mr . */ -matrix_t* _matrix_alloc_int(size_t nbrows, size_t nbcols, bool s) +pk_matrix_t* _pk_matrix_alloc_int(size_t nbrows, size_t nbcols, bool s) { size_t i; assert(nbcols>0 || nbrows==0); - matrix_t* mat = (matrix_t*)malloc(sizeof(matrix_t)); + pk_matrix_t* mat = (pk_matrix_t*)malloc(sizeof(pk_matrix_t)); mat->nbrows = mat->_maxrows = nbrows; mat->nbcolumns = nbcols; mat->_sorted = s; @@ -39,13 +39,13 @@ matrix_t* _matrix_alloc_int(size_t nbrows, size_t nbcols, bool s) } /* Standard allocation function, with initialization of the elements. */ -matrix_t* matrix_alloc(size_t nbrows, size_t nbcols, bool s) +pk_matrix_t* pk_matrix_alloc(size_t nbrows, size_t nbcols, bool s) { size_t i; assert(nbcols>0 || nbrows==0); - matrix_t* mat = (matrix_t*)malloc(sizeof(matrix_t)); + pk_matrix_t* mat = (pk_matrix_t*)malloc(sizeof(pk_matrix_t)); mat->nbrows = mat->_maxrows = nbrows; mat->nbcolumns = nbcols; mat->_sorted = s; @@ -57,7 +57,7 @@ matrix_t* matrix_alloc(size_t nbrows, size_t nbcols, bool s) } /* Reallocation function, to scale up or to downsize a matrix */ -void matrix_resize_rows(matrix_t* mat, size_t nbrows) +void pk_matrix_resize_rows(pk_matrix_t* mat, size_t nbrows) { size_t i; @@ -81,10 +81,10 @@ void matrix_resize_rows(matrix_t* mat, size_t nbrows) } /* Ensures a minimum size */ -void matrix_resize_rows_lazy(matrix_t* mat, size_t nbrows) +void pk_matrix_resize_rows_lazy(pk_matrix_t* mat, size_t nbrows) { if (nbrows>mat->_maxrows) - matrix_resize_rows(mat,nbrows); + pk_matrix_resize_rows(mat,nbrows); else { mat->_sorted = mat->_sorted && nbrowsnbrows; mat->nbrows = nbrows; @@ -92,13 +92,13 @@ void matrix_resize_rows_lazy(matrix_t* mat, size_t nbrows) } /* Minimization */ -void matrix_minimize(matrix_t* mat) +void pk_matrix_minimize(pk_matrix_t* mat) { - matrix_resize_rows(mat,mat->nbrows); + pk_matrix_resize_rows(mat,mat->nbrows); } /* Deallocation function. */ -void matrix_free(matrix_t* mat) +void pk_matrix_free(pk_matrix_t* mat) { size_t i; @@ -110,7 +110,7 @@ void matrix_free(matrix_t* mat) } /* Set all elements to zero. */ -void matrix_clear(matrix_t* mat) +void pk_matrix_clear(pk_matrix_t* mat) { size_t i,j; for (i=0; inbrows; i++){ @@ -122,10 +122,10 @@ void matrix_clear(matrix_t* mat) /* Create a copy of the matrix of size nbrows (and not _maxrows). Only ``used'' rows are copied. */ -matrix_t* matrix_copy(matrix_t* mat) +pk_matrix_t* pk_matrix_copy(pk_matrix_t* mat) { size_t i,j; - matrix_t* nmat = _matrix_alloc_int(mat->nbrows,mat->nbcolumns,mat->_sorted); + pk_matrix_t* nmat = _pk_matrix_alloc_int(mat->nbrows,mat->nbcolumns,mat->_sorted); for (i=0;inbrows;i++){ for (j=0; jnbcolumns; j++){ numint_init_set(nmat->p[i][j],mat->p[i][j]); @@ -135,7 +135,7 @@ matrix_t* matrix_copy(matrix_t* mat) } /* Return true iff the matrices are equal, coeff by coeff */ -bool matrix_equal(matrix_t* mata, matrix_t* matb) +bool pk_matrix_equal(pk_matrix_t* mata, pk_matrix_t* matb) { int i; size_t j; @@ -153,7 +153,7 @@ bool matrix_equal(matrix_t* mata, matrix_t* matb) } /* Raw printing function. */ -void matrix_fprint(FILE* stream, matrix_t* mat) +void pk_matrix_fprint(FILE* stream, pk_matrix_t* mat) { size_t i,j; fprintf(stream,"%lu %lu\n", @@ -166,9 +166,9 @@ void matrix_fprint(FILE* stream, matrix_t* mat) fprintf(stream,"\n"); } } -void matrix_print(matrix_t* mat) +void pk_matrix_print(pk_matrix_t* mat) { - matrix_fprint(stdout,mat); + pk_matrix_fprint(stdout,mat); } @@ -182,34 +182,34 @@ void matrix_print(matrix_t* mat) l1 and l2 and puts the result in l3 such that l3[k] is zero. */ -int matrix_compare_rows(pk_internal_t* pk, - matrix_t* mat, size_t l1, size_t l2) +int pk_matrix_compare_rows(pk_internal_t* pk, + pk_matrix_t* mat, size_t l1, size_t l2) { return vector_compare(pk, mat->p[l1], mat->p[l2],mat->nbcolumns); } -void matrix_normalize_row(pk_internal_t* pk, - matrix_t* mat, size_t l) +void pk_matrix_normalize_row(pk_internal_t* pk, + pk_matrix_t* mat, size_t l) { vector_normalize(pk, mat->p[l],mat->nbcolumns); } -void matrix_combine_rows(pk_internal_t* pk, - matrix_t* mat, size_t l1, size_t l2, size_t l3, size_t k) +void pk_matrix_combine_rows(pk_internal_t* pk, + pk_matrix_t* mat, size_t l1, size_t l2, size_t l3, size_t k) { vector_combine(pk, mat->p[l1], mat->p[l2], mat->p[l3],k,mat->nbcolumns); } -void matrix_exch_rows(matrix_t* mat, size_t l1, size_t l2) +void pk_matrix_exch_rows(pk_matrix_t* mat, size_t l1, size_t l2) { numint_t* aux=mat->p[l1]; mat->p[l1]=mat->p[l2]; mat->p[l2]=aux; } -void matrix_move_rows(matrix_t* mat, size_t destrow, size_t orgrow, size_t size) +void pk_matrix_move_rows(pk_matrix_t* mat, size_t destrow, size_t orgrow, size_t size) { int offset; int i; @@ -218,12 +218,12 @@ void matrix_move_rows(matrix_t* mat, size_t destrow, size_t orgrow, size_t size) if (offset>0){ assert(destrow+size<=mat->_maxrows); for (i=(int)(destrow+size)-1; i>=(int)destrow; i--){ - matrix_exch_rows(mat,(size_t)i,(size_t)(i-offset)); + pk_matrix_exch_rows(mat,(size_t)i,(size_t)(i-offset)); } } else { assert(orgrow+size<=mat->_maxrows); for(i=(int)destrow; i<(int)(destrow+size); i++){ - matrix_exch_rows(mat,(size_t)i,(size_t)(i-offset)); + pk_matrix_exch_rows(mat,(size_t)i,(size_t)(i-offset)); } } } @@ -232,8 +232,8 @@ void matrix_move_rows(matrix_t* mat, size_t destrow, size_t orgrow, size_t size) /* */ /* ********************************************************************** */ -bool matrix_normalize_constraint(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_normalize_constraint(pk_internal_t* pk, + pk_matrix_t* mat, size_t intdim, size_t realdim) { bool change1, change2; @@ -249,7 +249,7 @@ bool matrix_normalize_constraint(pk_internal_t* pk, mat->_sorted = false; /* Add again \xi-\epsilon<=1 */ size_t nbrows= mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+1); + pk_matrix_resize_rows_lazy(mat,nbrows+1); vector_clear(mat->p[nbrows],mat->nbcolumns); numint_set_int(mat->p[nbrows][0],1); numint_set_int(mat->p[nbrows][polka_cst],1); @@ -260,8 +260,8 @@ bool matrix_normalize_constraint(pk_internal_t* pk, else return false; } -bool matrix_normalize_constraint_int(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_normalize_constraint_int(pk_internal_t* pk, + pk_matrix_t* mat, size_t intdim, size_t realdim) { bool change1, change2; @@ -306,8 +306,8 @@ static int qsort_rows_compar(void* qsort_man, void* pq1, void* pq2) MAKE_SORT(qsort_rows, numint_t*, qsort_rows_compar) -void matrix_sort_rows(pk_internal_t* pk, - matrix_t* mat) +void pk_matrix_sort_rows(pk_internal_t* pk, + pk_matrix_t* mat) { qsort_man_t qsort_man; @@ -340,8 +340,8 @@ static int qsort_rows_with_sat_compar(void* qsort_man, void* q1, void* q2) MAKE_SORT(qsort_rows_with_sat, qsort_t, qsort_rows_with_sat_compar) -void matrix_sort_rows_with_sat(pk_internal_t* pk, - matrix_t* mat, satmat_t* sat) +void pk_matrix_sort_rows_with_sat(pk_internal_t* pk, + pk_matrix_t* mat, satmat_t* sat) { size_t i; qsort_t* qsort_tab; @@ -370,13 +370,13 @@ void matrix_sort_rows_with_sat(pk_internal_t* pk, /* ====================================================================== */ /* Appending matrices */ -matrix_t* matrix_append(matrix_t* mata, matrix_t* matb) +pk_matrix_t* pk_matrix_append(pk_matrix_t* mata, pk_matrix_t* matb) { - matrix_t* mat; + pk_matrix_t* mat; size_t i,l; assert (mata->nbcolumns == matb->nbcolumns); - mat = _matrix_alloc_int(mata->nbrows+matb->nbrows,mata->nbcolumns,false); + mat = _pk_matrix_alloc_int(mata->nbrows+matb->nbrows,mata->nbcolumns,false); for (i=0;inbrows; i++){ for (l=0; lnbcolumns; l++) numint_init_set(mat->p[i][l],mata->p[i][l]); @@ -388,7 +388,7 @@ matrix_t* matrix_append(matrix_t* mata, matrix_t* matb) return mat; } -void matrix_append_with(matrix_t* mat, matrix_t* cmat) +void pk_matrix_append_with(pk_matrix_t* mat, pk_matrix_t* cmat) { size_t i,l; size_t nbrows; @@ -396,7 +396,7 @@ void matrix_append_with(matrix_t* mat, matrix_t* cmat) assert (mat->nbcolumns == cmat->nbcolumns); nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+cmat->nbrows); + pk_matrix_resize_rows_lazy(mat,nbrows+cmat->nbrows); for (i=0;inbrows; i++){ for (l=0; lnbcolumns; l++) numint_set(mat->p[nbrows+i][l],cmat->p[i][l]); @@ -407,7 +407,7 @@ void matrix_append_with(matrix_t* mat, matrix_t* cmat) /* Given matrices with rows p1,p2,... and q1,q2,...., fills the initial matrix with rows q1,q2,...,p1,p2,.... */ -void matrix_revappend_with(matrix_t* mat, matrix_t* cmat) +void pk_matrix_revappend_with(pk_matrix_t* mat, pk_matrix_t* cmat) { int i; size_t l; @@ -415,7 +415,7 @@ void matrix_revappend_with(matrix_t* mat, matrix_t* cmat) assert(mat->nbcolumns == cmat->nbcolumns); nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+cmat->nbrows); + pk_matrix_resize_rows_lazy(mat,nbrows+cmat->nbrows); for (i=nbrows-1; i>=0; i--){ /* exchanging rows i and i+cmat->nbrows */ numint_t* q = mat->p[i+cmat->nbrows]; @@ -436,19 +436,19 @@ void matrix_revappend_with(matrix_t* mat, matrix_t* cmat) /* Merging with sorting */ -matrix_t* matrix_merge_sort(pk_internal_t* pk, - matrix_t* mata, matrix_t* matb) +pk_matrix_t* pk_matrix_merge_sort(pk_internal_t* pk, + pk_matrix_t* mata, pk_matrix_t* matb) { size_t i,ia,ib,l; - matrix_t* mat; + pk_matrix_t* mat; size_t nbrows; assert (mata->nbcolumns == matb->nbcolumns); if (!mata->_sorted || !matb->_sorted){ - mat = matrix_append(mata,matb); - matrix_sort_rows(pk,mat); + mat = pk_matrix_append(mata,matb); + pk_matrix_sort_rows(pk,mat); } else { - mat = _matrix_alloc_int(mata->nbrows+matb->nbrows,mata->nbcolumns,true); + mat = _pk_matrix_alloc_int(mata->nbrows+matb->nbrows,mata->nbcolumns,true); i = 0; ia = 0; ib = 0; @@ -501,8 +501,8 @@ matrix_t* matrix_merge_sort(pk_internal_t* pk, and leaves the resulting matrix sorted. Identical rows are eliminated. The modified matrix is supposed to be big enough to store the new rows. */ -void matrix_merge_sort_with(pk_internal_t* pk, - matrix_t* mata, matrix_t* matb) +void pk_matrix_merge_sort_with(pk_internal_t* pk, + pk_matrix_t* mata, pk_matrix_t* matb) { size_t i,ia,ib,j,k,nbrows,nbrowsa, nbcols; numint_t** numintpp; @@ -512,7 +512,7 @@ void matrix_merge_sort_with(pk_internal_t* pk, nbrowsa = mata->nbrows; nbcols = mata->nbcolumns; - matrix_resize_rows_lazy(mata, nbrowsa + matb->nbrows); + pk_matrix_resize_rows_lazy(mata, nbrowsa + matb->nbrows); /* one adds the coefficients of matb to mata */ for (i=0; inbrows; i++){ diff --git a/newpolka/pk_matrix.h b/newpolka/pk_matrix.h index 23b3cec..e80f30b 100644 --- a/newpolka/pk_matrix.h +++ b/newpolka/pk_matrix.h @@ -32,7 +32,7 @@ used. extern "C" { #endif -typedef struct matrix_t { +typedef struct pk_matrix_t { /* public part */ numint_t** p; /* array of pointers to rows */ size_t nbrows; /* number of effective rows */ @@ -41,66 +41,66 @@ typedef struct matrix_t { /* private part */ size_t _maxrows; /* number of rows allocated */ bool _sorted; -} matrix_t; +} pk_matrix_t; /* Normal functions */ /* information about private part */ -static inline size_t matrix_get_maxrows(matrix_t* mat) +static inline size_t pk_matrix_get_maxrows(pk_matrix_t* mat) { return mat->_maxrows; } -static inline bool matrix_is_sorted(matrix_t* mat) +static inline bool pk_matrix_is_sorted(pk_matrix_t* mat) { return mat->_sorted; } /* Basic Operations */ -matrix_t* matrix_alloc(size_t nbrows, size_t nbcols, bool s); -void matrix_resize_rows(matrix_t* mat, size_t nbrows); -void matrix_resize_rows_lazy(matrix_t* mat, size_t nbrows); -void matrix_minimize(matrix_t* mat); -void matrix_free(matrix_t* mat); -void matrix_clear(matrix_t* mat); -void matrix_print(matrix_t* mat); -void matrix_fprint(FILE* stream, matrix_t* mat); -matrix_t* matrix_copy(matrix_t* mat); -bool matrix_equal(matrix_t* mata, matrix_t* matb); +pk_matrix_t* pk_matrix_alloc(size_t nbrows, size_t nbcols, bool s); +void pk_matrix_resize_rows(pk_matrix_t* mat, size_t nbrows); +void pk_matrix_resize_rows_lazy(pk_matrix_t* mat, size_t nbrows); +void pk_matrix_minimize(pk_matrix_t* mat); +void pk_matrix_free(pk_matrix_t* mat); +void pk_matrix_clear(pk_matrix_t* mat); +void pk_matrix_print(pk_matrix_t* mat); +void pk_matrix_fprint(FILE* stream, pk_matrix_t* mat); +pk_matrix_t* pk_matrix_copy(pk_matrix_t* mat); +bool pk_matrix_equal(pk_matrix_t* mata, pk_matrix_t* matb); /* Operations on rows */ -void matrix_normalize_row(pk_internal_t* pk, - matrix_t* mat, size_t l); -void matrix_combine_rows(pk_internal_t* pk, - matrix_t* mat, size_t l1, size_t l2, size_t l3, size_t k); -int matrix_compare_rows(pk_internal_t* pk, - matrix_t* mat, size_t l1, size_t l2); -void matrix_exch_rows(matrix_t* mat, size_t l1, size_t l2); -void matrix_move_rows(matrix_t* mat, size_t destrow, size_t orgrow, size_t size); +void pk_matrix_normalize_row(pk_internal_t* pk, + pk_matrix_t* mat, size_t l); +void pk_matrix_combine_rows(pk_internal_t* pk, + pk_matrix_t* mat, size_t l1, size_t l2, size_t l3, size_t k); +int pk_matrix_compare_rows(pk_internal_t* pk, + pk_matrix_t* mat, size_t l1, size_t l2); +void pk_matrix_exch_rows(pk_matrix_t* mat, size_t l1, size_t l2); +void pk_matrix_move_rows(pk_matrix_t* mat, size_t destrow, size_t orgrow, size_t size); /* Normalization of rows */ -bool matrix_normalize_constraint(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_normalize_constraint(pk_internal_t* pk, + pk_matrix_t* mat, size_t intdim, size_t realdim); -bool matrix_normalize_constraint_int(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_normalize_constraint_int(pk_internal_t* pk, + pk_matrix_t* mat, size_t intdim, size_t realdim); /* Sorting & Merging */ -void matrix_sort_rows(pk_internal_t* pk, - matrix_t* mat); -void matrix_sort_rows_with_sat(pk_internal_t* pk, - matrix_t* mat, satmat_t* sat); +void pk_matrix_sort_rows(pk_internal_t* pk, + pk_matrix_t* mat); +void pk_matrix_sort_rows_with_sat(pk_internal_t* pk, + pk_matrix_t* mat, satmat_t* sat); -matrix_t* matrix_append(matrix_t* ma, matrix_t* mb); -void matrix_append_with(matrix_t* ma, matrix_t* mb); -void matrix_revappend_with(matrix_t* ma, matrix_t* mb); +pk_matrix_t* pk_matrix_append(pk_matrix_t* ma, pk_matrix_t* mb); +void pk_matrix_append_with(pk_matrix_t* ma, pk_matrix_t* mb); +void pk_matrix_revappend_with(pk_matrix_t* ma, pk_matrix_t* mb); -matrix_t* matrix_merge_sort(pk_internal_t* pk, - matrix_t* ma, matrix_t* mb); -void matrix_merge_sort_with(pk_internal_t* pk, - matrix_t* mat, matrix_t* cmat); +pk_matrix_t* pk_matrix_merge_sort(pk_internal_t* pk, + pk_matrix_t* ma, pk_matrix_t* mb); +void pk_matrix_merge_sort_with(pk_internal_t* pk, + pk_matrix_t* mat, pk_matrix_t* cmat); /* Predicates that can be useful for users */ static inline -bool matrix_is_row_dummy_constraint(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_is_row_dummy_constraint(pk_internal_t* pk, + pk_matrix_t* mat, size_t l) { return vector_is_dummy_constraint(pk, @@ -109,7 +109,7 @@ bool matrix_is_row_dummy_constraint(pk_internal_t* pk, /* Functions meant to be internal */ -matrix_t* _matrix_alloc_int(size_t nr, size_t nc, bool s); +pk_matrix_t* _pk_matrix_alloc_int(size_t nr, size_t nc, bool s); #ifdef __cplusplus } diff --git a/newpolka/pk_meetjoin.c b/newpolka/pk_meetjoin.c index 46c71a4..745badb 100644 --- a/newpolka/pk_meetjoin.c +++ b/newpolka/pk_meetjoin.c @@ -56,7 +56,7 @@ bool poly_meet_matrix(bool meet, bool lazy, ap_manager_t* man, pk_t* po, - pk_t* pa, matrix_t* mat) + pk_t* pa, pk_matrix_t* mat) { pk_internal_t* pk = (pk_internal_t*)man->internal; @@ -69,11 +69,11 @@ bool poly_meet_matrix(bool meet, if (lazy){ poly_obtain_sorted_C(pk,pa); if (po != pa){ - po->C = matrix_merge_sort(pk,pa->C,mat); + po->C = pk_matrix_merge_sort(pk,pa->C,mat); } else { - matrix_merge_sort_with(pk,pa->C,mat); - if (pa->F){ matrix_free(pa->F); pa->F=NULL; } + pk_matrix_merge_sort_with(pk,pa->C,mat); + if (pa->F){ pk_matrix_free(pa->F); pa->F=NULL; } if (pa->satC){ satmat_free(pa->satC); pa->satC=NULL; } if (pa->satF){ satmat_free(pa->satF); pa->satF=NULL; } pa->nbeq = pa->nbline = 0; @@ -85,15 +85,15 @@ bool poly_meet_matrix(bool meet, size_t start = pa->C->nbrows; assert(pa->satC); if (po != pa){ - po->C = matrix_append(pa->C,mat); - po->F = matrix_copy(pa->F); + po->C = pk_matrix_append(pa->C,mat); + po->F = pk_matrix_copy(pa->F); po->satC = satmat_copy_resize_cols(pa->satC, bitindex_size(po->C->nbrows)); po->nbline = pa->nbline; po->nbeq = pa->nbeq; } else { - matrix_append_with(pa->C,mat); + pk_matrix_append_with(pa->C,mat); satmat_resize_cols(pa->satC, bitindex_size(pa->C->nbrows)); } @@ -354,7 +354,7 @@ pk_t* poly_meet_array(bool meet, } /* 2. General case */ else { - matrix_t* C; + pk_matrix_t* C; size_t nbrows; size_t i,j; @@ -419,13 +419,13 @@ pk_t* poly_meet_array(bool meet, } /* 2.1. lazy behaviour */ if (lazy){ - C = matrix_alloc(nbrows,pk->dec+intdim+realdim,true); + C = pk_matrix_alloc(nbrows,pk->dec+intdim+realdim,true); C->nbrows = 0; C->_sorted = true; for (i=0; iC){ poly_obtain_sorted_C(pk,po[i]); - matrix_merge_sort_with(pk,C,po[i]->C); + pk_matrix_merge_sort_with(pk,C,po[i]->C); } } poly->C = C; @@ -444,19 +444,19 @@ pk_t* poly_meet_array(bool meet, j=i; } /* Add the other polyehdra to the polyhedra of index j */ - C = matrix_alloc(nbrows, pk->dec+intdim+realdim,true); + C = pk_matrix_alloc(nbrows, pk->dec+intdim+realdim,true); C->nbrows = 0; C->_sorted = true; for (i=0; iC); + pk_matrix_merge_sort_with(pk,C,po[i]->C); } } - matrix_revappend_with(C,po[j]->C); + pk_matrix_revappend_with(C,po[j]->C); C->_sorted = false; poly->C = C; - poly->F = matrix_copy(po[j]->F); + poly->F = pk_matrix_copy(po[j]->F); poly_obtain_satC(po[j]); poly->satC = satmat_copy_resize_cols(po[j]->satC, bitindex_size(C->nbrows)); @@ -524,7 +524,7 @@ void poly_meet_itv_lincons_array(bool lazy, pk_t* po, pk_t* pa, itv_lincons_array_t* array) { - matrix_t* mat; + pk_matrix_t* mat; bool quasilinear; pk_internal_t* pk = (pk_internal_t*)man->internal; @@ -553,17 +553,17 @@ void poly_meet_itv_lincons_array(bool lazy, /* quasilinearize if needed */ if (!quasilinear){ - itv_t* env = matrix_to_box(pk,pa->F); + itv_t* env = pk_matrix_to_box(pk,pa->F); itv_quasilinearize_lincons_array(pk->itv,array,env,true); itv_array_free(env,pa->intdim+pa->realdim); } itv_linearize_lincons_array(pk->itv,array,true); itv_lincons_array_reduce_integer(pk->itv,array,po->intdim); - bool exact = matrix_set_itv_lincons_array(pk,&mat,array,po->intdim,po->realdim,true); - matrix_sort_rows(pk,mat); + bool exact = pk_matrix_set_itv_lincons_array(pk,&mat,array,po->intdim,po->realdim,true); + pk_matrix_sort_rows(pk,mat); if (!lazy) poly_obtain_satC(pa); poly_meet_matrix(true,lazy,man,po,pa,mat); - matrix_free(mat); + pk_matrix_free(mat); if (pk->exn){ pk->exn = AP_EXC_NONE; man->result.flag_exact = man->result.flag_best = false; @@ -687,7 +687,7 @@ void poly_add_ray_array(bool lazy, pk_t* po, pk_t* pa, ap_generator0_array_t* array) { bool exact; - matrix_t* mat; + pk_matrix_t* mat; pk_internal_t* pk = (pk_internal_t*)man->internal; @@ -712,8 +712,8 @@ void poly_add_ray_array(bool lazy, poly_set(po,pa); return; } - exact = matrix_set_ap_generator0_array(pk,&mat,array,pa->intdim,pa->realdim); - matrix_sort_rows(pk,mat); + exact = pk_matrix_set_ap_generator0_array(pk,&mat,array,pa->intdim,pa->realdim); + pk_matrix_sort_rows(pk,mat); if (!lazy) poly_obtain_satF(pa); poly_dual(po); @@ -721,7 +721,7 @@ void poly_add_ray_array(bool lazy, poly_meet_matrix(false,lazy,man,po,pa,mat); poly_dual(po); if (po!=pa) poly_dual(pa); - matrix_free(mat); + pk_matrix_free(mat); man->result.flag_exact = exact; } diff --git a/newpolka/pk_meetjoin.h b/newpolka/pk_meetjoin.h index 47e53f7..32f43cb 100644 --- a/newpolka/pk_meetjoin.h +++ b/newpolka/pk_meetjoin.h @@ -47,7 +47,7 @@ extern "C" { bool poly_meet_matrix(bool meet, bool lazy, ap_manager_t* man, pk_t* po, - pk_t* pa, matrix_t* mat); + pk_t* pa, pk_matrix_t* mat); void poly_meet_itv_lincons_array(bool lazy, ap_manager_t* man, diff --git a/newpolka/pk_project.c b/newpolka/pk_project.c index f662f8b..9da508a 100644 --- a/newpolka/pk_project.c +++ b/newpolka/pk_project.c @@ -33,7 +33,7 @@ void poly_projectforget_array(bool project, ap_dim_t* tdim, size_t size) { bool res; - matrix_t* mat; + pk_matrix_t* mat; size_t i,j; pk_internal_t* pk = (pk_internal_t*)man->internal; pk_internal_realloc_lazy(pk,pa->intdim+pa->realdim); @@ -65,19 +65,19 @@ void poly_projectforget_array(bool project, /* Project: assign the dimension to zero */ if (po==pa){ /* Forget the other matrices */ - if (po->C){ matrix_free(po->C); po->C = NULL; } + if (po->C){ pk_matrix_free(po->C); po->C = NULL; } if (po->satC){ satmat_free(po->satC); po->satC = NULL; } if (po->satF){ satmat_free(po->satF); po->satF = NULL; } } else { /* Copy the old one */ - po->F = matrix_copy(pa->F); + po->F = pk_matrix_copy(pa->F); } mat = po->F; for (i=0; inbrows; i++){ for (j=0; jp[i][pk->dec+tdim[j]],0); } - matrix_normalize_row(pk,mat,(size_t)i); + pk_matrix_normalize_row(pk,mat,(size_t)i); } po->status = 0; if (!lazy){ @@ -86,18 +86,18 @@ void poly_projectforget_array(bool project, } else { /* Forget */ - mat = matrix_alloc(size,pa->F->nbcolumns,false); + mat = pk_matrix_alloc(size,pa->F->nbcolumns,false); for (i=0; ip[i][pk->dec+tdim[i]],1); } - matrix_sort_rows(pk,mat); + pk_matrix_sort_rows(pk,mat); poly_dual(pa); if (po!=pa) poly_dual(po); if (!lazy) poly_obtain_satC(pa); res = poly_meet_matrix(false,lazy,man,po,pa,mat); poly_dual(pa); if (po!=pa) poly_dual(po); - matrix_free(mat); + pk_matrix_free(mat); } if (res || pk->exn){ pk->exn = AP_EXC_NONE; diff --git a/newpolka/pk_representation.c b/newpolka/pk_representation.c index 51749a7..ec6a870 100644 --- a/newpolka/pk_representation.c +++ b/newpolka/pk_representation.c @@ -76,8 +76,8 @@ pk_t* poly_alloc(size_t intdim, size_t realdim) /* Clearing a polyhedron */ void poly_clear(pk_t* po) { - if (po->C) matrix_free(po->C); - if (po->F) matrix_free(po->F); + if (po->C) pk_matrix_free(po->C); + if (po->F) pk_matrix_free(po->F); if (po->satC) satmat_free(po->satC); if (po->satF) satmat_free(po->satF); po->C = NULL; @@ -96,8 +96,8 @@ void poly_set(pk_t* pa, pk_t* pb) poly_clear(pa); pa->intdim = pb->intdim; pa->realdim = pb->realdim; - pa->C = pb->C ? matrix_copy(pb->C) : NULL; - pa->F = pb->F ? matrix_copy(pb->F) : NULL; + pa->C = pb->C ? pk_matrix_copy(pb->C) : NULL; + pa->F = pb->F ? pk_matrix_copy(pb->F) : NULL; pa->satC = pb->satC ? satmat_copy(pb->satC) : NULL; pa->satF = pb->satF ? satmat_copy(pb->satF) : NULL; pa->status = pb->status; @@ -111,8 +111,8 @@ void poly_set(pk_t* pa, pk_t* pb) pk_t* pk_copy(ap_manager_t* man, pk_t* po) { pk_t* npo = poly_alloc(po->intdim,po->realdim); - npo->C = po->C ? matrix_copy(po->C) : 0; - npo->F = po->F ? matrix_copy(po->F) : 0; + npo->C = po->C ? pk_matrix_copy(po->C) : 0; + npo->F = po->F ? pk_matrix_copy(po->F) : 0; npo->satC = po->satC ? satmat_copy(po->satC) : 0; npo->satF = po->satF ? satmat_copy(po->satF) : 0; npo->nbeq = po->nbeq; @@ -165,16 +165,16 @@ void poly_chernikova(ap_manager_t* man, else { if (po->C){ if (!poly_is_conseps(pk,po) ){ - matrix_normalize_constraint(pk,po->C,po->intdim,po->realdim); + pk_matrix_normalize_constraint(pk,po->C,po->intdim,po->realdim); } - matrix_sort_rows(pk,po->C); + pk_matrix_sort_rows(pk,po->C); cherni_minimize(pk,true,po); if (pk->exn) goto poly_chernikova_exit0; po->status = pk_status_consgauss; } else { po->C = po->F; po->F = NULL; - matrix_sort_rows(pk,po->C); + pk_matrix_sort_rows(pk,po->C); cherni_minimize(pk,false,po); poly_dual(po); if (pk->exn) goto poly_chernikova_exit0; @@ -228,7 +228,7 @@ void poly_chernikova2(ap_manager_t* man, assert((po->status & pk_status_minimaleps) && (po->status & pk_status_conseps)); if (change){ - matrix_sort_rows(pk,po->C); + pk_matrix_sort_rows(pk,po->C); cherni_minimize(pk, true, po); if (pk->exn) goto poly_chernikova2_exit0; assert(po->C && po->F); @@ -285,8 +285,8 @@ void poly_chernikova3(ap_manager_t* man, (po->status | pk_status_consgauss) && (po->status | pk_status_gengauss) && (po->status | pk_status_minimaleps)); - assert(matrix_check_gauss(po->C,po->nbeq)); - assert(matrix_check_gauss(po->F,po->nbline)); + assert(pk_matrix_check_gauss(po->C,po->nbeq)); + assert(pk_matrix_check_gauss(po->F,po->nbline)); } } @@ -294,18 +294,18 @@ void poly_obtain_sorted_F(pk_internal_t* pk, pk_t* po) { assert (po->F); - if (!matrix_is_sorted(po->F)){ + if (!pk_matrix_is_sorted(po->F)){ if (po->satC){ if (po->satF){ satmat_free(po->satF); po->satF = 0; } - matrix_sort_rows_with_sat(pk,po->F,po->satC); + pk_matrix_sort_rows_with_sat(pk,po->F,po->satC); } else if (po->satF){ po->satC = satmat_transpose(po->satF,po->F->nbrows); satmat_free(po->satF); po->satF = 0; - matrix_sort_rows_with_sat(pk,po->F,po->satC); + pk_matrix_sort_rows_with_sat(pk,po->F,po->satC); } else { - matrix_sort_rows(pk,po->F); + pk_matrix_sort_rows(pk,po->F); } } } @@ -314,18 +314,18 @@ void poly_obtain_sorted_C(pk_internal_t* pk, pk_t* po) { assert (po->C); - if (!matrix_is_sorted(po->C)){ + if (!pk_matrix_is_sorted(po->C)){ if (po->satF){ if (po->satC){ satmat_free(po->satC); po->satC = 0; } - matrix_sort_rows_with_sat(pk,po->C,po->satF); + pk_matrix_sort_rows_with_sat(pk,po->C,po->satF); } else if (po->satC){ po->satF = satmat_transpose(po->satC,po->C->nbrows); satmat_free(po->satC); po->satC = 0; - matrix_sort_rows_with_sat(pk,po->C,po->satF); + pk_matrix_sort_rows_with_sat(pk,po->C,po->satF); } else { - matrix_sort_rows(pk,po->C); + pk_matrix_sort_rows(pk,po->C); } } } @@ -397,15 +397,15 @@ void pk_minimize(ap_manager_t* man, pk_t* po) if (po->satF) satmat_free(po->satF); po->satC = po->satF = NULL; if (po->C->nbrows > po->F->nbrows){ - matrix_free(po->C); + pk_matrix_free(po->C); po->C = NULL; - matrix_minimize(po->F); + pk_matrix_minimize(po->F); po->status &= ~pk_status_consgauss; } else { - matrix_free(po->F); + pk_matrix_free(po->F); po->F = NULL; - matrix_minimize(po->C); + pk_matrix_minimize(po->C); po->status &= ~pk_status_gengauss; } } @@ -446,8 +446,8 @@ bool pk_is_canonical(ap_manager_t* man, pk_t* po) po->status & pk_status_consgauss && po->status & pk_status_gengauss && poly_is_minimaleps(pk,po)){ - assert(matrix_check_gauss(po->C,po->nbeq)); - assert(matrix_check_gauss(po->F,po->nbline)); + assert(pk_matrix_check_gauss(po->C,po->nbeq)); + assert(pk_matrix_check_gauss(po->F,po->nbline)); res = true; } else @@ -508,11 +508,11 @@ void pk_fdump(FILE* stream, ap_manager_t* man, pk_t* po) (unsigned long)po->intdim,(unsigned long)po->realdim); if (po->C){ fprintf(stream,"Constraints: "); - matrix_fprint(stream, po->C); + pk_matrix_fprint(stream, po->C); } if (po->F){ fprintf(stream,"Frames: "); - matrix_fprint(stream, po->F); + pk_matrix_fprint(stream, po->F); } if (po->satC){ fprintf(stream,"satC: "); @@ -551,7 +551,7 @@ pk_t* pk_deserialize_raw(ap_manager_t* man, void* ptr, size_t* size) /* Should be true If false, implies that there is no positivity constraint */ -static bool matrix_check1cons(pk_internal_t* pk, matrix_t* mat) +static bool pk_matrix_check1cons(pk_internal_t* pk, pk_matrix_t* mat) { size_t i; bool res; @@ -565,7 +565,7 @@ static bool matrix_check1cons(pk_internal_t* pk, matrix_t* mat) return res; } /* true <=> \xi or \epsilon always positive */ -static bool matrix_check1ray(pk_internal_t* pk, matrix_t* mat) +static bool pk_matrix_check1ray(pk_internal_t* pk, pk_matrix_t* mat) { size_t i; bool res; @@ -580,7 +580,7 @@ static bool matrix_check1ray(pk_internal_t* pk, matrix_t* mat) } /* Return false if not normalized constraint */ -static bool matrix_check2(pk_internal_t* pk, matrix_t* mat) +static bool pk_matrix_check2(pk_internal_t* pk, pk_matrix_t* mat) { size_t i; bool res; @@ -600,7 +600,7 @@ static bool matrix_check2(pk_internal_t* pk, matrix_t* mat) } /* If false, _sorted is true without sorted rows */ -static bool matrix_check3(pk_internal_t* pk, matrix_t* mat) +static bool pk_matrix_check3(pk_internal_t* pk, pk_matrix_t* mat) { size_t i; bool res; @@ -610,7 +610,7 @@ static bool matrix_check3(pk_internal_t* pk, matrix_t* mat) res = true; for (i=0; inbrows-1; i++){ - if (matrix_compare_rows(pk,mat,i,i+1)>0){ + if (pk_matrix_compare_rows(pk,mat,i,i+1)>0){ res = false; break; } @@ -618,7 +618,7 @@ static bool matrix_check3(pk_internal_t* pk, matrix_t* mat) return res; } -bool matrix_check_gauss(matrix_t* mat, size_t nbeq) +bool pk_matrix_check_gauss(pk_matrix_t* mat, size_t nbeq) { size_t i,j,k; @@ -629,13 +629,13 @@ bool matrix_check_gauss(matrix_t* mat, size_t nbeq) break; } if (j<=1){ - fprintf(stderr,"matrix_check_gauss: equality with all std coefficients set to zero !\n"); + fprintf(stderr,"pk_matrix_check_gauss: equality with all std coefficients set to zero !\n"); return false; } /* Check that this coeff is zero on all other rows */ for (i=0; inbrows; i++){ if (i != k && numint_sgn(mat->p[i][j])!=0){ - fprintf(stderr,"matrix_check_gauss: row %llu col %llu should be zero !\n",(unsigned long long)i,(unsigned long long)j); + fprintf(stderr,"pk_matrix_check_gauss: row %llu col %llu should be zero !\n",(unsigned long long)i,(unsigned long long)j); return false; } } @@ -662,34 +662,34 @@ bool poly_check(pk_internal_t* pk, pk_t* po) return false; } if (po->C){ - res = matrix_check1cons(pk,po->C); + res = pk_matrix_check1cons(pk,po->C); if (!res){ /* should not arise */ fprintf(stderr,"poly_check: unvalid constraint system, does not imply the positivity constraint\n"); return false; } - res = matrix_check2(pk,po->C); + res = pk_matrix_check2(pk,po->C); if (!res){ fprintf(stderr,"poly_check: C not normalized\n"); return false; } - res = matrix_check3(pk,po->C); + res = pk_matrix_check3(pk,po->C); if (!res){ fprintf(stderr,"poly_check: C not sorted although _sorted=true\n"); return false; } } if (po->F){ - res = matrix_check1ray(pk,po->F); + res = pk_matrix_check1ray(pk,po->F); if (!res){ /* should not arise */ fprintf(stderr,"poly_check: unvalid generator system, does not imply the positivity constraint\n"); return false; } - res = matrix_check2(pk,po->F); + res = pk_matrix_check2(pk,po->F); if (!res){ fprintf(stderr,"poly_check: F not normalized\n"); return false; } - res = matrix_check3(pk,po->F); + res = pk_matrix_check3(pk,po->F); if (!res){ fprintf(stderr,"poly_check: F not sorted although _sorted=true\n"); return false; @@ -697,7 +697,7 @@ bool poly_check(pk_internal_t* pk, pk_t* po) /* In strict mode, check that it satisfies \xi-\epsilon>=0 */ if (pk->strict){ numint_t* tab = pk->vector_numintp; - matrix_t* F = po->F; + pk_matrix_t* F = po->F; vector_clear(tab,F->nbcolumns); numint_set_int(tab[0],1); numint_set_int(tab[polka_cst],1); @@ -733,8 +733,8 @@ bool poly_check(pk_internal_t* pk, pk_t* po) return false; } if (po->status & pk_status_consgauss && po->status & pk_status_gengauss){ - assert(matrix_check_gauss(po->C,po->nbeq)); - assert(matrix_check_gauss(po->F,po->nbline)); + assert(pk_matrix_check_gauss(po->C,po->nbeq)); + assert(pk_matrix_check_gauss(po->F,po->nbline)); } } else @@ -785,7 +785,7 @@ bool poly_check(pk_internal_t* pk, pk_t* po) } /* Check status: conseps */ if (pk->strict && (po->status & pk_status_conseps) && po->C){ - matrix_t* mat = po->C; + pk_matrix_t* mat = po->C; size_t i; numint_t* vec = vector_alloc(mat->nbcolumns); res = true; diff --git a/newpolka/pk_representation.h b/newpolka/pk_representation.h index 820e76b..3211367 100644 --- a/newpolka/pk_representation.h +++ b/newpolka/pk_representation.h @@ -92,7 +92,7 @@ static inline void poly_obtain_F_dual(ap_manager_t* man,pk_t* po, char* msg, boo /* ********************************************************************** */ /* Checks gauss elimination */ -bool matrix_check_gauss(matrix_t* mat, size_t nbeq); +bool pk_matrix_check_gauss(pk_matrix_t* mat, size_t nbeq); /* Perform rather detailed and costly checks on a polyhedron, to detect inconsistencies */ diff --git a/newpolka/pk_resize.c b/newpolka/pk_resize.c index 3d8ee6e..b1440e2 100644 --- a/newpolka/pk_resize.c +++ b/newpolka/pk_resize.c @@ -115,7 +115,7 @@ void vector_remove_dimensions(pk_internal_t* pk, /* Modifications of the number of columns in-place */ static -void matrix_resize_diffcols(matrix_t* mat, int diff) +void pk_matrix_resize_diffcols(pk_matrix_t* mat, int diff) { if (diff != 0){ size_t i; @@ -128,21 +128,21 @@ void matrix_resize_diffcols(matrix_t* mat, int diff) } } -matrix_t* matrix_add_dimensions(pk_internal_t* pk, +pk_matrix_t* pk_matrix_add_dimensions(pk_internal_t* pk, bool destructive, - matrix_t* mat, + pk_matrix_t* mat, ap_dimchange_t* dimchange) { - matrix_t* nmat; + pk_matrix_t* nmat; size_t i,dimsup; dimsup = dimchange->intdim+dimchange->realdim; if (destructive){ nmat = mat; - matrix_resize_diffcols(nmat,(int)dimsup); + pk_matrix_resize_diffcols(nmat,(int)dimsup); } else { - nmat = matrix_alloc(mat->nbrows,mat->nbcolumns+dimsup,mat->_sorted); + nmat = pk_matrix_alloc(mat->nbrows,mat->nbcolumns+dimsup,mat->_sorted); } for (i=0; inbrows; i++){ vector_add_dimensions(pk,nmat->p[i],mat->p[i],nmat->nbcolumns-dimsup,dimchange); @@ -150,19 +150,19 @@ matrix_t* matrix_add_dimensions(pk_internal_t* pk, return nmat; } static -matrix_t* matrix_remove_dimensions(pk_internal_t* pk, +pk_matrix_t* pk_matrix_remove_dimensions(pk_internal_t* pk, bool destructive, - matrix_t* mat, + pk_matrix_t* mat, ap_dimchange_t* dimchange) { - matrix_t* nmat; + pk_matrix_t* nmat; size_t i,dimsup; dimsup = dimchange->intdim + dimchange->realdim; nmat = destructive ? mat : - matrix_alloc(mat->nbrows, mat->nbcolumns-dimsup, false); + pk_matrix_alloc(mat->nbrows, mat->nbcolumns-dimsup, false); for (i=0; inbrows; i++){ vector_remove_dimensions(pk, nmat->p[i], @@ -172,21 +172,21 @@ matrix_t* matrix_remove_dimensions(pk_internal_t* pk, vector_normalize(pk,nmat->p[i],mat->nbcolumns-dimsup); } if (destructive){ - matrix_resize_diffcols(nmat, -(int)dimsup); + pk_matrix_resize_diffcols(nmat, -(int)dimsup); } nmat->_sorted = false; return nmat; } static -matrix_t* matrix_permute_dimensions(pk_internal_t* pk, +pk_matrix_t* pk_matrix_permute_dimensions(pk_internal_t* pk, bool destructive, - matrix_t* mat, + pk_matrix_t* mat, ap_dim_t* permutation) { - matrix_t* nmat; + pk_matrix_t* nmat; size_t i; - nmat = destructive ? mat : matrix_alloc(mat->nbrows,mat->nbcolumns,false); + nmat = destructive ? mat : pk_matrix_alloc(mat->nbrows,mat->nbcolumns,false); for (i=0; inbrows; i++){ vector_permute_dimensions(pk,nmat->p[i],mat->p[i],mat->nbcolumns,permutation); } @@ -233,16 +233,16 @@ pk_t* cherni_add_dimensions(pk_internal_t* pk, } /* Extend constraints */ if (pa->C){ - po->C = matrix_add_dimensions(pk,destructive,pa->C,dimchange); + po->C = pk_matrix_add_dimensions(pk,destructive,pa->C,dimchange); po->C->_sorted = false; } /* Extend generators and add new lines */ if (pa->F){ size_t nbrows = pa->F->nbrows; - po->F = matrix_add_dimensions(pk,destructive,pa->F,dimchange); - matrix_resize_rows_lazy(po->F,po->F->nbrows+dimsup); + po->F = pk_matrix_add_dimensions(pk,destructive,pa->F,dimchange); + pk_matrix_resize_rows_lazy(po->F,po->F->nbrows+dimsup); /* translate rows [0,oldF->nbrows-1] to [dimsup,oldF->nbrows+dimsup-1] */ - matrix_move_rows(po->F,dimsup,0,nbrows); + pk_matrix_move_rows(po->F,dimsup,0,nbrows); /* addition of new lines at the beginning of the matrix */ k=dimsup-1; for (i=po->intdim+po->realdim - dimsup; i>=0; i--){ @@ -255,7 +255,7 @@ pk_t* cherni_add_dimensions(pk_internal_t* pk, } po->F->_sorted = pa->F->_sorted && - (matrix_compare_rows(pk,po->F,dimsup-1,dimsup) < 0); + (pk_matrix_compare_rows(pk,po->F,dimsup-1,dimsup) < 0); } if (pa->satC){ if (destructive){ @@ -388,11 +388,11 @@ pk_t* pk_remove_dimensions(ap_manager_t* man, } return po; } - if (po->C){ matrix_free(po->C); po->C = NULL; } + if (po->C){ pk_matrix_free(po->C); po->C = NULL; } if (po->satC){ satmat_free(po->satC); po->satC = NULL; } if (po->satF){ satmat_free(po->satF); po->satF = NULL; } dimsup = dimchange->intdim+dimchange->realdim; - po->F = matrix_remove_dimensions(pk,destructive,pa->F,dimchange); + po->F = pk_matrix_remove_dimensions(pk,destructive,pa->F,dimchange); if (pk->funopt->algorithm>0){ poly_chernikova(man,po,"of the result"); if (pk->exn){ @@ -424,10 +424,10 @@ pk_t* pk_permute_dimensions(ap_manager_t* man, man->result.flag_best = man->result.flag_exact = true; po = destructive ? pa : poly_alloc(pa->intdim,pa->realdim); if (pa->C){ - po->C = matrix_permute_dimensions(pk,destructive,pa->C,permutation->dim); + po->C = pk_matrix_permute_dimensions(pk,destructive,pa->C,permutation->dim); } if (pa->F){ - po->F = matrix_permute_dimensions(pk,destructive,pa->F,permutation->dim); + po->F = pk_matrix_permute_dimensions(pk,destructive,pa->F,permutation->dim); } if (!destructive){ po->satC = pa->satC ? satmat_copy(pa->satC) : NULL; diff --git a/newpolka/pk_resize.h b/newpolka/pk_resize.h index 160ad18..4604ab4 100644 --- a/newpolka/pk_resize.h +++ b/newpolka/pk_resize.h @@ -27,8 +27,8 @@ void vector_remove_dimensions(pk_internal_t* pk, numint_t* q, size_t size, ap_dimchange_t* dimchange); -matrix_t* matrix_add_dimensions(pk_internal_t* pk, - bool destructive, matrix_t* mat, +pk_matrix_t* pk_matrix_add_dimensions(pk_internal_t* pk, + bool destructive, pk_matrix_t* mat, ap_dimchange_t* dimchange); #ifdef __cplusplus diff --git a/newpolka/pk_test.c b/newpolka/pk_test.c index ffee5d9..de1b33f 100644 --- a/newpolka/pk_test.c +++ b/newpolka/pk_test.c @@ -94,7 +94,7 @@ This enables to test the satisfiability of a strict constraint in non-strict mode for the library. */ -bool do_generators_sat_vector(pk_internal_t* pk, matrix_t* F, numint_t* tab, bool is_strict) +bool do_generators_sat_vector(pk_internal_t* pk, pk_matrix_t* F, numint_t* tab, bool is_strict) { size_t i; @@ -231,7 +231,7 @@ bool pk_is_eq(ap_manager_t* man, pk_t* pa, pk_t* pb) (!pa->C && !pb->C) || (pa->C && pb->C && pa->C->nbrows == pb->C->nbrows && pa->F->nbrows == pb->F->nbrows && - (pa->C->nbrows <= pa->F->nbrows ? matrix_equal(pa->C,pb->C) : matrix_equal(pa->F,pb->F))); + (pa->C->nbrows <= pa->F->nbrows ? pk_matrix_equal(pa->C,pb->C) : pk_matrix_equal(pa->F,pb->F))); assert(res == (pk_is_leq(man,pa,pb) && pk_is_leq(man,pb,pa))); return res; } @@ -277,7 +277,7 @@ bool pk_sat_lincons(ap_manager_t* man, pk_t* po, ap_lincons0_t* lincons0) dim = po->intdim + po->realdim; if (!ap_linexpr0_is_quasilinear(lincons0->linexpr0)){ - itv_t* env = matrix_to_box(pk,po->F); + itv_t* env = pk_matrix_to_box(pk,po->F); exact = itv_lincons_set_ap_lincons0(pk->itv, &pk->poly_itv_lincons, lincons0); @@ -343,7 +343,7 @@ bool pk_sat_tcons(ap_manager_t* man, pk_t* po, ap_tcons0_t* cons) } dim = po->intdim + po->realdim; - itv_t* env = matrix_to_box(pk,po->F); + itv_t* env = pk_matrix_to_box(pk,po->F); itv_intlinearize_ap_tcons0(pk->itv,&pk->poly_itv_lincons, cons,env,po->intdim); itv_quasilinearize_lincons(pk->itv,&pk->poly_itv_lincons,env,false); @@ -380,7 +380,7 @@ tests if: - dim >= -bound if sgn<0 */ -bool do_generators_sat_bound(pk_internal_t* pk, matrix_t* F, +bool do_generators_sat_bound(pk_internal_t* pk, pk_matrix_t* F, ap_dim_t dim, numrat_t bound, int sgn) { @@ -472,8 +472,8 @@ bool pk_is_dimension_unconstrained(ap_manager_t* man, pk_t* po, { size_t i,j; bool res; - matrix_t* F; - matrix_t* C; + pk_matrix_t* F; + pk_matrix_t* C; pk_internal_t* pk = pk_init_from_manager(man,AP_FUNID_SAT_INTERVAL); poly_chernikova3(man,po,NULL); diff --git a/newpolka/pk_test.h b/newpolka/pk_test.h index cf2a14d..3c167f7 100644 --- a/newpolka/pk_test.h +++ b/newpolka/pk_test.h @@ -28,7 +28,7 @@ This enables to test the satisfiability of a strict constraint in non-strict mode for the library. */ bool do_generators_sat_vector(pk_internal_t* pk, - matrix_t* F, + pk_matrix_t* F, numint_t* tab, bool is_strict); #ifdef __cplusplus diff --git a/newpolka/pk_user.c b/newpolka/pk_user.c index 08d3fc7..f7a2198 100644 --- a/newpolka/pk_user.c +++ b/newpolka/pk_user.c @@ -315,8 +315,8 @@ bool vector_set_ap_generator0(pk_internal_t* pk, } static -bool matrix_append_ap_generator0_array(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_append_ap_generator0_array(pk_internal_t* pk, + pk_matrix_t* mat, ap_generator0_array_t* array, size_t intdim, size_t realdim) { @@ -324,7 +324,7 @@ bool matrix_append_ap_generator0_array(pk_internal_t* pk, size_t i,nbrows; nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+array->size); + pk_matrix_resize_rows_lazy(mat,nbrows+array->size); res = true; for (i=0; isize; i++){ exact = vector_set_ap_generator0(pk,mat->p[nbrows+i],&array->p[i],intdim,realdim); @@ -332,19 +332,19 @@ bool matrix_append_ap_generator0_array(pk_internal_t* pk, } return res; } -bool matrix_set_ap_generator0_array(pk_internal_t* pk, - matrix_t** matrix, +bool pk_matrix_set_ap_generator0_array(pk_internal_t* pk, + pk_matrix_t** matrix, ap_generator0_array_t* array, size_t intdim, size_t realdim) { - *matrix = matrix_alloc(array->size,pk->dec+intdim+realdim,false); + *matrix = pk_matrix_alloc(array->size,pk->dec+intdim+realdim,false); (*matrix)->nbrows = 0; - return matrix_append_ap_generator0_array(pk,*matrix,array,intdim,realdim); + return pk_matrix_append_ap_generator0_array(pk,*matrix,array,intdim,realdim); } /* static -bool matrix_append_ap_lincons0_array(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_append_ap_lincons0_array(pk_internal_t* pk, + pk_matrix_t* mat, size_t** tabindex, size_t* size, ap_lincons0_array_t* array, size_t intdim, size_t realdim, @@ -355,7 +355,7 @@ bool matrix_append_ap_lincons0_array(pk_internal_t* pk, size_t* tab; nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+2*array->size); + pk_matrix_resize_rows_lazy(mat,nbrows+2*array->size); res = true; tab = NULL; @@ -409,24 +409,24 @@ bool matrix_append_ap_lincons0_array(pk_internal_t* pk, return res; } -bool matrix_set_ap_lincons0_array(pk_internal_t* pk, - matrix_t** mat, +bool pk_matrix_set_ap_lincons0_array(pk_internal_t* pk, + pk_matrix_t** mat, size_t** tabindex, size_t* size, ap_lincons0_array_t* array, size_t intdim, size_t realdim, bool integer) { - *mat = matrix_alloc(2*array->size,pk->dec+intdim+realdim,false); + *mat = pk_matrix_alloc(2*array->size,pk->dec+intdim+realdim,false); (*mat)->nbrows = 0; - return matrix_append_ap_lincons0_array(pk, + return pk_matrix_append_ap_lincons0_array(pk, *mat, tabindex,size, array, intdim,realdim,integer); } static -bool matrix_append_ap_intlincons0_array(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_append_ap_intlincons0_array(pk_internal_t* pk, + pk_matrix_t* mat, itv_t* titv, ap_lincons0_array_t* array, size_t* tab, size_t size, @@ -437,7 +437,7 @@ bool matrix_append_ap_intlincons0_array(pk_internal_t* pk, size_t nbrows,i,j; nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+2*array->size); + pk_matrix_resize_rows_lazy(mat,nbrows+2*array->size); exact = true; j = nbrows; for (i=0; isize,pk->dec+intdim+realdim,false); + *mat = pk_matrix_alloc(2*array->size,pk->dec+intdim+realdim,false); (*mat)->nbrows = 0; - return matrix_append_ap_intlincons0_array(pk, + return pk_matrix_append_ap_intlincons0_array(pk, *mat, titv, array,tab,size, @@ -474,8 +474,8 @@ bool matrix_set_ap_intlincons0_array(pk_internal_t* pk, } */ static -bool matrix_append_itv_lincons_array(pk_internal_t* pk, - matrix_t* mat, +bool pk_matrix_append_itv_lincons_array(pk_internal_t* pk, + pk_matrix_t* mat, itv_lincons_array_t* array, size_t intdim, size_t realdim, bool integer) @@ -485,7 +485,7 @@ bool matrix_append_itv_lincons_array(pk_internal_t* pk, size_t* tab; nbrows = mat->nbrows; - matrix_resize_rows_lazy(mat,nbrows+array->size); + pk_matrix_resize_rows_lazy(mat,nbrows+array->size); res = true; j = nbrows; @@ -509,17 +509,17 @@ bool matrix_append_itv_lincons_array(pk_internal_t* pk, mat->nbrows = j; return res; } -bool matrix_set_itv_lincons_array(pk_internal_t* pk, - matrix_t** mat, +bool pk_matrix_set_itv_lincons_array(pk_internal_t* pk, + pk_matrix_t** mat, itv_lincons_array_t* array, size_t intdim, size_t realdim, bool integer) { - *mat = matrix_alloc(array->size,pk->dec+intdim+realdim,false); + *mat = pk_matrix_alloc(array->size,pk->dec+intdim+realdim,false); (*mat)->nbrows = 0; - return matrix_append_itv_lincons_array(pk, + return pk_matrix_append_itv_lincons_array(pk, *mat,array, intdim,realdim,integer); } diff --git a/newpolka/pk_user.h b/newpolka/pk_user.h index 8ccc400..23d38da 100644 --- a/newpolka/pk_user.h +++ b/newpolka/pk_user.h @@ -81,19 +81,19 @@ bool vector_set_ap_generator0(pk_internal_t* pk, numint_t* vec, ap_generator0_t* gen, size_t intdim, size_t realdim); -bool matrix_set_ap_generator0_array(pk_internal_t* pk, - matrix_t** matrix, +bool pk_matrix_set_ap_generator0_array(pk_internal_t* pk, + pk_matrix_t** matrix, ap_generator0_array_t* array, size_t intdim, size_t realdim); /* -bool matrix_set_ap_lincons0_array(pk_internal_t* pk, - matrix_t** mat, +bool pk_matrix_set_ap_lincons0_array(pk_internal_t* pk, + pk_matrix_t** mat, size_t** tabindex, size_t* size, ap_lincons0_array_t* array, size_t intdim, size_t realdim, bool integer); -bool matrix_set_ap_intlincons0_array(pk_internal_t* pk, - matrix_t** mat, +bool pk_matrix_set_ap_intlincons0_array(pk_internal_t* pk, + pk_matrix_t** mat, itv_t* titv, ap_lincons0_array_t* array, size_t* tab, size_t size, @@ -101,8 +101,8 @@ bool matrix_set_ap_intlincons0_array(pk_internal_t* pk, bool integer); */ /* From ITV to PK */ -bool matrix_set_itv_lincons_array(pk_internal_t* pk, - matrix_t** mat, +bool pk_matrix_set_itv_lincons_array(pk_internal_t* pk, + pk_matrix_t** mat, itv_lincons_array_t* array, size_t intdim, size_t realdim, bool integer); diff --git a/newpolka/pk_widening.c b/newpolka/pk_widening.c index 69a6d71..ea7b2a1 100644 --- a/newpolka/pk_widening.c +++ b/newpolka/pk_widening.c @@ -176,8 +176,8 @@ pk_t* pk_widening(ap_manager_t* man, pk_t* pa, pk_t* pb) po = poly_alloc(pa->intdim,pa->realdim); - po->C = matrix_alloc(pk->dec-1+pb->C->nbrows, pb->C->nbcolumns, false); - matrix_fill_constraint_top(pk,po->C,0); + po->C = pk_matrix_alloc(pk->dec-1+pb->C->nbrows, pb->C->nbcolumns, false); + pk_matrix_fill_constraint_top(pk,po->C,0); nbrows = pk->dec-1; /* Adding constraints of pb mutually redundant with some of pa, except if @@ -230,7 +230,7 @@ pk_t* pk_widening_threshold(ap_manager_t* man, /* We assume that both pa and pb are minimized, and that po->F==NULL */ nbcols = po->C->nbcolumns; nbrows = po->C->nbrows; - matrix_resize_rows_lazy(po->C, nbrows + array->size); + pk_matrix_resize_rows_lazy(po->C, nbrows + array->size); for (i=0; isize; i++){ switch(array->p[i].constyp){ case AP_CONS_EQ: @@ -260,7 +260,7 @@ pk_t* pk_widening_threshold(ap_manager_t* man, } } po->C->nbrows = nbrows; - matrix_minimize(po->C); + pk_matrix_minimize(po->C); assert(poly_check(pk,po)); return po; } diff --git a/newpolka/pkeq.c b/newpolka/pkeq.c index 40ed8c5..fbe6e99 100644 --- a/newpolka/pkeq.c +++ b/newpolka/pkeq.c @@ -69,10 +69,10 @@ bool equality_check(pk_internal_t* pk, pkeq_t* po) static -void matrix_reduce(matrix_t* mat) +void pk_matrix_reduce(pk_matrix_t* mat) { if (mat->nbrows + 4 <= mat->_maxrows){ - matrix_minimize(mat); + pk_matrix_minimize(mat); } } @@ -85,9 +85,9 @@ void equality_reduce(ap_manager_t* man, pkeq_t* po) pk_internal_t* pk = (pk_internal_t*)man->internal; po->C->nbrows = po->nbeq + 1; - matrix_fill_constraint_top(pk,po->C,po->nbeq); - matrix_reduce(po->C); - matrix_free(po->F); po->F = NULL; + pk_matrix_fill_constraint_top(pk,po->C,po->nbeq); + pk_matrix_reduce(po->C); + pk_matrix_free(po->F); po->F = NULL; if (po->satC){ satmat_free(po->satC); po->satC = NULL; @@ -164,7 +164,7 @@ pkeq_t* pkeq_of_box(ap_manager_t* man, pk_status_conseps; dim = intdim + realdim; - po->C = matrix_alloc(pk->dec-1 + dim, pk->dec + dim, false); + po->C = pk_matrix_alloc(pk->dec-1 + dim, pk->dec + dim, false); /* constraints */ row = 0; @@ -178,7 +178,7 @@ pkeq_t* pkeq_of_box(ap_manager_t* man, intdim,realdim, true); if (!ok){ - matrix_free(po->C); + pk_matrix_free(po->C); po->C = NULL; return po; } @@ -186,9 +186,9 @@ pkeq_t* pkeq_of_box(ap_manager_t* man, } } itv_clear(itv); - matrix_fill_constraint_top(pk,po->C,row); + pk_matrix_fill_constraint_top(pk,po->C,row); po->C->nbrows = pk->dec - 1 + row; - matrix_reduce(po->C); + pk_matrix_reduce(po->C); pk_canonicalize(man,po); man->result.flag_exact = man->result.flag_best = true; return po; @@ -214,8 +214,8 @@ bool pkeq_is_eq(ap_manager_t* man, pkeq_t* pa, pkeq_t* pb) else { size_t i,j; - matrix_t* mata = pa->C; - matrix_t* matb = pb->C; + pk_matrix_t* mata = pa->C; + pk_matrix_t* matb = pb->C; bool res = true; for (i=0; inbrows; i++){ for (j=0; jnbcolumns; j++){ diff --git a/pplite/Makefile b/pplite/Makefile index 9491faa..5a3c8d6 100644 --- a/pplite/Makefile +++ b/pplite/Makefile @@ -55,8 +55,8 @@ CAMLLIB_TO_INSTALL = dllap_pplite_caml.$(EXT_DLL) CAMLLIB_TO_INSTALL_DEBUG = dllap_pplite_caml_debug.$(EXT_DLL) endif -LIBS = -lapron -lpplite -lflint -lgmpxx -lmpfr -lgmp -lm -LIBS_DEBUG = -lapron_debug -lpplite -lflint -lgmpxx -lmpfr -lgmp -lm +LIBS = -lapron -lpplite -lflint -lmpfr -lgmp -lm +LIBS_DEBUG = -lapron_debug -lpplite -lflint -lmpfr -lgmp -lm #--------------------------------------- # Rules diff --git a/pplite/README b/pplite/README index 657ec12..5b20f79 100644 --- a/pplite/README +++ b/pplite/README @@ -3,7 +3,7 @@ # APRON Library / PPLite library # # Copyright (C) Antoine Mine' 2006-2009 -# Copyright (C) Enea Zaffanella 2023 +# Copyright (C) Enea Zaffanella 2023-2024 # This file is part of the APRON Library, released under GPL license. # Please read the COPYING file packaged in the distribution @@ -14,8 +14,8 @@ This package is a wrapper for the PPLite library Requirements: - APRON - ITV -- PPLite library version 0.11 (to be installed from sources) -- Flint, MPFR and GMPXX (the latter normally installed with GMP) +- PPLite library version 0.12 (to be installed from sources) +- Flint, MPFR, GMP - for apron_pplite_test: NewPolka APRON module If HAS_PPLITE is defined in ../Makefile.config, then the main APRON Makefile diff --git a/pplite/ap_pplite.texi b/pplite/ap_pplite.texi index 38329bd..cf5b269 100644 --- a/pplite/ap_pplite.texi +++ b/pplite/ap_pplite.texi @@ -19,7 +19,7 @@ The wrapper offers (variants of) the convex polyhedra abstract domain. @c =================================================================== To use APRON PPLite you need to install PPLite and its dependencies -Flint and GMP; currently, the APRON wrapper requires PPLite version 0.11. +Flint and GMP; currently, the APRON wrapper requires PPLite version 0.12. You need to add @example #include "ap_pplite.h" @@ -33,7 +33,7 @@ using @samp{g++} (instead of @samp{gcc}) because @file{libpplite.a} is a C++ library, adding link options @samp{-L$(APRON_PREFIX)/lib -lap_pplite -L$(PPLITE_PREFIX)/lib -lpplite --L$(FLINT_PREFIX)/lib -lflint -L$(GMP_PREFIX)/lib -lgmpxx} +-L$(FLINT_PREFIX)/lib -lflint} (followed by the standard @samp{-lapron -litvmpq -litvdbl -L$(MPFR_PREFIX)/lib -lmpfr -L$(GMP_PREFIX)/lib -lgmp}). diff --git a/pplite/pplite.idl b/pplite/pplite.idl index 17a608b..f4b2861 100644 --- a/pplite/pplite.idl +++ b/pplite/pplite.idl @@ -292,7 +292,8 @@ ocamlc -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myr {[ocamlopt -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \\ bigarray.cmxa gmp.cmxa apron.cmxa pplite.cmxa mlexample.ml \\ -cclib \"-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib -L$PPLITE_PREFIX/lib\\ - -lap_pplite_caml_debug -lap_pplite_debug -lpplite -lflint -lgmpxx \\ + -lap_pplite_caml_debug -lap_pplite_debug -lpplite \\ + -L$FLINT_PREFIX/lib -lflint \\ -lapron_caml_debug -lapron_debug \\ -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \\ -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \\ diff --git a/pplite/pplite_poly.cc b/pplite/pplite_poly.cc index 176a37e..bdb0275 100644 --- a/pplite/pplite_poly.cc +++ b/pplite/pplite_poly.cc @@ -4,7 +4,7 @@ * APRON Library / PPLite library wrapper * * Copyright (C) Antoine Mine' 2006 - * Copyright (C) 2018-2023 Enea Zaffanella + * Copyright (C) 2018-2024 Enea Zaffanella * */ @@ -105,23 +105,26 @@ to_itv_array(pplite_poly* a) { return { true, nullptr }; auto dim = bbox.space_dim(); auto env = itv_array_alloc(dim); + mpq_t temp; + mpq_init(temp); for (auto i = 0; i != dim; ++i) { if (bbox.inf_ub(i)) bound_set_infty(env[i]->sup, 1); else { - mpq_class ub_i = bbox.ub(i); + mpq_set_Rational(temp, bbox.ub(i)); bound_set_int(env[i]->sup, 0); - numrat_set_mpq(env[i]->sup, ub_i.get_mpq_t()); + numrat_set_mpq(env[i]->sup, temp); } if (bbox.inf_lb(i)) bound_set_infty(env[i]->inf, -1); else { - mpq_class lb_i = bbox.lb(i); + mpq_set_Rational(temp, bbox.lb(i)); bound_set_int(env[i]->inf, 0); - numrat_set_mpq(env[i]->inf, lb_i.get_mpq_t()); + numrat_set_mpq(env[i]->inf, temp); numrat_neg(env[i]->inf, env[i]->inf); } } + mpq_clear(temp); return { false, env }; } diff --git a/pplite/pplite_poly.hh b/pplite/pplite_poly.hh index 6a4e31f..45df2bd 100644 --- a/pplite/pplite_poly.hh +++ b/pplite/pplite_poly.hh @@ -6,7 +6,7 @@ * Wrappers specific to the PPLite domains. * * Copyright (C) Antoine Mine' 2006 - * Copyright (C) 2018-2023 Enea Zaffanella + * Copyright (C) 2018-2024 Enea Zaffanella * */ diff --git a/pplite/pplite_user.cc b/pplite/pplite_user.cc index 262c17d..23670da 100644 --- a/pplite/pplite_user.cc +++ b/pplite/pplite_user.cc @@ -4,7 +4,7 @@ * APRON Library / PPLite library wrapper * * Copyright (C) Antoine Mine' 2006 - * Copyright (C) 2018-2023 Enea Zaffanella + * Copyright (C) 2018-2024 Enea Zaffanella * */ @@ -66,21 +66,23 @@ to_generator(const Gen& g, bool& exact) { Cons to_Cons(ap_interval_t** a, size_t intdim, size_t realdim, bool& exact) { exact = true; - mpq_class temp; size_t nb = intdim+realdim; - mpq_ptr mpq = temp.get_mpq_t(); + mpq_t temp; + mpq_init(temp); + mpz_ptr temp_num = mpq_numref(temp); + mpz_ptr temp_den = mpq_denref(temp); Cons r; for (size_t i = 0; i < nb; ++i) { /* inf */ switch (ap_scalar_infty(a[i]->inf)) { case 0: - exact = !ap_mpq_set_scalar(mpq,a[i]->inf, GMP_RNDD) && exact; + exact = !ap_mpq_set_scalar(temp, a[i]->inf, GMP_RNDD) && exact; if (i < intdim) { - mpz_fdiv_q(mpq_numref(mpq), mpq_numref(mpq), mpq_denref(mpq)); - mpz_set_ui(mpq_denref(mpq), 1); + mpz_fdiv_q(temp_num, temp_num, temp_den); + mpz_set_ui(temp_den, 1); } - r.push_back(Integer(temp.get_den()) * Var(i) >= Integer(temp.get_num())); + r.push_back(Integer(temp_den) * Var(i) >= Integer(temp_num)); break; case -1: break; @@ -88,6 +90,7 @@ to_Cons(ap_interval_t** a, size_t intdim, size_t realdim, bool& exact) { r.clear(); r.push_back(Con::zero_dim_false()); exact = true; + mpq_clear(temp); return r; default: assert(false); @@ -95,12 +98,12 @@ to_Cons(ap_interval_t** a, size_t intdim, size_t realdim, bool& exact) { /* sup */ switch (ap_scalar_infty(a[i]->sup)) { case 0: - exact = !ap_mpq_set_scalar(mpq,a[i]->sup, GMP_RNDU) && exact; + exact = !ap_mpq_set_scalar(temp, a[i]->sup, GMP_RNDU) && exact; if (i + * Copyright (C) 2018-2024 Enea Zaffanella * */ @@ -39,6 +39,29 @@ namespace apron { */ class cannot_convert: public std::exception {}; + +/**********************************************/ +/* Conversions from PPLite to GMP mpz_t/mpq_t */ +/* (backward compatibility helpers) */ +/**********************************************/ + +inline void mpz_set_Integer(mpz_t z, const Integer& i) { +#ifdef HAVE_PPLITE_0_11 + mpz_set(z, i); +#else + i.get_mpz(z); +#endif +} + +inline void mpq_set_Rational(mpq_t q, const Rational& r) { + // No need to canonicalize +#ifdef HAVE_PPLITE_0_11 + mpq_set(q, mpq_class(r).get_mpq_t()); +#else + r.get_mpq(q); +#endif +} + /************************************/ /* Conversions from PPLite to Apron */ /************************************/ @@ -47,7 +70,7 @@ class cannot_convert: public std::exception {}; inline void to_scalar(ap_scalar_t* s, const Integer& i) { ap_scalar_reinit(s, AP_SCALAR_MPQ); - mpz_set(mpq_numref(s->val.mpq), i); + mpz_set_Integer(mpq_numref(s->val.mpq), i); mpz_set_ui(mpq_denref(s->val.mpq), 1); } @@ -56,8 +79,8 @@ inline void to_scalar(ap_scalar_t* s, const Integer& n, const Integer& d) { ap_scalar_reinit(s, AP_SCALAR_MPQ); - mpz_set(mpq_numref(s->val.mpq), n); - mpz_set(mpq_denref(s->val.mpq), d); + mpz_set_Integer(mpq_numref(s->val.mpq), n); + mpz_set_Integer(mpq_denref(s->val.mpq), d); mpq_canonicalize(s->val.mpq); } @@ -65,9 +88,7 @@ to_scalar(ap_scalar_t* s, inline void to_scalar(ap_scalar_t* s, const Rational& r) { ap_scalar_reinit(s, AP_SCALAR_MPQ); - mpz_set(mpq_numref(s->val.mpq), r.get_num()); - mpz_set(mpq_denref(s->val.mpq), r.get_den()); - // No need to canonicalize + mpq_set_Rational(s->val.mpq, r); } /* Con::Type => ap_constyp_t */