From f2d91eaca29de3f4ed45d3afb1ff0b53d72831e7 Mon Sep 17 00:00:00 2001 From: "Matthias C. M. Troffaes" Date: Thu, 19 Sep 2024 14:12:38 +0100 Subject: [PATCH] Strong redundancy with tests. --- cython/pycddlib.pxi | 21 +++++++++++++++++---- src/cdd/__init__.pyi | 4 +++- src/cdd/gmp.pyi | 4 +++- stubgen.py | 2 +- test/test_redundant.py | 29 ++++++++++++++++++++++++++--- 5 files changed, 50 insertions(+), 10 deletions(-) diff --git a/cython/pycddlib.pxi b/cython/pycddlib.pxi index b204c27..0a24a30 100644 --- a/cython/pycddlib.pxi +++ b/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) diff --git a/src/cdd/__init__.pyi b/src/cdd/__init__.pyi index 92e5563..b03ce27 100644 --- a/src/cdd/__init__.pyi +++ b/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]]: ... diff --git a/src/cdd/gmp.pyi b/src/cdd/gmp.pyi index d98765a..b375887 100644 --- a/src/cdd/gmp.pyi +++ b/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]]: ... diff --git a/stubgen.py b/stubgen.py index 7f9bfb1..9a13a75 100644 --- a/stubgen.py +++ b/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 diff --git a/test/test_redundant.py b/test/test_redundant.py index 97b548a..245ceab 100644 --- a/test/test_redundant.py +++ b/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)