kdrag.utils

Various term manipulation helpers. Pattern matchers, unifiers, rewriters, term orderings, etc.

Functions

`all_values`(*es)	Generate all values possible for an expression.
`alpha_eq`(t1, t2)	Alpha equivalent equality.
`alpha_norm`(expr)	Recursively rename all variables in an expression to canonical names.
`antipattern`(xs)	Anti pattern matching.
`ast_size_sexpr`(t)	Get an approximate size of an AST node by its s-expression length. This is probably faster than any python layer traversal one can do. Pretty printed ast size will be correlated to expression size, maybe even DAG size, since Z3 inserts `let`s to avoid duplication.
`consts`(t)	Return all constants in a term.
`decls`(t)	Return all function declarations in a term.
`defined_decls`(t)
`domain`(f)	Get the domain sorts of a lambda or an array.
`find_calls`(decl, t)	Find subterms that are calls of decl in t.
`free_vars`(t)	Return free variables in an expression.
`generate`(sort[, pred])	A generator of values for a sort.
`is_func`(f)	Check if a term is a function or an array.
`is_strict_subterm`(t, t2)
`is_subterm`(t, t2)	TODO: Not alpha invariant or going into binders
`is_value`(t)
`lemma_db`()	Scan all modules for Proof objects and return a dictionary of them.
`occurs`(x, t)	Does x occur in t?
`open_binder`(lam)	Open a quantifier with fresh variables.
`open_binder_unhygienic`(lam)	Do not use this.
`pathmap`(function, e, path)	Apply function at position in term >>> x,y,z = smt.Ints("x y z") >>> pathmap(lambda t: t + 1, x + y * z, [1,0]) x + (y + 1)*z
`pmatch`(vs, pat, t[, subst])	Pattern match t against pat considering vs as variables.
`pmatch_fo`(vs, pat, t[, subst])	First order pattern matching.
`pmatch_rec`(vs, pat, t[, into_binder])
`prompt`(prompt)	Ask an AI.
`prune`(thm[, by, timeout])	Prune the theorems used using unsat core.
`quant_kind_eq`(t1, t2)	Check both quantifiers are of the same kind
`range_`(f)
`sanity_check_consistency`(thms[, timeout])	Sanity check theorems or proofs for consistency.
`search`(*es[, db])	Search for function declarations or expressions.
`search_decl`(f, db)	Search for declarations in the proof database that contain function declaration f
`search_expr`(e, pfs)	Search for expressions in the proof database that match e using pattern matching.
`sorts`(t)	Generate all sorts in a term
`subterms`(t[, into_binder])	Generate all subterms of a term
`unify`(vs, p1, p2)	Unification
`unify_db`(p1, p2)	Unification using de Bruijn indices as variables

kdrag.utils.all_values(*es: ExprRef) → Generator[list[ExprRef], None, None]

Generate all values possible for an expression. Generator won’t terminate if there are infinite possible values. Concretization.

>>> assert set(all_values(smt.If(smt.Bool("x"), 2, 3))) == {smt.IntVal(2), smt.IntVal(3)}

Parameters:: es (ExprRef)
Return type:: Generator[list[ExprRef], None, None]

kdrag.utils.alpha_eq(t1, t2)

Alpha equivalent equality. Z3’s fast built-in t.eq is not alpha invariant.

>>> x,y = smt.Ints("x y")
>>> t1,t2 = smt.Lambda([x], x), smt.Lambda([y], y)
>>> t1.eq(t2) # syntactic equality
False
>>> alpha_eq(t1, t2)
True
>>> alpha_eq(smt.Lambda([x], x)[3], smt.IntVal(3)) # No beta equivalence
False

kdrag.utils.alpha_norm(expr: ExprRef) → ExprRef

Recursively rename all variables in an expression to canonical names. Printed form may become ambiguous because internally de Bruijn indices are used.

>>> x,y,z,w = smt.Consts("x y z w", smt.IntSort())
>>> p = smt.Real("p")
>>> assert not smt.Lambda([x,y], x + y).eq(smt.Lambda([z,w], z + w))
>>> assert alpha_norm(smt.Lambda([x,y], x + y)).eq(alpha_norm(smt.Lambda([z,w], z + w)))
>>> _ = kd.prove(alpha_norm(smt.Lambda([x,p], p)) == smt.Lambda([x,p], p))

Parameters:: expr (ExprRef)
Return type:: ExprRef

kdrag.utils.antipattern(xs: list[ExprRef]) → tuple[list[ExprRef], ExprRef]

