func (expr *valueImpl) Context() *Context {
	if expr == nil {
		return nil
	}
	return expr.ctx
}
Context returns the Context that created expr.
package z3
import (
	"math/big"
	"runtime"
	"unsafe"
)
import "C"
type Value interface {
	AsAST() AST
	Sort() Sort
	Context() *Context
	String() string
	astKind() C.Z3_ast_kind
	impl() *valueImpl
}
type noEq struct {
	_ [0]func()
}
type value struct {
	*valueImpl
	noEq
}
type valueImpl astImpl
func wrapValue(ctx *Context, ctor func() C.Z3_ast) value {
	var val value
	ctx.do(func() {
		cast := ctor()
		val = value{(*valueImpl)(wrapAST(ctx, cast).astImpl), noEq{}}
	})
	return val
}
func (x value) lift(kind Kind) Value {
	if kind == KindUnknown {
		kind = x.Sort().Kind()
	}
	wrap, ok := kindWrappers[kind]
	if !ok {
		panic("value has unknown kind " + kind.String())
	}
	return wrap(x)
}
func (ctx *Context) Const(name string, sort Sort) Value {
	sym := ctx.symbol(name)
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_const(ctx.c, sym, sort.c)
	})
	runtime.KeepAlive(sort)
	return val.lift(sort.Kind())
}
func (ctx *Context) FreshConst(prefix string, sort Sort) Value {
	cprefix := C.CString(prefix)
	defer C.free(unsafe.Pointer(cprefix))
	val := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_fresh_const(ctx.c, cprefix, sort.c)
	})
	runtime.KeepAlive(sort)
	return val.lift(sort.Kind())
}
func (ctx *Context) FromBigInt(val *big.Int, sort Sort) Value {
	if sort.Kind() == KindFloatingPoint {
		return ctx.floatFromBigInt(val, sort)
	}
	cstr := C.CString(val.Text(10))
	defer C.free(unsafe.Pointer(cstr))
	sval := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_numeral(ctx.c, cstr, sort.c)
	})
	runtime.KeepAlive(sort)
	return sval.lift(sort.Kind())
}
func (ctx *Context) FromInt(val int64, sort Sort) Value {
	if sort.Kind() == KindFloatingPoint {
		return ctx.floatFromInt(val, sort)
	}
	sval := wrapValue(ctx, func() C.Z3_ast {
		return C.Z3_mk_int64(ctx.c, C.__int64(val), sort.c)
	})
	runtime.KeepAlive(sort)
	return sval.lift(sort.Kind())
}
func (expr *valueImpl) impl() *valueImpl {
	return expr
}