kdrag.reflect

Reflecting and reifying SMT expressions from/into Python values.

Functions

`datatype`(s[, locals, globals])	Use python type syntax to define an algebraic datatype datatype.
`eval_`(e[, globals, locals, default])	Evaluate a z3 expression in a given environment.
`expr`(expr[, globals, locals])	Turn a string of a python expression into a z3 expressions.
`infer_sort`(x)
`namedtuple_of_constructor`(sort, idx)	Given a datatype sort and an index, return a named tuple with field names and the constructor.
`nbe`(x)	Normalization by evaluation.
`reflect`(f[, globals])	Reflect a function definition by injecting the parameters and recursive self call into the local environment.
`reify`(s, x)	sort directed reification of a python value.
`sort_of_type`(t)	Give equivalent SMT sort for a given Python type.
`type_of_sort`(s)	Give equivalent Python type for a given SMT sort.

Classes

KnuckleClosure(lam, globals, locals, default)

A closure that can be used to evaluate expressions in a given environment.

class kdrag.reflect.KnuckleClosure(lam: QuantifierRef, globals: dict[str, object], locals: dict[str, object], default: Callable[[ExprRef], object])

Bases: object

A closure that can be used to evaluate expressions in a given environment. We don’t use lambda so that we can inspect

Parameters:

lam (QuantifierRef)
globals (dict[str, object])
locals (dict[str, object])
default (Callable[[ExprRef], object])

default: Callable[[ExprRef], object]

globals: dict[str, object]

lam: QuantifierRef

locals: dict[str, object]

kdrag.reflect.datatype(s: str, locals=None, globals=None) → DatatypeSortRef

Use python type syntax to define an algebraic datatype datatype. Fields can be specified positionally or by name. Reads the inner types from current environment.

>>> Int = smt.IntSort()
>>> Real = smt.RealSort()
>>> Foo = datatype("type Foo = Biz | Bar | Baz(Int, Int, smt.IntSort()) | Boz(x = Int, y = Int)")
>>> Foo.Baz.domain(1)
Int
>>> Foo.x.range()
Int

Parameters:: s (str)
Return type:: DatatypeSortRef

kdrag.reflect.eval_(e: ~z3.z3.ExprRef, globals={}, locals={}, default=<function __default_error>)

Evaluate a z3 expression in a given environment. The analog of python’s eval.

>>> eval_(smt.IntVal(42))
42
>>> eval_(smt.IntVal(1) + smt.IntVal(2))
3
>>> x = smt.Int("x")
>>> eval_(smt.Lambda([x], x + 1)[3])
4
>>> R = kd.Struct("R", ("x", kd.Z), ("y", smt.BoolSort()))
>>> eval_(R(42, True).x)
42
>>> eval_(R(42,True).is_R)
True

Parameters:: e (ExprRef)

kdrag.reflect.expr(expr: str, globals=None, locals=None) → ExprRef

Turn a string of a python expression into a z3 expressions. Globals are inferred to be current scope if not given.

>>> expr("x + 1", globals={"x": smt.Int("x")})
x + 1
>>> x = smt.Int("x")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> expr("f(x) + 1 if 0 < x < 5 < 7 else x * x")
If(And(0 < x, 5 > x, 5 < 7), f(x) + 1, x*x)

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

kdrag.reflect.infer_sort(x: object) → SortRef

Parameters:: x (object)
Return type:: SortRef

kdrag.reflect.namedtuple_of_constructor(sort: DatatypeSortRef, idx: int)

Given a datatype sort and an index, return a named tuple with field names and the constructor. >>> Nat = smt.Datatype(“Nat”) >>> Nat.declare(“Z”) >>> Nat.declare(“S”, (“pred”, Nat)) >>> Nat = Nat.create() >>> namedtuple_of_constructor(Nat, 1)(0) S(pred=0)

Parameters:

sort (DatatypeSortRef)
idx (int)

kdrag.reflect.nbe(x: ExprRef) → ExprRef

Normalization by evaluation.

>>> nbe(smt.IntVal(41) + smt.IntVal(1))
42
>>> x,y = smt.Ints("x y")
>>> nbe(smt.Lambda([x], x + 1)[3])
4
>>> nbe(smt.Lambda([x], x + 1))
Lambda(x, x + 1)
>>> nbe(smt.Lambda([x], smt.IntVal(3) + 1))
Lambda(x, 3 + 1)

Parameters:: x (ExprRef)
Return type:: ExprRef

kdrag.reflect.reflect(f, globals=None) → FuncDeclRef

Reflect a function definition by injecting the parameters and recursive self call into the local environment. Uses type annotations to do so.

Only handles a purely functional subset of python. Simple assignment is handled as a let who’s scope extends to the end of it’s subbranch. Every branch must end with a return.

You can still call original function under attribute __wrapped__.

>>> def foo(x : int) -> int:
...     return x + 3
>>> foo = reflect(foo)
>>> foo.__wrapped__(3)
6
>>> foo.defn
|= ForAll(x, foo(x) == x + 3)

>>> @reflect
... def bar(x : int, y : str) -> int:
...     if x > 4:
...         return x + 3
...     elif y == "fred":
...        return 14
...     else:
...        return bar(x - 1, y)
>>> bar.defn
|= ForAll([x, y],
       bar(x, y) ==
       If(4 < x, x + 3, If(y == "fred", 14, bar(x - 1, y))))

Return type:: FuncDeclRef

kdrag.reflect.reify(s: SortRef, x: object) → ExprRef

sort directed reification of a python value. https://en.wikipedia.org/wiki/Normalisation_by_evaluation >>> reify(smt.IntSort(), 42) 42 >>> reify(smt.IntSort(), 42).sort() Int >>> x = smt.Int(“x”) >>> kd.utils.alpha_eq(reify(smt.ArraySort(smt.IntSort(), smt.IntSort()), lambda x: x + 1), smt.Lambda([x], x + 1)) True >>> reify(smt.RealSort(), fractions.Fraction(10,16)) 5/8

Parameters:

s (SortRef)
x (object)

Return type:

ExprRef

kdrag.reflect.sort_of_type(t: type) → SortRef

Give equivalent SMT sort for a given Python type.

>>> sort_of_type(int)
Int
>>> sort_of_type(list[int])
Seq(Int)
>>> sort_of_type(dict[str, int])
Array(String, Int)

Parameters:: t (type)
Return type:: SortRef

kdrag.reflect.type_of_sort(s: SortRef) → type

Give equivalent Python type for a given SMT sort.

>>> type_of_sort(smt.IntSort())
<class 'int'>
>>> type_of_sort(smt.ArraySort(smt.StringSort(), smt.IntSort()))
dict[str, int]
>>> type_of_sort(smt.SeqSort(smt.IntSort()))
list[int]

Parameters:: s (SortRef)
Return type:: type