func (f FuncDecl) AsAST() AST {
	var ast AST
	f.ctx.do(func() {
		ast = wrapAST(f.ctx, C.Z3_func_decl_to_ast(f.ctx.c, f.c))
	})
	runtime.KeepAlive(f)
	return ast
}
AsAST returns the AST representation of f.
package z3
import (
	"runtime"
	"unsafe"
)
import "C"
type FuncDecl struct {
	*funcDeclImpl
	noEq
}
type funcDeclImpl struct {
	ctx *Context
	c   C.Z3_func_decl
}
func wrapFuncDecl(ctx *Context, c C.Z3_func_decl) FuncDecl {
	impl := &funcDeclImpl{ctx, c}
	C.Z3_inc_ref(ctx.c, C.Z3_func_decl_to_ast(ctx.c, c))
	runtime.SetFinalizer(impl, func(impl *funcDeclImpl) {
		impl.ctx.do(func() {
			C.Z3_dec_ref(impl.ctx.c, C.Z3_func_decl_to_ast(impl.ctx.c, impl.c))
		})
	})
	runtime.KeepAlive(ctx)
	return FuncDecl{impl, noEq{}}
}
func (ctx *Context) FuncDecl(name string, domain []Sort, range_ Sort) FuncDecl {
	sym := ctx.symbol(name)
	cdomain := make([]C.Z3_sort, len(domain))
	for i, sort := range domain {
		cdomain[i] = sort.c
	}
	var funcdecl FuncDecl
	ctx.do(func() {
		var cdp *C.Z3_sort
		if len(cdomain) > 0 {
			cdp = &cdomain[0]
		}
		funcdecl = wrapFuncDecl(ctx, C.Z3_mk_func_decl(ctx.c, sym, C.uint(len(cdomain)), cdp, range_.c))
	})
	runtime.KeepAlive(domain)
	runtime.KeepAlive(range_)
	return funcdecl
}
func (ctx *Context) FreshFuncDecl(prefix string, domain []Sort, range_ Sort) FuncDecl {
	cprefix := C.CString(prefix)
	defer C.free(unsafe.Pointer(cprefix))
	cdomain := make([]C.Z3_sort, len(domain))
	for i, sort := range domain {
		cdomain[i] = sort.c
	}
	var funcdecl FuncDecl
	ctx.do(func() {
		var cdp *C.Z3_sort
		if len(cdomain) > 0 {
			cdp = &cdomain[0]
		}
		funcdecl = wrapFuncDecl(ctx, C.Z3_mk_fresh_func_decl(ctx.c, cprefix, C.uint(len(cdomain)), cdp, range_.c))
	})
	runtime.KeepAlive(domain)
	runtime.KeepAlive(range_)
	return funcdecl
}
func (f FuncDecl) Context() *Context {
	if f.funcDeclImpl == nil {
		return nil
	}
	return f.ctx
}
func (f FuncDecl) String() string {
	var res string
	f.ctx.do(func() {
		res = C.GoString(C.Z3_func_decl_to_string(f.ctx.c, f.c))
	})
	runtime.KeepAlive(f)
	return res
}