func (x Int) sym(c *cache) z3.BV {
	if !x.IsConcrete() {
		return x.S
	}
	return c.z3.FromInt(int64(x.C), c.sortInt).(z3.BV)
}
sym returns x's symbolic value, creating it if necessary.
package st
import (
	"fmt"
	"github.com/aclements/go-z3/z3"
	"math/big"
)
type sorts struct {
	sortBool    z3.Sort
	sortInt     z3.Sort
	sortInt8    z3.Sort
	sortInt16   z3.Sort
	sortInt32   z3.Sort
	sortInt64   z3.Sort
	sortUint    z3.Sort
	sortUint8   z3.Sort
	sortUint16  z3.Sort
	sortUint32  z3.Sort
	sortUint64  z3.Sort
	sortUintptr z3.Sort
	sortInteger z3.Sort
	sortReal    z3.Sort
}
func initSorts(s *sorts, ctx *z3.Context) {
	s.sortBool = ctx.BoolSort()
	s.sortInt = ctx.BVSort(64)
	s.sortInt8 = ctx.BVSort(8)
	s.sortInt16 = ctx.BVSort(16)
	s.sortInt32 = ctx.BVSort(32)
	s.sortInt64 = ctx.BVSort(64)
	s.sortUint = ctx.BVSort(64)
	s.sortUint8 = ctx.BVSort(8)
	s.sortUint16 = ctx.BVSort(16)
	s.sortUint32 = ctx.BVSort(32)
	s.sortUint64 = ctx.BVSort(64)
	s.sortUintptr = ctx.BVSort(64)
	s.sortInteger = ctx.IntSort()
	s.sortReal = ctx.RealSort()
}
type Bool struct {
	C bool
	S z3.Bool
}
func AnyBool(ctx *z3.Context, name string) Bool {
	cache := getCache(ctx)
	sym := cache.z3.FreshConst(name, cache.sortBool).(z3.Bool)
	return Bool{S: sym}
}
func (x Bool) String() string {
	if x.IsConcrete() {
		return fmt.Sprint(x.C)
	}
	return x.S.String()
}
func (x Bool) IsConcrete() bool {
	return x.S.Context() == nil
}
func (x Bool) Eval(m *z3.Model) bool {
	if x.IsConcrete() {
		return x.C
	}
	c := m.Eval(x.S, true).(z3.Bool)
	val, ok := c.AsBool()
	if !ok {
		panic("model evaluation produced non-concrete value " + c.String())
	}
	return (bool)(val)
}
func (x Bool) sym(c *cache) z3.Bool {
	if !x.IsConcrete() {
		return x.S
	}
	return c.z3.FromBool(x.C)
}
func (x Bool) And(y Bool) Bool {
	if x.IsConcrete() && y.IsConcrete() {
		return Bool{C: x.C && y.C}
	}
	ctx := x.S.Context()
	if ctx == nil {
		ctx = y.S.Context()
	}
	cache := getCache(ctx)
	return Bool{S: x.sym(cache).And(y.sym(cache))}
}
func (x Bool) Or(y Bool) Bool {
	if x.IsConcrete() && y.IsConcrete() {
		return Bool{C: x.C || y.C}
	}
	ctx := x.S.Context()
	if ctx == nil {
		ctx = y.S.Context()
	}
	cache := getCache(ctx)
	return Bool{S: x.sym(cache).Or(y.sym(cache))}
}
func (x Bool) Eq(y Bool) Bool {
	if x.IsConcrete() && y.IsConcrete() {
		return Bool{C: x.C == y.C}
	}
	ctx := x.S.Context()
	if ctx == nil {
		ctx = y.S.Context()
	}
	cache := getCache(ctx)
	return Bool{S: x.sym(cache).Eq(y.sym(cache))}
}
func (x Bool) NE(y Bool) Bool {
	if x.IsConcrete() && y.IsConcrete() {
		return Bool{C: x.C != y.C}
	}
	ctx := x.S.Context()
	if ctx == nil {
		ctx = y.S.Context()
	}
	cache := getCache(ctx)
	return Bool{S: x.sym(cache).NE(y.sym(cache))}
}
func (x Bool) Not() Bool {
	if x.IsConcrete() {
		return Bool{C: !x.C}
	}
	return Bool{S: x.S.Not()}
}
type Int struct {
	C int
	S z3.BV
}
func AnyInt(ctx *z3.Context, name string) Int {
	cache := getCache(ctx)
	sym := cache.z3.FreshConst(name, cache.sortInt).(z3.BV)
	return Int{S: sym}
}
func (x Int) String() string {
	if x.IsConcrete() {
		return fmt.Sprint(x.C)
	}
	return x.S.String()
}
func (x Int) IsConcrete() bool {
	return x.S.Context() == nil
}
func (x Int) Eval(m *z3.Model) int {
	if x.IsConcrete() {
		return x.C
	}
	c := m.Eval(x.S, true).(z3.BV)
	val, ok, _ := c.AsInt64()
	if !ok {
		panic("model evaluation produced non-concrete value " + c.String())
	}
	return (int)(val)
}