Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update obvinf.hpp for v1/3 #193

Merged
merged 6 commits into from
Sep 24, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
88 changes: 50 additions & 38 deletions docs/source/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ def sig_alternative(doc, signature, return_annotation):
return new_sig, return_annotation


def change_sig(
def change_sig( # pylint: disable=too-many-arguments,too-many-positional-arguments
app=None,
what=None,
name=None,
Expand Down Expand Up @@ -291,59 +291,67 @@ def change_sig(
def make_only_doc(lines):
"""
Extract the unique docstrings from a sequence of overloaded functions.

This function assumes that the the first n overloaded functions are unique,
and that they then repeat periodically.
"""

# Find the lines the signatures occur in
sigs = defaultdict(list)
lines_to_sig = {}
for i, line in enumerate(lines):
# To keep track of unique strings
sigs = set()

# To track how many overloaded functions there should be
overload_counter = 1

# To track whether or not to delete overloads
deleting = False

# To track if we actually have any repeated documentation
called_correctly = False
i = 0
while i < len(lines):
line = lines[i]
m = re.search(r":sig=(.*):$", line)
if m is not None:
sig = m.group(1)
sigs[sig] += [i]
lines_to_sig[i] = sig
current = sigs[sig]
if len(current) > 1:
break
if sig in sigs:
deleting = True
called_correctly = True
else:
deleting = False
sigs.add(sig)
lines[i - 3] = re.sub(
r"\d+(\. .*)\(.*$",
str(overload_counter) + r"\1" + sig,
lines[i - 3],
)
overload_counter += 1

if deleting:
# We do i - 3 because the :sig=...: appears three lines later than
# the actual signatures
del lines[i - 3]
else:
i += 1

locations = list(sigs.values())
locations.sort()
# If we were deleting when we got to the end of lines, we should delete the
# last 3 lines that got missed.
if deleting:
del lines[-3:]

if len(locations) == 0 or len(locations[0]) <= 1:
if not called_correctly:
raise RuntimeError(
":only-document-once: has been invoked in a function where "
"documentation has not been repeated. Invoked in:\n"
+ "\n".join(lines)
)

# Find the period of repetition, and remove all lines after the end of the
# first period
start = locations[0][0]
end = locations[0][1]
del lines[end - 3 :]

# If the new doc shouldn't be overloaded, remove the "Overloaded
# function" part
if len(sigs) == 1:
del lines[: start + 2]
return

# Otherwise, replace the signature in the correct place
for line_sequence in locations[::-1]:
first = line_sequence[0]
decl_line = first - 3
lines[decl_line] = re.sub(
r"(\s*?\d+\. .*)\(.*$",
r"\1" + lines_to_sig[first],
lines[decl_line],
)
del lines[first : first + 2]
while ":sig=" not in lines[0]:
del lines[0]


def only_doc_once(app, what, name, obj, options, lines):
def only_doc_once(
app, what, name, obj, options, lines
): # pylint:disable=too-many-arguments,too-many-positional-arguments
"""
Edit docstring to only include one version of the doc for an overloaded
function if necessary
Expand All @@ -353,7 +361,9 @@ def only_doc_once(app, what, name, obj, options, lines):
make_only_doc(lines)


def fix_overloads(app, what, name, obj, options, lines):
def fix_overloads(
app, what, name, obj, options, lines
): # pylint:disable=too-many-arguments,too-many-positional-arguments
"""Indent overloaded function documentation and format signatures"""
overloading = False
overloaded_function = ""
Expand Down Expand Up @@ -426,7 +436,9 @@ def fix_overloads(app, what, name, obj, options, lines):
}


def remove_doc_annotations(app, what, name, obj, options, lines):
def remove_doc_annotations(
app, what, name, obj, options, lines
): # pylint:disable=too-many-arguments,too-many-positional-arguments
"""Remove any special decorations from the documentation"""
for i in range(len(lines) - 1, -1, -1):
for bad, good in docstring_replacements.items():
Expand Down
1 change: 1 addition & 0 deletions docs/source/data-structures/misc/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ In this section we describe some miscellaneous functionality in
:maxdepth: 1

constants
obvinf
runner
reporter

Expand Down
58 changes: 58 additions & 0 deletions docs/source/data-structures/misc/obvinf.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
.. Copyright (c) 2024 J. D. Mitchell

Distributed under the terms of the GPL license version 3.

The full license is in the file LICENSE, distributed with this software.

.. currentmodule:: _libsemigroups_pybind11

Obviously infinite
==================

This page collects the documentation for the functionality in
``libsemigroups_pybind11`` for checking if a finitely presented semigroup or
monoid is obviously infinite.

The functions below implement a number of checks for whether or not a finitely
presented semigroup or monoid is infinite. These checks are all decidable, and
always return an answer within an amount of time that is linear in the size of
the input.

These checks are:

1. For every generator there is at least one side of one relation that
consists solely of that generator. If this condition is not met, then
there is a generator of infinite order.

2. The number of occurrences of every generator is not preserved by the
relations. Otherwise, it is not possible to use the relations to
reduce the number of occurrences of a generator in a word, and so
there are infinitely many distinct words.

3. The number of generators on the left hand side of a relation is not
the same as the number of generators on the right hand side for at
least one generator. Otherwise the relations preserve the length of
any word and so there are infinitely many distinct words.

4. There are at least as many relations as there are generators.
Otherwise we can find a surjective homomorphism onto an infinite
subsemigroup of the rationals under addition.

5. The checks 2., 3. and 4. are a special case of a more general matrix
based condition. We construct a matrix whose columns correspond to
generators and rows correspond to relations. The ``(i, j)``-th entry is
the number of occurrences of the ``j``-th generator in the left hand side
of the ``i``-th relation minus the number of occurrences of it on the
right hand side. If this matrix has a non-trivial kernel, then we can
construct a surjective homomorphism onto an infinite subsemigroup of
the rationals under addition. So we check that the matrix is full
rank.

6. The presentation is not that of a free product. To do this we consider
a graph whose vertices are generators and an edge connects two
generators if they occur on either side of the same relation. If this
graph is disconnected then the presentation is a free product and is
therefore infinite. Note that we currently do not consider the case
where the identity occurs in the presentation.

.. autofunction:: is_obviously_infinite
29 changes: 24 additions & 5 deletions src/knuth-bendix.cpp
Joseph-Edwards marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -550,15 +550,34 @@ is returned.
['ab', 'ba', 'bab', 'abb']
>>> knuth_bendix.redundant_rule(p, t)
2
)pbdoc");
)pbdoc");
m.def(
"is_obviously_infinite",
[](KnuthBendix<Rewriter>& kb) { return is_obviously_infinite(kb); },
R"pbdoc(
:sig=(kb: KnuthBendixRewriteTrie):
:only-document-once:
TODO
)pbdoc");
:sig=(kb: KnuthBendixRewriteTrie) -> bool:

Function for checking if the quotient of a finitely presented
semigroup or monoid defined by a :any:`KnuthBendix` object is obviously infinite
or not.

This function returns ``True`` if the quotient of the finitely presented
semigroup or monoid defined by the :any:`KnuthBendix` object *kb* is obviously
infinite; ``False`` is returned if it is not.

:param kb: the :any:`KnuthBendix` instance.
:type kb: KnuthBendix

:returns:
Whether or not the quotient defined by a :any:`KnuthBendix` instance is
obviously infinite.
james-d-mitchell marked this conversation as resolved.
Show resolved Hide resolved
:rtype:
bool

.. note::
If this function returns ``False``, it is still possible that the quotient
defined by the :any:`KnuthBendix` object *kb* is infinite.
)pbdoc");
}
} // namespace

Expand Down
1 change: 1 addition & 0 deletions src/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,7 @@ namespace libsemigroups {
init_gabow(m);
init_knuth_bendix(m);
init_order(m);
init_obvinf(m);
init_paths(m);
init_present(m);
init_inverse_present(m);
Expand Down
1 change: 1 addition & 0 deletions src/main.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ namespace libsemigroups {
void init_freeband(py::module&);
void init_dot(py::module&);
void init_matrix(py::module&);
void init_obvinf(py::module&);

} // namespace libsemigroups

Expand Down
Loading