Created lp_feasibility_set_count_int

SRI-CSL · Oct 7, 2024 · 13bc940 · 13bc940
1 parent ece4f77
commit 13bc940
Show file tree

Hide file tree

Showing 7 changed files with 102 additions and 3 deletions.
diff --git a/include/feasibility_set.h b/include/feasibility_set.h
@@ -93,6 +93,16 @@ int lp_feasibility_set_is_full(const lp_feasibility_set_t* set);
  */
 int lp_feasibility_set_is_point(const lp_feasibility_set_t* set);
 
+/**
+ * Check if the set contains only one integer value.
+ */
+int lp_feasibility_set_is_point_int(const lp_feasibility_set_t* set);
+
+/**
+ * Returns the number of integers in set (up to LONG_MAX).
+ */
+long lp_feasibility_set_count_int(const lp_feasibility_set_t* set);
+
 /**
  * Check if the given value belongs to the set.
  */

diff --git a/include/interval.h b/include/interval.h
@@ -86,6 +86,9 @@ int lp_interval_contains(const lp_interval_t* I, const lp_value_t* v);
 /** Check if the interval contains an integer value */
 int lp_interval_contains_int(const lp_interval_t* I);
 
+/** Counts the number of integers in the interval (up to LONG_MAX) */
+long lp_interval_count_int(const lp_interval_t* I);
+
 /** Returns an approximation of the log interval size */
 int lp_interval_size_approx(const lp_interval_t* I);
 

diff --git a/include/polyxx/interval.h b/include/polyxx/interval.h
@@ -83,7 +83,8 @@ namespace poly {
   bool contains(const Interval& i, const Value& v);
   /** Check whether an interval contains an integer value. */
   bool contains_int(const Interval& i);
-
+  /** Counts the number of integers in the interval up to LONG_MAX. */
+  long count_int(const Interval& i);
   /** Get an approximation of the log interval size. */
   int log_size(const Interval& i);
 

diff --git a/src/interval/interval.c b/src/interval/interval.c
@@ -715,6 +715,46 @@ int lp_interval_contains_int(const lp_interval_t* I) {
   return result;
 }
 
+long lp_interval_count_int(const lp_interval_t* I) {
+  if (lp_value_is_infinity(&I->a)) return LONG_MAX;
+  int a_int = lp_value_is_integer(&I->a);
+  if (I->is_point) {
+    return a_int ? 1 : 0;
+  }
+  if (lp_value_is_infinity(&I->b)) return LONG_MAX;
+
+  long result = 0;
+  int b_int = lp_value_is_integer(&I->b);
+  if (!I->a_open && a_int) result++;
+  if (!I->b_open && b_int) result++;
+
+  lp_integer_t m, n;
+  lp_integer_construct(&m);
+  lp_integer_construct(&n);
+
+  lp_value_ceiling(&I->a, &m);
+  lp_value_floor(&I->b, &n);
+
+  if (a_int) lp_integer_inc(lp_Z, &m);
+  if (b_int) lp_integer_dec(lp_Z, &n);
+
+  lp_integer_sub(lp_Z, &n, &n, &m);
+  if (lp_integer_sgn(lp_Z, &n) >= 0) {
+    if (lp_integer_fits_int(&n)) {
+      result += lp_integer_to_int(&n) + 1;
+      // check for overflow
+      if (result < 0) result = LONG_MAX;
+    } else {
+      result = LONG_MAX;
+    }
+  }
+
+  lp_integer_destruct(&m);
+  lp_integer_destruct(&n);
+
+  return result;
+}
+
 int lp_dyadic_interval_contains_dyadic_rational(const lp_dyadic_interval_t* I, const lp_dyadic_rational_t* q) {
   int cmp_a_q = dyadic_rational_cmp(&I->a, q);
   if (I->is_point) {

diff --git a/src/polynomial/feasibility_set.c b/src/polynomial/feasibility_set.c
@@ -144,11 +144,37 @@ int lp_feasibility_set_is_point(const lp_feasibility_set_t* set) {
   return set->size == 1 && set->intervals->is_point;
 }
 
+int lp_feasibility_set_is_point_int(const lp_feasibility_set_t* set) {
+  long cnt = 0;
+  for (size_t i = 0; i < set->size; ++i) {
+    long tmp = lp_interval_count_int(set->intervals + i);
+    assert(tmp >= 0);
+    if (tmp > 1 || tmp + cnt > 1) {
+      return 0;
+    }
+    cnt += tmp;
+  }
+  return cnt == 1;
+}
+
+long lp_feasibility_set_count_int(const lp_feasibility_set_t* set) {
+  long cnt = 0;
+  for (size_t i = 0; i < set->size; ++i) {
+    long tmp = lp_interval_count_int(set->intervals + i);
+    assert(tmp >= 0);
+    // check for overflow
+    if (tmp >= LONG_MAX - cnt) {
+      return LONG_MAX;
+    }
+    cnt += tmp;
+  }
+  return cnt;
+}
+
 int lp_feasibility_set_print(const lp_feasibility_set_t* set, FILE* out) {
   int ret = 0;
-  size_t i;
   ret += fprintf(out, "{ ");
-  for(i = 0; i < set->size; ++ i) {
+  for(size_t i = 0; i < set->size; ++ i) {
     if (i) {
       ret += fprintf(out, ", ");
     }

diff --git a/src/polyxx/interval.cpp b/src/polyxx/interval.cpp
@@ -73,6 +73,10 @@ namespace poly {
     return lp_interval_contains_int(i.get_internal());
   }
 
+  long count_int(const Interval& i) {
+    return lp_interval_count_int(i.get_internal());
+  }
+
   int log_size(const Interval& i) {
     return lp_interval_size_approx(i.get_internal());
   }

diff --git a/test/polyxx/test_interval.cpp b/test/polyxx/test_interval.cpp
@@ -64,6 +64,21 @@ TEST_CASE("interval::contains_int") {
   CHECK_FALSE(contains_int(Interval(Rational(1,4), Rational(3,4))));
 }
 
+TEST_CASE("interval::count_int") {
+  CHECK(count_int(Interval(0,1)) == 0);
+  CHECK(count_int(Interval(0,2)) == 1);
+  CHECK(count_int(Interval()) == 1);
+  CHECK(count_int(Interval(Rational(1,2))) == 0);
+  CHECK(count_int(Interval(Rational(3,4), Rational(5,4))) == 1);
+  CHECK(count_int(Interval(0, false, 2, false)) == 3);
+  CHECK(count_int(Interval(0,LONG_MAX)) == LONG_MAX - 1);
+  CHECK(count_int(Interval(0,false, LONG_MAX, true)) == LONG_MAX);
+  CHECK(count_int(Interval(0,false, LONG_MAX, false)) == LONG_MAX);
+  CHECK(count_int(Interval(-1,LONG_MAX)) == LONG_MAX);
+  CHECK(count_int(Interval(-2,LONG_MAX)) == LONG_MAX);
+  CHECK(count_int(Interval(LONG_MIN, LONG_MAX)) == LONG_MAX);
+}
+
 TEST_CASE("interval::pick_value") {
   Interval i(1,3);
   CHECK(contains(i, pick_value(i)));