Anti pattern matching. Given a list of concrete examples, return the most specific pattern that matches them all. Returns tuple of list of pattern variables and pattern expression.

https://arxiv.org/pdf/2302.00277 Anti-unification and Generalization: A Survey https://arxiv.org/abs/2212.04596 babble: Learning Better Abstractions with E-Graphs and Anti-Unification https://ericlippert.com/2018/10/29/anti-unification-part-1/

>>> a,b,c,d = smt.Ints("a b c d")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort())
>>> g = smt.Function("g", smt.IntSort(), smt.IntSort(), smt.IntSort())
>>> t1 = f(a,g(a,b))
>>> t2 = f(c,g(c,d))
>>> t3 = f(a,g(d,b))
>>> antipattern([t1,t2])
([a!..., b!...], f(a!..., g(a!..., b!...)))
>>> antipattern([t1,t2,t3])
([a!..., a!..., b!...], f(a!..., g(a!..., b!...)))

Parameters:: xs (list[ExprRef])
Return type:: tuple[list[ExprRef], ExprRef]

kdrag.utils.ast_size_sexpr(t: AstRef) → int

Get an approximate size of an AST node by its s-expression length. This is probably faster than any python layer traversal one can do. Pretty printed ast size will be correlated to expression size, maybe even DAG size, since Z3 inserts `let`s to avoid duplication.

>>> ast_size_sexpr(smt.Int("x"))
1
>>> ast_size_sexpr(smt.Int("x") + smt.Int("y"))
7

Parameters:: t (AstRef)
Return type:: int

kdrag.utils.consts(t: ExprRef) → set[ExprRef]

Return all constants in a term.

>>> x,y = smt.Ints("x y")
>>> consts(x + (y * y) + 1) == {smt.IntVal(1), x, y}
True

Parameters:: t (ExprRef)
Return type:: set[ExprRef]

kdrag.utils.decls(t: ExprRef) → set[FuncDeclRef]

Return all function declarations in a term.

Parameters:: t (ExprRef)
Return type:: set[FuncDeclRef]

kdrag.utils.defined_decls(t: ExprRef) → list[FuncDeclRef]

>>> x,y = smt.Ints("x y")
>>> f = kd.define("test_f", [x,y], x + y)
>>> g = smt.Function("g", smt.IntSort(), smt.IntSort())
>>> defined_decls(f(x,y) + g(1))
[test_f]

Parameters:: t (ExprRef)
Return type:: list[FuncDeclRef]

kdrag.utils.domain(f: FuncRef) → list[SortRef]

Get the domain sorts of a lambda or an array.

>>> x = smt.Int("x")
>>> y = smt.Real("y")
>>> f = smt.Array("f", smt.IntSort(), smt.RealSort(), smt.IntSort())
>>> domain(f)
[Int, Real]
>>> lam = smt.Lambda([x, y], x + y)
>>> domain(lam)
[Int, Real]

Parameters:: f (FuncRef)
Return type:: list[SortRef]

kdrag.utils.find_calls(decl: FuncDeclRef, t: ExprRef) → list[ExprRef]

Find subterms that are calls of decl in t.

>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> find_calls(f, f(f(4*f(3)) + 2))
[f(f(4*f(3)) + 2), f(4*f(3)), f(3)]

Parameters:

decl (FuncDeclRef)
t (ExprRef)

Return type:

list[ExprRef]

kdrag.utils.free_vars(t: ExprRef) → set[ExprRef]

Return free variables in an expression. Looks at kernel.defns to determine if contacts are free. If you have meaningful constants no registered there, this may not work.

>>> x,y = smt.Ints("x y")
>>> free_vars(smt.Lambda([x], x + y + 1))
{y}

Parameters:: t (ExprRef)
Return type:: set[ExprRef]

kdrag.utils.generate(sort: SortRef, pred=None) → Generator[ExprRef, None, None]

A generator of values for a sort. Repeatedly calls z3 to get a new value.

>>> set(generate(smt.BoolSort()))
{True, False}
>>> sorted([v.as_long() for v in generate(smt.IntSort(), pred=lambda x: smt.And(0 <= x, x < 5))])
[0, 1, 2, 3, 4]
>>> import itertools
>>> len(list(itertools.islice(generate(smt.ArraySort(smt.IntSort(), smt.IntSort())), 3)))
3

Parameters:: sort (SortRef)
Return type:: Generator[ExprRef, None, None]

kdrag.utils.is_func(f: FuncRef) → bool

