kdrag.reflect.reify

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: