kdrag.rewrite

Utilities for rewriting and simplification including pattern matching and unification.

Functions

`all_narrow`(vs, t, lhs, rhs)	Look for pattern lhs to unify with a subterm of t.
`apply`(goal, vs, head, body)
`backward_rule`(r, tgt)	Apply a rule to a target term.
`beta`(e)	Do one pass of beta normalization.
`decl_index`(rules)	Build a dictionary of rules indexed by their lhs head function declaration.
`def_eq`(e1, e2[, trace])	A notion of computational equality.
`forward_rule`(r, tgt)	Apply a rule to a target term.
`full_simp`(e[, trace])	Fully simplify using definitions and built in z3 simplifier until no progress is made.
`kbo`(vs, t1, t2)	Knuth Bendix Ordering, naive implementation.
`lpo`(vs, t1, t2)	Lexicographic path ordering.
`rewrite`(t, rules[, trace])	Repeat rewrite until no more rewrites are possible.
`rewrite1`(t, vs, lhs, rhs)	Rewrite at root a single time.
`rewrite1_rule`(t, rule[, trace])	Rewrite at root a single time.
`rewrite_of_expr`(thm)	Unpack theorem of form forall vs, lhs = rhs into a Rule tuple
`rewrite_once`(t, rules[, trace])	Sweep through term once performing rewrites.
`rewrite_slow`(t, rules[, trace])	Repeat rewrite until no more rewrites are possible.
`rule_of_expr`(pf_or_thm)	Unpack theorem of form forall vs, body => head into a Rule tuple
`simp`(e[, trace, max_iter])	Simplify using definitions and built in z3 simplifier until no progress is made.
`simp1`(t)	simplify a term using z3 built in simplifier
`simp2`(t)	simplify a term using z3 built in simplifier
`unfold`(e[, decls, trace])

Classes

`Order`(*values)
`RewriteRule`(vs, lhs, rhs[, pf])	A rewrite rule tuple
`Rule`(vs, hyp, conc, pf)

Exceptions

RewriteRuleException

class kdrag.rewrite.Order(*values)

Bases: Enum

EQ = 0

GR = 1

NGE = 2

classmethod __contains__(value)

Return True if value is in cls.

value is in cls if: 1) value is a member of cls, or 2) value is the value of one of the cls’s members. 3) value is a pseudo-member (flags)

classmethod __getitem__(name): Return the member matching name.

classmethod __iter__(): Return members in definition order.

classmethod __len__(): Return the number of members (no aliases)

class kdrag.rewrite.RewriteRule(vs: list[ExprRef], lhs: ExprRef, rhs: ExprRef, pf: Proof | None = None)

Bases: NamedTuple

A rewrite rule tuple

Parameters:

vs (list[ExprRef])
lhs (ExprRef)
rhs (ExprRef)
pf (Proof | None)

count(value, /): Return number of occurrences of value.

freshen() → RewriteRule

Freshen the rule by renaming variables.

>>> x,y= smt.Reals("x y")
>>> rule = RewriteRule([x,y], x*y, y*x)
>>> rule.freshen()
RewriteRule(vs=[x..., y...], lhs=x...*y..., rhs=y...*x..., pf=None)

Return type:: RewriteRule

classmethod from_expr(expr: BoolRef | QuantifierRef | Proof) → RewriteRule

Convert a theorem of form forall vs, lhs = rhs to a rule.

Parameters:: expr (BoolRef | QuantifierRef | Proof)
Return type:: RewriteRule

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

lhs: ExprRef: Alias for field number 1

pf: Proof | None: Alias for field number 3

rhs: ExprRef: Alias for field number 2

to_expr() → BoolRef | QuantifierRef

Convert the rule to a theorem of form forall vs, lhs = rhs.

>>> x,y = smt.Reals("x y")
>>> RewriteRule([x,y], x*y, y*x).to_expr()
ForAll([x, y], x*y == y*x)

Return type:: BoolRef | QuantifierRef

vs: list[ExprRef]: Alias for field number 0

exception kdrag.rewrite.RewriteRuleException

Bases: Exception

add_note(object, /): Exception.add_note(note) – add a note to the exception

args

with_traceback(object, /): Exception.with_traceback(tb) – set self.__traceback__ to tb and return self.

class kdrag.rewrite.Rule(vs, hyp, conc, pf)

Bases: NamedTuple

Parameters:

vs (list[ExprRef])
hyp (BoolRef)
conc (BoolRef)
pf (Proof | None)

conc: BoolRef: Alias for field number 2

count(value, /): Return number of occurrences of value.

freshen()

Freshen the rule by renaming variables.

>>> x,y= smt.Reals("x y")
>>> rule = Rule([x], x > 0, x < 0)
>>> rule.freshen()
Rule(vs=[x...], hyp=x... > 0, conc=x... < 0, pf=None)

