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])
`unfold_old`(e[, decls, trace])	Do a single unfold sweep, unfolding definitions defined by kd.define.

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

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

Do a single unfold sweep, unfolding definitions defined by kd.define. The optional trace parameter will record proof along the way. decls is an optional list of declarations to unfold. If None, all definitions are unfolded.

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

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

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