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.
`bysect`(thm, by, **kwargs)	Bisect the by list to find a minimal set of premises that prove thm.
`consts`(t)	Return all constants in a term.
`decls`(t)	Return all function declarations in a term.
`defined_decls`(t)
`find_calls`(decl, t)	Find subterms that are calls of decl in t.
`free_in`(vs, t)	Returns True if none of the variables in vs exist unbound in t.
`free_vars`(t)	Return free variables in an expression.
`generate`(sort[, pred])	A generator of values for a sort.
`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])
`pmatch_rec_ctx`(vs, pat, t)	Pattern match pat against subterms of t, returning the context, matched term, and substitution if successful.
`prompt`(prompt)	Ask an AI.
`propagate`(maybes, known)	Prune the list of maybes to the ones implies by known
`propagate_eqs`(terms, known)	Given a list of terms, propagate equalities among them that are implied by known.
`prune`(thm[, by, timeout])	Prune the theorems used using unsat core.
`quant_kind_eq`(t1, t2)	Check both quantifiers are of the same kind
`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

Classes

`DeclHole`(f, _left, _right)
`ExistsHole`(vs, orig_vs)
`ExprCtx`([iterable])	A context of holes for an expression.
`ForAllHole`(vs, orig_vs)
`LambdaHole`(vs, orig_vs)
`QuantifierHole`(vs, orig_vs)
`Zipper`(ctx, t)	A zipper for traversing and modifying terms.

class kdrag.utils.DeclHole(f: z3.z3.FuncDeclRef, _left: tuple[z3.z3.ExprRef, ...], _right: tuple[z3.z3.ExprRef, ...])

Bases: object

Parameters:

f (FuncDeclRef)
_left (tuple[ExprRef, ...])
_right (tuple[ExprRef, ...])

f: FuncDeclRef

has_left() → bool

Return type:: bool

has_right() → bool

Return type:: bool

left(t: ExprRef) → tuple[DeclHole, ExprRef]

Parameters:: t (ExprRef)
Return type:: tuple[DeclHole, ExprRef]

right(t: ExprRef) → tuple[DeclHole, ExprRef]

Parameters:: t (ExprRef)
Return type:: tuple[DeclHole, ExprRef]

wrap(e: ExprRef) → ExprRef

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

class kdrag.utils.ExistsHole(vs: list[ExprRef], orig_vs: list[ExprRef])

Bases: QuantifierHole

Parameters:

vs (list[ExprRef])
orig_vs (list[ExprRef])

has_right() → bool

Return type:: bool

orig_vs: list[ExprRef]

vs: list[ExprRef]

wrap(body: ExprRef) → ExprRef

Parameters:: body (ExprRef)
Return type:: ExprRef

class kdrag.utils.ExprCtx(iterable=(), /)

Bases: list

A context of holes for an expression. Similar to Zipper, but with a nonmutating api

append(object, /): Append object to the end of the list.

arg(t: ExprRef, n: int) → tuple[ExprCtx, ExprRef]

>>> x,y,z = smt.Ints("x y z")
>>> t = (x + y) * (y + z)
>>> ExprCtx().arg(t, 1)
([DeclHole(f=*, _left=(x + y,), _right=())], y + z)

Parameters:

t (ExprRef)
n (int)

Return type:

tuple[ExprCtx, ExprRef]

children(t) → list[tuple[ExprCtx, ExprRef]]

>>> x,y,z = smt.Ints("x y z")
>>> t = (x + y) * (y + z)
>>> ExprCtx().children(t)
[([DeclHole(f=*, _left=(), _right=(y + z,))], x + y), ([DeclHole(f=*, _left=(x + y,), _right=())], y + z)]

Return type:: list[tuple[ExprCtx, ExprRef]]

clear(): Remove all items from list.

copy() → ExprCtx

Return a shallow copy of the list.

Return type:: ExprCtx

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

extend(iterable, /): Extend list by appending elements from the iterable.

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

