From ae1856ee0c2b9e4fd2be1a049d68950d1972dc59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 27 Jun 2023 10:51:12 +0200 Subject: [PATCH 01/24] Fix for sat_tcons (#31). --- itv/itv_linearize.c | 16 ++++++++-------- itv/itv_linexpr.c | 8 ++++---- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/itv/itv_linearize.c b/itv/itv_linearize.c index bf27e513..5864539e 100644 --- a/itv/itv_linearize.c +++ b/itv/itv_linearize.c @@ -1544,24 +1544,24 @@ ITVFUN(itv_intlinearize_ap_tcons0)(itv_internal_t* intern, itv_init(bound); itv_intlinearize_texpr0_rec(intern,cons->texpr0,env,intdim,&res->linexpr,i); - /* checks that the contraint is satisfiable */ + /* checks that the constraint is satisfiable */ switch (cons->constyp){ case AP_CONS_EQ: itv_set_int(bound,0); - itv_meet(intern,i,i,bound); + itv_meet(intern,bound,i,bound); break; case AP_CONS_SUPEQ: case AP_CONS_SUP: itv_set_top(bound); bound_set_int(bound->inf,0); bound_set_infty(bound->sup,1); - itv_meet(intern,i,i,bound); + itv_meet(intern,bound,i,bound); break; default: break; } - if (!itv_is_bottom(intern,i) && !itv_is_bottom(intern,res->linexpr.cst)) { + if (!itv_is_bottom(intern,bound) && !itv_is_bottom(intern,res->linexpr.cst)) { if (res->linexpr.size==0){ itv_meet(intern,res->linexpr.cst,res->linexpr.cst,i); res->linexpr.equality = itv_is_point(intern,res->linexpr.cst); @@ -1609,24 +1609,24 @@ ITVFUN(itv_intlinearize_ap_tcons0_array)(itv_internal_t* intern, num_set_int(res->p[i].num,0); } - /* checks that the contraint is satisfiable */ + /* checks that the constraint is satisfiable */ switch (array->p[i].constyp){ case AP_CONS_EQ: itv_set_int(bound,0); - itv_meet(intern,itv,itv,bound); + itv_meet(intern,bound,itv,bound); break; case AP_CONS_SUPEQ: case AP_CONS_SUP: itv_set_top(bound); bound_set_int(bound->inf,0); bound_set_infty(bound->sup,1); - itv_meet(intern,itv,itv,bound); + itv_meet(intern,bound,itv,bound); break; default: break; } - if (itv_is_bottom(intern,itv) || + if (itv_is_bottom(intern,bound) || itv_is_bottom(intern,res->p[i].linexpr.cst) || (res->p[i].linexpr.size==0 ? itv_eval_cstlincons(intern,&res->p[i])==tbool_false : diff --git a/itv/itv_linexpr.c b/itv/itv_linexpr.c index c4ab9c20..1231e220 100644 --- a/itv/itv_linexpr.c +++ b/itv/itv_linexpr.c @@ -39,7 +39,7 @@ void ITVFUN(itv_linexpr_set)(itv_linexpr_t* res, itv_linexpr_t* expr) for (i=expr->size; isize; i++){ itv_linterm_clear(&res->linterm[i]); } - res->linterm = realloc(res->linterm,expr->size*sizeof(itv_linterm_t)); + res->linterm = realloc(res->linterm, expr->size ? expr->size*sizeof(itv_linterm_t) : 1); size = res->size < expr->size ? res->size : expr->size; for (i=0;ilinterm[i],&expr->linterm[i]); @@ -57,7 +57,7 @@ void ITVFUN(itv_linexpr_reinit)(itv_linexpr_t* expr, size_t size) for (i=size; isize; i++){ itv_linterm_clear(&expr->linterm[i]); } - expr->linterm = realloc(expr->linterm,size*sizeof(itv_linterm_t)); + expr->linterm = realloc(expr->linterm, size ? size*sizeof(itv_linterm_t) : 1); for (i=expr->size;ilinterm[i]); } @@ -145,10 +145,10 @@ void ITVFUN(itv_lincons_array_reinit)(itv_lincons_array_t* array, size_t size) for (i=size; isize; i++){ itv_lincons_clear(&array->p[i]); } - array->p = realloc(array->p,size*sizeof(itv_lincons_t)); + array->p = realloc(array->p, size ? size*sizeof(itv_lincons_t) : 1); } else { /* size > array->size */ - array->p = realloc(array->p,size*sizeof(itv_lincons_t)); + array->p = realloc(array->p, size ? size*sizeof(itv_lincons_t) : 1); for (i=array->size; ip[i]); } From d02d7802f7879c29c43ce31d7040d6c767d871f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 4 Jul 2023 19:37:30 +0200 Subject: [PATCH 02/24] Replace GPL quicksort with an original (LGPL) implementation. --- newpolka/Makefile | 3 +- newpolka/mf_qsort.c | 210 ----------------------------------------- newpolka/mf_qsort.h | 22 ----- newpolka/pk_matrix.c | 15 ++- newpolka/pk_qsort.h | 73 ++++++++++++++ newpolka/pk_widening.c | 9 +- 6 files changed, 85 insertions(+), 247 deletions(-) delete mode 100644 newpolka/mf_qsort.c delete mode 100644 newpolka/mf_qsort.h create mode 100644 newpolka/pk_qsort.h diff --git a/newpolka/Makefile b/newpolka/Makefile index 536f93ef..f3a0eaec 100644 --- a/newpolka/Makefile +++ b/newpolka/Makefile @@ -18,7 +18,6 @@ CMXSINC = $(APRON_CMXSINC) -I . #--------------------------------------- CCMODULES = \ -mf_qsort \ pk_user pk_internal pk_bit pk_satmat pk_vector pk_matrix pk_cherni \ pk_representation pk_approximate pk_constructor pk_test pk_extract \ pk_meetjoin pk_assign pk_project pk_resize pk_expandfold \ @@ -27,7 +26,7 @@ pkeq CCINC = \ pk_config.h pk.h pkeq.h \ -mf_qsort.h pk_internal.h \ +pk_qsort.h pk_internal.h \ pk_user.h pk_bit.h pk_satmat.h pk_vector.h pk_matrix.h pk_cherni.h \ pk_representation.h pk_constructor.h pk_test.h pk_extract.h \ pk_meetjoin.h pk_assign.h pk_resize.h diff --git a/newpolka/mf_qsort.c b/newpolka/mf_qsort.c deleted file mode 100644 index 242b7bd6..00000000 --- a/newpolka/mf_qsort.c +++ /dev/null @@ -1,210 +0,0 @@ -/* Copyright (C) 2000 MySQL AB - - This program is free software; you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation; either version 2 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program; if not, write to the Free Software - Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA */ - -/* Modified by Bertrand Jeannet */ - -/* - qsort implementation optimized for comparison of pointers - Inspired by the qsort implementations by Douglas C. Schmidt, - and Bentley & McIlroy's "Engineering a Sort Function". -*/ - -#include -#include -#include "mf_qsort.h" - - -#define QSORT_EXTRA_CMP_ARGUMENT - -/* We need to use qsort with 2 different compare functions */ -#ifdef QSORT_EXTRA_CMP_ARGUMENT -#define CMP(A,B) ((*cmp)(cmp_argument,(A),(B))) -#else -#define CMP(A,B) ((*cmp)((A),(B))) -#endif - -#define SWAP(A, B, size,swap_ptrs) \ -do { \ - if (swap_ptrs) \ - { \ - char **a = (char**) (A), **b = (char**) (B); \ - char *tmp = *a; *a++ = *b; *b++ = tmp; \ - } \ - else \ - { \ - char *a = (A), *b = (B); \ - char *end= a+size; \ - do \ - { \ - char tmp = *a; *a++ = *b; *b++ = tmp; \ - } while (a < end); \ - } \ -} while (0) - -/* Put the median in the middle argument */ -#define MEDIAN(low, mid, high) \ -{ \ - if (CMP(high,low) < 0) \ - SWAP(high, low, size, ptr_cmp); \ - if (CMP(mid, low) < 0) \ - SWAP(mid, low, size, ptr_cmp); \ - else if (CMP(high, mid) < 0) \ - SWAP(mid, high, size, ptr_cmp); \ -} - -/* The following node is used to store ranges to avoid recursive calls */ - -typedef struct st_stack -{ - char *low,*high; -} stack_node; - -#define PUSH(LOW,HIGH) {stack_ptr->low = LOW; stack_ptr++->high = HIGH;} -#define POP(LOW,HIGH) {LOW = (--stack_ptr)->low; HIGH = stack_ptr->high;} - -/* The following stack size is enough for ulong ~0 elements */ -#define STACK_SIZE (8 * sizeof(unsigned long int)) -#define THRESHOLD_FOR_INSERT_SORT 10 - -/**************************************************************************** -** 'standard' quicksort with the following extensions: -** -** Can be compiled with the qsort2_cmp compare function -** Store ranges on stack to avoid recursion -** Use insert sort on small ranges -** Optimize for sorting of pointers (used often by MySQL) -** Use median comparison to find partition element -*****************************************************************************/ - -#ifdef QSORT_EXTRA_CMP_ARGUMENT -void qsort2(void *base_ptr, size_t count, size_t size, qsort2_cmp cmp, - void *cmp_argument) -#else -void qsort(void *base_ptr, size_t count, size_t size, qsort_cmp cmp) -#endif -{ - char *low, *high, *pivot; - stack_node stack[STACK_SIZE], *stack_ptr; - char ptr_cmp; - /* Handle the simple case first */ - /* This will also make the rest of the code simpler */ - if (count <= 1) - return; - - low = (char*) base_ptr; - high = low + size * (count - 1); - stack_ptr = stack + 1; - pivot = (char *) malloc(size); - ptr_cmp= size == sizeof(char*) && !((low - (char*) 0)& (sizeof(char*)-1)); - - /* The following loop sorts elements between high and low */ - do - { - char *low_ptr, *high_ptr, *mid; - - count=((size_t) (high - low) / size)+1; - /* If count is small, then an insert sort is faster than qsort */ - if (count < THRESHOLD_FOR_INSERT_SORT) - { - for (low_ptr = low + size; low_ptr <= high; low_ptr += size) - { - char *ptr; - for (ptr = low_ptr; ptr > low && CMP(ptr - size, ptr) > 0; - ptr -= size) - SWAP(ptr, ptr - size, size, ptr_cmp); - } - POP(low, high); - continue; - } - - /* Try to find a good middle element */ - mid= low + size * (count >> 1); - if (count > 40) /* Must be bigger than 24 */ - { - size_t step = size* (count / 8); - MEDIAN(low, low + step, low+step*2); - MEDIAN(mid - step, mid, mid+step); - MEDIAN(high - 2 * step, high-step, high); - /* Put best median in 'mid' */ - MEDIAN(low+step, mid, high-step); - low_ptr = low; - high_ptr = high; - } - else - { - MEDIAN(low, mid, high); - /* The low and high argument are already in sorted against 'pivot' */ - low_ptr = low + size; - high_ptr = high - size; - } - memcpy(pivot, mid, size); - - do - { - while (CMP(low_ptr, pivot) < 0) - low_ptr += size; - while (CMP(pivot, high_ptr) < 0) - high_ptr -= size; - - if (low_ptr < high_ptr) - { - SWAP(low_ptr, high_ptr, size, ptr_cmp); - low_ptr += size; - high_ptr -= size; - } - else - { - if (low_ptr == high_ptr) - { - low_ptr += size; - high_ptr -= size; - } - break; - } - } - while (low_ptr <= high_ptr); - - /* - Prepare for next iteration. - Skip partitions of size 1 as these doesn't have to be sorted - Push the larger partition and sort the smaller one first. - This ensures that the stack is keept small. - */ - - if ((int) (high_ptr - low) <= 0) - { - if ((int) (high - low_ptr) <= 0) - { - POP(low, high); /* Nothing more to sort */ - } - else - low = low_ptr; /* Ignore small left part. */ - } - else if ((int) (high - low_ptr) <= 0) - high = high_ptr; /* Ignore small right part. */ - else if ((high_ptr - low) > (high - low_ptr)) - { - PUSH(low, high_ptr); /* Push larger left part */ - low = low_ptr; - } - else - { - PUSH(low_ptr, high); /* Push larger right part */ - high = high_ptr; - } - } while (stack_ptr > stack); - free(pivot); -} diff --git a/newpolka/mf_qsort.h b/newpolka/mf_qsort.h deleted file mode 100644 index 80a208bf..00000000 --- a/newpolka/mf_qsort.h +++ /dev/null @@ -1,22 +0,0 @@ -/* ********************************************************************** */ -/* mf_qsort.h: quicksort */ -/* ********************************************************************** */ - -#include - -#ifdef __cplusplus -extern "C" { -#endif - -#define QSORT_EXTRA_CMP_ARGUMENT - -typedef int (*qsort2_cmp)(void*, void *, void *); - -void qsort2(void *base_ptr, size_t count, size_t size, - qsort2_cmp cmp, - void *cmp_argument); - -#ifdef __cplusplus -} -#endif - diff --git a/newpolka/pk_matrix.c b/newpolka/pk_matrix.c index efc81326..a3e6d8a6 100644 --- a/newpolka/pk_matrix.c +++ b/newpolka/pk_matrix.c @@ -12,7 +12,7 @@ #include "pk_vector.h" #include "pk_satmat.h" #include "pk_matrix.h" -#include "mf_qsort.h" +#include "pk_qsort.h" /* ********************************************************************** */ /* I. basic operations: creation, destruction, copying and printing */ @@ -304,6 +304,8 @@ static int qsort_rows_compar(void* qsort_man, void* pq1, void* pq2) return vector_compare(qm->pk,q1,q2,qm->size); } +MAKE_SORT(qsort_rows, numint_t*, qsort_rows_compar) + void matrix_sort_rows(pk_internal_t* pk, matrix_t* mat) { @@ -312,9 +314,7 @@ void matrix_sort_rows(pk_internal_t* pk, if (!mat->_sorted){ qsort_man.pk = pk; qsort_man.size = mat->nbcolumns; - qsort2(mat->p, mat->nbrows, sizeof(numint_t*), - qsort_rows_compar, - &qsort_man); + qsort_rows(mat->p, mat->nbrows, &qsort_man); mat->_sorted = true; } } @@ -338,6 +338,8 @@ static int qsort_rows_with_sat_compar(void* qsort_man, void* q1, void* q2) qm->size ); } +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) { @@ -353,10 +355,7 @@ void matrix_sort_rows_with_sat(pk_internal_t* pk, qsort_tab[i].p = mat->p[i]; qsort_tab[i].satp = sat->p[i]; } - qsort2(qsort_tab, - mat->nbrows, sizeof(qsort_t), - qsort_rows_with_sat_compar, - &qsort_man); + qsort_rows_with_sat(qsort_tab, mat->nbrows, &qsort_man); for (i=0; inbrows; i++){ mat->p[i] = qsort_tab[i].p; sat->p[i] = qsort_tab[i].satp; diff --git a/newpolka/pk_qsort.h b/newpolka/pk_qsort.h new file mode 100644 index 00000000..31ca98ec --- /dev/null +++ b/newpolka/pk_qsort.h @@ -0,0 +1,73 @@ +/* ********************************************************************** */ +/* pk_qsort.h: generic sort */ +/* ********************************************************************** */ + +/* This file is part of the APRON Library, released under LGPL license + with an exception allowing the redistribution of statically linked + executables. + + Please read the COPYING file packaged in the distribution */ + +#ifndef __PK_QSORT_H__ +#define __PK_QSORT_H__ + +#define MAKE_SORT(NAME, TYPE, CMP) \ + \ + static void NAME(TYPE* data, size_t size, void* param) { \ + \ + if (size >= 12) { \ + \ + /* choose pivot: median of begining, middle, end */ \ + TYPE* beg = data; \ + TYPE* mid = data + (size/2); \ + TYPE* end = data + (size-1); \ + TYPE pivot; \ + if (CMP(param, beg, mid) <= 0) { \ + if (CMP(param, mid, end) <= 0) \ + pivot = *mid; /* beg <= mid <= end */ \ + else if (CMP(param, beg, end) <= 0) \ + pivot = *end; /* beg <= end < mid */ \ + else \ + pivot = *beg; /* end < beg < mid */ \ + } \ + else { \ + if (CMP(param, end, mid) <= 0) \ + pivot = *mid; /* end <= mid < beg */ \ + else if (CMP(param, end, beg) <= 0) \ + pivot = *end; /* mid < end <= beg */ \ + else \ + pivot = *beg; /* mid < beg < end */ \ + } \ + \ + /* partition */ \ + while (true) { \ + while (CMP(param, beg, &pivot) < 0) beg++; \ + while (CMP(param, &pivot, end) < 0) end--; \ + if (beg >= end) break; \ + TYPE x = *beg; *beg = *end; *end = x; \ + beg++; end--; \ + } \ + \ + /* recursive calls */ \ + if (end+1 > data) NAME(data, end-data+1, param); \ + if (data+size > end+1) NAME(end+1, data+size-end-1, param); \ + } \ + \ + else if (size > 1) { \ + /* simple insertion sort */ \ + for (TYPE* p = data+1; p < data+size; p++) { \ + for (TYPE* q = p; q > data && CMP(param, q-1, q) > 0; q--) { \ + TYPE x = *(q-1); *(q-1) = *q; *q = x; \ + } \ + } \ + } \ + } \ + \ + static void checked_##NAME(TYPE* data, size_t size, void* param) { \ + NAME(data, size, param); \ + for (size_t i = 0; i + 1 < size; i++) { \ + assert(CMP(param, data+i, data+i+1) <= 0); \ + } \ + } + +#endif diff --git a/newpolka/pk_widening.c b/newpolka/pk_widening.c index 86c6ef26..69a6d71e 100644 --- a/newpolka/pk_widening.c +++ b/newpolka/pk_widening.c @@ -19,8 +19,7 @@ #include "pk_user.h" #include "pk_constructor.h" #include "pk_test.h" - -#include "mf_qsort.h" +#include "pk_qsort.h" typedef struct satmat_row_t { bitstring_t* p; @@ -76,14 +75,14 @@ static int qsort_rows_compar(void* qsort_man, void* p1, void* p2) qm->size)); } +MAKE_SORT(qsort_rows, satmat_row_t, qsort_rows_compar) + static void esatmat_sort_rows(satmat_row_t* tab, satmat_t* sat) { if (sat->nbrows>=6){ qsort_man_t qsort_man; qsort_man.size = sat->nbcolumns; - qsort2(tab, - (size_t)sat->nbrows, sizeof(satmat_row_t), - qsort_rows_compar, &qsort_man); + qsort_rows(tab, (size_t)sat->nbrows, &qsort_man); } else { esatmat_isort_rows(tab,sat); From 6c2f2f0b3f8ae299dc9941b83d4ae927ec63d1d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 4 Jul 2023 22:23:01 +0200 Subject: [PATCH 03/24] qsort test --- newpolka/pk_qsort.h | 2 +- test/sorttest.c | 91 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+), 1 deletion(-) create mode 100644 test/sorttest.c diff --git a/newpolka/pk_qsort.h b/newpolka/pk_qsort.h index 31ca98ec..c6480b8a 100644 --- a/newpolka/pk_qsort.h +++ b/newpolka/pk_qsort.h @@ -40,7 +40,7 @@ } \ \ /* partition */ \ - while (true) { \ + while (1) { \ while (CMP(param, beg, &pivot) < 0) beg++; \ while (CMP(param, &pivot, end) < 0) end--; \ if (beg >= end) break; \ diff --git a/test/sorttest.c b/test/sorttest.c new file mode 100644 index 00000000..b1d63e27 --- /dev/null +++ b/test/sorttest.c @@ -0,0 +1,91 @@ +#include +#include +#include +#include + +#include "../newpolka/pk_qsort.h" + +int cmp_int(void* unused, int* a, int* b) { + return (*a > *b) ? 1 : (*a < *b) ? -1 : 0; +} + +MAKE_SORT(sort_int, int, cmp_int) + +int sum(int* a, size_t size) { + int x = 0; + for (size_t i = 0; i < size; i++) x += a[i]; + return x; +} + +void check_cst_array(size_t size) { + int x = lrand48(); + int* a = malloc(sizeof(int)*size); + for (size_t i = 0; i < size; i++) + a[i] = x; + int s = sum(a,size); + checked_sort_int(a, size, NULL); + assert(s == sum(a,size)); + free(a); +} + +void check_inc_array(size_t size) { + int* a = malloc(sizeof(int)*size); + for (size_t i = 0; i < size; i++) + a[i] = i; + int s = sum(a,size); + checked_sort_int(a, size, NULL); + assert(s == sum(a,size)); + free(a); +} + +void check_dec_array(size_t size) { + int* a = malloc(sizeof(int)*size); + for (size_t i = 0; i < size; i++) + a[i] = size-i; + int s = sum(a,size); + checked_sort_int(a, size, NULL); + assert(s == sum(a,size)); + free(a); +} + +void check_rnd_array(size_t size, int max_rand) { + int* a = malloc(sizeof(int)*size); + for (size_t i = 0; i < size; i++) + a[i] = lrand48() & max_rand; + int s = sum(a,size); + checked_sort_int(a, size, NULL); + assert(s == sum(a,size)); + free(a); +} + + +int main() { + for (int i = 0; i < 1000; i++) { + printf("check constant array of size %i\n",i); + check_cst_array(i); + } + for (int i = 1; i < 1000; i++) { + printf("check increasing array of size %i\n",i); + check_inc_array(i); + } + for (int i = 1; i < 1000; i++) { + printf("check decreasing array of size %i\n",i); + check_dec_array(i); + } + for (int i = 1; i < 1000; i++) { + printf("check random array of size %i\n",i); + for (int j = i/2; j < i*2; j += 2) { + check_rnd_array(i, j); + } + for (int j = 0; j < 1000; j++) { + check_rnd_array(i, INT_MAX); + } + } + for (int i = 1000; i < 1000000; i = i*4/3) { + printf("check random array of size %i\n",i); + for (int j = 0; j < 100; j++) { + check_rnd_array(i, INT_MAX); + } + } + return 0; +} From cc9b5b464445a4d1e1ab47c1028b4035c9960495 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 27 Jun 2023 23:24:39 +0200 Subject: [PATCH 04/24] Install debug libraries only if -debug is passed to ./configure. Strip non-debug libraries. --- Makefile | 18 ++++++------- Makefile.config.model | 1 + apron.opam | 2 ++ apron/Makefile | 13 ++++++--- apronxx/Makefile | 13 ++++++++- avoct/Makefile | 61 ++++++++++++++++++++++++++++++++----------- box/Makefile | 57 +++++++++++++++++++++++++--------------- configure | 14 ++++++++++ fppol/Makefile | 59 ++++++++++++++++++++++++++++++----------- itv/Makefile | 55 ++++++++++++++++++++++++++++---------- japron/Makefile | 2 +- mlapronidl/Makefile | 13 ++++++--- newpolka/Makefile | 33 +++++++++++++++-------- octagons/Makefile | 58 ++++++++++++++++++++++++++++++---------- ppl/Makefile | 42 ++++++++++++++++++++++++----- pplite/Makefile | 41 ++++++++++++++++++++++++----- products/Makefile | 40 +++++++++++++++++++--------- taylor1plus/Makefile | 29 ++++++++++++++------ 18 files changed, 409 insertions(+), 142 deletions(-) diff --git a/Makefile b/Makefile index 86504ac5..bd9cb119 100755 --- a/Makefile +++ b/Makefile @@ -78,8 +78,10 @@ apronglpktop: rebuild: @echo "$(MAKE) rebuild is no longer necessary" -OCAMLFIND_PROTO = xxx.cma $(call OCAMLOPT_TARGETS, xxx) libxxx_caml.a \ - libxxx_caml_debug.a +OCAMLFIND_PROTO = xxx.cma $(call OCAMLOPT_TARGETS, xxx) libxxx_caml.a +ifneq ($(HAS_DEBUG),) +OCAMLFIND_PROTO += $(call OCAMLOPT_TARGETS, xxx.d) libxxx_caml_debug.a +endif ifneq ($(HAS_SHARED),) OCAMLFIND_PROTO += dllxxx_caml.$(EXT_DLL) endif @@ -111,13 +113,13 @@ disjunction) \ ifneq ($(HAS_PPL),) OCAMLFIND_FILES += \ - $(patsubst %,ppl/%, ppl.idl ppl.mli ppl.cmi ppl.cma ppl.cmx $(call OCAMLOPT_TARGETS, ppl) libap_ppl_caml.a libap_ppl_caml_debug.a dllap_ppl_caml.$(EXT_DLL)) \ + $(patsubst %,ppl/%, ppl.idl ppl.mli ppl.cmi ppl.cma ppl.cmx $(call OCAMLOPT_TARGETS, ppl) libap_ppl_caml.a dllap_ppl_caml.$(EXT_DLL)) \ $(patsubst %,products/%, polkaGrid.idl polkaGrid.mli polkaGrid.cmi polkaGrid.cmx) \ $(patsubst %,products/%, $(subst xxx,polkaGrid, $(OCAMLFIND_PROTO))) endif ifneq ($(HAS_PPLITE),) OCAMLFIND_FILES += \ - $(patsubst %,pplite/%, pplite.idl pplite.mli pplite.cmi pplite.cma pplite.cmx $(call OCAMLOPT_TARGETS, pplite) libap_pplite_caml.a libap_pplite_caml_debug.a dllap_pplite_caml.$(EXT_DLL)) + $(patsubst %,pplite/%, pplite.idl pplite.mli pplite.cmi pplite.cma pplite.cmx $(call OCAMLOPT_TARGETS, pplite) libap_pplite_caml.a dllap_pplite_caml.$(EXT_DLL)) endif ifneq ($(HAS_GLPK),) OCAMLFIND_FILES += \ @@ -184,11 +186,7 @@ ifneq ($(HAS_GLPK),) endif else $(OCAMLFIND) remove apron - $(OCAMLFIND) install apron mlapronidl/META $(OCAMLFIND_FILES) \ - $(call OCAMLOPT_TARGETS, mlapronidl/apron.d \ - newpolka/polkaMPQ.d \ - newpolka/polkaRll.d \ - taylor1plus/t1pMPQ.d taylor1plus/t1pD.d taylor1plus/t1pMPFR.d) + $(OCAMLFIND) install apron mlapronidl/META $(OCAMLFIND_FILES) endif endif ifneq ($(HAS_CPP),) @@ -199,7 +197,7 @@ ifneq ($(HAS_JAVA),) endif ifneq ($(OCAMLFIND),) -install: mlapronidl/META +ml: mlapronidl/META mlapronidl/META: mlapronidl/META.in mlapronidl/META.ppl.in mlapronidl/META.pplite.in $(SED) -e "s!@VERSION@!$(VERSION_STR)!g;" $< > $@; ifneq ($(HAS_PPL),) diff --git a/Makefile.config.model b/Makefile.config.model index ded020b6..060b976c 100755 --- a/Makefile.config.model +++ b/Makefile.config.model @@ -182,6 +182,7 @@ RANLIB = ranlib SED = sed PERL = perl INSTALL = install +INSTALLSTRIP = install --strip INSTALLd = install -d OCAMLC = ocamlc.opt diff --git a/apron.opam b/apron.opam index 70d0b4d1..64e6cbc2 100644 --- a/apron.opam +++ b/apron.opam @@ -17,6 +17,7 @@ build: [ "--prefix" "%{share}%/apron" "--no-ppl" {!conf-ppl:installed} + "--no-pplite" {!conf-pplite:installed} "--no-ocaml-plugins" {os = "freebsd"} "--absolute-dylibs" {os = "macos"} "--ext-dll" {os = "win32"} "dll" {os = "win32"} @@ -36,6 +37,7 @@ depends: [ ] depopts: [ "conf-ppl" + "conf-pplite" ] description:""" Apron is a library to represent properties of numeric variables, such as variable bounds or linear relations between variables, and to manipulate these properties through semantic operations, such as variable assignments, tests, conjunctions, entailment. Apron is intended to be used in static program analyzers, in order to infer invariants of numeric variables, i.e., properties that hold for all executions of a program. It is based on the theory of Abstract Interpretation.""" diff --git a/apron/Makefile b/apron/Makefile index 669a3a6d..a4bbf5c8 100644 --- a/apron/Makefile +++ b/apron/Makefile @@ -53,12 +53,14 @@ LDFLAGS += $(MP_LIFLAGS) -lm -lmpfr -lgmp # Rules #--------------------------------------- -LIB_FILES = libapron.a libapron_debug.a +LIB_FILES = libapron.a +LIB_FILES_DEBUG = libapron_debug.a ifneq ($(HAS_SHARED),) -LIB_FILES += libapron.$(EXT_DLL) libapron_debug.$(EXT_DLL) +LIB_FILES += libapron.$(EXT_DLL) +LIB_FILES_DEBUG += libapron_debug.$(EXT_DLL) endif -all: $(LIB_FILES) +all: $(LIB_FILES) $(LIB_FILES_DEBUG) #--------------------------------------- # Misc rules @@ -82,7 +84,10 @@ install: all mkdir -p $(APRON_INCLUDE) cp $(H_FILES) $(APRON_INCLUDE) mkdir -p $(APRON_LIB) - for i in $(LIB_FILES); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done + for i in $(LIB_FILES); do if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; done +ifneq ($(HAS_DEBUG),) + for i in $(LIB_FILES_DEBUG); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done +endif uninstall: /bin/rm -f $(H_FILES:%=$(APRON_INCLUDE)/%) diff --git a/apronxx/Makefile b/apronxx/Makefile index 2ad3c3fb..4359b94d 100644 --- a/apronxx/Makefile +++ b/apronxx/Makefile @@ -52,6 +52,14 @@ CCINC = \ LIBS = $(LDFLAGS) -lapron -lmpfr -lgmpxx -lgmp -lm LIBS_DEBUG = $(LDFLAGS) -lapron_debug -lmpfr -lgmpxx -lgmp -lm +CCLIB_TO_INSTALL = libapronxx.a +CCLIB_TO_INSTALL_DEBUG = libapronxx_debug.a + +ifneq ($(HAS_SHARED),) +CCLIB_TO_INSTALL += libapronxx.$(EXT_DLL) +CCLIB_TO_INSTALL_DEBUG += libapronxx_debug.$(EXT_DLL) +endif + ifneq ($(HAS_PPL),) DEFS := $(DEFS) -DHAS_PPL LIBS := $(LIBS) $(PPL_LIFLAGS) -L../ppl -L../products -lap_pkgrid -lap_ppl -lppl @@ -77,7 +85,10 @@ distclean: clean install: $(INSTALLd) $(APRON_INCLUDE) $(APRON_INCLUDE)/apronxx $(APRON_LIB) $(INSTALL) $(CCINC) $(APRON_INCLUDE)/apronxx - $(INSTALL) libapronxx.* libapronxx_debug.* $(APRON_LIB) + $(INSTALLSTRIP) $(CCLIB_TO_INSTALL) $(APRON_LIB) +ifneq ($(HAS_DEBUG),) + $(INSTALL) $(CCLIB_TO_INSTALL_DEBUG) $(APRON_LIB) +endif uninstall: /bin/rm -rf $(APRON_INCLUDE)/apronxx diff --git a/avoct/Makefile b/avoct/Makefile index 0cf501d3..e19bb320 100755 --- a/avoct/Makefile +++ b/avoct/Makefile @@ -40,6 +40,24 @@ CCINC = avo_internal.h avo_fun.h LIBS = -lapron -lmpfr -lgmp -lm LIBS_DEBUG = -lapron_debug -lmpfr -lgmp -lm +CCLIB_TO_INSTALL = libavoIl.a libavoIll.a libavoMPZ.a libavoRl.a libavoRll.a libavoMPQ.a libavoD.a libavoDl.a libavoMPFR.a +CCLIB_TO_INSTALL_DEBUG = libavoIl_debug.a libavoIll_debug.a libavoMPZ_debug.a libavoRl_debug.a libavoRll_debug.a libavoMPQ_debug.a libavoD_debug.a libavoDl_debug.a libavoMPFR_debug.a +CAMLLIB_TO_INSTALL = libavoIl_caml.a libavoIll_caml.a libavoMPZ_caml.a libavoRl_caml.a libavoRll_caml.a libavoMPQ_caml.a libavoD_caml.a libavoDl_caml.a libavoMPFR_caml.a +CAMLLIB_TO_INSTALL_DEBUG = libavoIl_caml_debug.a libavoIll_caml_debug.a libavoMPZ_caml_debug.a libavoRl_caml_debug.a libavoRll_caml_debug.a libavoMPQ_caml_debug.a libavoD_caml_debug.a libavoDl_caml_debug.a libavoMPFR_caml_debug.a + +ifneq ($(HAS_OCAMLOPT),) +CAMLLIB_TO_INSTALL += $(call OCAMLOPT_TARGETS, avoIl avoIll avoMPZ avoRl avoRll avoMPQ avoD avoDl avoMPFR) +CAMLLIB_TO_INSTALL_DEBUG += $(call OCAMLOPT_TARGETS, avoIl.d avoIll.d avoMPZ.d avoRl.d avoRll.d avoMPQ.d avoD.d avoDl.d avoMPFR.d) +endif + +ifneq ($(HAS_SHARED),) +CCLIB_TO_INSTALL += libavoIl.$(EXT_DLL) libavoIll.$(EXT_DLL) libavoMPZ.$(EXT_DLL) libavoRl.$(EXT_DLL) libavoRll.$(EXT_DLL) libavoMPQ.$(EXT_DLL) libavoD.$(EXT_DLL) libavoDl.$(EXT_DLL) libavoMPFR.$(EXT_DLL) +CCLIB_TO_INSTALL_DEBUG += libavoIl_debug.$(EXT_DLL) libavoIll_debug.$(EXT_DLL) libavoMPZ_debug.$(EXT_DLL) libavoRl_debug.$(EXT_DLL) libavoRll_debug.$(EXT_DLL) libavoMPQ_debug.$(EXT_DLL) libavoD_debug.$(EXT_DLL) libavoDl_debug.$(EXT_DLL) libavoMPFR_debug.$(EXT_DLL) +CAMLLIB_TO_INSTALL += dllavoIl_caml.$(EXT_DLL) dllavoIll_caml.$(EXT_DLL) dllavoMPZ_caml.$(EXT_DLL) dllavoRl_caml.$(EXT_DLL) dllavoRll_caml.$(EXT_DLL) dllavoMPQ_caml.$(EXT_DLL) dllavoD_caml.$(EXT_DLL) dllavoDl_caml.$(EXT_DLL) dllavoMPFR_caml.$(EXT_DLL) +CAMLLIB_TO_INSTALL_DEBUG += dllavoIl_caml_debug.$(EXT_DLL) dllavoIll_caml_debug.$(EXT_DLL) dllavoMPZ_caml_debug.$(EXT_DLL) dllavoRl_caml_debug.$(EXT_DLL) dllavoRll_caml_debug.$(EXT_DLL) dllavoMPQ_caml_debug.$(EXT_DLL) dllavoD_caml_debug.$(EXT_DLL) dllavoDl_caml_debug.$(EXT_DLL) dllavoMPFR_caml_debug.$(EXT_DLL) +endif + + #--------------------------------------- # Rules #--------------------------------------- @@ -113,20 +131,30 @@ install: $(INSTALLd) $(APRON_INCLUDE) $(APRON_INCLUDE)/avo $(APRON_LIB) $(APRON_BIN) $(INSTALL) avo.h $(APRON_INCLUDE) $(INSTALL) $(CCINC) $(APRON_INCLUDE)/avo - for i in avotest* avotop* avorun*; do \ - if test -f $$i; then $(INSTALL) $$i $(APRON_BIN); fi; \ + for i in avotop* avorun*; do \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_BIN); fi; \ done - for i in libavo*.* libavo*_debug.*; do \ - if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ + for i in $(CCLIB_TO_INSTALL); do \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ done ifeq ($(OCAMLFIND),) - for i in libavo*_caml.* dllavo*_caml.$(EXT_DLL); do \ - if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ + for i in $(CAMLLIB_TO_INSTALL); do \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ done for i in avo.idl avo.mli avo.cmi avo.cmx avo*.cma avo*.cmxa avo*.a; do \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + done +endif +ifneq ($(HAS_DEBUG),) + for i in $(CCLIB_TO_INSTALL_DEBUG); do \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ + done +ifeq ($(OCAMLFIND),) + for i in $(CAMLLIB_TO_INSTALL_DEBUG); do \ if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif +endif uninstall: /bin/rm -fr $(APRON_INCLUDE)/avo.h @@ -241,15 +269,15 @@ mlD: ml avoD.cma libavoD_caml.a libavoD_caml_debug.a mlDl: ml avoDl.cma libavoDl_caml.a libavoDl_caml_debug.a mlMPFR: ml avoMPFR.cma libavoMPFR_caml.a libavoMPFR_caml_debug.a ifneq ($(HAS_OCAMLOPT),) -mlIl: $(call OCAMLOPT_TARGETS, avoIl) -mlIll: $(call OCAMLOPT_TARGETS, avoIll) -mlMPZ: $(call OCAMLOPT_TARGETS, avoMPZ) -mlRi: $(call OCAMLOPT_TARGETS, avoRi) -mlRll: $(call OCAMLOPT_TARGETS, avoRll) -mlMPQ: $(call OCAMLOPT_TARGETS, avoMPQ) -mlD: $(call OCAMLOPT_TARGETS, avoD) -mlDl: $(call OCAMLOPT_TARGETS, avoDl) -mlMPFR: $(call OCAMLOPT_TARGETS, avoMPFR) +mlIl: $(call OCAMLOPT_TARGETS, avoIl avoIl.d) +mlIll: $(call OCAMLOPT_TARGETS, avoIll avoIll.d) +mlMPZ: $(call OCAMLOPT_TARGETS, avoMPZ avoMPZ.d) +mlRi: $(call OCAMLOPT_TARGETS, avoRi avoRi.d) +mlRll: $(call OCAMLOPT_TARGETS, avoRll avoRll.d) +mlMPQ: $(call OCAMLOPT_TARGETS, avoMPQ avoMPQ.d) +mlD: $(call OCAMLOPT_TARGETS, avoD avoD.d) +mlDl: $(call OCAMLOPT_TARGETS, avoDl avoDl.d) +mlMPFR: $(call OCAMLOPT_TARGETS, avoMPFR avoMPFR.d) endif ifneq ($(HAS_SHARED),) mlIl: dllavoIl_caml.$(EXT_DLL) @@ -274,6 +302,9 @@ avo%.cma: avo.cmo libavo%_caml.a libavo%.a avo%.cmxa avo%.a: avo.cmx libavo%_caml.a libavo%.a $(OCAMLMKLIB) -o avo$* -oc avo$*_caml avo.cmx -lavo$* $(LIBS) +avo%.d.cmxa avo%.d.a: avo.cmx libavo%_caml_debug.a libavo%_debug.a + $(OCAMLMKLIB) -o avo$*.d -oc avo$*_caml_debug avo.cmx -lavo$*_debug $(LIBS_DEBUG) + dllavo%_caml.$(EXT_DLL) libavo%_caml.a: avo_caml.o libavo%.a $(OCAMLMKLIB) -o avo$*_caml $< -L. -lavo$* $(LDFLAGS) $(LIBS) diff --git a/box/Makefile b/box/Makefile index 85e39912..e7e72a90 100644 --- a/box/Makefile +++ b/box/Makefile @@ -23,28 +23,30 @@ CCSRC = box_config.h box.h $(CCMODULES:%=%.h) $(CCMODULES:%=%.c) CCINC_TO_INSTALL = box.h CCBIN_TO_INSTALL = -CCLIB_TO_INSTALL = libboxMPQ.a libboxD.a libboxMPFR.a \ -libboxMPQ_debug.a libboxD_debug.a libboxMPFR_debug.a +CCLIB_TO_INSTALL = libboxMPQ.a libboxD.a libboxMPFR.a +CCLIB_TO_INSTALL_DEBUG = libboxMPQ_debug.a libboxD_debug.a libboxMPFR_debug.a ifneq ($(HAS_SHARED),) - CCLIB_TO_INSTALL := $(CCLIB_TO_INSTALL) libboxMPQ.$(EXT_DLL) libboxD.$(EXT_DLL) \ - libboxMPFR.$(EXT_DLL) libboxMPQ_debug.$(EXT_DLL) libboxD_debug.$(EXT_DLL) \ - libboxMPFR_debug.$(EXT_DLL) + CCLIB_TO_INSTALL := $(CCLIB_TO_INSTALL) libboxMPQ.$(EXT_DLL) libboxD.$(EXT_DLL) libboxMPFR.$(EXT_DLL) + CCLIB_TO_INSTALL_DEBUG := $(CCLIB_TO_INSTALL_DEBUG) libboxMPQ_debug.$(EXT_DLL) libboxD_debug.$(EXT_DLL) libboxMPFR_debug.$(EXT_DLL) endif -ifneq ($(HAS_OCAML),) - CAML_TO_INSTALL = box.idl box.ml box.mli box.cmi boxMPQ.cma \ - boxD.cma boxMPFR.cma libboxMPQ_caml.a libboxD_caml.a \ - libboxMPFR_caml.a libboxMPQ_caml_debug.a libboxD_caml_debug.a \ - libboxMPFR_caml_debug.a - ifneq ($(HAS_OCAMLOPT),) - CAML_TO_INSTALL += $(call OCAMLOPT_TARGETS, boxMPQ boxD boxMPFR) - endif - ifneq ($(HAS_SHARED),) - CAML_TO_INSTALL += dllboxMPQ_caml.$(EXT_DLL) dllboxD_caml.$(EXT_DLL) \ - dllboxMPFR_caml.$(EXT_DLL) - endif +CAML_TO_INSTALL = box.idl box.ml box.mli box.cmi boxMPQ.cma \ +boxD.cma boxMPFR.cma libboxMPQ_caml.a libboxD_caml.a \ +libboxMPFR_caml.a +CAML_TO_INSTALL_DEBUG = libboxMPQ_caml_debug.a libboxD_caml_debug.a \ +libboxMPFR_caml_debug.a +ifneq ($(HAS_OCAMLOPT),) + CAML_TO_INSTALL += $(call OCAMLOPT_TARGETS, boxMPQ boxD boxMPFR) + CAML_TO_INSTALL_DEBUG += $(call OCAMLOPT_TARGETS, boxMPQ.d boxD.d boxMPFR.d) +endif +ifneq ($(HAS_SHARED),) + CAML_TO_INSTALL += dllboxMPQ_caml.$(EXT_DLL) dllboxD_caml.$(EXT_DLL) \ + dllboxMPFR_caml.$(EXT_DLL) + CAML_TO_INSTALL_DEBUG += dllboxMPQ_caml_debug.$(EXT_DLL) dllboxD_caml_debug.$(EXT_DLL) \ + dllboxMPFR_caml_debug.$(EXT_DLL) endif + LIBS = -lapron -lmpfr -lgmp -lm LIBS_DEBUG = -lapron_debug -lmpfr -lgmp -lm @@ -73,9 +75,9 @@ mlMPQ: boxMPQ.cma libboxMPQ_caml.a libboxMPQ_caml_debug.a mlD: boxD.cma libboxD_caml.a libboxD_caml_debug.a mlMPFR: boxMPFR.cma libboxMPFR_caml.a libboxMPFR_caml_debug.a ifneq ($(HAS_OCAMLOPT),) - mlMPQ: $(call OCAMLOPT_TARGETS, boxMPQ) - mlD: $(call OCAMLOPT_TARGETS, boxD) - mlMPFR: $(call OCAMLOPT_TARGETS, boxMPFR) + mlMPQ: $(call OCAMLOPT_TARGETS, boxMPQ boxMPQ.d) + mlD: $(call OCAMLOPT_TARGETS, boxD boxD.d) + mlMPFR: $(call OCAMLOPT_TARGETS, boxMPFR boxMPFR.d) endif ifneq ($(HAS_SHARED),) mlMPQ: dllboxMPQ_caml.$(EXT_DLL) @@ -103,13 +105,23 @@ install: $(CCINC_TO_INSTALL) $(CCLIB_TO_INSTALL) $(INSTALLd) $(APRON_INCLUDE) $(APRON_LIB) $(INSTALL) $(CCINC_TO_INSTALL) $(APRON_INCLUDE) for i in $(CCLIB_TO_INSTALL); do \ - if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ done ifeq ($(OCAMLFIND),) for i in $(CAML_TO_INSTALL); do \ + if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + done +endif +ifneq ($(HAS_DEBUG),) + for i in $(CCLIB_TO_INSTALL_DEBUG); do \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ + done +ifeq ($(OCAMLFIND),) + for i in $(CAML_TO_INSTALL_DEBUG); do \ if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif +endif uninstall: for i in $(CCINC_TO_INSTALL); do /bin/rm -f $(APRON_INCLUDE)/$$i; done @@ -193,6 +205,9 @@ box%.cma: box.cmo libbox%_caml.a libbox%.a box%.cmxa box%.a: box.cmx libbox%_caml.a libbox%.a $(OCAMLMKLIB) -o box$* -oc box$*_caml box.cmx -lbox$* $(LIBS) +box%.d.cmxa box%.d.a: box.cmx libbox%_caml_debug.a libbox%_debug.a + $(OCAMLMKLIB) -o box$*.d -oc box$*_caml_debug box.cmx -lbox$*_debug $(LIBS_DEBUG) + #--------------------------------------- # IDL rules #--------------------------------------- diff --git a/configure b/configure index a44550fb..18050563 100755 --- a/configure +++ b/configure @@ -32,6 +32,8 @@ where options include: -no-glpk disable GLPK support -no-java disable Java support -absolute-dylibs force absolute library names (OSX only) + -debug install also debug library version + -no-strip don't strip libraries Environment variables that affect configuration: CC C compiler to use (default: gcc) @@ -68,6 +70,8 @@ has_ocaml_plugins=1 has_java=1 force_absolute_dylib_install_names=0; ext_dll=so +has_debug=0 +do_strip=--strip while : ; do case "$1" in "") @@ -119,6 +123,10 @@ while : ; do has_java=0;; -absolute-dylibs|--absolute-dylibs) force_absolute_dylib_install_names=1;; + -debug|--debug) + has_debug=1;; + -no-strip|--no-strip) + do_strip=;; -help|--help) help;; *) @@ -600,9 +608,11 @@ detected configuration: optional PPL support $has_ppl optional PPLite support $has_pplite optional GLPK support $has_glpk + optional debug libraries $has_debug installation path $apron_prefix dynamic libraries extension $ext_dll + install (stripped) command $install ($do_strip) EOF @@ -622,6 +632,8 @@ if test "$has_java" -eq 0; then has_java=; fi if test "$has_ppl" -eq 0; then has_ppl=; fi if test "$has_pplite" -eq 0; then has_pplite=; fi if test "$has_glpk" -eq 0; then has_glpk=; fi +if test "$has_debug" -eq 0; then has_debug=; fi + cat > Makefile.config < Date: Tue, 27 Jun 2023 23:46:07 +0200 Subject: [PATCH 05/24] opam build defaults to include debug libraries and symbols --- apron.opam | 2 ++ 1 file changed, 2 insertions(+) diff --git a/apron.opam b/apron.opam index 64e6cbc2..c6bcbedd 100644 --- a/apron.opam +++ b/apron.opam @@ -21,6 +21,8 @@ build: [ "--no-ocaml-plugins" {os = "freebsd"} "--absolute-dylibs" {os = "macos"} "--ext-dll" {os = "win32"} "dll" {os = "win32"} + "--debug" + "--no-strip" ] [make "-j%{jobs}%"] ] From de41e59fb53d178918dabea3bafd410d30ed663b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 27 Jun 2023 23:59:10 +0200 Subject: [PATCH 06/24] don't install tests --- octagons/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/octagons/Makefile b/octagons/Makefile index 674d8119..52b1cf60 100644 --- a/octagons/Makefile +++ b/octagons/Makefile @@ -130,7 +130,7 @@ install: $(INSTALLd) $(APRON_INCLUDE) $(APRON_INCLUDE)/oct $(APRON_LIB) $(APRON_BIN) $(INSTALL) oct.h $(APRON_INCLUDE) $(INSTALL) $(CCINC) $(APRON_INCLUDE)/oct - for i in octtest* octtop* octrun*; do \ + for i in octtop* octrun*; do \ if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_BIN); fi; \ done for i in $(CCLIB_TO_INSTALL); do \ From d2709df877e5c4a9c10a317e54a534399a2bd357 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Tue, 27 Jun 2023 23:59:24 +0200 Subject: [PATCH 07/24] OCaml packages for debug versions --- mlapronidl/META.in | 8 ++++++++ mlapronidl/META.ppl.in | 2 ++ mlapronidl/META.pplite.in | 1 + 3 files changed, 11 insertions(+) diff --git a/mlapronidl/META.in b/mlapronidl/META.in index 5f5e0bff..24102aa6 100755 --- a/mlapronidl/META.in +++ b/mlapronidl/META.in @@ -11,26 +11,31 @@ package "boxD" ( requires = "apron.apron" archive(byte) = "boxD.cma" archive(native) = "boxD.cmxa" +archive(native,debug) = "boxD.d.cmxa" ) package "boxMPQ" ( requires = "apron.apron" archive(byte) = "boxMPQ.cma" archive(native) = "boxMPQ.cmxa" +archive(native,debug) = "boxMPQ.d.cmxa" ) package "boxMPFR" ( requires = "apron.apron" archive(byte) = "boxMPFR.cma" archive(native) = "boxMPFR.cmxa" +archive(native,debug) = "boxMPFR.d.cmxa" ) package "octD" ( requires = "apron.apron" archive(byte) = "octD.cma" archive(native) = "octD.cmxa" +archive(native,debug) = "octD.d.cmxa" ) package "octMPQ" ( requires = "apron.apron" archive(byte) = "octMPQ.cma" archive(native) = "octMPQ.cmxa" +archive(native,debug) = "octMPQ.d.cmxa" ) package "polkaMPQ" ( requires = "apron.apron" @@ -66,14 +71,17 @@ package "avoD" ( requires = "apron.apron" archive(byte) = "avoD.cma" archive(native) = "avoD.cmxa" +archive(native,debug) = "avoD.d.cmxa" ) package "avoMPQ" ( requires = "apron.apron" archive(byte) = "avoMPQ.cma" archive(native) = "avoMPQ.cmxa" +archive(native,debug) = "avoMPQ.d.cmxa" ) package "fppD" ( requires = "apron.apron" archive(byte) = "fppD.cma" archive(native) = "fppD.cmxa" +archive(native,debug) = "fppD.d.cmxa" ) \ No newline at end of file diff --git a/mlapronidl/META.ppl.in b/mlapronidl/META.ppl.in index 07511191..6e9cef36 100644 --- a/mlapronidl/META.ppl.in +++ b/mlapronidl/META.ppl.in @@ -2,9 +2,11 @@ package "ppl" ( requires = "apron.apron" archive(byte) = "ppl.cma" archive(native) = "ppl.cmxa" +archive(native,debug) = "ppl.d.cmxa" ) package "polkaGrid" ( requires = "apron.apron apron.ppl apron.polkaMPQ" archive(byte) = "polkaGrid.cma" archive(native) = "polkaGrid.cmxa" +archive(native,debug) = "polkaGrid.d.cmxa" ) diff --git a/mlapronidl/META.pplite.in b/mlapronidl/META.pplite.in index d7718def..f0ec2019 100644 --- a/mlapronidl/META.pplite.in +++ b/mlapronidl/META.pplite.in @@ -2,4 +2,5 @@ package "pplite" ( requires = "apron.apron" archive(byte) = "pplite.cma" archive(native) = "pplite.cmxa" +archive(native,debug) = "pplite.d.cmxa" ) From ce39b06cfdf09407a551de4e7a4bea6a4cf7c1fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Wed, 28 Jun 2023 13:43:48 +0200 Subject: [PATCH 08/24] OCaml installation --- avoct/Makefile | 4 ++-- box/Makefile | 2 +- fppol/Makefile | 4 ++-- mlapronidl/Makefile | 6 ++---- newpolka/Makefile | 2 +- octagons/Makefile | 4 ++-- ppl/Makefile | 10 +++++++--- pplite/Makefile | 2 +- products/Makefile | 2 +- taylor1plus/Makefile | 2 +- 10 files changed, 20 insertions(+), 18 deletions(-) diff --git a/avoct/Makefile b/avoct/Makefile index e19bb320..422fcd4a 100755 --- a/avoct/Makefile +++ b/avoct/Makefile @@ -139,10 +139,10 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done for i in avo.idl avo.mli avo.cmi avo.cmx avo*.cma avo*.cmxa avo*.a; do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/box/Makefile b/box/Makefile index e7e72a90..1b18b0fa 100644 --- a/box/Makefile +++ b/box/Makefile @@ -109,7 +109,7 @@ install: $(CCINC_TO_INSTALL) $(CCLIB_TO_INSTALL) done ifeq ($(OCAMLFIND),) for i in $(CAML_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/fppol/Makefile b/fppol/Makefile index 8641365a..ae26c9ee 100755 --- a/fppol/Makefile +++ b/fppol/Makefile @@ -139,10 +139,10 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done for i in fpp.idl fpp.mli fpp.cmi fpp.cmx fpp*.cma fpp*.cmxa fpp*.a; do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/mlapronidl/Makefile b/mlapronidl/Makefile index 9bf381d9..bdc41ff8 100644 --- a/mlapronidl/Makefile +++ b/mlapronidl/Makefile @@ -103,12 +103,10 @@ install: $(MLLIB_TOINSTALL) $(CCLIB_TOINSTALL) $(CCINC_TOINSTALL) ifeq ($(OCAMLFIND),) mkdir -p $(APRON_LIB) mkdir -p $(APRON_INCLUDE) - for i in $(CCLIB_TOINSTALL); do if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; done + for i in $(CCLIB_TOINSTALL); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done $(INSTALL) $(CCINC_TOINSTALL) $(APRON_INCLUDE) - for i in $(MLLIB_TOINSTALL); do if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; done -endif + for i in $(MLLIB_TOINSTALL); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done ifneq ($(HAS_DEBUG),) -ifeq ($(OCAMLFIND),) for i in $(CCLIB_TOINSTALL_DEBUG); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done for i in $(MLLIB_TOINSTALL_DEBUG); do if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; done endif diff --git a/newpolka/Makefile b/newpolka/Makefile index 1a6b2ee1..9128290d 100644 --- a/newpolka/Makefile +++ b/newpolka/Makefile @@ -123,7 +123,7 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAML_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/octagons/Makefile b/octagons/Makefile index 52b1cf60..740c47cd 100644 --- a/octagons/Makefile +++ b/octagons/Makefile @@ -138,10 +138,10 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTAL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done for i in oct.idl oct.mli oct.cmi oct.cmx oct*.cma oct*.cmxa oct*.a; do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/ppl/Makefile b/ppl/Makefile index b72d813e..8095f092 100644 --- a/ppl/Makefile +++ b/ppl/Makefile @@ -83,24 +83,28 @@ install: for i in $(CCLIB_TO_INSTALL); do \ if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ done +ifneq ($(HAS_OCAML),) ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL) ppl.idl ppl.cmi ppl.cma; do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done - for i in ap_ppl_test pplrun ppltop; do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_BIN); fi; \ + for i in pplrun ppltop; do \ + if test -f $$i; then $(INSTALL) $$i $(APRON_BIN); fi; \ done endif +endif ifneq ($(HAS_DEBUG),) for i in $(CCLIB_TO_INSTALL_DEBUG); do \ if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done +ifneq ($(HAS_OCAML),) ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL_DEBUG); do \ if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif endif +endif uninstall: /bin/rm -f $(APRON_INCLUDE)/ap_ppl* diff --git a/pplite/Makefile b/pplite/Makefile index c0d48352..3722bb7b 100644 --- a/pplite/Makefile +++ b/pplite/Makefile @@ -97,7 +97,7 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/products/Makefile b/products/Makefile index 9cfa474e..c7cbb3bb 100644 --- a/products/Makefile +++ b/products/Makefile @@ -90,7 +90,7 @@ install: done ifeq ($(OCAMLFIND),) for i in $(CAMLLIB_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) diff --git a/taylor1plus/Makefile b/taylor1plus/Makefile index a5dda112..03dc7ddf 100644 --- a/taylor1plus/Makefile +++ b/taylor1plus/Makefile @@ -139,7 +139,7 @@ install: $(CCINC_TO_INSTALL) $(CCLIB_TO_INSTALL) done ifeq ($(OCAMLFIND),) for i in $(CAML_TO_INSTALL); do \ - if test -f $$i; then $(INSTALLSTRIP) $$i $(APRON_LIB); fi; \ + if test -f $$i; then $(INSTALL) $$i $(APRON_LIB); fi; \ done endif ifneq ($(HAS_DEBUG),) From ec71e668472f0ac480a6c3dc3c4554b4a738d64f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Thu, 6 Jul 2023 16:55:59 +0200 Subject: [PATCH 09/24] document -debug and -no-strip options --- README.md | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index d61ffb49..b76a501c 100644 --- a/README.md +++ b/README.md @@ -22,9 +22,9 @@ Apron includes the following numeric domains: * zonotopes (taylor1plus) Additional domains are made available through the optional PPL and PPLite third-party libraries: -* alternate polyhedra implementation -* grids -* reduced products of polyhedra and grids +* alternate polyhedra implementation (PPL, PPLite) +* grids (PPL) +* reduced products of polyhedra and grids (PPL) The domains are made available under a common interface, so that changing the abstract domain of interpretation in a static analysis should only take a one-line change. @@ -104,6 +104,17 @@ In case some components fail to compile, it is possible to disable them through See `./configure -help` for more options. +### Debug versions + +By default, `make install` now only install non-debug versions of the C libraries. +Moreover, these are striped of symbols. + +Use the `-debug` `./configure` option to also install debug (non-stripped) C versions, and `-no-strip` to avoid stripping the non-debug C versions. +The C debug versions have a `_debug` suffix (such as `libapron_debug.so`). + +When installing with `opam`, debug versions are always available. +OCaml debug libraries use the `.d` suffix (such as `apron.d.cmxa`). + ### Installation on MacOS X From 0003a8001c97e582ff18ee8750c42cf2a04dcba1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Thu, 6 Jul 2023 17:03:20 +0200 Subject: [PATCH 10/24] Preparation for 0.9.14 release --- Changes | 29 +++++++++++++++++++++++++++++ apron/apron.texi | 2 +- apronxx/doc/Doxyfile | 2 +- version.mk | 2 +- 4 files changed, 32 insertions(+), 3 deletions(-) diff --git a/Changes b/Changes index c2a47438..5c51a4ed 100644 --- a/Changes +++ b/Changes @@ -1,9 +1,38 @@ +Version 0.9.14 + +- Add support for PPLite 0.11 polyhedra library [Enea Zaffanella] (#71) + +- Add Fppol domain (floating-point polyhedra) [Liqian Chen] (#33) + +- Add Avoct domain (absolute value octagons) [Liqian Chen] (#33) + +- Add OCaml 5.0.0 support + +- Replace quicksort implementation with a new, LGPL one (#87) + +- make install installs non-debug version only, unless -debug is used (#86) + +- Non-debug C libraries are stripped (#86) + +- Compilation and installation fixes (#80, #75, #65, #62, #61, #60, #59, #54, #52, #49, #48, #45, #34) + +- Apple M1 support (#68) + +- Fix some corner cases for boxes and polyehdra (#85, #83, #82, #81, #80, #63, #43, #35) + + Version 0.9.13 + - Fix Java version detection & compilation (#30) + - Minor grammar and spelling fixes (#22), (#26) + - Use texi2any instead of (dead) texi2html (#23) + - Fix best and exact flags in octagons (#25) + - Fix linking under MaxOS X (#28) + - Taylor1+ fixes diff --git a/apron/apron.texi b/apron/apron.texi index d65933dc..53a58b09 100755 --- a/apron/apron.texi +++ b/apron/apron.texi @@ -2,7 +2,7 @@ @c -*-texinfo-*- @c %**start of header @setfilename apron.info -@settitle APRON 0.9.13 +@settitle APRON 0.9.14 @c @setcontentsaftertitlepage @c include version.texi @iftex diff --git a/apronxx/doc/Doxyfile b/apronxx/doc/Doxyfile index db47794b..c1457602 100644 --- a/apronxx/doc/Doxyfile +++ b/apronxx/doc/Doxyfile @@ -38,7 +38,7 @@ PROJECT_NAME = APRONXX # could be handy for archiving the generated documentation or if some version # control system is used. -PROJECT_NUMBER = 0.9.12 +PROJECT_NUMBER = 0.9.14 # Using the PROJECT_BRIEF tag one can provide an optional one line description # for a project that appears at the top of each page and should give viewer a diff --git a/version.mk b/version.mk index b62fc371..a2fde5b3 100644 --- a/version.mk +++ b/version.mk @@ -1,7 +1,7 @@ # bump here at each release VERSION_MAJOR = 0 VERSION_MINOR = 9 -VERSION_MICRO = 13 +VERSION_MICRO = 14 # automatically generated VERSION_STR = "${VERSION_MAJOR}.${VERSION_MINOR}.${VERSION_MICRO}" From 59015eb06a87486d48a59fa49729f06082a8fc70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Thu, 6 Jul 2023 17:11:46 +0200 Subject: [PATCH 11/24] fix opam link check (license name) --- apron.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apron.opam b/apron.opam index c6bcbedd..b2f4cd80 100644 --- a/apron.opam +++ b/apron.opam @@ -5,7 +5,7 @@ authors: [ "Antoine Miné" "https://github.com/antoinemine/apron/graphs/contributors" ] -license: "LGPL-2.1 with linking exception" +license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception" homepage: "https://antoinemine.github.io/Apron/doc/" maintainer: "Nicolas Berthier " dev-repo: "git+https://github.com/antoinemine/apron.git" From 7efcfa0a20ad4348eab880cc332a5d509718d88c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Sun, 9 Jul 2023 11:58:59 +0200 Subject: [PATCH 12/24] minor fixes: don;t depent on OCaml's Stdlib, typo --- Changes | 2 +- mlapronidl/scalar.idl | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Changes b/Changes index 5c51a4ed..10bd0c3a 100644 --- a/Changes +++ b/Changes @@ -18,7 +18,7 @@ Version 0.9.14 - Apple M1 support (#68) -- Fix some corner cases for boxes and polyehdra (#85, #83, #82, #81, #80, #63, #43, #35) +- Fix some corner cases for boxes and polyhedra (#85, #83, #82, #81, #80, #63, #43, #35) Version 0.9.13 diff --git a/mlapronidl/scalar.idl b/mlapronidl/scalar.idl index 1a724063..3a945fa2 100644 --- a/mlapronidl/scalar.idl +++ b/mlapronidl/scalar.idl @@ -157,8 +157,8 @@ let of_int x = Mpqf(Mpqf.of_int x)\n\ let of_frac x y = Mpqf(Mpqf.of_frac x y)\n\ let of_float x = Float(x)\n\ let of_infty s = \n\ - if s>0 then Float(Stdlib.infinity)\n\ - else if s<0 then Float(Stdlib.neg_infinity)\n\ + if s>0 then Float(infinity)\n\ + else if s<0 then Float(neg_infinity)\n\ else Float(0.0)\n\ let is_infty scalar =\n\ match scalar with\n\ @@ -175,8 +175,8 @@ let is_infty scalar =\n\ if Mpfrf.sgn x > 0 then 1 else -1\n\ else 0\n\ | Float x ->\n\ - if x = Stdlib.infinity then 1\n\ - else if x = Stdlib.neg_infinity then -1\n\ + if x = infinity then 1\n\ + else if x = neg_infinity then -1\n\ else 0\n\ let sgn scalar =\n\ match scalar with\n\ @@ -216,7 +216,7 @@ let cmp_int scalar n =\n\ match scalar with\n\ | Mpqf x -> Mpqf.cmp_int x n\n\ | Mpfrf x -> Mpfrf.cmp_int x n\n\ - | Float x -> Stdlib.compare x (float_of_int n)\n\ + | Float x -> compare x (float_of_int n)\n\ let equal_int scalar n =\n\ match scalar with\n\ | Mpqf x -> (Mpqf.cmp_int x n)=0\n\ From 2db72d6e0571255dac24b86b3708ee859dc63e54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Fri, 11 Aug 2023 16:03:15 +0200 Subject: [PATCH 13/24] Fix the variable permutation performed at the end of level 1 fold. --- apron/ap_abstract1.c | 48 +++++++++++++++++++------------------------- 1 file changed, 21 insertions(+), 27 deletions(-) diff --git a/apron/ap_abstract1.c b/apron/ap_abstract1.c index a3c23628..6818253a 100644 --- a/apron/ap_abstract1.c +++ b/apron/ap_abstract1.c @@ -1203,30 +1203,24 @@ ap_abstract1_t ap_abstract1_fold(ap_manager_t* man, /* Compute the permutation for "exchanging" dim and tdim[0] if necessary */ if (dim!=tdim[0]){ size_t rank; - /* We have the following situation - - Initially: - env: A B C D E F G - dim: 0 1 2 3 4 5 6 - gen: a b c d e f g - We fold with F,B,D, translated to [5,1,3] and reordered to [1,3,5] - env: A C E F G - dim: 0 1 2 3 4 - gen: a b c e g - a d c e g - a f c e g - We need now to apply the permutation - rank: 0 1 2 3 4 - perm: 0 2 3 1 4 - - var: Y Z Q - dim: 0 1 2 - gen: b a e - b c e - b d e - - So we have to perform a to the right between dim[0] and dim-(rank of dim in - tdim) + /* Due to reordering tdim, we have now folded the variables in tdim[0] + instead of dim. + + We construct a permutation to exchange dim and tdim[0]. + + Due to folding, the oroginal position of dim has changed: + it is now dim-index, where index is the index of dim in + the (unsorted) original array. + + We thus rotate all indices between tdim[0] and dim-index left. + + tdim[0] dim + v v + original: 0 1 2 3 4 5 + folded: 0 f 2 3 5 (where f = 1 U 4) + permuted: 0 2 3 f 5 + + The permutation is: 0->0, 1->3, 2->1, 3->2, 5->5 */ /* look for the position of dim in tdim array */ void* p = bsearch(&dim,&tdim[1],size-1,sizeof(ap_dim_t),compar_dim); @@ -1235,10 +1229,10 @@ ap_abstract1_t ap_abstract1_fold(ap_manager_t* man, /* compute permutation */ ap_dimperm_init(&perm, nenv->intdim+nenv->realdim); ap_dimperm_set_id(&perm); - for (rank=tdim[0]; rank Date: Sun, 13 Aug 2023 19:44:07 +0200 Subject: [PATCH 14/24] update explanation --- apron/ap_abstract1.c | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/apron/ap_abstract1.c b/apron/ap_abstract1.c index 6818253a..07fea652 100644 --- a/apron/ap_abstract1.c +++ b/apron/ap_abstract1.c @@ -1203,16 +1203,24 @@ ap_abstract1_t ap_abstract1_fold(ap_manager_t* man, /* Compute the permutation for "exchanging" dim and tdim[0] if necessary */ if (dim!=tdim[0]){ size_t rank; - /* Due to reordering tdim, we have now folded the variables in tdim[0] - instead of dim. + /* Due to reordering of tdim, we have now folded the variables + into tdim[0] instead of dim. - We construct a permutation to exchange dim and tdim[0]. + To fix this, we construct a permutation to exchange dim and tdim[0]. - Due to folding, the oroginal position of dim has changed: - it is now dim-index, where index is the index of dim in - the (unsorted) original array. + Due to folding, the position of dim has changed in the result. + Then new position is dim-index, where index is the position of + dim in tdim, i.e., the number of variables that have been removed + before dim. - We thus rotate all indices between tdim[0] and dim-index left. + We then rotate all indices between tdim[0] and dim-index left. + + Example: + We want to fold 1 into 4 (dim). + We first sort tdmin as [1;4]. + Level 0 folding will actuall fold 4 (dim) into 1 (tdim[0]), + and remove 4. + We thus rotate left variables at positions 1, 2, 3 (after folding). tdim[0] dim v v From f1651882a57fc289f1cf0ab0d5b07405afffcfac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Wed, 20 Sep 2023 21:51:33 +0200 Subject: [PATCH 15/24] Removed reference to conf-pplite. --- apron.opam | 2 -- 1 file changed, 2 deletions(-) diff --git a/apron.opam b/apron.opam index b2f4cd80..1b63e0e2 100644 --- a/apron.opam +++ b/apron.opam @@ -17,7 +17,6 @@ build: [ "--prefix" "%{share}%/apron" "--no-ppl" {!conf-ppl:installed} - "--no-pplite" {!conf-pplite:installed} "--no-ocaml-plugins" {os = "freebsd"} "--absolute-dylibs" {os = "macos"} "--ext-dll" {os = "win32"} "dll" {os = "win32"} @@ -39,7 +38,6 @@ depends: [ ] depopts: [ "conf-ppl" - "conf-pplite" ] description:""" Apron is a library to represent properties of numeric variables, such as variable bounds or linear relations between variables, and to manipulate these properties through semantic operations, such as variable assignments, tests, conjunctions, entailment. Apron is intended to be used in static program analyzers, in order to infer invariants of numeric variables, i.e., properties that hold for all executions of a program. It is based on the theory of Abstract Interpretation.""" From d8795583a511371996534f13bc8232d5a5ce8239 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antoine=20Min=C3=A9?= Date: Wed, 20 Sep 2023 21:55:04 +0200 Subject: [PATCH 16/24] Prepare for 0.9.14 release. --- Changes | 1 + 1 file changed, 1 insertion(+) diff --git a/Changes b/Changes index 10bd0c3a..594aa146 100644 --- a/Changes +++ b/Changes @@ -20,6 +20,7 @@ Version 0.9.14 - Fix some corner cases for boxes and polyhedra (#85, #83, #82, #81, #80, #63, #43, #35) +- Fix level 1 fold (#90) Version 0.9.13 From 7fa0b315bc73ce4cc70e3dcf4f11e997eb9f9750 Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Wed, 14 Feb 2024 13:37:50 +0100 Subject: [PATCH 17/24] PPLite no longer depends on gmpxx (GMP C++ interface). --- pplite/Makefile | 4 ++-- pplite/ap_pplite.texi | 2 +- pplite/pplite.idl | 3 ++- pplite/pplite_poly.cc | 11 +++++++---- pplite/pplite_user.cc | 25 +++++++++++++++---------- 5 files changed, 27 insertions(+), 18 deletions(-) diff --git a/pplite/Makefile b/pplite/Makefile index 3722bb7b..834c6c91 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/ap_pplite.texi b/pplite/ap_pplite.texi index 38329bd9..036a5f24 100644 --- a/pplite/ap_pplite.texi +++ b/pplite/ap_pplite.texi @@ -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 17a608ba..f4b2861b 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 176a37ef..3bec6c9e 100644 --- a/pplite/pplite_poly.cc +++ b/pplite/pplite_poly.cc @@ -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(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(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_user.cc b/pplite/pplite_user.cc index 262c17df..d6d1d4b3 100644 --- a/pplite/pplite_user.cc +++ b/pplite/pplite_user.cc @@ -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 Date: Thu, 15 Feb 2024 15:25:13 +0100 Subject: [PATCH 18/24] Avoid a name clash with a GMP's macro. --- pplite/pplite_poly.cc | 4 ++-- pplite/pplite_user.hh | 9 ++++----- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/pplite/pplite_poly.cc b/pplite/pplite_poly.cc index 3bec6c9e..e61e789f 100644 --- a/pplite/pplite_poly.cc +++ b/pplite/pplite_poly.cc @@ -111,14 +111,14 @@ to_itv_array(pplite_poly* a) { if (bbox.inf_ub(i)) bound_set_infty(env[i]->sup, 1); else { - mpq_set(temp, bbox.ub(i)); + bbox.ub(i).get_mpq(temp); bound_set_int(env[i]->sup, 0); numrat_set_mpq(env[i]->sup, temp); } if (bbox.inf_lb(i)) bound_set_infty(env[i]->inf, -1); else { - mpq_set(temp, bbox.lb(i)); + bbox.lb(i).get_mpq(temp); bound_set_int(env[i]->inf, 0); numrat_set_mpq(env[i]->inf, temp); numrat_neg(env[i]->inf, env[i]->inf); diff --git a/pplite/pplite_user.hh b/pplite/pplite_user.hh index 39bdf8a0..97675d9a 100644 --- a/pplite/pplite_user.hh +++ b/pplite/pplite_user.hh @@ -47,7 +47,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); + i.get_mpz(mpq_numref(s->val.mpq)); mpz_set_ui(mpq_denref(s->val.mpq), 1); } @@ -56,8 +56,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); + n.get_mpz(mpq_numref(s->val.mpq)); + d.get_mpz(mpq_denref(s->val.mpq)); mpq_canonicalize(s->val.mpq); } @@ -65,8 +65,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()); + r.get_mpq(s->val.mpq); // No need to canonicalize } From 7c43da1574f2eb2b1b41e08fc0ec7031c89f8f6e Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Thu, 11 Apr 2024 11:51:23 +0200 Subject: [PATCH 19/24] Renamed "matrix_t" and related functions, adding prefix "pk_". Patch contributed by Michele Spotti. This renaming is needed to avoid a name clash with (version 3 of) the FLINT library, which is a required dependency when enabling PPLite. Note: name clash is caused by functions matrix_clear and matrix_equal. --- newpolka/pk.h | 4 +- newpolka/pk_approximate.c | 54 ++++++++-------- newpolka/pk_assign.c | 56 ++++++++--------- newpolka/pk_cherni.c | 116 +++++++++++++++++------------------ newpolka/pk_cherni.h | 18 +++--- newpolka/pk_closure.c | 8 +-- newpolka/pk_constructor.c | 28 ++++----- newpolka/pk_constructor.h | 2 +- newpolka/pk_expandfold.c | 32 +++++----- newpolka/pk_extract.c | 32 +++++----- newpolka/pk_extract.h | 10 +-- newpolka/pk_internal.c | 4 +- newpolka/pk_internal.h | 2 +- newpolka/pk_matrix.c | 104 +++++++++++++++---------------- newpolka/pk_matrix.h | 80 ++++++++++++------------ newpolka/pk_meetjoin.c | 46 +++++++------- newpolka/pk_meetjoin.h | 2 +- newpolka/pk_project.c | 14 ++--- newpolka/pk_representation.c | 92 +++++++++++++-------------- newpolka/pk_representation.h | 2 +- newpolka/pk_resize.c | 48 +++++++-------- newpolka/pk_resize.h | 4 +- newpolka/pk_test.c | 14 ++--- newpolka/pk_test.h | 2 +- newpolka/pk_user.c | 56 ++++++++--------- newpolka/pk_user.h | 16 ++--- newpolka/pk_widening.c | 8 +-- newpolka/pkeq.c | 22 +++---- 28 files changed, 438 insertions(+), 438 deletions(-) diff --git a/newpolka/pk.h b/newpolka/pk.h index 44e028bd..8e9df778 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 228416be..8fe5ff4e 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 09e77bdb..d5ab7208 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 b90ab731..06974b37 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 c74afd4b..7dae1919 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 d97fc982..720c441a 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 e0a64cea..36f4fa79 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 0824f7f5..85cbbb02 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 1be0bfb2..5fd3e741 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 2ff00fef..c8e4245b 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 a89aa41f..4a4ab98f 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 b1e4cecc..843215fd 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 554c256a..119f004f 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 a3e6d8a6..9a371b8a 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 23b3cec0..e80f30b3 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 46c71a44..745badb2 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 47e53f74..32f43cbb 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 f662f8bb..9da508a3 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 51749a78..ec6a8707 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 820e76b4..32113670 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 3d8ee6e0..b1440e2c 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 160ad186..4604ab4e 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 ffee5d93..de1b33f8 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 cf2a14d2..3c167f75 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 08d3fc7d..f7a21980 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 8ccc4002..23d38dab 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 69a6d71e..ea7b2a10 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 40ed8c54..fbe6e993 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++){ From 94726fcf016c36118df67313ced7aa49c1f02c7a Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Thu, 11 Apr 2024 15:08:01 +0200 Subject: [PATCH 20/24] The pplite wrapper has been updated to PPLite version 0.12. --- pplite/README | 6 +++--- pplite/ap_pplite.texi | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pplite/README b/pplite/README index 657ec12a..5b20f79b 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 036a5f24..cf5b2699 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" From 8705371a05ffd5b57e9634e1477e23d5f9115108 Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Sun, 26 May 2024 09:46:52 +0200 Subject: [PATCH 21/24] Minor changes for backward compatibility with PPLite 0.11. (Maybe) Define macro HAVE_PPLITE_0_11 at configuration time. Added a couple of backward compatibility helpers. --- configure | 17 ++++++++++++++--- pplite/pplite_poly.cc | 6 +++--- pplite/pplite_poly.hh | 2 +- pplite/pplite_user.cc | 2 +- pplite/pplite_user.hh | 34 ++++++++++++++++++++++++++++------ 5 files changed, 47 insertions(+), 14 deletions(-) diff --git a/configure b/configure index a6c014ec..7d278080 100755 --- a/configure +++ b/configure @@ -448,6 +448,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 + pplite_version=`grep "define PPLITE_PACKAGE_VERSION" $pplite_prefix/include/pplite/pplite-config.h | cut -d'"' -f2` + 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 fi if test $has_glpk -eq 1 @@ -606,7 +617,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 @@ -681,8 +692,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/pplite/pplite_poly.cc b/pplite/pplite_poly.cc index e61e789f..bdb0275d 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 * */ @@ -111,14 +111,14 @@ to_itv_array(pplite_poly* a) { if (bbox.inf_ub(i)) bound_set_infty(env[i]->sup, 1); else { - bbox.ub(i).get_mpq(temp); + mpq_set_Rational(temp, bbox.ub(i)); bound_set_int(env[i]->sup, 0); numrat_set_mpq(env[i]->sup, temp); } if (bbox.inf_lb(i)) bound_set_infty(env[i]->inf, -1); else { - bbox.lb(i).get_mpq(temp); + mpq_set_Rational(temp, bbox.lb(i)); bound_set_int(env[i]->inf, 0); numrat_set_mpq(env[i]->inf, temp); numrat_neg(env[i]->inf, env[i]->inf); diff --git a/pplite/pplite_poly.hh b/pplite/pplite_poly.hh index 6a4e31f9..45df2bd5 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 d6d1d4b3..23670dab 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 * */ diff --git a/pplite/pplite_user.hh b/pplite/pplite_user.hh index 97675d9a..c927fddd 100644 --- a/pplite/pplite_user.hh +++ b/pplite/pplite_user.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 * */ @@ -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); - i.get_mpz(mpq_numref(s->val.mpq)); + 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); - n.get_mpz(mpq_numref(s->val.mpq)); - d.get_mpz(mpq_denref(s->val.mpq)); + mpz_set_Integer(mpq_numref(s->val.mpq), n); + mpz_set_Integer(mpq_denref(s->val.mpq), d); mpq_canonicalize(s->val.mpq); } @@ -65,8 +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); - r.get_mpq(s->val.mpq); - // No need to canonicalize + mpq_set_Rational(s->val.mpq, r); } /* Con::Type => ap_constyp_t */ From 04d58df11006d85fb1e7c9bde177f0c7bc94eab4 Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Sun, 26 May 2024 10:50:37 +0200 Subject: [PATCH 22/24] Hopefully more robust test for PPLite version. --- configure | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/configure b/configure index 7d278080..e9d97f06 100755 --- a/configure +++ b/configure @@ -427,6 +427,35 @@ then ppl_prefix="$prefix" 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 -I$PPLITE_PREFIX/include -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 + else + $cxx -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 @@ -451,7 +480,7 @@ then # check if pplite version is 0.11 if test $has_pplite -eq 1 then - pplite_version=`grep "define PPLITE_PACKAGE_VERSION" $pplite_prefix/include/pplite/pplite-config.h | cut -d'"' -f2` + get_pplite_version if test "x$pplite_version" != "x0.11" then have_pplite_0_11_cxxflags= From 3ec955ffee01780c40972e0623acba1eab20cdcc Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Sun, 26 May 2024 19:37:43 +0200 Subject: [PATCH 23/24] Further fix for get_pplite_version. --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure b/configure index e9d97f06..1ce071de 100755 --- a/configure +++ b/configure @@ -439,9 +439,9 @@ get_pplite_version() r=1 if test "x$PPLITE_PREFIX" != "x" then - $cxx -I$PPLITE_PREFIX/include -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 + $cxx $cxxflags $deps -I$PPLITE_PREFIX/include -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 else - $cxx -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 + $cxx $cxxflags $deps -o tmp tmp.cc >/dev/null 2>/dev/null || r=0 fi if test $r -eq 0 -o ! -f tmp then From d9f764f76e4a49c8d164146ce3f48dd23199f4e9 Mon Sep 17 00:00:00 2001 From: Enea Zaffanella Date: Tue, 28 May 2024 10:00:37 +0200 Subject: [PATCH 24/24] Follow Antoine hints for get_pplite_version. --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure b/configure index 6a3ab800..043526dd 100755 --- a/configure +++ b/configure @@ -439,9 +439,9 @@ get_pplite_version() echo " std::cout << PPLITE_PACKAGE_VERSION << std::endl;" >> tmp.cc echo "}" >> tmp.cc r=1 - if test "x$PPLITE_PREFIX" != "x" + 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 + $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