kdrag.solvers.kb.string

See https://www.philipzucker.com/string_knuth/

Functions

KB(E)	String Knuth-Bendix completion algorithm.
deduce(R)	deduce all possible critical pairs from R
overlaps(s, t)	critical pairs https://en.wikipedia.org/wiki/Critical_pair_(term_rewriting)
replace(s, lhs, rhs)	Find and replace the first occurrence of lhs in s with rhs.
rewrite(s, R[, exclude])	Rewrite to a fixed point using rules R.
shortlex_swap(s, t)	Order by length, then tie break by contents lexicographically.
simplify(R)
subseq(s, t)	Return index when s is a subsequence of t, None otherwise

kdrag.solvers.kb.string.KB(E)

String Knuth-Bendix completion algorithm.

>>> e = 0
>>> a = 1 # a is rotate square
>>> b = 2 # b is flip square horizontally.
>>> E = [        ((-a, a), ()),        ((-b,b), ()),        ((a,a,a,a), ()),        ((b,b), ()),        ((a,a,a,b), (b,a))        ]
>>> R = KB(E)
>>> E,R = simplify(R)

kdrag.solvers.kb.string.deduce(R)

deduce all possible critical pairs from R

kdrag.solvers.kb.string.overlaps(s, t)

critical pairs https://en.wikipedia.org/wiki/Critical_pair_(term_rewriting)

>>> assert set(overlaps((1,2), (2,3))) == {(1,2,3)}
>>> assert set(overlaps((1,2), (3,2))) == set()
>>> assert set(overlaps((1,2), (2,1))) == {(1,2,1), (2,1,2)}
>>> assert set(overlaps((1,2), (1,2))) == {(1,2)}
>>> assert set(overlaps((2,2), (2,2,3))) == {(2,2,3), (2,2,2,3)}
>>> assert set(overlaps((), (1,2))) == {(1,2)}

kdrag.solvers.kb.string.replace(s: tuple, lhs: tuple, rhs: tuple) → tuple

Find and replace the first occurrence of lhs in s with rhs.

>>> replace((1,2,3,4), (2,3), (5,6))
(1, 5, 6, 4)
>>> replace((1,2,3,4), (2,3), (5,6,7))
(1, 5, 6, 7, 4)
>>> replace((1,2,3,4), (2,3), (5,6,7,8))
(1, 5, 6, 7, 8, 4)
>>> replace((1,1), (4,4), (2,2))
(1, 1)

Parameters:

• s (tuple)

• lhs (tuple)

• rhs (tuple)

Return type:

tuple

kdrag.solvers.kb.string.rewrite(s, R, exclude=-1)

Rewrite to a fixed point using rules R.

Exclude is useful for simplifying a rule

>>> rewrite((1,2,3,4), [((2,3), (5,6)), ((5,6), (7,8))])
(1, 7, 8, 4)
>>> rewrite((1,1,1,1,1,1), [((1,1), ())])
()
>>> rewrite((1,1,1,1,2,1), [((1,1), ())])
(2, 1)

kdrag.solvers.kb.string.shortlex_swap(s, t)

Order by length, then tie break by contents lexicographically. Returns a tuple (s’, t’) where t’ is the “shorter” or “smaller” of the two. Asserts False if s and t are equal.

>>> shortlex_swap((1,2,3), (0,0))
((1, 2, 3), (0, 0))
>>> shortlex_swap((1,2,3), (1,2,4))
((1, 2, 4), (1, 2, 3))

kdrag.solvers.kb.string.simplify(R)

kdrag.solvers.kb.string.subseq(s: Sequence, t: Sequence) → int | None

Return index when s is a subsequence of t, None otherwise

>>> subseq("abc", "abacabadabacaba") is None
True
>>> subseq("abc", "abacabc")
4

Parameters:

• s (Sequence)

• t (Sequence)

Return type:

int | None