Return first index of value.

Raises ValueError if the value is not present.

insert(index, object, /): Insert object before index.

open_binder(t: QuantifierRef) → tuple[ExprCtx, ExprRef]

>>> x,y = smt.Ints("x y")
>>> t = smt.Lambda([x], x + y)
>>> ExprCtx().open_binder(t)
([LambdaHole(vs=[X!...], orig_vs=[x])], X!... + y)

Parameters:: t (QuantifierRef)
Return type:: tuple[ExprCtx, ExprRef]

pop(index=-1, /)

Remove and return item at index (default last).

Raises IndexError if list is empty or index is out of range.

remove(value, /)

Remove first occurrence of value.

Raises ValueError if the value is not present.

reverse(): Reverse IN PLACE.

sort(*, key=None, reverse=False)

Sort the list in ascending order and return None.

The sort is in-place (i.e. the list itself is modified) and stable (i.e. the order of two equal elements is maintained).

If a key function is given, apply it once to each list item and sort them, ascending or descending, according to their function values.

The reverse flag can be set to sort in descending order.

wrap(t) → ExprRef

Wrap a term t in the context >>> x,y,z = smt.Ints(“x y z”) >>> t = (x + y) * (y + z) >>> ctx, t1 = ExprCtx().arg(t, 1) >>> ctx.wrap(t1) (x + y)*(y + z)

Return type:: ExprRef

class kdrag.utils.ForAllHole(vs: list[ExprRef], orig_vs: list[ExprRef])

Bases: QuantifierHole

Parameters:

vs (list[ExprRef])
orig_vs (list[ExprRef])

has_right() → bool

Return type:: bool

orig_vs: list[ExprRef]

vs: list[ExprRef]

wrap(body: ExprRef) → ExprRef

Parameters:: body (ExprRef)
Return type:: ExprRef

class kdrag.utils.LambdaHole(vs: list[ExprRef], orig_vs: list[ExprRef])

Bases: QuantifierHole

Parameters:

vs (list[ExprRef])
orig_vs (list[ExprRef])

has_right() → bool

Return type:: bool

orig_vs: list[ExprRef]

vs: list[ExprRef]

wrap(body: ExprRef) → ExprRef

Parameters:: body (ExprRef)
Return type:: ExprRef

class kdrag.utils.QuantifierHole(vs: list[z3.z3.ExprRef], orig_vs: list[z3.z3.ExprRef])

Bases: object

Parameters:

vs (list[ExprRef])
orig_vs (list[ExprRef])

has_right() → bool

Return type:: bool

orig_vs: list[ExprRef]

vs: list[ExprRef]

class kdrag.utils.Zipper(ctx: list[Hole], t: ExprRef)

Bases: object

A zipper for traversing and modifying terms. The Zipper retains a context stack of “holes” and the current term. https://en.wikipedia.org/wiki/Zipper_(data_structure)

>>> x,y,z = smt.Ints("x y z")
>>> t = smt.Lambda([x,y], (x + y) * (y + z))
>>> z1 = Zipper.from_term(t)
>>> z1.open_binder().arg(1).left().arg(0)
Zipper(ctx=[LambdaHole(vs=[X!..., Y!...], orig_vs=[x, y]), DeclHole(f=*, _left=(), _right=(Y!... + z,)), DeclHole(f=+, _left=(), _right=(Y!...,))], t=X!...)
>>> z1.up().up().up()
Zipper(ctx=[], t=Lambda([x, y], (x + y)*(y + z)))

Parameters:

ctx (list[Hole])
t (ExprRef)

__hash__(): Warning: If you are hashing Zippers, make sure you are copying them.

__next__() → ExprRef

All subterms of the term in a pre-order traversal.

>>> x,y,z = smt.Ints("x y z")
>>> list(Zipper([], x + y*z))
[x, y*z, y, z]

Return type:: ExprRef

arg(n: int) → Zipper