hyp: BoolRef: Alias for field number 1

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

pf: Proof | None: Alias for field number 3

to_expr() → ExprRef | QuantifierRef

Convert the rule to a theorem of form forall vs, hyp => conc.

>>> x = smt.Real("x")
>>> Rule([x], x > 0, x < 0).to_expr()
ForAll(x..., Implies(x... > 0, x... < 0))

Return type:: ExprRef | QuantifierRef

vs: list[ExprRef]: Alias for field number 0

kdrag.rewrite.all_narrow(vs: list[ExprRef], t: ExprRef, lhs: ExprRef, rhs: ExprRef) → list[tuple[ExprRef, dict[ExprRef, ExprRef]]]

Look for pattern lhs to unify with a subterm of t. returns a list of all of those lhs -> rhs applied + the substitution resulting from the unification. The substitution is so that we can apply the other t -> s rule once we return.

This helper is asymmettric between t and lhs. You need to call it twice to get all critical pairs.

>>> x,y,z = smt.Reals("x y z")
>>> all_narrow([x,y], -(-(-(x))), -(-(y)), y)
[(y, {y: -x}), (-y, {x: y}), (--y, {x: -y})]

Parameters:

vs (list[ExprRef])
t (ExprRef)
lhs (ExprRef)
rhs (ExprRef)

Return type:

list[tuple[ExprRef, dict[ExprRef, ExprRef]]]

kdrag.rewrite.apply(goal: BoolRef, vs: list[ExprRef], head: BoolRef, body: BoolRef) → BoolRef | None

Parameters:

goal (BoolRef)
vs (list[ExprRef])
head (BoolRef)
body (BoolRef)

Return type:

BoolRef | None

kdrag.rewrite.backward_rule(r: Rule, tgt: BoolRef) → tuple[dict[ExprRef, ExprRef], BoolRef] | None

Apply a rule to a target term.

Parameters:

r (Rule)
tgt (BoolRef)

Return type:

tuple[dict[ExprRef, ExprRef], BoolRef] | None

kdrag.rewrite.beta(e: ExprRef) → ExprRef

Do one pass of beta normalization.

>>> x = smt.Int("x")
>>> y = smt.String("y")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> beta(f(x))
f(x)
>>> beta(f(smt.Lambda([x], f(x))[1]))
f(f(1))
>>> beta(f(smt.Select(smt.Lambda([x,y], x), 1, smt.StringVal("fred"))))
f(1)

Parameters:: e (ExprRef)
Return type:: ExprRef

kdrag.rewrite.decl_index(rules: list[RewriteRule]) → dict[FuncDeclRef, RewriteRule]

Build a dictionary of rules indexed by their lhs head function declaration.

Parameters:: rules (list[RewriteRule])
Return type:: dict[FuncDeclRef, RewriteRule]

kdrag.rewrite.def_eq(e1: ExprRef, e2: ExprRef, trace=None) → bool

A notion of computational equality. Unfold and simp.

>>> import kdrag.theories.nat as nat
>>> def_eq(nat.one + nat.one, nat.S(nat.S(nat.Z)))
True

Parameters:

e1 (ExprRef)
e2 (ExprRef)

Return type:

bool

kdrag.rewrite.forward_rule(r: Rule, tgt: BoolRef)

Apply a rule to a target term.

Parameters:

r (Rule)
tgt (BoolRef)

kdrag.rewrite.full_simp(e: ExprRef, trace=None) → ExprRef

Fully simplify using definitions and built in z3 simplifier until no progress is made.

>>> import kdrag.theories.nat as nat
>>> full_simp(nat.one + nat.one + nat.S(nat.one))
S(S(S(S(Z))))

>>> p = smt.Bool("p")
>>> full_simp(smt.If(p, 42, 3))
If(p, 42, 3)

Parameters:: e (ExprRef)
Return type:: ExprRef

kdrag.rewrite.kbo(vs: list[ExprRef], t1: ExprRef, t2: ExprRef) → Order

Knuth Bendix Ordering, naive implementation. All weights are 1. Source: Term Rewriting and All That section 5.4.4

Parameters:

vs (list[ExprRef])
t1 (ExprRef)
t2 (ExprRef)

Return type:

Order

kdrag.rewrite.lpo(vs: list[ExprRef], t1: ExprRef, t2: ExprRef) → Order

Lexicographic path ordering. Based on https://www21.in.tum.de/~nipkow/TRaAT/programs/termorders.ML TODO add ordering parameter.

Parameters:

vs (list[ExprRef])
t1 (ExprRef)
t2 (ExprRef)

Return type:

Order

kdrag.rewrite.rewrite(t: ExprRef, rules: Sequence[BoolRef | QuantifierRef | Proof | RewriteRule], trace=None) → ExprRef

Repeat rewrite until no more rewrites are possible.

