kdrag.theories.fun

Functions

`MultiStore`(a, addr, *vs)
`store_view`(a)	Strips off the stores from an array and returns the base array and a list of (index, value) pairs.

kdrag.theories.fun.MultiStore(a: ArrayRef, addr: ExprRef, *vs: ExprRef) → ArrayRef

>>> a = smt.Array('a', smt.IntSort(), smt.IntSort())
>>> MultiStore(a, 42, 1,2,3)
Store(Store(Store(a, 42, 1), 43, 2), 44, 3)

Parameters:

Return type:

ArrayRef

kdrag.theories.fun.store_view(a: ArrayRef) → tuple[ArrayRef, list[tuple[ExprRef, ExprRef]]]

Strips off the stores from an array and returns the base array and a list of (index, value) pairs.

>>> a = smt.Array('a', smt.IntSort(), smt.IntSort())
>>> b = MultiStore(a, 42, 1,2,3)
>>> store_view(b)
(a, [(42, 1), (43, 2), (44, 3)])