# `Zee3.StdLib.Sort`

Standard SMT-LIB2 Sorts (Types) for the Zee3 DSL.

All functions return an AST node representing an S-Expression.

# `t`

```elixir
@type t() :: Zee3.Smt2.t()
```

# `array`

Creates an Array sort mapping a domain to a range.
Generates SMT: (Array domain_sort range_sort)

# `bit_vec`

```elixir
@spec bit_vec(integer() | Zee3.Smt2.t()) :: Zee3.Smt2.t()
```

Creates a BitVector sort of a specific size.
Generates SMT: (_ BitVec size)

# `bool`

```elixir
@spec bool() :: Zee3.Smt2.t()
```

A Z3 `Bool` sort.

# `entity_id`

```elixir
@spec entity_id() :: Zee3.Smt2.t()
```

A special sort which serves as an alias for a BitVec of length 32.

This is meant to be used as the type of entity IDs for the datalog
engine, which needs a finite sort, and defaulting to a BitVec
of this size seems like a safe option.

# `float16`

```elixir
@spec float16() :: Zee3.Smt2.t()
```

A Z3 `Float16` (16-bit float) sort.

# `float32`

```elixir
@spec float32() :: Zee3.Smt2.t()
```

A Z3 `Float32` (32-bit float) sort.

# `float64`

```elixir
@spec float64() :: Zee3.Smt2.t()
```

A Z3 `Float64` (64-bit float) sort.

# `float128`

```elixir
@spec float128() :: Zee3.Smt2.t()
```

A Z3 `Float128` (128-bit float) sort.

# `floating_point`

```elixir
@spec floating_point(integer() | Zee3.Smt2.t(), integer() | Zee3.Smt2.t()) ::
  Zee3.Smt2.t()
@spec floating_point(Zee3.Smt2.t(), Zee3.Smt2.t()) :: Zee3.Smt2.t()
```

Creates a custom FloatingPoint sort.
eb: exponent bits, sb: significand bits.
Generates SMT: (_ FloatingPoint eb sb)

# `int`

```elixir
@spec int() :: Zee3.Smt2.t()
```

A Z3 `Int` sort.

# `real`

```elixir
@spec real() :: Zee3.Smt2.t()
```

A Z3 `Real` sort.

# `reg_lan`

```elixir
@spec reg_lan() :: Zee3.Smt2.t()
```

A Z3 `RegLang` (regular language) sort.

# `rounding_mode`

```elixir
@spec rounding_mode() :: Zee3.Smt2.t()
```

A Z3 `RoundingMode` sort.

# `string`

```elixir
@spec string() :: Zee3.Smt2.t()
```

A Z3 `String` sort.

---

*Consult [api-reference.md](api-reference.md) for complete listing*