array.go - Z3 Go API

func (c *Context) MkArrayDefault(array *Expr) *Expr

MkArrayDefault returns the default value of an array.

func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr

MkArrayExt returns the extensionality witness for two arrays. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

func (c *Context) MkArraySort(domain, range_ *Sort) *Sort

Array operations and sorts MkArraySort creates an array sort.

func (c *Context) MkAsArray(f *FuncDecl) *Expr

MkAsArray creates an array from a function declaration. The resulting array maps each input to the output of the function.

func (c *Context) MkConstArray(sort *Sort, value *Expr) *Expr

MkConstArray creates a constant array.

func (c *Context) MkMap(f *FuncDecl, arrays ...*Expr) *Expr

MkMap applies a function to the elements of one or more arrays, returning a new array. The function f is applied element-wise to the given arrays.

func (c *Context) MkSelect(array, index *Expr) *Expr

MkSelect creates an array read (select) operation.

func (c *Context) MkSelectN(array *Expr, indices []*Expr) *Expr

MkSelectN creates a multi-index array read (select) operation.

func (c *Context) MkStore(array, index, value *Expr) *Expr

MkStore creates an array write (store) operation.

func (c *Context) MkStoreN(array *Expr, indices []*Expr, value *Expr) *Expr

MkStoreN creates a multi-index array write (store) operation.

Functions