Check if a term is a function or an array.

>>> x = smt.Int("x")
>>> assert is_func(smt.Lambda([x], x))

Parameters:: f (FuncRef)
Return type:: bool

kdrag.utils.is_strict_subterm(t: ExprRef, t2: ExprRef) → bool

Parameters:

t (ExprRef)
t2 (ExprRef)

Return type:

bool

kdrag.utils.is_subterm(t: ExprRef, t2: ExprRef) → bool

TODO: Not alpha invariant or going into binders

Parameters:

t (ExprRef)
t2 (ExprRef)

Return type:

bool

kdrag.utils.is_value(t: ExprRef)

Parameters:: t (ExprRef)

kdrag.utils.lemma_db() → dict[str, Proof]

Scan all modules for Proof objects and return a dictionary of them.

Return type:: dict[str, Proof]

kdrag.utils.occurs(x: ExprRef, t: ExprRef) → bool

Does x occur in t?

>>> x,y,z = smt.Ints("x y z")
>>> assert occurs(x + y, x + y + z)
>>> assert not occurs(x + y, x + z)
>>> assert occurs(x, x + y + z)
>>> v0 = smt.Var(0, smt.IntSort())
>>> assert occurs(v0, v0 + x + y)

Parameters:

x (ExprRef)
t (ExprRef)

Return type:

bool

kdrag.utils.open_binder(lam: QuantifierRef) → tuple[list[ExprRef], ExprRef]

Open a quantifier with fresh variables. This achieves the locally nameless representation https://chargueraud.org/research/2009/ln/main.pdf where it is harder to go wrong.

The variables are schema variables which when used in a proof may be generalized

>>> x = smt.Int("x")
>>> open_binder(smt.ForAll([x], x > 0))
([X!...], X!... > 0)

Parameters:: lam (QuantifierRef)
Return type:: tuple[list[ExprRef], ExprRef]

kdrag.utils.open_binder_unhygienic(lam: QuantifierRef) → tuple[list[ExprRef], ExprRef]

Do not use this. Use open_binder. Opens a quantifier with unfresh variables.

>>> x = smt.Int("x")
>>> open_binder_unhygienic(smt.ForAll([x], x > 0))
([x], x > 0)

Parameters:: lam (QuantifierRef)
Return type:: tuple[list[ExprRef], ExprRef]

kdrag.utils.pathmap(function: Callable[[ExprRef], ExprRef], e: ExprRef, path: list[int] | None) → ExprRef

Apply function at position in term >>> x,y,z = smt.Ints(“x y z”) >>> pathmap(lambda t: t + 1, x + y * z, [1,0]) x + (y + 1)*z

Parameters:

function (Callable[[ExprRef], ExprRef])
e (ExprRef)
path (list[int] | None)

Return type:

ExprRef

kdrag.utils.pmatch(vs: list[ExprRef], pat: ExprRef, t: ExprRef, subst=None) → dict[ExprRef, ExprRef] | None

Pattern match t against pat considering vs as variables. Returns substitution dictionary if succeeds https://www.philipzucker.com/ho_unify/

Parameters:

