array.wrap.go

// Generated by genwrap.go. DO NOT EDIT

package z3

import "runtime"

/*
#cgo LDFLAGS: -lz3
#include <z3.h>
#include <stdlib.h>
*/
import "C"

// Eq returns a Value that is true if l and r are equal.
func (l Array) Eq(r Array) Bool {
	ctx := l.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_eq(ctx.c, l.c, r.c)
	})
	runtime.KeepAlive(l)
	runtime.KeepAlive(r)
	return Bool(val)
}

// NE returns a Value that is true if l and r are not equal.
func (l Array) NE(r Array) Bool {
	return l.ctx.Distinct(l, r)
}

// Select returns the value of array x at index i.
//
// i's sort must match x's domain. The result has the sort of x's
// range.
func (x Array) Select(i Value) Value {
	// Generated from array.go:63.
	ctx := x.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_select(ctx.c, x.c, i.impl().c)
	})
	runtime.KeepAlive(x)
	runtime.KeepAlive(i)
	return val.lift(KindUnknown)
}

// Store returns an array y that's identical to x except that
// y.Select(i) == v.
//
// i's sort must match x's domain and v's sort must match x's range.
// The result has the same sort as x.
func (x Array) Store(i Value, v Value) Array {
	// Generated from array.go:71.
	ctx := x.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_store(ctx.c, x.c, i.impl().c, v.impl().c)
	})
	runtime.KeepAlive(x)
	runtime.KeepAlive(i)
	runtime.KeepAlive(v)
	return Array(val)
}

// Default returns the default value of an array, for arrays that can
// be represented as finite maps plus a default value.
//
// This is useful for extracting array values interpreted by models.
func (x Array) Default() Value {
	// Generated from array.go:78.
	ctx := x.ctx
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_array_default(ctx.c, x.c)
	})
	runtime.KeepAlive(x)
	return val.lift(KindUnknown)
}