Parameters:: n (int)
Return type:: Zipper

copy() → Zipper

Return type:: Zipper

ctx: list[Hole]

classmethod from_term(t: ExprRef) → Zipper

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

left() → Zipper

Return type:: Zipper

open_binder() → Zipper

Return type:: Zipper

pmatch(vs: list[ExprRef], pat: ExprRef) → dict[ExprRef, ExprRef] | None

Pattern match the current term against a pattern with variables vs. Leaves the zipper in a context state. This can be used to replace but rebuild using original context

>>> x,y,z,a,b,c = smt.Ints("x y z a b c")
>>> zip = Zipper([], x + smt.Lambda([y], y*z)[x])
>>> (subst := zip.pmatch([a,b], a*b))
{b: z, a: Y!...}
>>> zip.t = smt.IntVal(1) * subst[a]
>>> zip.rebuild()
x + Lambda(y, 1*y)[x]

Parameters:

vs (list[ExprRef])
pat (ExprRef)

Return type:

dict[ExprRef, ExprRef] | None

rebuild() → ExprRef

Return type:: ExprRef

right() → Zipper

Return type:: Zipper

t: ExprRef

up() → Zipper

Return type:: Zipper

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.bysect(thm, by: list[Proof] | dict[object, Proof], **kwargs) → Sequence[tuple[object, Proof]]

Bisect the by list to find a minimal set of premises that prove thm. Presents the same interface as prove

>>> x,y,z = smt.Ints("x y z")
>>> by = [kd.prove(x + 1 > x), kd.axiom(x == y), kd.prove(y + 1 > y), kd.axiom(y == z)]
>>> bysect(x == z, by=by)
[(1, |= x == y), (3, |= y == z)]

Parameters:: by (list[Proof] | dict[object, Proof])
Return type:: Sequence[tuple[object, Proof]]

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.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_in(vs: list[ExprRef], t: ExprRef) → bool

Returns True if none of the variables in vs exist unbound in t. Distinct from occurs in that vs have to be constants, not general terms.

>>> x,y,z = smt.Ints("x y z")
>>> assert not free_in([x], x + y + z)
>>> assert free_in([x], y + z)
>>> assert free_in([x], smt.Lambda([x], x + y + z))

Parameters:

vs (list[ExprRef])
t (ExprRef)

Return type:

bool

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_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.pmatch_rec_ctx(vs: list[ExprRef], pat: ExprRef, t: ExprRef) → tuple[ExprCtx, ExprRef, dict[ExprRef, ExprRef]] | None

Pattern match pat against subterms of t, returning the context, matched term, and substitution if successful. >>> x,y,z,a,b = smt.Ints(“x y z a b”) >>> kd.utils.pmatch_rec_ctx([a,b], a*b, smt.Lambda([x], x * y)) ([LambdaHole(vs=[X!…], orig_vs=[x])], X!…*y, {b: y, a: X!…})

Parameters:

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

Return type:

tuple[ExprCtx, 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.propagate(maybes: list[BoolRef], known: BoolRef) → list[BoolRef]

Prune the list of maybes to the ones implies by known

>>> p,q,r = smt.Bools("p q r")
>>> propagate([p, q, r, smt.And(p,q)], p & q)
[p, q, And(p, q)]

Parameters:

maybes (list[BoolRef])
known (BoolRef)

Return type:

list[BoolRef]

kdrag.utils.propagate_eqs(terms: list[ExprRef], known: BoolRef) → list[BoolRef]

Given a list of terms, propagate equalities among them that are implied by known. >>> x,y,z = smt.Ints(“x y z”) >>> terms = [x, y, z, x + 1, y + 1] >>> known = smt.And(x == y, y == z) >>> propagate_eqs(terms, known) [y == x, z == x, z == y, y + 1 == x + 1]

Parameters:

terms (list[ExprRef])
known (BoolRef)

Return type:

list[BoolRef]

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.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