>>> x,y,z = smt.Reals("x y z")
>>> unit = kd.prove(smt.ForAll([x], x + 0 == x))
>>> x + 0 + 0 + 0 + 0
x + 0 + 0 + 0 + 0
>>> rewrite(x + 0 + 0 + 0 + 0, [unit])
x

Parameters:

t (ExprRef)
rules (Sequence[BoolRef | QuantifierRef | Proof | RewriteRule])

Return type:

ExprRef

kdrag.rewrite.rewrite1(t: ExprRef, vs: list[ExprRef], lhs: ExprRef, rhs: ExprRef) → ExprRef | None

Rewrite at root a single time.

Parameters:

t (ExprRef)
vs (list[ExprRef])
lhs (ExprRef)
rhs (ExprRef)

Return type:

ExprRef | None

kdrag.rewrite.rewrite1_rule(t: ExprRef, rule: RewriteRule, trace: list[tuple[RewriteRule, dict[ExprRef, ExprRef]]] | None = None) → ExprRef | None

Rewrite at root a single time.

Parameters:

t (ExprRef)
rule (RewriteRule)
trace (list[tuple[RewriteRule, dict[ExprRef, ExprRef]]] | None)

Return type:

ExprRef | None

kdrag.rewrite.rewrite_of_expr(thm: BoolRef | QuantifierRef | Proof) → RewriteRule

Unpack theorem of form forall vs, lhs = rhs into a Rule tuple

>>> x = smt.Real("x")
>>> rewrite_of_expr(smt.ForAll([x], x**2 == x*x))
RewriteRule(vs=[X...], lhs=X...**2, rhs=X...*X...)

Parameters:: thm (BoolRef | QuantifierRef | Proof)
Return type:: RewriteRule

kdrag.rewrite.rewrite_once(t: ExprRef, rules: list[RewriteRule], trace=None) → ExprRef

Sweep through term once performing rewrites.

>>> x = smt.Real("x")
>>> rule = RewriteRule([x], x**2, x*x)
>>> rewrite_once((x**2)**2, [rule])
x*x*x*x

Parameters:

t (ExprRef)
rules (list[RewriteRule])

Return type:

ExprRef

kdrag.rewrite.rewrite_slow(t: ExprRef, rules: list[BoolRef | QuantifierRef | Proof], trace=None) → ExprRef

Repeat rewrite until no more rewrites are possible.

>>> x,y,z = smt.Reals("x y z")
>>> unit = kd.prove(smt.ForAll([x], x + 0 == x))
>>> x + 0 + 0 + 0 + 0
x + 0 + 0 + 0 + 0
>>> rewrite(x + 0 + 0 + 0 + 0, [unit])
x

Parameters:

t (ExprRef)
rules (list[BoolRef | QuantifierRef | Proof])

Return type:

ExprRef

kdrag.rewrite.rule_of_expr(pf_or_thm: ExprRef | Proof) → Rule

Unpack theorem of form forall vs, body => head into a Rule tuple

>>> x = smt.Real("x")
>>> rule_of_expr(smt.ForAll([x], smt.Implies(x**2 == x*x, x > 0)))
Rule(vs=[X...], hyp=X...**2 == X...*X..., conc=X... > 0, pf=None)
>>> rule_of_expr(x > 0)
Rule(vs=[], hyp=True, conc=x > 0, pf=None)

Parameters:: pf_or_thm (ExprRef | Proof)
Return type:: Rule

kdrag.rewrite.simp(e: ExprRef, trace=None, max_iter=3) → ExprRef

Simplify using definitions and built in z3 simplifier until no progress is made.

>>> import kdrag.theories.nat as nat
>>> simp(nat.one + nat.one + nat.S(nat.one))
S(S(S(S(Z))))

>>> p = smt.Bool("p")
>>> simp(smt.If(p, 42, 3))
If(p, 42, 3)

Parameters:: e (ExprRef)
Return type:: ExprRef

kdrag.rewrite.simp1(t: ExprRef) → ExprRef

simplify a term using z3 built in simplifier

Parameters:: t (ExprRef)
Return type:: ExprRef

kdrag.rewrite.simp2(t: ExprRef) → ExprRef

simplify a term using z3 built in simplifier

Parameters:: t (ExprRef)
Return type:: ExprRef

kdrag.rewrite.unfold(e: ExprRef, decls: Sequence[FuncDeclRef] | None = None, trace=None) → ExprRef

>>> x = smt.Int("x")
>>> f = kd.define("f", [x], x + 42)
>>> trace = []
>>> unfold(f(1), trace=trace)
1 + 42
>>> trace
[|= f(1) == 1 + 42]

>>> unfold(smt.Lambda([x], f(x)))
Lambda(x, x + 42)

Parameters:

e (ExprRef)
decls (Sequence[FuncDeclRef] | None)

Return type:

ExprRef