vs (list[ExprRef])
pat (ExprRef)
t (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None

kdrag.utils.pmatch_fo(vs: list[ExprRef], pat: ExprRef, t: ExprRef, subst=None) → dict[ExprRef, ExprRef] | None

First order pattern matching. Faster and simpler. Pattern match t against pat considering vs as variables. Returns substitution dictionary if succeeds

>>> x, y = smt.Ints("x y")
>>> pmatch_fo([x], x + x, y + y)
{x: y}

Parameters:

vs (list[ExprRef])
pat (ExprRef)
t (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None

kdrag.utils.pmatch_rec(vs: list[ExprRef], pat: ExprRef, t: ExprRef, into_binder=False) → tuple[ExprRef, dict[ExprRef, ExprRef]] | None

Parameters:

vs (list[ExprRef])
pat (ExprRef)
t (ExprRef)

Return type:

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

kdrag.utils.prompt(prompt: str)

Ask an AI.

Get the root directory of the current package, find all .py files within that directory, and concatenate their contents into a single string separated by —.

Returns:: A single string with all .py files concatenated, separated by —.
Return type:: str
Parameters:: prompt (str)

kdrag.utils.prune(thm: BoolRef | QuantifierRef | Proof, by=[], timeout=1000) → list[ExprRef | Proof]

Prune the theorems used using unsat core. Helpful to speedup future proof verification.

>>> p,q,r = smt.Bools("p q r")
>>> sorted(prune(p & q, [p, q, r]), key=lambda b: b.decl().name())
[p, q]

Parameters:: thm (BoolRef | QuantifierRef | Proof)
Return type:: list[ExprRef | Proof]

kdrag.utils.quant_kind_eq(t1: QuantifierRef, t2: QuantifierRef) → bool

Check both quantifiers are of the same kind

>>> x = smt.Int("x")
>>> forall = smt.ForAll([x], x > 0)
>>> exists = smt.Exists([x], x > 0)
>>> lamb = smt.Lambda([x], x > 0)
>>> assert quant_kind_eq(forall, forall)
>>> assert quant_kind_eq(exists, exists)
>>> assert quant_kind_eq(lamb, lamb)
>>> assert not quant_kind_eq(forall, exists)

Parameters:

t1 (QuantifierRef)
t2 (QuantifierRef)

Return type:

bool

kdrag.utils.range_(f: FuncRef) → SortRef

>>> x = smt.Int("x")
>>> y = smt.Int("y")
>>> f = smt.Array("f", smt.IntSort(), smt.RealSort())
>>> range_(f)
Real
>>> lam = smt.Lambda([x, y], x + y)
>>> range_(lam)
Int

Parameters:: f (FuncRef)
Return type:: SortRef

kdrag.utils.sanity_check_consistency(thms: list[ExprRef | Proof], timeout=1000)

Sanity check theorems or proofs for consistency. If they are inconsistent, raise an error. Otherwise, return the result of the check. A sat result shows consistency, but an unknown result does not imply anything.

It may be nice to try and apply this function to your axioms or theory in CI.

>>> x,y = smt.Ints("x y")
>>> sanity_check_consistency([x == y])
sat

Parameters:: thms (list[ExprRef | Proof])

kdrag.utils.search(*es: FuncDeclRef | ExprRef, db: dict[Any, Proof] = {}) → dict[tuple[str, Proof], Any]

Search for function declarations or expressions. Takes intersection of found results if given multiple arguments. Builds a database by scanning loaded modules by default.

Parameters:

es (FuncDeclRef | ExprRef)
db (dict[Any, Proof])

Return type:

dict[tuple[str, Proof], Any]

kdrag.utils.search_decl(f: FuncDeclRef, db: dict[object, Proof]) → dict[tuple[str, Proof], Any]

Search for declarations in the proof database that contain function declaration f

Parameters:

f (FuncDeclRef)
db (dict[object, Proof])

Return type:

dict[tuple[str, Proof], Any]

kdrag.utils.search_expr(e: ExprRef, pfs: dict[object, Proof]) → dict[tuple[str, Proof], Any]

Search for expressions in the proof database that match e using pattern matching.

>>> x,z = smt.Ints("x z")
>>> search_expr(z + 0, {        "thm1": kd.prove(smt.ForAll([x], x + 0 == x)),        "thm2" : kd.prove(z + 0 == z),        "thm3" : kd.prove(smt.ForAll([x], x + 1 == 1 + x)),        "thm4" : kd.prove(smt.BoolVal(True))})
{('thm1', |= ForAll(x, x + 0 == x)): [z], ('thm2', |= z + 0 == z): []}

Parameters:

e (ExprRef)
pfs (dict[object, Proof])

Return type:

dict[tuple[str, Proof], Any]

kdrag.utils.sorts(t: ExprRef)

Generate all sorts in a term

Parameters:: t (ExprRef)

kdrag.utils.subterms(t: ExprRef, into_binder=False)

Generate all subterms of a term

>>> x,y = smt.Ints("x y")
>>> list(subterms(x + y == y))
[x + y == y, y, x + y, y, x]
>>> list(subterms(smt.ForAll([x], x + y == y)))
[ForAll(x, x + y == y)]
>>> list(subterms(smt.ForAll([x], x + y == y), into_binder=True))
[ForAll(x, x + y == y), Var(0) + y == y, y, Var(0) + y, y, Var(0)]

Parameters:: t (ExprRef)

kdrag.utils.unify(vs: list[ExprRef], p1: ExprRef, p2: ExprRef) → dict[ExprRef, ExprRef] | None

Unification

Parameters:

vs (list[ExprRef])
p1 (ExprRef)
p2 (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None

kdrag.utils.unify_db(p1: ExprRef, p2: ExprRef) → dict[ExprRef, ExprRef] | None

Unification using de Bruijn indices as variables

Parameters:

p1 (ExprRef)
p2 (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None