From 2a02fc5f3be1ab8d9d12928088664e2e6bd9c42e Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 5 Mar 2024 10:53:03 -0800 Subject: [PATCH 01/10] WIP WIP: intersection/union done --- include/feasibility_set_int.h | 152 ++++++++++++ include/poly.h | 1 + src/CMakeLists.txt | 1 + src/polynomial/feasibility_set.c | 10 +- src/polynomial/feasibility_set.h | 2 - src/polynomial/feasibility_set_int.c | 343 +++++++++++++++++++++++++++ src/polynomial/feasibility_set_int.h | 21 ++ 7 files changed, 524 insertions(+), 6 deletions(-) create mode 100644 include/feasibility_set_int.h create mode 100644 src/polynomial/feasibility_set_int.c create mode 100644 src/polynomial/feasibility_set_int.h diff --git a/include/feasibility_set_int.h b/include/feasibility_set_int.h new file mode 100644 index 00000000..f2b27d83 --- /dev/null +++ b/include/feasibility_set_int.h @@ -0,0 +1,152 @@ +/** + * Copyright 2024, SRI International. + * + * This file is part of LibPoly. + * + * LibPoly is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * LibPoly 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 Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with LibPoly. If not, see . + */ + +#pragma once + +#include "poly.h" +#include "integer.h" +#include + +#ifdef __cplusplus +extern "C" { +#endif + +/** + * Set of disjoint intervals representing an algebraic set, ordered from + * left to right (-inf to +inf). + */ +struct lp_feasibility_set_int_struct { + /** The ring in which the feasibility set lives. */ + lp_int_ring_t *K; + + /** If true, set represents K \setminus elements */ + bool inverted; + + /** Number of elements */ + size_t size; + + /** Capacity of the elements table */ + size_t capacity; + + /** Vector feasibility elements */ + lp_integer_t* elements; +}; + +/** + * Create a new feasibility set K. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_new_full(lp_int_ring_t *K); + +/** + * Create a new feasibility set {}. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_new_empty(lp_int_ring_t *K); + +/** + * Construct a copy. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_new_copy(const lp_feasibility_set_int_t* set); + +/** + * Construct from integers. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_new_from_integer(lp_int_ring_t *K, const lp_integer_t* integers, size_t integers_size, bool inverted); + +/** + * Delete the given feasibility set. + */ +void lp_feasibility_set_int_delete(lp_feasibility_set_int_t* set); + +/** + * Assignment. + */ +void lp_feasibility_set_int_assign(lp_feasibility_set_int_t* set, const lp_feasibility_set_int_t* from); + +/** + * Swap. + */ +void lp_feasibility_set_int_swap(lp_feasibility_set_int_t* s1, lp_feasibility_set_int_t* s2); + +/** + * Check if the given set is empty. + */ +int lp_feasibility_set_int_is_empty(const lp_feasibility_set_int_t* set); + +/** + * Check if the given set is full. + */ +int lp_feasibility_set_int_is_full(const lp_feasibility_set_int_t* set); + +/** + * Check if the set is a point {a}. + */ +int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set); + +/** + * Check if the given value belongs to the set. + */ +int lp_feasibility_set_int_contains(const lp_feasibility_set_int_t* set, const lp_integer_t* value); + +/** + * Pick a value from the feasible set (must be non-empty). + */ +void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_integer_t* value); + +/** + * Get intersection of the two sets. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); + +/** + * Get union of the two sets. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); + +typedef enum { + LP_FEASIBILITY_SET_INT_INTERSECT_S1, + LP_FEASIBILITY_SET_INT_INTERSECT_S2, + LP_FEASIBILITY_SET_INT_NEW, + LP_FEASIBILITY_SET_INT_EMPTY +} lp_feasibility_set_int_intersect_status_t; + +/** + * Get intersection of the two sets, returns the status in the given variable. + * The set s1 is given precedence so LP_FEASIBILITY_SET_INTERSECT_S2 is the + * status only if the intersect is not s1. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_intersect_status_t* status); + +/** + * Add one set to another, i.e. s = s \cup from. + */ +void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from); + +/** + * Print the set. + */ +int lp_feasibility_set_int_print(const lp_feasibility_set_int_t* set, FILE* out); + +/** + * Return the string representation of the set. + */ +char* lp_feasibility_set_int_to_string(const lp_feasibility_set_int_t* set); + +#ifdef __cplusplus +} /* close extern "C" { */ +#endif diff --git a/include/poly.h b/include/poly.h index 99b43cbf..557a9591 100644 --- a/include/poly.h +++ b/include/poly.h @@ -66,6 +66,7 @@ typedef struct lp_dyadic_interval_struct lp_dyadic_interval_t; typedef struct lp_interval_struct lp_interval_t; typedef struct lp_feasibility_set_struct lp_feasibility_set_t; +typedef struct lp_feasibility_set_int_struct lp_feasibility_set_int_t; typedef struct lp_polynomial_hash_set_struct lp_polynomial_hash_set_t; typedef struct lp_polynomial_vector_struct lp_polynomial_vector_t; typedef struct lp_polynomial_heap_struct lp_polynomial_heap_t; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7c790e18..eb9a7e55 100755 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -34,6 +34,7 @@ set(poly_SOURCES polynomial/polynomial.c polynomial/polynomial_context.c polynomial/feasibility_set.c + polynomial/feasibility_set_int.c polynomial/polynomial_hash_set.c polynomial/polynomial_heap.c polynomial/polynomial_vector.c diff --git a/src/polynomial/feasibility_set.c b/src/polynomial/feasibility_set.c index af7bea5c..79d919ec 100644 --- a/src/polynomial/feasibility_set.c +++ b/src/polynomial/feasibility_set.c @@ -32,17 +32,18 @@ #include "polynomial/feasibility_set.h" static -void lp_feasibility_set_ensure_capacity(lp_feasibility_set_t* s, size_t size) { - if (size && size > s->capacity) { - s->capacity = size; +void lp_feasibility_set_ensure_capacity(lp_feasibility_set_t* s, size_t capacity) { + if (capacity && capacity > s->capacity) { + s->capacity = capacity; s->intervals = realloc(s->intervals, s->capacity * sizeof(lp_interval_t)); } } +static void lp_feasibility_set_construct(lp_feasibility_set_t* s, size_t size) { s->size = 0; s->capacity = 0; - s->intervals = 0; + s->intervals = NULL; lp_feasibility_set_ensure_capacity(s, size); } @@ -86,6 +87,7 @@ void lp_feasibility_set_delete(lp_feasibility_set_t* set) { free(set); } +static void lp_feasibility_set_construct_copy(lp_feasibility_set_t* set, const lp_feasibility_set_t* from) { lp_feasibility_set_construct(set, from->size); size_t i; diff --git a/src/polynomial/feasibility_set.h b/src/polynomial/feasibility_set.h index 3ca631ed..ea90efa8 100644 --- a/src/polynomial/feasibility_set.h +++ b/src/polynomial/feasibility_set.h @@ -19,6 +19,4 @@ #pragma once -void lp_feasibility_set_construct(lp_feasibility_set_t* s, size_t size); - lp_feasibility_set_t* lp_feasibility_set_new_internal(size_t size); diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c new file mode 100644 index 00000000..36b1052b --- /dev/null +++ b/src/polynomial/feasibility_set_int.c @@ -0,0 +1,343 @@ +/** + * Copyright 2024, SRI International. + * + * This file is part of LibPoly. + * + * LibPoly is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * LibPoly 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 Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with LibPoly. If not, see . + */ + +#include +#include "polynomial/feasibility_set_int.h" + +#include +#include + +static +int int_cmp(const void *i1, const void *i2) { + return lp_integer_cmp(lp_Z, i1, i2); +} + +static +void lp_feasibility_set_int_ensure_capacity(lp_feasibility_set_int_t* s, size_t capacity) { + if (capacity && capacity > s->capacity) { + s->capacity = capacity; + s->elements = realloc(s->elements, s->capacity * sizeof(lp_integer_t)); + } +} + +static +void lp_feasibility_set_int_construct(lp_int_ring_t *K, lp_feasibility_set_int_t* s, size_t size, bool inverted) { + s->K = K; + lp_int_ring_attach(s->K); + s->capacity = 0; + s->size = size; + s->inverted = inverted; + s->elements = NULL; + lp_feasibility_set_int_ensure_capacity(s, size); +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_new_empty(lp_int_ring_t *K) { + lp_feasibility_set_int_t *s = malloc(sizeof(lp_feasibility_set_int_t)); + lp_feasibility_set_int_construct(K, s, 0, false); + return s; +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_new_full(lp_int_ring_t *K) { + lp_feasibility_set_int_t *s = malloc(sizeof(lp_feasibility_set_int_t)); + lp_feasibility_set_int_construct(K, s, 0, true); + return s; +} + +static +void lp_feasibility_set_int_construct_from_integer(lp_feasibility_set_int_t *set, lp_int_ring_t *K, const lp_integer_t *elements, size_t size, bool inverted) { + lp_feasibility_set_int_construct(K, set, size, inverted); + for (size_t i = 0; i < size; ++ i) { + lp_integer_construct_copy(K, set->elements + i, elements + i); + } + set->size = size; + qsort(set->elements, size, sizeof(lp_integer_t), int_cmp); +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_new_from_integer(lp_int_ring_t *K, const lp_integer_t* elements, size_t elements_size, bool inverted) { + lp_feasibility_set_int_t *result = malloc(sizeof(lp_feasibility_set_int_t)); + lp_feasibility_set_int_construct_from_integer(result, K, elements, elements_size, inverted); + return result; +} + +static +void lp_feasibility_set_int_construct_copy(lp_feasibility_set_int_t *set, const lp_feasibility_set_int_t* from) { + // we assume that from is valid, thus no sorting + lp_feasibility_set_int_construct(from->K, set, from->size, from->inverted); + for (size_t i = 0; i < from->size; ++ i) { + lp_integer_construct_copy(lp_Z, set->elements + i, from->elements + i); + } + set->size = from->size; +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_new_copy(const lp_feasibility_set_int_t* set) { + lp_feasibility_set_int_t *result = malloc(sizeof(lp_feasibility_set_int_t)); + lp_feasibility_set_int_construct_copy(result, set); + return result; +} + +static +void lp_feasibility_set_int_destruct(lp_feasibility_set_int_t* set) { + lp_int_ring_detach(set->K); + free(set->elements); +} + +void lp_feasibility_set_int_delete(lp_feasibility_set_int_t* set) { + assert(set); + lp_feasibility_set_int_destruct(set); + free(set); +} + +void lp_feasibility_set_int_assign(lp_feasibility_set_int_t* set, const lp_feasibility_set_int_t* from) { + if (set != from) { + lp_feasibility_set_int_destruct(set); + lp_feasibility_set_int_construct_copy(set, from); + } +} + +void lp_feasibility_set_int_swap(lp_feasibility_set_int_t* s1, lp_feasibility_set_int_t* s2) { + lp_feasibility_set_int_t tmp = *s1; + *s1 = *s2; + *s2 = tmp; +} + +int lp_feasibility_set_int_is_empty(const lp_feasibility_set_int_t* set) { + if (!set->inverted && set->size == 0) return 1; + if (set->inverted && lp_integer_cmp_int(lp_Z, &set->K->M, set->size) == 0) return 1; + return 0; +} + +int lp_feasibility_set_int_is_full(const lp_feasibility_set_int_t* set) { + if (set->inverted && set->size == 0) return 1; + if (!set->inverted && lp_integer_cmp_int(lp_Z, &set->K->M, set->size) == 0) return 1; + return 0; +} + +int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set) { + assert(lp_integer_cmp_int(lp_Z, &set->K->M, 2) > 0); + if (set->inverted && set->size == 1) return 1; + if (!set->inverted && lp_integer_cmp_int(lp_Z, &set->K->M, set->size + 1) == 0) return 1; + return 0; +} + +/** returns true if value is in elements. Assumes that the elements are sorted. */ +static +bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_integer_t* value, size_t *pos) { + if (set->size == 0){ + return false; + } + assert(set->elements); + // including l and r + size_t l = 0, r = set->size - 1; + while (l <= r) { + size_t p = (r + l) >> 1; + int cmp = lp_integer_cmp(lp_Z, set->elements + p, value); + if (cmp < 0) { + // continue left + r = p - 1; + } else if (cmp > 0) { + // continue right + l = p + 1; + } else { + // found + if (pos) + *pos = p; + return true; + } + } + return false; +} + +int lp_feasibility_set_int_contains(const lp_feasibility_set_int_t* set, const lp_integer_t* value) { + bool found = lp_feasibility_set_int_find(set, value, NULL); + return found != set->inverted; +} + +void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_integer_t* value) { + assert(!lp_feasibility_set_int_is_empty(set)); + if (!set->inverted) { + size_t pos = random() % set->size; + lp_integer_assign(lp_Z, value, set->elements + pos); + } else { + assert(false); + // TODO implement + // get random element between (incl.) 0 and (|K| - size) + // find and add number of <= element + } +} + +/** Calculates i1 \cup i2 */ +static +size_t ordered_integer_set_union(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size + i2_size; + *result = malloc(max_size * sizeof(lp_integer_t)); + size_t result_size = 0; + + size_t p1 = 0, p2 = 0; + while (p1 < i1_size && p2 < i2_size) { + int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); + if (cmp < 0) { + lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + p1 ++; + } else if (cmp > 0) { + lp_integer_construct_copy(lp_Z, *result + result_size, i2 + p2); + p2 ++; + } else { + lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + p1 ++; p2 ++; + } + result_size ++; + } + while (p1 < i1_size) { + lp_integer_construct_copy(lp_Z, *result + result_size++, i1 + p1++); + } + while (p2 < i2_size) { + lp_integer_construct_copy(lp_Z, *result + result_size++, i2 + p2++); + } + *result = realloc(*result, result_size * sizeof(lp_integer_t)); + return result_size; +} + +/** Calculates i1 \cap i2 */ +static +size_t ordered_integer_set_intersect(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size < i2_size ? i1_size : i2_size; + *result = malloc(max_size * sizeof(lp_integer_t)); + size_t result_size = 0; + + size_t p1 = 0, p2 = 0; + while (p1 < i1_size && p2 < i2_size) { + int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); + if (cmp < 0) { + p2 ++; + } else if (cmp > 0) { + p1 ++; + } else { + lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + p1 ++; p2 ++; + result_size ++; + } + } + *result = realloc(*result, result_size * sizeof(lp_integer_t)); + return result_size; +} + +/** Calculates i1 \setminus i2 */ +static +size_t ordered_integer_set_minus(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size; + *result = malloc(max_size * sizeof(lp_integer_t)); + size_t result_size = 0; + + size_t p1 = 0, p2 = 0; + while (p1 < i1_size) { + bool i2_found = false; + while(p2 < i2_size) { + // as long i2's value is smaller than current i1, we continue + int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); + if (cmp == 0) { + i2_found = true; + } + if (cmp <= 0) { + break; + } + p2 ++; + } + if (!i2_found) { + lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + result_size ++; + } + p1 ++; + } + *result = realloc(*result, result_size * sizeof(lp_integer_t)); + return result_size; +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + assert(lp_int_ring_equal(s1->K, s2->K)); + + lp_feasibility_set_int_t *result = lp_feasibility_set_int_new_empty(s1->K); + size_t s; + + if (s1->inverted && s2->inverted) { + result->inverted = true; + s = ordered_integer_set_union(&result->elements, + s1->elements,s1->size, + s2->elements, s2->size); + } else if (s1->inverted && !s2->inverted) { + result->inverted = false; + s = ordered_integer_set_minus(&result->elements, + s2->elements, s2->size, + s1->elements, s1->size); + } else if (!s1->inverted && s2->inverted) { + result->inverted = false; + s = ordered_integer_set_minus(&result->elements, + s1->elements, s1->size, + s2->elements, s2->size); + } else { + assert(!s1->inverted && !s2->inverted); + result->inverted = false; + s = ordered_integer_set_intersect(&result->elements, + s1->elements, s1->size, + s2->elements, s2->size); + } + result->capacity = result->size = s; + return result; +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_intersect_status_t* status) { + +} + +void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from) { + lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_union(s, from); + lp_feasibility_set_int_swap(tmp, s); + lp_feasibility_set_int_delete(tmp); +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + assert(lp_int_ring_equal(s1->K, s2->K)); + + lp_feasibility_set_int_t *result = lp_feasibility_set_int_new_empty(s1->K); + size_t s; + + if (s1->inverted && s2->inverted) { + result->inverted = true; + s = ordered_integer_set_intersect(&result->elements, + s1->elements,s1->size, + s2->elements, s2->size); + } else if (s1->inverted && !s2->inverted) { + result->inverted = true; + s = ordered_integer_set_minus(&result->elements, + s1->elements, s1->size, + s2->elements, s2->size); + } else if (!s1->inverted && s2->inverted) { + result->inverted = true; + s = ordered_integer_set_minus(&result->elements, + s2->elements, s2->size, + s1->elements, s1->size); + } else { + assert(!s1->inverted && !s2->inverted); + result->inverted = false; + s = ordered_integer_set_union(&result->elements, + s1->elements, s1->size, + s2->elements, s2->size); + } + result->capacity = result->size = s; + return result; +} diff --git a/src/polynomial/feasibility_set_int.h b/src/polynomial/feasibility_set_int.h new file mode 100644 index 00000000..46c937ff --- /dev/null +++ b/src/polynomial/feasibility_set_int.h @@ -0,0 +1,21 @@ +/** + * Copyright 2024, SRI International. + * + * This file is part of LibPoly. + * + * LibPoly is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * LibPoly 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 Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with LibPoly. If not, see . + */ + +#pragma once + From 0b603a8385f3bd3eda95f5bd3054439551757197 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 6 Mar 2024 14:56:03 -0800 Subject: [PATCH 02/10] intersection and printing done --- include/feasibility_set_int.h | 23 +- src/polynomial/feasibility_set_int.c | 324 +++++++++++++++++++++------ 2 files changed, 269 insertions(+), 78 deletions(-) diff --git a/include/feasibility_set_int.h b/include/feasibility_set_int.h index f2b27d83..61aff761 100644 --- a/include/feasibility_set_int.h +++ b/include/feasibility_set_int.h @@ -41,6 +41,7 @@ struct lp_feasibility_set_int_struct { /** Number of elements */ size_t size; + // TODO remove capacity? /** Capacity of the elements table */ size_t capacity; @@ -98,6 +99,11 @@ int lp_feasibility_set_int_is_full(const lp_feasibility_set_int_t* set); */ int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set); +/** + * assigns the size of the set to out + */ +void lp_feasibility_set_int_size(const lp_feasibility_set_int_t *set, lp_integer_t *out); + /** * Check if the given value belongs to the set. */ @@ -119,18 +125,25 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_ lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); typedef enum { - LP_FEASIBILITY_SET_INT_INTERSECT_S1, - LP_FEASIBILITY_SET_INT_INTERSECT_S2, + LP_FEASIBILITY_SET_INT_S1, + LP_FEASIBILITY_SET_INT_S2, LP_FEASIBILITY_SET_INT_NEW, LP_FEASIBILITY_SET_INT_EMPTY -} lp_feasibility_set_int_intersect_status_t; +} lp_feasibility_set_int_status_t; /** * Get intersection of the two sets, returns the status in the given variable. - * The set s1 is given precedence so LP_FEASIBILITY_SET_INTERSECT_S2 is the + * The set s1 is given precedence so LP_FEASIBILITY_SET_S2 is the * status only if the intersect is not s1. */ -lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_intersect_status_t* status); +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t * status); + +/** + * Get union of the two sets, returns the status in the given variable. + * The set s1 is given precedence so LP_FEASIBILITY_SET_S2 is the + * status only if the union is not s1. + */ +lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t* status); /** * Add one set to another, i.e. s = s \cup from. diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index 36b1052b..800b3c63 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -23,6 +23,8 @@ #include #include +#include "utils/u_memstream.h" + static int int_cmp(const void *i1, const void *i2) { return lp_integer_cmp(lp_Z, i1, i2); @@ -128,6 +130,27 @@ int lp_feasibility_set_int_is_full(const lp_feasibility_set_int_t* set) { return 0; } +void lp_feasibility_set_int_size(const lp_feasibility_set_int_t *set, lp_integer_t *out) { + lp_integer_assign_int(lp_Z, out, set->size); + if (set->inverted) { + lp_integer_sub(lp_Z, out, &set->K->M, out); + } +} + +static +size_t lp_feasibility_set_int_size_approx(const lp_feasibility_set_int_t *set) { + if (!set->inverted) { + return set->size; + } else { + if (mpz_fits_ulong_p(&set->K->M)) { + return lp_integer_to_int(&set->K->M) - set->size; + } else { + // size can't be big enough for an actual size of 0 or 1 + return ULONG_MAX; + } + } +} + int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set) { assert(lp_integer_cmp_int(lp_Z, &set->K->M, 2) > 0); if (set->inverted && set->size == 1) return 1; @@ -183,161 +206,316 @@ void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_i /** Calculates i1 \cup i2 */ static -size_t ordered_integer_set_union(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { +lp_feasibility_set_int_status_t ordered_integer_set_union( + lp_integer_t **result, size_t *result_size, + const lp_integer_t *i1, size_t i1_size, + const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size + i2_size; + *result_size = 0; + if (i1_size == 0 && i2_size == 0) { + return LP_FEASIBILITY_SET_INT_EMPTY; + } + *result = malloc(max_size * sizeof(lp_integer_t)); - size_t result_size = 0; + bool just_i1 = true, just_i2 = true; size_t p1 = 0, p2 = 0; while (p1 < i1_size && p2 < i2_size) { int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); if (cmp < 0) { - lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); + just_i2 = false; p1 ++; } else if (cmp > 0) { - lp_integer_construct_copy(lp_Z, *result + result_size, i2 + p2); + lp_integer_construct_copy(lp_Z, *result + *result_size, i2 + p2); + just_i1 = false; p2 ++; } else { - lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); p1 ++; p2 ++; } - result_size ++; + (*result_size) ++; } while (p1 < i1_size) { - lp_integer_construct_copy(lp_Z, *result + result_size++, i1 + p1++); + lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1++); + (*result_size) ++; + just_i2 = false; } while (p2 < i2_size) { - lp_integer_construct_copy(lp_Z, *result + result_size++, i2 + p2++); + lp_integer_construct_copy(lp_Z, *result + *result_size, i2 + p2++); + (*result_size) ++; + just_i1 = false; + } + *result = realloc(*result, *result_size * sizeof(lp_integer_t)); + + if (just_i1) { + return LP_FEASIBILITY_SET_INT_S1; + } else if (just_i2) { + return LP_FEASIBILITY_SET_INT_S2; + } else { + return LP_FEASIBILITY_SET_INT_NEW; } - *result = realloc(*result, result_size * sizeof(lp_integer_t)); - return result_size; } /** Calculates i1 \cap i2 */ static -size_t ordered_integer_set_intersect(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { +lp_feasibility_set_int_status_t ordered_integer_set_intersect( + lp_integer_t **result, size_t *result_size, + const lp_integer_t *i1, size_t i1_size, + const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size < i2_size ? i1_size : i2_size; + *result_size = 0; + if (i1_size == 0 || i2_size == 0) { + return LP_FEASIBILITY_SET_INT_EMPTY; + } + *result = malloc(max_size * sizeof(lp_integer_t)); - size_t result_size = 0; size_t p1 = 0, p2 = 0; + bool all_i1 = true, all_i2 = true; while (p1 < i1_size && p2 < i2_size) { int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); if (cmp < 0) { p2 ++; + all_i2 = false; } else if (cmp > 0) { p1 ++; + all_i1 = false; } else { - lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); + lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); p1 ++; p2 ++; - result_size ++; + (*result_size) ++; } } - *result = realloc(*result, result_size * sizeof(lp_integer_t)); - return result_size; + + *result = realloc(*result, *result_size * sizeof(lp_integer_t)); + + if (*result_size == 0) { + return LP_FEASIBILITY_SET_INT_EMPTY; + } else if (all_i1) { + return LP_FEASIBILITY_SET_INT_S1; + } else if (all_i2) { + return LP_FEASIBILITY_SET_INT_S2; + } else { + return LP_FEASIBILITY_SET_INT_NEW; + } } /** Calculates i1 \setminus i2 */ static -size_t ordered_integer_set_minus(lp_integer_t **result, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { +lp_feasibility_set_int_status_t ordered_integer_set_minus( + lp_integer_t **result, size_t *result_size, + const lp_integer_t *i1, size_t i1_size, + const lp_integer_t *i2, size_t i2_size) { + size_t max_size = i1_size; + *result_size = 0; *result = malloc(max_size * sizeof(lp_integer_t)); - size_t result_size = 0; size_t p1 = 0, p2 = 0; while (p1 < i1_size) { - bool i2_found = false; + bool found = false; while(p2 < i2_size) { // as long i2's value is smaller than current i1, we continue int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); if (cmp == 0) { - i2_found = true; + found = true; } if (cmp <= 0) { break; } p2 ++; } - if (!i2_found) { - lp_integer_construct_copy(lp_Z, *result + result_size, i1 + p1); - result_size ++; + if (!found) { + lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); + (*result_size) ++; } p1 ++; } - *result = realloc(*result, result_size * sizeof(lp_integer_t)); - return result_size; + *result = realloc(*result, *result_size * sizeof(lp_integer_t)); + + if (*result_size == 0) { + return LP_FEASIBILITY_SET_INT_EMPTY; + } else if (*result_size == i1_size) { + return LP_FEASIBILITY_SET_INT_S1; + } else { + return LP_FEASIBILITY_SET_INT_NEW; + } +} + +static +void lp_feasibility_set_int_invert(lp_feasibility_set_int_t *set) { + assert(set->K != lp_Z); + // don't invert big fields + assert(lp_integer_cmp_int(lp_Z, &set->K->M, 10000) < 0); + + size_t cnt = lp_integer_to_int(&set->K->M); + assert(set->size <= cnt); + cnt -= set->size; + + lp_integer_t *new = malloc(cnt * sizeof(lp_integer_t)); + lp_integer_t *old = set->elements; + size_t pos_new = 0; + size_t pos_old = 0; + + long lb = lp_integer_to_int(&set->K->lb); + long ub = lp_integer_to_int(&set->K->ub); + for (long val = lb; val <= ub; ++val) { + assert(pos_new < cnt); + assert(pos_old >= set->size || lp_integer_cmp_int(lp_Z, old + pos_old, val) >= 0); + if (pos_old < set->size && lp_integer_cmp_int(lp_Z, old + pos_old, val) == 0) { + ++ pos_old; + } else { + lp_integer_construct_from_int(lp_Z, new + pos_new, val); + ++ pos_new; + } + } + + free(old); + set->elements = new; + set->size = cnt; + set->capacity = cnt; + set->inverted = !set->inverted; +} + +static inline +lp_feasibility_set_int_status_t invert_i1_i2(lp_feasibility_set_int_status_t status) { + if (status == LP_FEASIBILITY_SET_INT_S1) { return LP_FEASIBILITY_SET_INT_S2; } + if (status == LP_FEASIBILITY_SET_INT_S2) { return LP_FEASIBILITY_SET_INT_S1; } + return status; } lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + lp_feasibility_set_int_status_t status; + return lp_feasibility_set_int_intersect_with_status(s1, s2, &status); +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t * status) { assert(lp_int_ring_equal(s1->K, s2->K)); - lp_feasibility_set_int_t *result = lp_feasibility_set_int_new_empty(s1->K); - size_t s; + lp_feasibility_set_int_t *result; if (s1->inverted && s2->inverted) { + result = lp_feasibility_set_int_new_empty(s1->K); + *status = ordered_integer_set_union(&result->elements, &result->size, + s1->elements, s1->size, s2->elements, + s2->size); result->inverted = true; - s = ordered_integer_set_union(&result->elements, - s1->elements,s1->size, - s2->elements, s2->size); - } else if (s1->inverted && !s2->inverted) { + result->capacity = result->size; + } else if (!s1->inverted && !s2->inverted) { + result = lp_feasibility_set_int_new_empty(s1->K); + *status = ordered_integer_set_intersect(&result->elements, &result->size, + s1->elements, s1->size, s2->elements, + s2->size); result->inverted = false; - s = ordered_integer_set_minus(&result->elements, - s2->elements, s2->size, - s1->elements, s1->size); - } else if (!s1->inverted && s2->inverted) { - result->inverted = false; - s = ordered_integer_set_minus(&result->elements, - s1->elements, s1->size, - s2->elements, s2->size); + result->capacity = result->size; + } else if (s1->inverted && !s2->inverted) { + result = lp_feasibility_set_int_intersect_with_status(s2, s1, status); + // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. + *status = invert_i1_i2(*status); } else { - assert(!s1->inverted && !s2->inverted); - result->inverted = false; - s = ordered_integer_set_intersect(&result->elements, - s1->elements, s1->size, - s2->elements, s2->size); + assert(!s1->inverted && s2->inverted); + if (s1->size > lp_feasibility_set_int_size_approx(s2)) { + // s2 could be the smaller set, LP_FEASIBILITY_SET_INT_S2 is possible + // TODO this effort could be saved in case we don't care about the status + lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_new_copy(s2); + lp_feasibility_set_int_invert(tmp); + result = lp_feasibility_set_int_intersect_with_status(s1, tmp, status); + lp_feasibility_set_int_delete(tmp); + } else { + // s1 is the smaller set, LP_FEASIBILITY_SET_INT_S2 is not possible + result = lp_feasibility_set_int_new_empty(s1->K); + *status = ordered_integer_set_minus(&result->elements, &result->size, + s1->elements, s1->size, + s2->elements, s2->size); + result->inverted = false; + result->capacity = result->size; + } } - result->capacity = result->size = s; - return result; -} - -lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_intersect_status_t* status) { + return result; } -void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from) { - lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_union(s, from); - lp_feasibility_set_int_swap(tmp, s); - lp_feasibility_set_int_delete(tmp); +lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + lp_feasibility_set_int_status_t status; + return lp_feasibility_set_int_union_with_status(s1, s2, &status); } -lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { +lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t* status) { assert(lp_int_ring_equal(s1->K, s2->K)); lp_feasibility_set_int_t *result = lp_feasibility_set_int_new_empty(s1->K); - size_t s; if (s1->inverted && s2->inverted) { + *status = ordered_integer_set_intersect(&result->elements, &result->size, + s1->elements, s1->size, + s2->elements, s2->size); result->inverted = true; - s = ordered_integer_set_intersect(&result->elements, - s1->elements,s1->size, - s2->elements, s2->size); - } else if (s1->inverted && !s2->inverted) { - result->inverted = true; - s = ordered_integer_set_minus(&result->elements, - s1->elements, s1->size, - s2->elements, s2->size); + result->capacity = result->size; + } else if (!s1->inverted && !s2->inverted) { + *status = ordered_integer_set_union(&result->elements, &result->size, + s1->elements, s1->size, + s2->elements, s2->size); + result->inverted = false; + result->capacity = result->size; } else if (!s1->inverted && s2->inverted) { - result->inverted = true; - s = ordered_integer_set_minus(&result->elements, - s2->elements, s2->size, - s1->elements, s1->size); + result = lp_feasibility_set_int_union_with_status(s2, s1, status); + // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. + *status = invert_i1_i2(*status); } else { - assert(!s1->inverted && !s2->inverted); - result->inverted = false; - s = ordered_integer_set_union(&result->elements, - s1->elements, s1->size, - s2->elements, s2->size); + assert (s1->inverted && !s2->inverted); + if (s2->size > lp_feasibility_set_int_size_approx(s1)) { + // s2 is be the bigger set, LP_FEASIBILITY_SET_INT_S2 is possible + // TODO this effort could be saved in case we don't care about the status + lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_new_copy(s1); + lp_feasibility_set_int_invert(tmp); + result = lp_feasibility_set_int_intersect_with_status(tmp, s2, status); + lp_feasibility_set_int_delete(tmp); + } else { + // s1 is the bigger set, LP_FEASIBILITY_SET_INT_S2 is not possible + *status = ordered_integer_set_minus(&result->elements, &result->size, + s1->elements, s1->size, + s2->elements, s2->size); + result->inverted = true; + result->capacity = result->size; + } } - result->capacity = result->size = s; + return result; } + +void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from) { + lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_union(s, from); + lp_feasibility_set_int_swap(tmp, s); + lp_feasibility_set_int_delete(tmp); +} + +int lp_feasibility_set_int_print(const lp_feasibility_set_int_t* set, FILE* out) { + int ret = 0; + if (set->inverted) { + ret += fprintf(out, "F \\"); + } + ret += fprintf(out, "{ "); + for(size_t i = 0; i < set->size; ++ i) { + if (i) { + ret += fprintf(out, ", "); + } + ret += lp_integer_print(&set->elements[i], out); + } + ret += fprintf(out, " } in "); + ret += lp_int_ring_print(set->K, out); + return ret; +} + +char* lp_feasibility_set_int_to_string(const lp_feasibility_set_int_t* set) { + struct u_memstream mem; + char* str = 0; + size_t size = 0; + u_memstream_open(&mem, &str, &size); + FILE* f = u_memstream_get(&mem); + lp_feasibility_set_int_print(set, f); + u_memstream_close(&mem); + return str; +} From f0dfdd4e7ef8682fd95d602c6b8b84847126d088 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 6 Mar 2024 16:52:52 -0800 Subject: [PATCH 03/10] removed capacity --- include/feasibility_set_int.h | 4 ---- src/polynomial/feasibility_set_int.c | 19 +------------------ 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/include/feasibility_set_int.h b/include/feasibility_set_int.h index 61aff761..2ce4bd95 100644 --- a/include/feasibility_set_int.h +++ b/include/feasibility_set_int.h @@ -41,10 +41,6 @@ struct lp_feasibility_set_int_struct { /** Number of elements */ size_t size; - // TODO remove capacity? - /** Capacity of the elements table */ - size_t capacity; - /** Vector feasibility elements */ lp_integer_t* elements; }; diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index 800b3c63..6cbb2ead 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -30,23 +30,13 @@ int int_cmp(const void *i1, const void *i2) { return lp_integer_cmp(lp_Z, i1, i2); } -static -void lp_feasibility_set_int_ensure_capacity(lp_feasibility_set_int_t* s, size_t capacity) { - if (capacity && capacity > s->capacity) { - s->capacity = capacity; - s->elements = realloc(s->elements, s->capacity * sizeof(lp_integer_t)); - } -} - static void lp_feasibility_set_int_construct(lp_int_ring_t *K, lp_feasibility_set_int_t* s, size_t size, bool inverted) { s->K = K; lp_int_ring_attach(s->K); - s->capacity = 0; s->size = size; s->inverted = inverted; - s->elements = NULL; - lp_feasibility_set_int_ensure_capacity(s, size); + s->elements = size ? malloc(s->size * sizeof(lp_integer_t)) : NULL; } lp_feasibility_set_int_t* lp_feasibility_set_int_new_empty(lp_int_ring_t *K) { @@ -376,7 +366,6 @@ void lp_feasibility_set_int_invert(lp_feasibility_set_int_t *set) { free(old); set->elements = new; set->size = cnt; - set->capacity = cnt; set->inverted = !set->inverted; } @@ -403,14 +392,12 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ s1->elements, s1->size, s2->elements, s2->size); result->inverted = true; - result->capacity = result->size; } else if (!s1->inverted && !s2->inverted) { result = lp_feasibility_set_int_new_empty(s1->K); *status = ordered_integer_set_intersect(&result->elements, &result->size, s1->elements, s1->size, s2->elements, s2->size); result->inverted = false; - result->capacity = result->size; } else if (s1->inverted && !s2->inverted) { result = lp_feasibility_set_int_intersect_with_status(s2, s1, status); // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. @@ -431,7 +418,6 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ s1->elements, s1->size, s2->elements, s2->size); result->inverted = false; - result->capacity = result->size; } } @@ -453,13 +439,11 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feas s1->elements, s1->size, s2->elements, s2->size); result->inverted = true; - result->capacity = result->size; } else if (!s1->inverted && !s2->inverted) { *status = ordered_integer_set_union(&result->elements, &result->size, s1->elements, s1->size, s2->elements, s2->size); result->inverted = false; - result->capacity = result->size; } else if (!s1->inverted && s2->inverted) { result = lp_feasibility_set_int_union_with_status(s2, s1, status); // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. @@ -479,7 +463,6 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feas s1->elements, s1->size, s2->elements, s2->size); result->inverted = true; - result->capacity = result->size; } } From ed799c6c00ba08fc892647e7d0fdf040acd49230 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 6 Mar 2024 16:53:23 -0800 Subject: [PATCH 04/10] added lp_polynomial_constraint_get_feasible_set_Zp --- include/polynomial.h | 11 +++++++++ src/polynomial/polynomial.c | 46 +++++++++++++++++++++++++++++++++++++ 2 files changed, 57 insertions(+) diff --git a/include/polynomial.h b/include/polynomial.h index 734bfa90..58604ec3 100644 --- a/include/polynomial.h +++ b/include/polynomial.h @@ -343,6 +343,17 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t */ lp_feasibility_set_t* lp_polynomial_constraint_get_feasible_set(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, int negated, const lp_assignment_t* M); +/** + * Given a polynomial A(x1, ..., xn, y) with y being the top variable, a sign + * condition, and an assignment M that assigns x1, ..., xn, the function returns + * a subset of Zp where + * + * sgn(A(M(x1), ..., M(xn), y)) = sgn_condition . + * + * If negated is true, the constraint is considered negated. + */ +lp_feasibility_set_int_t* lp_polynomial_constraint_get_feasible_set_Zp(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, int negated, const lp_assignment_t* M); + /** * Given a polynomial A(x1, ..., xn) and a sign condition, the function returns * tries to infer bounds on the variables and stores them into the given interval diff --git a/src/polynomial/polynomial.c b/src/polynomial/polynomial.c index 80c07c21..19ad809c 100644 --- a/src/polynomial/polynomial.c +++ b/src/polynomial/polynomial.c @@ -19,6 +19,7 @@ #include #include +#include #include #include @@ -33,6 +34,7 @@ #include "number/integer.h" #include "polynomial/feasibility_set.h" +#include "polynomial/feasibility_set_int.h" #include "polynomial/polynomial_vector.h" #include "utils/debug_trace.h" @@ -2036,6 +2038,50 @@ lp_feasibility_set_t* lp_polynomial_root_constraint_get_feasible_set(const lp_po } +lp_feasibility_set_int_t* lp_polynomial_constraint_get_feasible_set_Zp(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, int negated, const lp_assignment_t* M) { + const lp_polynomial_context_t *ctx = lp_polynomial_get_context(A); + assert(ctx->K != lp_Z); + assert(lp_sign_condition_Zp_valid(sgn_condition)); + + // The ring + lp_int_ring_t *K = ctx->K; + + // Negate the constraint if negated + if (negated) { + sgn_condition = lp_sign_condition_negate(sgn_condition); + } + + assert(lp_polynomial_is_univariate_m(A, M)); + + lp_upolynomial_t *upoly = lp_polynomial_to_univariate_m(A, M); + if (lp_upolynomial_degree(upoly) == 0) { + if (lp_upolynomial_is_zero(upoly)) { + return sgn_condition == LP_SGN_EQ_0 ? lp_feasibility_set_int_new_full(K) : lp_feasibility_set_int_new_empty(K); + } else { + return sgn_condition == LP_SGN_EQ_0 ? lp_feasibility_set_int_new_empty(K) : lp_feasibility_set_int_new_full(K); + } + } + + lp_feasibility_set_int_t *result = sgn_condition == LP_SGN_EQ_0 ? lp_feasibility_set_int_new_empty(K) : lp_feasibility_set_int_new_full(K); + + lp_upolynomial_roots_find_Zp(upoly, &result->elements, &result->size); + +#ifndef NDEBUG + { + lp_integer_t tmp; + lp_integer_construct(&tmp); + for (size_t i = 0; i < result->size; ++i) { + lp_upolynomial_evaluate_at_integer(upoly, &result->elements[i], &tmp); + assert(lp_integer_is_zero(lp_upolynomial_ring(upoly) , &tmp)); + } + lp_integer_destruct(&tmp); + } +#endif + + lp_upolynomial_delete(upoly); + return result; +} + void lp_polynomial_get_variables(const lp_polynomial_t* A, lp_variable_list_t* vars) { coefficient_get_variables(&A->data, vars); } From 709d2dfb05e93a6298feb13f1689f304eba27478 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 6 Mar 2024 18:53:24 -0800 Subject: [PATCH 05/10] added doctest tests for c files --- CMakeLists.txt | 1 + test/poly/CMakeLists.txt | 14 +++++++ test/poly/test_feasible_int_set.cpp | 58 +++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+) create mode 100644 test/poly/CMakeLists.txt create mode 100644 test/poly/test_feasible_int_set.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index c22590e6..32b5534d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -82,6 +82,7 @@ endif() if (BUILD_TESTING) # Configure the C++ tests enable_testing() + add_subdirectory(test/poly) add_subdirectory(test/polyxx) endif() diff --git a/test/poly/CMakeLists.txt b/test/poly/CMakeLists.txt new file mode 100644 index 00000000..49bcf872 --- /dev/null +++ b/test/poly/CMakeLists.txt @@ -0,0 +1,14 @@ +set(poly_tests + test_feasible_int_set +) + +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Werror -Wextra -std=c++11") + +include_directories(${GMP_INCLUDE_DIR}) + +foreach(file ${poly_tests}) + add_executable(${file} ${file}.cpp) + target_include_directories(${file} PUBLIC ${CMAKE_SOURCE_DIR}/include) + add_test(NAME ${file} COMMAND ${file}) + target_link_libraries(${file} poly polyxx) +endforeach() diff --git a/test/poly/test_feasible_int_set.cpp b/test/poly/test_feasible_int_set.cpp new file mode 100644 index 00000000..3aa5b648 --- /dev/null +++ b/test/poly/test_feasible_int_set.cpp @@ -0,0 +1,58 @@ +#define DOCTEST_CONFIG_IMPLEMENT_WITH_MAIN +#include "../polyxx/doctest.h" + +#include +#include + +#include +using namespace poly; +using namespace std; + +static +vector* integer_list_gen(std::initializer_list values) { + auto result = new vector(); + for (int x : values) { + lp_integer_t tmp; + lp_integer_construct_from_int(lp_Z, &tmp, x); + result->push_back(tmp); + } + return result; +} + +static +void integer_list_del(vector *list) { + for (lp_integer_t i : *list) { + lp_integer_destruct(&i); + } + delete list; +} + +TEST_CASE("feasibility_set_int::construct") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 13); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + SUBCASE("feasibility_set_int::construct::full") { + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_full(K); + CHECK(lp_feasibility_set_int_is_full(set)); + lp_feasibility_set_int_delete(set); + } + SUBCASE("feasibility_set_int::construct::empty") { + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_empty(K); + CHECK(lp_feasibility_set_int_is_empty(set)); + lp_feasibility_set_int_delete(set); + } + SUBCASE("feasibility_set_int::construct::integer") { + auto *ints = integer_list_gen({2,1,4,3}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, ints->data(), ints->size(), false); + CHECK_FALSE(lp_feasibility_set_int_is_empty(set)); + CHECK_FALSE(lp_feasibility_set_int_is_full(set)); + CHECK(lp_feasibility_set_int_size_approx(set) == 4); + lp_feasibility_set_int_delete(set); + integer_list_del(ints); + } + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} From da2ac89435807f771d2bed9405a6aac776dd6085 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 7 Mar 2024 10:56:07 -0800 Subject: [PATCH 06/10] Update doc --- include/feasibility_set_int.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/include/feasibility_set_int.h b/include/feasibility_set_int.h index 2ce4bd95..248c025e 100644 --- a/include/feasibility_set_int.h +++ b/include/feasibility_set_int.h @@ -112,11 +112,13 @@ void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_i /** * Get intersection of the two sets. + * s1 and s2 must be over the same ring K. */ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); /** * Get union of the two sets. + * s1 and s2 must be over the same ring K. */ lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); @@ -131,6 +133,7 @@ typedef enum { * Get intersection of the two sets, returns the status in the given variable. * The set s1 is given precedence so LP_FEASIBILITY_SET_S2 is the * status only if the intersect is not s1. + * s1 and s2 must be over the same ring K. */ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t * status); @@ -138,6 +141,7 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ * Get union of the two sets, returns the status in the given variable. * The set s1 is given precedence so LP_FEASIBILITY_SET_S2 is the * status only if the union is not s1. + * s1 and s2 must be over the same ring K. */ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t* status); From e08aa6ef18c2d2d3ce3ab14e0702dee622debc5c Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 6 Mar 2024 18:54:23 -0800 Subject: [PATCH 07/10] adds further test and fixes --- include/feasibility_set_int.h | 15 +- src/polynomial/feasibility_set_int.c | 250 +++++++----- test/poly/test_feasible_int_set.cpp | 584 ++++++++++++++++++++++++++- 3 files changed, 740 insertions(+), 109 deletions(-) diff --git a/include/feasibility_set_int.h b/include/feasibility_set_int.h index 248c025e..5858b154 100644 --- a/include/feasibility_set_int.h +++ b/include/feasibility_set_int.h @@ -41,7 +41,10 @@ struct lp_feasibility_set_int_struct { /** Number of elements */ size_t size; - /** Vector feasibility elements */ + /** + * Vector feasibility elements + * Values are normalized wrt to K, kept sorted and unique + */ lp_integer_t* elements; }; @@ -100,6 +103,11 @@ int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set); */ void lp_feasibility_set_int_size(const lp_feasibility_set_int_t *set, lp_integer_t *out); +/** + * returns the size; guaranteed to be correct if it fits in long + */ +size_t lp_feasibility_set_int_size_approx(const lp_feasibility_set_int_t *set); + /** * Check if the given value belongs to the set. */ @@ -150,6 +158,11 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feas */ void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from); +/** + * Returns true if both sets are equal + */ +bool lp_feasibility_set_int_eq(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2); + /** * Print the set. */ diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index 6cbb2ead..d97a5012 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -51,14 +51,38 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_new_full(lp_int_ring_t *K) { return s; } +static +size_t unique_lp_integer(lp_integer_t *b, size_t size) { + if (size <= 1) return size; + + size_t new_size = 1; + lp_integer_t *first = b, *last = b + size; + lp_integer_t *result = first; + while (++first != last) { + if (lp_integer_cmp(lp_Z, result, first) != 0) { + lp_integer_swap(++result, first); + ++new_size; + } + } + while (++result != last) { + lp_integer_destruct(result); + } + assert(new_size <= size); + return new_size; +} + static void lp_feasibility_set_int_construct_from_integer(lp_feasibility_set_int_t *set, lp_int_ring_t *K, const lp_integer_t *elements, size_t size, bool inverted) { lp_feasibility_set_int_construct(K, set, size, inverted); for (size_t i = 0; i < size; ++ i) { lp_integer_construct_copy(K, set->elements + i, elements + i); } - set->size = size; qsort(set->elements, size, sizeof(lp_integer_t), int_cmp); + size_t new_size = unique_lp_integer(set->elements, size); + if (new_size < size) { + set->elements = realloc(set->elements, new_size * sizeof(lp_integer_t)); + } + set->size = new_size; } lp_feasibility_set_int_t* lp_feasibility_set_int_new_from_integer(lp_int_ring_t *K, const lp_integer_t* elements, size_t elements_size, bool inverted) { @@ -127,7 +151,6 @@ void lp_feasibility_set_int_size(const lp_feasibility_set_int_t *set, lp_integer } } -static size_t lp_feasibility_set_int_size_approx(const lp_feasibility_set_int_t *set) { if (!set->inverted) { return set->size; @@ -148,7 +171,7 @@ int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set) { return 0; } -/** returns true if value is in elements. Assumes that the elements are sorted. */ +/** returns true if value is in elements. Assumes that the elements are sorted and that value is normalized wrt set->K */ static bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_integer_t* value, size_t *pos) { if (set->size == 0){ @@ -156,20 +179,19 @@ bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_i } assert(set->elements); // including l and r - size_t l = 0, r = set->size - 1; + long l = 0, r = set->size - 1; while (l <= r) { - size_t p = (r + l) >> 1; + long p = (r + l) / 2; int cmp = lp_integer_cmp(lp_Z, set->elements + p, value); - if (cmp < 0) { + if (cmp > 0) { // continue left r = p - 1; - } else if (cmp > 0) { + } else if (cmp < 0) { // continue right l = p + 1; } else { // found - if (pos) - *pos = p; + if (pos) { *pos = p; } return true; } } @@ -177,7 +199,11 @@ bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_i } int lp_feasibility_set_int_contains(const lp_feasibility_set_int_t* set, const lp_integer_t* value) { - bool found = lp_feasibility_set_int_find(set, value, NULL); + lp_integer_t value_normalized; + // normalize value before check + lp_integer_construct_copy(set->K, &value_normalized, value); + bool found = lp_feasibility_set_int_find(set, &value_normalized, NULL); + lp_integer_destruct(&value_normalized); return found != set->inverted; } @@ -194,117 +220,116 @@ void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_i } } +typedef enum { + NONE = 0, + S1 = 1, + S2 = 2, + BOTH = 3, +} set_status_internal_t; + /** Calculates i1 \cup i2 */ static -lp_feasibility_set_int_status_t ordered_integer_set_union( +set_status_internal_t ordered_integer_set_union( lp_integer_t **result, size_t *result_size, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { size_t max_size = i1_size + i2_size; - *result_size = 0; if (i1_size == 0 && i2_size == 0) { - return LP_FEASIBILITY_SET_INT_EMPTY; + if (result_size) { *result_size = 0; } + return BOTH; } - *result = malloc(max_size * sizeof(lp_integer_t)); + if (result) { *result = malloc(max_size * sizeof(lp_integer_t)); } bool just_i1 = true, just_i2 = true; - size_t p1 = 0, p2 = 0; + size_t p1 = 0, p2 = 0, pr = 0; while (p1 < i1_size && p2 < i2_size) { int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); if (cmp < 0) { - lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); + if (result) { lp_integer_construct_copy(lp_Z, *result + pr, i1 + p1); } just_i2 = false; p1 ++; } else if (cmp > 0) { - lp_integer_construct_copy(lp_Z, *result + *result_size, i2 + p2); + if (result) { lp_integer_construct_copy(lp_Z, *result + pr, i2 + p2); } just_i1 = false; p2 ++; } else { - lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); + if (result) { lp_integer_construct_copy(lp_Z, *result + pr, i1 + p1); } p1 ++; p2 ++; } - (*result_size) ++; - } - while (p1 < i1_size) { - lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1++); - (*result_size) ++; - just_i2 = false; - } - while (p2 < i2_size) { - lp_integer_construct_copy(lp_Z, *result + *result_size, i2 + p2++); - (*result_size) ++; - just_i1 = false; + pr ++; } - *result = realloc(*result, *result_size * sizeof(lp_integer_t)); - - if (just_i1) { - return LP_FEASIBILITY_SET_INT_S1; - } else if (just_i2) { - return LP_FEASIBILITY_SET_INT_S2; + if (result) { + while (p1 < i1_size) { + lp_integer_construct_copy(lp_Z, *result + pr, i1 + p1); + p1++; pr++; + just_i2 = false; + } + while (p2 < i2_size) { + lp_integer_construct_copy(lp_Z, *result + pr, i2 + p2); + p2++; pr++; + just_i1 = false; + } + *result = realloc(*result, pr * sizeof(lp_integer_t)); } else { - return LP_FEASIBILITY_SET_INT_NEW; + if (p1 < i1_size) { just_i2 = false; pr += (i1_size - p1); } + if (p2 < i2_size) { just_i1 = false; pr += (i2_size - p2); } } + + if (result_size) { *result_size = pr; } + return (just_i1 ? S1 : NONE) | (just_i2 ? S2 : NONE); } /** Calculates i1 \cap i2 */ static -lp_feasibility_set_int_status_t ordered_integer_set_intersect( +set_status_internal_t ordered_integer_set_intersect( lp_integer_t **result, size_t *result_size, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { size_t max_size = i1_size < i2_size ? i1_size : i2_size; - *result_size = 0; if (i1_size == 0 || i2_size == 0) { - return LP_FEASIBILITY_SET_INT_EMPTY; + if (result_size) { *result_size = 0; } + return (i1_size == 0 ? S1 : NONE) | (i2_size == 0 ? S2 : NONE); } - *result = malloc(max_size * sizeof(lp_integer_t)); + if (result) { *result = malloc(max_size * sizeof(lp_integer_t)); } - size_t p1 = 0, p2 = 0; + size_t p1 = 0, p2 = 0, pr = 0; bool all_i1 = true, all_i2 = true; while (p1 < i1_size && p2 < i2_size) { int cmp = lp_integer_cmp(lp_Z, i1 + p1, i2 + p2); - if (cmp < 0) { + if (cmp > 0) { p2 ++; all_i2 = false; - } else if (cmp > 0) { + } else if (cmp < 0) { p1 ++; all_i1 = false; } else { - lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); - p1 ++; p2 ++; - (*result_size) ++; + if (result) { lp_integer_construct_copy(lp_Z, *result + pr, i1 + p1); } + p1 ++; p2 ++; pr ++; } } + if (p1 < i1_size) { all_i1 = false; } + if (p2 < i2_size) { all_i2 = false; } - *result = realloc(*result, *result_size * sizeof(lp_integer_t)); - - if (*result_size == 0) { - return LP_FEASIBILITY_SET_INT_EMPTY; - } else if (all_i1) { - return LP_FEASIBILITY_SET_INT_S1; - } else if (all_i2) { - return LP_FEASIBILITY_SET_INT_S2; - } else { - return LP_FEASIBILITY_SET_INT_NEW; - } + if (result) { *result = realloc(*result, pr * sizeof(lp_integer_t)); } + if (result_size) { *result_size = pr; } + return (all_i1 ? S1 : NONE) | (all_i2 ? S2 : NONE); } /** Calculates i1 \setminus i2 */ static -lp_feasibility_set_int_status_t ordered_integer_set_minus( +set_status_internal_t ordered_integer_set_minus( lp_integer_t **result, size_t *result_size, const lp_integer_t *i1, size_t i1_size, const lp_integer_t *i2, size_t i2_size) { size_t max_size = i1_size; - *result_size = 0; - *result = malloc(max_size * sizeof(lp_integer_t)); + if (result) { *result = malloc(max_size * sizeof(lp_integer_t)); } - size_t p1 = 0, p2 = 0; + size_t p1 = 0, p2 = 0, pr = 0; while (p1 < i1_size) { bool found = false; while(p2 < i2_size) { @@ -319,20 +344,15 @@ lp_feasibility_set_int_status_t ordered_integer_set_minus( p2 ++; } if (!found) { - lp_integer_construct_copy(lp_Z, *result + *result_size, i1 + p1); - (*result_size) ++; + if (result) { lp_integer_construct_copy(lp_Z, *result + pr, i1 + p1); } + pr ++; } p1 ++; } - *result = realloc(*result, *result_size * sizeof(lp_integer_t)); - if (*result_size == 0) { - return LP_FEASIBILITY_SET_INT_EMPTY; - } else if (*result_size == i1_size) { - return LP_FEASIBILITY_SET_INT_S1; - } else { - return LP_FEASIBILITY_SET_INT_NEW; - } + if (result) { *result = realloc(*result, pr * sizeof(lp_integer_t)); } + if (result_size) { *result_size = pr; } + return (pr == i1_size ? S1 : NONE); } static @@ -370,18 +390,26 @@ void lp_feasibility_set_int_invert(lp_feasibility_set_int_t *set) { } static inline -lp_feasibility_set_int_status_t invert_i1_i2(lp_feasibility_set_int_status_t status) { - if (status == LP_FEASIBILITY_SET_INT_S1) { return LP_FEASIBILITY_SET_INT_S2; } - if (status == LP_FEASIBILITY_SET_INT_S2) { return LP_FEASIBILITY_SET_INT_S1; } - return status; +set_status_internal_t invert_i1_i2(set_status_internal_t status) { + return (status & S1 ? S2 : NONE) | (status & S2 ? S1: NONE); } -lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { - lp_feasibility_set_int_status_t status; - return lp_feasibility_set_int_intersect_with_status(s1, s2, &status); +static inline +lp_feasibility_set_int_status_t status_internal_to_external(set_status_internal_t is) { + switch (is) { + case BOTH: + case S1: + return LP_FEASIBILITY_SET_INT_S1; + case S2: + return LP_FEASIBILITY_SET_INT_S2; + default: + case NONE: + return LP_FEASIBILITY_SET_INT_NEW; + } } -lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t * status) { +static +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_internal(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, set_status_internal_t *status) { assert(lp_int_ring_equal(s1->K, s2->K)); lp_feasibility_set_int_t *result; @@ -399,8 +427,7 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ s2->size); result->inverted = false; } else if (s1->inverted && !s2->inverted) { - result = lp_feasibility_set_int_intersect_with_status(s2, s1, status); - // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. + result = lp_feasibility_set_int_intersect_internal(s2, s1, status); *status = invert_i1_i2(*status); } else { assert(!s1->inverted && s2->inverted); @@ -409,7 +436,7 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ // TODO this effort could be saved in case we don't care about the status lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_new_copy(s2); lp_feasibility_set_int_invert(tmp); - result = lp_feasibility_set_int_intersect_with_status(s1, tmp, status); + result = lp_feasibility_set_int_intersect_internal(s1, tmp, status); lp_feasibility_set_int_delete(tmp); } else { // s1 is the smaller set, LP_FEASIBILITY_SET_INT_S2 is not possible @@ -424,29 +451,38 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_ return result; } -lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { - lp_feasibility_set_int_status_t status; - return lp_feasibility_set_int_union_with_status(s1, s2, &status); +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + set_status_internal_t is; + return lp_feasibility_set_int_intersect_internal(s1, s2, &is); } -lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t* status) { +lp_feasibility_set_int_t* lp_feasibility_set_int_intersect_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t *status) { + set_status_internal_t is; + lp_feasibility_set_int_t *result = lp_feasibility_set_int_intersect_internal(s1, s2, &is); + *status = lp_feasibility_set_int_is_empty(result) ? LP_FEASIBILITY_SET_INT_EMPTY : status_internal_to_external(is); + return result; +} + +static +lp_feasibility_set_int_t* lp_feasibility_set_int_union_internal(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, set_status_internal_t * status) { assert(lp_int_ring_equal(s1->K, s2->K)); - lp_feasibility_set_int_t *result = lp_feasibility_set_int_new_empty(s1->K); + lp_feasibility_set_int_t *result; if (s1->inverted && s2->inverted) { + result = lp_feasibility_set_int_new_empty(s1->K); *status = ordered_integer_set_intersect(&result->elements, &result->size, s1->elements, s1->size, s2->elements, s2->size); result->inverted = true; } else if (!s1->inverted && !s2->inverted) { + result = lp_feasibility_set_int_new_empty(s1->K); *status = ordered_integer_set_union(&result->elements, &result->size, s1->elements, s1->size, s2->elements, s2->size); result->inverted = false; } else if (!s1->inverted && s2->inverted) { - result = lp_feasibility_set_int_union_with_status(s2, s1, status); - // TODO this gives I2 precedence in case I1 == I2. Maybe introduce a BOTH option. + result = lp_feasibility_set_int_union_internal(s2, s1, status); *status = invert_i1_i2(*status); } else { assert (s1->inverted && !s2->inverted); @@ -455,9 +491,10 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feas // TODO this effort could be saved in case we don't care about the status lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_new_copy(s1); lp_feasibility_set_int_invert(tmp); - result = lp_feasibility_set_int_intersect_with_status(tmp, s2, status); + result = lp_feasibility_set_int_union_internal(tmp, s2, status); lp_feasibility_set_int_delete(tmp); } else { + result = lp_feasibility_set_int_new_empty(s1->K); // s1 is the bigger set, LP_FEASIBILITY_SET_INT_S2 is not possible *status = ordered_integer_set_minus(&result->elements, &result->size, s1->elements, s1->size, @@ -469,12 +506,45 @@ lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feas return result; } +lp_feasibility_set_int_t* lp_feasibility_set_int_union(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + set_status_internal_t status; + return lp_feasibility_set_int_union_internal(s1, s2, &status); +} + +lp_feasibility_set_int_t* lp_feasibility_set_int_union_with_status(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2, lp_feasibility_set_int_status_t* status) { + set_status_internal_t is; + lp_feasibility_set_int_t *result = lp_feasibility_set_int_union_internal(s1, s2, &is); + *status = lp_feasibility_set_int_is_empty(result) ? LP_FEASIBILITY_SET_INT_EMPTY : status_internal_to_external(is); + return result; +} + void lp_feasibility_set_int_add(lp_feasibility_set_int_t* s, const lp_feasibility_set_int_t* from) { lp_feasibility_set_int_t *tmp = lp_feasibility_set_int_union(s, from); lp_feasibility_set_int_swap(tmp, s); lp_feasibility_set_int_delete(tmp); } +bool lp_feasibility_set_int_eq(const lp_feasibility_set_int_t* s1, const lp_feasibility_set_int_t* s2) { + if (s1->inverted == s2->inverted) { + if (s1->size != s2->size) { + return false; + } + for (size_t i = 0; i < s1->size; ++i) { + if (lp_integer_cmp(lp_Z, s1->elements + i, s2->elements + i) != 0) { + return false; + } + } + return true; + } else { + if (lp_feasibility_set_int_size_approx(s1) != lp_feasibility_set_int_size_approx(s2)) { + return false; + } + size_t count; + ordered_integer_set_intersect(NULL, &count, s1->elements, s1->size, s2->elements, s2->size); + return count == 0; + } +} + int lp_feasibility_set_int_print(const lp_feasibility_set_int_t* set, FILE* out) { int ret = 0; if (set->inverted) { diff --git a/test/poly/test_feasible_int_set.cpp b/test/poly/test_feasible_int_set.cpp index 3aa5b648..6de318b9 100644 --- a/test/poly/test_feasible_int_set.cpp +++ b/test/poly/test_feasible_int_set.cpp @@ -8,24 +8,46 @@ using namespace poly; using namespace std; -static -vector* integer_list_gen(std::initializer_list values) { - auto result = new vector(); - for (int x : values) { - lp_integer_t tmp; - lp_integer_construct_from_int(lp_Z, &tmp, x); - result->push_back(tmp); +/** + * Struct to handle a list of lp_integer_t (and proper deallocate it) + */ +struct integer_list { +private: + vector *v; +public: + integer_list() : v(new vector()) {} + integer_list(initializer_list values) : integer_list() { + for (int x : values) { + lp_integer_t tmp; + lp_integer_construct_from_int(lp_Z, &tmp, x); + this->v->push_back(tmp); + } + } + integer_list(const integer_list &other) : integer_list() { + for (const lp_integer_t x : *other.v) { + lp_integer_t tmp; + lp_integer_construct_copy(lp_Z, &tmp, &x); + this->v->push_back(tmp); + } + } + integer_list(integer_list &&other) noexcept : v(other.v) { + other.v = nullptr; + } + ~integer_list() { + if (this->v == nullptr) return; + for (lp_integer_t i : *this->v) { + lp_integer_destruct(&i); + } + delete this->v; } - return result; -} -static -void integer_list_del(vector *list) { - for (lp_integer_t i : *list) { - lp_integer_destruct(&i); + lp_feasibility_set_int_t* gen_set(lp_int_ring_t *K, bool inverted) const { + return lp_feasibility_set_int_new_from_integer(K, this->v->data(), this->v->size(), inverted); } - delete list; -} + const lp_integer_t* data() const { return this->v->data(); } + size_t size() const { return this->v->size(); } +}; + TEST_CASE("feasibility_set_int::construct") { lp_integer_t prime; @@ -43,14 +65,540 @@ TEST_CASE("feasibility_set_int::construct") { lp_feasibility_set_int_delete(set); } SUBCASE("feasibility_set_int::construct::integer") { - auto *ints = integer_list_gen({2,1,4,3}); - lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, ints->data(), ints->size(), false); + integer_list l({2,1,4,3}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), false); CHECK_FALSE(lp_feasibility_set_int_is_empty(set)); CHECK_FALSE(lp_feasibility_set_int_is_full(set)); CHECK(lp_feasibility_set_int_size_approx(set) == 4); lp_feasibility_set_int_delete(set); - integer_list_del(ints); } + SUBCASE("feasibility_set_int::construct::integer::invert") { + integer_list l({2,1,4,3}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), true); + CHECK_FALSE(lp_feasibility_set_int_is_empty(set)); + CHECK_FALSE(lp_feasibility_set_int_is_full(set)); + CHECK(lp_feasibility_set_int_size_approx(set) == 9); + CHECK(!lp_feasibility_set_int_contains(set, Integer(3).get_internal())); + CHECK(!lp_feasibility_set_int_contains(set, Integer(1).get_internal())); + CHECK(lp_feasibility_set_int_contains(set, Integer(-1).get_internal())); + CHECK(lp_feasibility_set_int_contains(set, Integer(13).get_internal())); + CHECK(!lp_feasibility_set_int_contains(set, Integer(14).get_internal())); + lp_feasibility_set_int_delete(set); + } + SUBCASE("feasibility_set_int::construct::integer::duplicates") { + integer_list l({1,2,2,14}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), false); + CHECK_FALSE(lp_feasibility_set_int_is_empty(set)); + CHECK_FALSE(lp_feasibility_set_int_is_full(set)); + CHECK(lp_feasibility_set_int_size_approx(set) == 2); + lp_feasibility_set_int_delete(set); + } + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::intersect::inv") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set2_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::intersect::inv1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::intersect::inv_dual") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set2 = integer_list({1,2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set2_inv = integer_list({0,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set1_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::intersect::inv_dual1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv_dual2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv_dual") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::inv4_dual") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::union::inv") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set2_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::union::inv1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::union::inv_dual") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set2 = integer_list({1,2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set2_inv = integer_list({0,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set1_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::union::inv_dual1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv_dual2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv_dual3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union::inv_dual4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set2)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::union") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set2_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::union1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 3); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::intersect") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *set2_inv = integer_list({0,1,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::intersect1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_NEW); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::intersect_empty") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K); + + SUBCASE("feasibility_set_int::intersect_empty1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, empty, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 0); + CHECK(status == LP_FEASIBILITY_SET_INT_EMPTY); + CHECK(lp_feasibility_set_int_is_empty(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_empty2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(empty, set1, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 0); + CHECK(status == LP_FEASIBILITY_SET_INT_EMPTY); + CHECK(lp_feasibility_set_int_is_empty(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_empty3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, empty, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 0); + CHECK(status == LP_FEASIBILITY_SET_INT_EMPTY); + CHECK(lp_feasibility_set_int_is_empty(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_empty4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(empty, set1_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 0); + CHECK(status == LP_FEASIBILITY_SET_INT_EMPTY); + CHECK(lp_feasibility_set_int_is_empty(s)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(empty); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::intersect_full") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K); + + SUBCASE("feasibility_set_int::intersect::intersect_full1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, full, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::intersect_full2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(full, set1, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::intersect_full3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, full, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect::intersect_full4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(full, set1_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(full); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::union_full") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K); + + SUBCASE("feasibility_set_int::union_full1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, full, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 7); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_is_full(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_full2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(full, set1, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 7); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_is_full(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_full3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, full, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 7); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_is_full(s)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_full4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(full, set1_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 7); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_is_full(s)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(full); + + CHECK_EQ(K->ref_count, 1); + lp_int_ring_detach(K); + lp_integer_destruct(&prime); +} + +TEST_CASE("feasibility_set_int::union_empty") { + lp_integer_t prime; + lp_integer_construct_from_int(lp_Z, &prime, 7); + lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K); + + SUBCASE("feasibility_set_int::union_empty1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1, empty, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_empty2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(empty, set1, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_empty3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(set1_inv, empty, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S1); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::union_empty4") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_union_with_status(empty, set1_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 2); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_eq(s, set1)); + lp_feasibility_set_int_delete(s); + } + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(empty); CHECK_EQ(K->ref_count, 1); lp_int_ring_detach(K); From c39f9d17eb1beaf4e703f5f627ffafa06d1807ad Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 7 Mar 2024 18:07:46 -0800 Subject: [PATCH 08/10] further tests --- src/polynomial/feasibility_set_int.c | 32 +++-- test/poly/test_feasible_int_set.cpp | 193 ++++++++++++++++++--------- 2 files changed, 152 insertions(+), 73 deletions(-) diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index d97a5012..eadbc47e 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -166,15 +166,15 @@ size_t lp_feasibility_set_int_size_approx(const lp_feasibility_set_int_t *set) { int lp_feasibility_set_int_is_point(const lp_feasibility_set_int_t* set) { assert(lp_integer_cmp_int(lp_Z, &set->K->M, 2) > 0); - if (set->inverted && set->size == 1) return 1; - if (!set->inverted && lp_integer_cmp_int(lp_Z, &set->K->M, set->size + 1) == 0) return 1; + if (!set->inverted && set->size == 1) return 1; + if (set->inverted && lp_integer_cmp_int(lp_Z, &set->K->M, set->size + 1) == 0) return 1; return 0; } /** returns true if value is in elements. Assumes that the elements are sorted and that value is normalized wrt set->K */ static -bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_integer_t* value, size_t *pos) { - if (set->size == 0){ +bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t *set, const lp_integer_t *value) { + if (set->size == 0) { return false; } assert(set->elements); @@ -191,7 +191,6 @@ bool lp_feasibility_set_int_find(const lp_feasibility_set_int_t* set, const lp_i l = p + 1; } else { // found - if (pos) { *pos = p; } return true; } } @@ -202,7 +201,7 @@ int lp_feasibility_set_int_contains(const lp_feasibility_set_int_t* set, const l lp_integer_t value_normalized; // normalize value before check lp_integer_construct_copy(set->K, &value_normalized, value); - bool found = lp_feasibility_set_int_find(set, &value_normalized, NULL); + bool found = lp_feasibility_set_int_find(set, &value_normalized); lp_integer_destruct(&value_normalized); return found != set->inverted; } @@ -213,10 +212,27 @@ void lp_feasibility_set_int_pick_value(const lp_feasibility_set_int_t* set, lp_i size_t pos = random() % set->size; lp_integer_assign(lp_Z, value, set->elements + pos); } else { - assert(false); - // TODO implement + lp_integer_construct_from_int(lp_Z, value, 0); + // check 0 + if (!lp_feasibility_set_int_find(set, value)) { + return; + } + while (true) { + lp_integer_inc(lp_Z, value); + assert(lp_integer_in_ring(set->K, value)); + if (!lp_feasibility_set_int_find(set, value)) { + return; + } + lp_integer_neg(lp_Z, value, value); + if (!lp_feasibility_set_int_find(set, value)) { + return; + } + lp_integer_neg(lp_Z, value, value); + } + // TODO proper implementation // get random element between (incl.) 0 and (|K| - size) // find and add number of <= element + assert(false); } } diff --git a/test/poly/test_feasible_int_set.cpp b/test/poly/test_feasible_int_set.cpp index 6de318b9..94420e8e 100644 --- a/test/poly/test_feasible_int_set.cpp +++ b/test/poly/test_feasible_int_set.cpp @@ -40,10 +40,12 @@ struct integer_list { } delete this->v; } - lp_feasibility_set_int_t* gen_set(lp_int_ring_t *K, bool inverted) const { return lp_feasibility_set_int_new_from_integer(K, this->v->data(), this->v->size(), inverted); } + lp_feasibility_set_int_t* gen_set(IntegerRing &K, bool inverted) const { + return this->gen_set(K.get_internal(), inverted); + } const lp_integer_t* data() const { return this->v->data(); } size_t size() const { return this->v->size(); } }; @@ -56,12 +58,16 @@ TEST_CASE("feasibility_set_int::construct") { SUBCASE("feasibility_set_int::construct::full") { lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_full(K); + CHECK(!lp_feasibility_set_int_is_empty(set)); CHECK(lp_feasibility_set_int_is_full(set)); + CHECK(!lp_feasibility_set_int_is_point(set)); lp_feasibility_set_int_delete(set); } SUBCASE("feasibility_set_int::construct::empty") { lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_empty(K); CHECK(lp_feasibility_set_int_is_empty(set)); + CHECK(!lp_feasibility_set_int_is_full(set)); + CHECK(!lp_feasibility_set_int_is_point(set)); lp_feasibility_set_int_delete(set); } SUBCASE("feasibility_set_int::construct::integer") { @@ -72,6 +78,22 @@ TEST_CASE("feasibility_set_int::construct") { CHECK(lp_feasibility_set_int_size_approx(set) == 4); lp_feasibility_set_int_delete(set); } + SUBCASE("feasibility_set_int::construct::point") { + integer_list l({2}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), false); + CHECK(!lp_feasibility_set_int_is_empty(set)); + CHECK(!lp_feasibility_set_int_is_full(set)); + CHECK(lp_feasibility_set_int_is_point(set)); + lp_feasibility_set_int_delete(set); + } + SUBCASE("feasibility_set_int::construct::point_inv") { + integer_list l({0,1,/*2,*/3,4,5,6,7,8,9,10,11,12}); + lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), true); + CHECK(!lp_feasibility_set_int_is_empty(set)); + CHECK(!lp_feasibility_set_int_is_full(set)); + CHECK(lp_feasibility_set_int_is_point(set)); + lp_feasibility_set_int_delete(set); + } SUBCASE("feasibility_set_int::construct::integer::invert") { integer_list l({2,1,4,3}); lp_feasibility_set_int_t *set = lp_feasibility_set_int_new_from_integer(K, l.data(), l.size(), true); @@ -100,9 +122,8 @@ TEST_CASE("feasibility_set_int::construct") { } TEST_CASE("feasibility_set_int::intersect::inv") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2,3}).gen_set(K, false); lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); @@ -147,15 +168,12 @@ TEST_CASE("feasibility_set_int::intersect::inv") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::intersect::inv_dual") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set2 = integer_list({1,2,3}).gen_set(K, false); lp_feasibility_set_int_t *set1 = integer_list({2,3}).gen_set(K, false); @@ -200,15 +218,12 @@ TEST_CASE("feasibility_set_int::intersect::inv_dual") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::union::inv") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2,3}).gen_set(K, false); lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); @@ -252,15 +267,12 @@ TEST_CASE("feasibility_set_int::union::inv") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::union::inv_dual") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set2 = integer_list({1,2,3}).gen_set(K, false); lp_feasibility_set_int_t *set1 = integer_list({2,3}).gen_set(K, false); @@ -304,15 +316,12 @@ TEST_CASE("feasibility_set_int::union::inv_dual") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::union") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); @@ -352,15 +361,12 @@ TEST_CASE("feasibility_set_int::union") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::intersect") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set2 = integer_list({2,3}).gen_set(K, false); @@ -400,19 +406,16 @@ TEST_CASE("feasibility_set_int::intersect") { lp_feasibility_set_int_delete(set2); lp_feasibility_set_int_delete(set2_inv); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::intersect_empty") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); - lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K); + lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K.get_internal()); SUBCASE("feasibility_set_int::intersect_empty1") { lp_feasibility_set_int_status_t status; @@ -450,19 +453,16 @@ TEST_CASE("feasibility_set_int::intersect_empty") { lp_feasibility_set_int_delete(set1_inv); lp_feasibility_set_int_delete(empty); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::intersect_full") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); - lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K); + lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K.get_internal()); SUBCASE("feasibility_set_int::intersect::intersect_full1") { lp_feasibility_set_int_status_t status; @@ -500,19 +500,16 @@ TEST_CASE("feasibility_set_int::intersect_full") { lp_feasibility_set_int_delete(set1_inv); lp_feasibility_set_int_delete(full); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::union_full") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); - lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K); + lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K.get_internal()); SUBCASE("feasibility_set_int::union_full1") { lp_feasibility_set_int_status_t status; @@ -550,19 +547,16 @@ TEST_CASE("feasibility_set_int::union_full") { lp_feasibility_set_int_delete(set1_inv); lp_feasibility_set_int_delete(full); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); } TEST_CASE("feasibility_set_int::union_empty") { - lp_integer_t prime; - lp_integer_construct_from_int(lp_Z, &prime, 7); - lp_int_ring_t *K = lp_int_ring_create(&prime, 1); + Integer prime(7); + IntegerRing K(prime, true); lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); - lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K); + lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K.get_internal()); SUBCASE("feasibility_set_int::union_empty1") { lp_feasibility_set_int_status_t status; @@ -600,7 +594,76 @@ TEST_CASE("feasibility_set_int::union_empty") { lp_feasibility_set_int_delete(set1_inv); lp_feasibility_set_int_delete(empty); - CHECK_EQ(K->ref_count, 1); - lp_int_ring_detach(K); - lp_integer_destruct(&prime); + CHECK_EQ(K.get_internal()->ref_count, 1); +} + +TEST_CASE("feasibility_set_int::size") { + Integer prime(7); + IntegerRing K(prime, true); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + lp_feasibility_set_int_t *empty = lp_feasibility_set_int_new_empty(K.get_internal()); + lp_feasibility_set_int_t *full = lp_feasibility_set_int_new_full(K.get_internal()); + + SUBCASE("feasibility_set_int::size::1") { + Integer size; + lp_feasibility_set_int_size(set1, size.get_internal()); + size_t size_approx = lp_feasibility_set_int_size_approx(set1); + CHECK(size == 2); + CHECK(size_approx == 2); + } + SUBCASE("feasibility_set_int::size::2") { + Integer size; + lp_feasibility_set_int_size(set1_inv, size.get_internal()); + size_t size_approx = lp_feasibility_set_int_size_approx(set1_inv); + CHECK(size == 2); + CHECK(size_approx == 2); + } + SUBCASE("feasibility_set_int::size::full") { + Integer size; + lp_feasibility_set_int_size(full, size.get_internal()); + size_t size_approx = lp_feasibility_set_int_size_approx(full); + CHECK(size == prime); + CHECK(size_approx == prime); + } + SUBCASE("feasibility_set_int::size::empty") { + Integer size; + lp_feasibility_set_int_size(empty, size.get_internal()); + size_t size_approx = lp_feasibility_set_int_size_approx(empty); + CHECK(size == 0); + CHECK(size_approx == 0); + } + + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(full); + lp_feasibility_set_int_delete(empty); + + CHECK_EQ(K.get_internal()->ref_count, 1); +} + +TEST_CASE("feasibility_set_int::pick") { + Integer prime(7); + IntegerRing K(prime, true); + + lp_feasibility_set_int_t *set1 = integer_list({1,2}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0,3,4,5,6}).gen_set(K, true); + + SUBCASE("feasibility_set_int::pick") { + Integer pick; + lp_feasibility_set_int_pick_value(set1, pick.get_internal()); + + CHECK((pick == 1 || pick == 2)); + } + SUBCASE("feasibility_set_int::pick_inv") { + Integer pick; + lp_feasibility_set_int_pick_value(set1_inv, pick.get_internal()); + CHECK((pick == 1 || pick == 2)); + } + + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + + CHECK_EQ(K.get_internal()->ref_count, 1); } From 4f1235d2237addb73378bdfca76f380bfab39276 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 15 Mar 2024 10:51:38 -0700 Subject: [PATCH 09/10] Removed unnecessary header file --- src/polynomial/feasibility_set_int.c | 1 - src/polynomial/feasibility_set_int.h | 21 --------------------- src/polynomial/polynomial.c | 1 - 3 files changed, 23 deletions(-) delete mode 100644 src/polynomial/feasibility_set_int.h diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index eadbc47e..f739476e 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -18,7 +18,6 @@ */ #include -#include "polynomial/feasibility_set_int.h" #include #include diff --git a/src/polynomial/feasibility_set_int.h b/src/polynomial/feasibility_set_int.h deleted file mode 100644 index 46c937ff..00000000 --- a/src/polynomial/feasibility_set_int.h +++ /dev/null @@ -1,21 +0,0 @@ -/** - * Copyright 2024, SRI International. - * - * This file is part of LibPoly. - * - * LibPoly is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * LibPoly 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 Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public License - * along with LibPoly. If not, see . - */ - -#pragma once - diff --git a/src/polynomial/polynomial.c b/src/polynomial/polynomial.c index 19ad809c..5c3474f2 100644 --- a/src/polynomial/polynomial.c +++ b/src/polynomial/polynomial.c @@ -34,7 +34,6 @@ #include "number/integer.h" #include "polynomial/feasibility_set.h" -#include "polynomial/feasibility_set_int.h" #include "polynomial/polynomial_vector.h" #include "utils/debug_trace.h" From b1153d21055a67790cc555317c728f3797f926d0 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 29 May 2024 15:04:00 +0200 Subject: [PATCH 10/10] Fixed assertion location --- src/polynomial/feasibility_set_int.c | 2 +- test/poly/test_feasible_int_set.cpp | 49 ++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+), 1 deletion(-) diff --git a/src/polynomial/feasibility_set_int.c b/src/polynomial/feasibility_set_int.c index f739476e..dbd5ae0b 100644 --- a/src/polynomial/feasibility_set_int.c +++ b/src/polynomial/feasibility_set_int.c @@ -388,11 +388,11 @@ void lp_feasibility_set_int_invert(lp_feasibility_set_int_t *set) { long lb = lp_integer_to_int(&set->K->lb); long ub = lp_integer_to_int(&set->K->ub); for (long val = lb; val <= ub; ++val) { - assert(pos_new < cnt); assert(pos_old >= set->size || lp_integer_cmp_int(lp_Z, old + pos_old, val) >= 0); if (pos_old < set->size && lp_integer_cmp_int(lp_Z, old + pos_old, val) == 0) { ++ pos_old; } else { + assert(pos_new < cnt); lp_integer_construct_from_int(lp_Z, new + pos_new, val); ++ pos_new; } diff --git a/test/poly/test_feasible_int_set.cpp b/test/poly/test_feasible_int_set.cpp index 94420e8e..0108dd2a 100644 --- a/test/poly/test_feasible_int_set.cpp +++ b/test/poly/test_feasible_int_set.cpp @@ -409,6 +409,55 @@ TEST_CASE("feasibility_set_int::intersect") { CHECK_EQ(K.get_internal()->ref_count, 1); } +TEST_CASE("feasibility_set_int::intersect_wrap_around") { + Integer prime(3); + IntegerRing K(prime, true); + + lp_feasibility_set_int_t *set1 = integer_list({1,-1}).gen_set(K, false); + lp_feasibility_set_int_t *set2 = integer_list({-1}).gen_set(K, false); + lp_feasibility_set_int_t *set1_inv = integer_list({0}).gen_set(K, true); + lp_feasibility_set_int_t *set2_inv = integer_list({0,1}).gen_set(K, true); + + SUBCASE("feasibility_set_int::intersect_wrap_around1") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_contains(s, Integer(K, -1).get_internal())); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_wrap_around2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_contains(s, Integer(K, -1).get_internal())); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_wrap_around3") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_contains(s, Integer(K, -1).get_internal())); + lp_feasibility_set_int_delete(s); + } + SUBCASE("feasibility_set_int::intersect_wrap_around2") { + lp_feasibility_set_int_status_t status; + lp_feasibility_set_int_t *s = lp_feasibility_set_int_intersect_with_status(set1_inv, set2_inv, &status); + CHECK(lp_feasibility_set_int_size_approx(s) == 1); + CHECK(status == LP_FEASIBILITY_SET_INT_S2); + CHECK(lp_feasibility_set_int_contains(s, Integer(K, -1).get_internal())); + lp_feasibility_set_int_delete(s); + } + + lp_feasibility_set_int_delete(set1); + lp_feasibility_set_int_delete(set1_inv); + lp_feasibility_set_int_delete(set2); + lp_feasibility_set_int_delete(set2_inv); + CHECK_EQ(K.get_internal()->ref_count, 1); +} + TEST_CASE("feasibility_set_int::intersect_empty") { Integer prime(7); IntegerRing K(prime, true);