kdrag.solvers.kb.multiset

Ground Multiset Rewriting and completion.

https://www.philipzucker.com/multiset_rw/

Functions

KB(E)
add(xs, ys)	Add two multisets
count(xs)
deduce(R)	deduce all possible critical pairs from R
ms_order(xs, ys)
overlap(xs, ys)	Find minimal multiset that is a supermultiset of both xs and ys.
replace(xs, lhs, rhs)	Replace multiset pattern lhs in multiset xs with rhs.
rewrite(s, R)
shortlex(xs, ys)
sub(xs, ys)	Difference two multisets.

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

kdrag.solvers.kb.multiset.add(xs, ys)

Add two multisets

>>> list(add([("a", 1), ("b", 2)], [("a", 1), ("c", 3)]))
[('a', 2), ('b', 2), ('c', 3)]

kdrag.solvers.kb.multiset.count(xs)

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

deduce all possible critical pairs from R

kdrag.solvers.kb.multiset.ms_order(xs, ys)

kdrag.solvers.kb.multiset.overlap(xs, ys)

Find minimal multiset that is a supermultiset of both xs and ys. Return None if this is just the union (trivial)

kdrag.solvers.kb.multiset.replace(xs, lhs, rhs)

Replace multiset pattern lhs in multiset xs with rhs.

>>> replace([("a", 1), ("b", 2)], [("a", 1)], [("a", 2), ("c", 3)])
[('a', 2), ('b', 2), ('c', 3)]
>>> replace([("a", 1), ("b", 2)], [("a", 1), ("b", 2)], [("a", 2), ("c", 3)])
[('a', 2), ('c', 3)]
>>> replace([("a", 1), ("b", 2)], [("a", 1), ("b", 4)], [("a", 2)]) == None
True
>>> replace([('p', 25)], [('p', 25)], [('q', 1)])
[('q', 1)]

kdrag.solvers.kb.multiset.rewrite(s, R)

kdrag.solvers.kb.multiset.shortlex(xs, ys)

kdrag.solvers.kb.multiset.sub(xs, ys)

Difference two multisets. Return None if the second is not a submultiset of the first

>>> sub([("a", 1), ("b", 2)], [("a", 1), ("c", 3)]) is None
True
>>> sub([("a", 1), ("b", 2)], [("a", 1), ("b", 2)])
[]