kdrag.solvers.kb

Knuth Bendix completion.

When it succeeds, completion converts equations or non confluent rewriting systems into confluent ones. The resulting system of rewrite rules is a decision procedure for the equivalence of terms.

It can be seen as a form of equational theorem proving, especially in it’s unfailing form.

For more see

Functions

all_pairs(rules)

Find all the ways the left hand side of two rules can overlap.

basic(E[, order])

Basic Knuth Bendix completion algorithm.

huet(E[, order])

Huet completion is a particular strategy.

huet_smt2_file(sexp_filename)

is_trivial(t)

See if equation is of form `s = s

orient(eq[, order])

Orient an equation into a rewrite rule.

simplify(t, rules)

Simplify an equation using a set of rewrite rules.
kdrag.solvers.kb.all_pairs(rules)

Find all the ways the left hand side of two rules can overlap. Return a derived equation

>>> a,b,c,d = smt.Reals("a b c d")
>>> all_pairs([rw.RewriteRule(vs=[], lhs=x, rhs=y) for x,y in [(a,b), (b,c), (a,c), (a,d)]])
[b == b, b == c, b == d, c == c, c == b, c == c, c == d, d == b, d == c, d == d]
kdrag.solvers.kb.basic(E, order=<function kbo>)

Basic Knuth Bendix completion algorithm.

TRaaT 7.1.1 Central Groupoid example

>>> import kdrag as kd
>>> T = smt.DeclareSort("CentralGroupoid")
>>> x,y,z = smt.Consts("x y z", T)
>>> mul = smt.Function("mul", T, T, T)
>>> kd.notation.mul.register(T, mul)
>>> E = [smt.ForAll([x,y,z], (x * y) * (y * z) == y)]
>>> assert len(basic(E)) == 3
kdrag.solvers.kb.huet(E: list[~z3.z3.BoolRef | ~z3.z3.QuantifierRef], order=<function kbo>) → list[RewriteRule]

Huet completion is a particular strategy.

Parameters:

E (list[BoolRef | QuantifierRef])

Return type:

list[RewriteRule]

kdrag.solvers.kb.huet_smt2_file(sexp_filename: str) → list[RewriteRule]
Parameters:

sexp_filename (str)

Return type:

list[RewriteRule]

kdrag.solvers.kb.is_trivial(t: BoolRef | QuantifierRef) → bool

See if equation is of form `s = s

>>> x = smt.Real("x")
>>> assert is_trivial(x == x)
>>> assert not is_trivial(x == -(-x))
Parameters:

t (BoolRef | QuantifierRef)

Return type:

bool

kdrag.solvers.kb.orient(eq: ~z3.z3.BoolRef | ~z3.z3.QuantifierRef, order=<function kbo>) → RewriteRule

Orient an equation into a rewrite rule.

>>> x,y,z = smt.Reals("x y z")
>>> orient(smt.ForAll([x], -(-x) == x))
RewriteRule(vs=[X!...], lhs=--X!..., rhs=X!..., pf=None)
>>> orient(smt.ForAll([x], x == -(-x)))
RewriteRule(vs=[X!...], lhs=--X!..., rhs=X!..., pf=None)
>>> orient(smt.ForAll([x,y,z], x + z == x + y + z + x + y))
RewriteRule(vs=[X!...], lhs=X!... + Y!... + Z!... + X!... + Y!..., rhs=X!... + Z!..., pf=None)
Parameters:

eq (BoolRef | QuantifierRef)

Return type:

RewriteRule

kdrag.solvers.kb.simplify(t: BoolRef | QuantifierRef, rules: list[RewriteRule]) → BoolRef | QuantifierRef

Simplify an equation using a set of rewrite rules.

>>> x = smt.Real("x")
>>> simplify(smt.ForAll([x], -(-(-(-(-x)))) == -x), [rw.rewrite_of_expr(smt.ForAll([x], -(-x) == x))])
ForAll(X!..., -X!... == -X!...)
Parameters:

  • t (BoolRef | QuantifierRef)

  • rules (list[RewriteRule])

Return type:

BoolRef | QuantifierRef

Modules

multiset

Ground Multiset Rewriting and completion.

string

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