Strong redundancy with tests.

cython/pycddlib.pxi

@@ -345,9 +345,19 @@ def matrix_append_to(mat1: Matrix, mat2: Matrix) -> None:
         raise ValueError("cannot append because column sizes differ")
 
 
-def redundant(mat: Matrix, row: int) -> tuple[bool, Sequence[NumberType]]:
-    """Checks whether *row* is redundant for the representation *mat*.
-    Linearity rows are not checked.
+def redundant(
+    mat: Matrix, row: int, strong: bool = False
+) -> tuple[bool, Sequence[NumberType]]:
+    """Checks whether *row* is (strongly) redundant for the representation *mat*.
+    Linearity rows are not checked
+    i.e. *row* should not be in the :attr:`~cdd.Matrix.lin_set`.
+
+    A row is redundant if its removal does not change the shape of the polyhedron.
+
+    A row is strongly redundant in the H-representation if every point in
+    the polyhedron satisfies it with strict inequality.
+    A row is strongly redundant in the V-representation if it is in
+    the interior of the polyhedron.
 
     Returns a certificate in case of non-redundancy.
     For the H-representation, the certificate x
@@ -369,7 +379,10 @@ def redundant(mat: Matrix, row: int) -> tuple[bool, Sequence[NumberType]]:
     cdef dd_rowrange crow = row
     dd_InitializeArow(certificate_size, &certificate)
     try:
-        is_redundant = dd_Redundant(mat.dd_mat, crow + 1, certificate, &error)
+        if strong:
+            is_redundant = dd_SRedundant(mat.dd_mat, crow + 1, certificate, &error)
+        else:
+            is_redundant = dd_Redundant(mat.dd_mat, crow + 1, certificate, &error)
         if error != dd_NoError:
             _raise_error(error)
         return bool(is_redundant), _get_arow(certificate_size, certificate)

src/cdd/__init__.pyi

@@ -116,4 +116,6 @@ def matrix_weak_adjacency(mat: Matrix) -> Sequence[Set[int]]: ...
 def polyhedron_from_matrix(
     mat: Matrix, row_order: Optional[RowOrderType] = None
 ) -> Polyhedron: ...
-def redundant(mat: Matrix, row: int) -> tuple[bool, Sequence[NumberType]]: ...
+def redundant(
+    mat: Matrix, row: int, strong: bool = False
+) -> tuple[bool, Sequence[NumberType]]: ...

src/cdd/gmp.pyi

@@ -84,4 +84,6 @@ def matrix_weak_adjacency(mat: Matrix) -> Sequence[Set[int]]: ...
 def polyhedron_from_matrix(
     mat: Matrix, row_order: Optional[RowOrderType] = None
 ) -> Polyhedron: ...
-def redundant(mat: Matrix, row: int) -> tuple[bool, Sequence[NumberType]]: ...
+def redundant(
+    mat: Matrix, row: int, strong: bool = False
+) -> tuple[bool, Sequence[NumberType]]: ...

stubgen.py

@@ -1,7 +1,7 @@
 # stubgen patch to make it play nice with Cython
 import inspect
 import typing
-from collections.abc import Callable, Iterable
+from collections.abc import Iterable
 from unittest import mock
 
 from mypy.stubgen import main

test/test_redundant.py

@@ -7,9 +7,9 @@
 
 
 def assert_redundant_equal(
-    mat: cdd.Matrix, row: int, exp_is_redundant: bool, exp_certificate: Sequence[float]
+    mat: cdd.Matrix, row: int, exp_is_redundant: bool, exp_certificate: Sequence[float], strong: bool = False,
 ) -> None:
-    is_redundant, certificate = cdd.redundant(mat, row)
+    is_redundant, certificate = cdd.redundant(mat, row, strong)
     assert is_redundant == exp_is_redundant
     assert_vector_almost_equal(certificate, exp_certificate)
 
@@ -49,13 +49,25 @@ def test_redundant_inequalities_3() -> None:
     assert_redundant_equal(mat, 2, True, [-14, 9])
 
 
+def test_redundant_inequalities_4() -> None:
+    # row 0: 0 <= 1 + x
+    # row 1: 0 <= 2 + 2x
+    mat = cdd.matrix_from_array([[1, 1], [2, 2]], rep_type=cdd.RepType.INEQUALITY)
+    assert_redundant_equal(mat, 0, True, [-1])
+    assert_redundant_equal(mat, 1, True, [-1])
+    assert_redundant_equal(mat, 0, False, [-1], True)
+    assert_redundant_equal(mat, 1, False, [-1], True)
+
+
 def test_redundant_generators_1() -> None:
     mat = cdd.matrix_from_array([[1, 1]], rep_type=cdd.RepType.GENERATOR, lin_set={0})
     assert cdd.redundant(mat, 0) == (False, [0, 0])
 
 
 def test_redundant_generators_2() -> None:
-    mat = cdd.matrix_from_array([[1, 1], [1, 2], [1, 3]], rep_type=cdd.RepType.GENERATOR)
+    mat = cdd.matrix_from_array(
+        [[1, 1], [1, 2], [1, 3]], rep_type=cdd.RepType.GENERATOR
+    )
     assert_redundant_equal(mat, 0, False, [-2, 1])
     assert_redundant_equal(mat, 1, True, [0, 0])
     assert_redundant_equal(mat, 2, False, [2, -1])
@@ -68,3 +80,14 @@ def test_redundant_generators_3() -> None:
     assert_redundant_equal(mat, 0, False, [-1.5, 0.5, 0])
     assert_redundant_equal(mat, 1, False, [1.5, -0.5, 0])
     assert_redundant_equal(mat, 2, True, [0, 0, 0])
+
+
+def test_redundant_generators_4() -> None:
+    mat = cdd.matrix_from_array([[1, 2], [1, 2], [1, 4]], rep_type=cdd.RepType.GENERATOR)
+    assert_redundant_equal(mat, 0, True, [0, 0])
+    assert_redundant_equal(mat, 1, True, [0, 0])
+    assert_redundant_equal(mat, 2, False, [1, -0.5])
+    # TODO is this a bug in cddlib? no certificate for rows 0 and 1...
+    assert_redundant_equal(mat, 0, False, [0, 0], True)
+    assert_redundant_equal(mat, 1, False, [0, 0], True)
+    assert_redundant_equal(mat, 2, False, [1, -0.5], True)