kdrag.utils.generate

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]