# `Zee3.Smt2`

# `smt2_like`

```elixir
@type smt2_like() :: t() | integer() | boolean() | list() | bitstring()
```

A value which is either an `Smt2` value or a literal
that can be unambiguously be converted into an `Smt2`
value.

# `t`

```elixir
@type t() ::
  Zee3.Smt2.Int.t()
  | Zee3.Smt2.Real.t()
  | Zee3.Smt2.Symbol.t()
  | Zee3.Smt2.String.t()
  | Zee3.Smt2.BitVec.t()
  | Zee3.Smt2.List.t()
```

An `Smt2` value, which can be serialized and sent to Z3.

# `bit_vec16_from_integer`

```elixir
@spec bit_vec16_from_integer(non_neg_integer()) :: t()
```

Encode an integer as a bit vector with 16 bits.

# `bit_vec32_from_integer`

```elixir
@spec bit_vec32_from_integer(non_neg_integer()) :: t()
```

Encode an integer as a bit vector with 32 bits.

# `bit_vec64_from_integer`

```elixir
@spec bit_vec64_from_integer(non_neg_integer()) :: t()
```

Encode an integer as a bit vector with 64 bits.

# `bit_vec`

```elixir
@spec bit_vec(bitstring()) :: t()
```

An `Smt2` bit vector.

# `bit_vec_from_integer`

```elixir
@spec bit_vec_from_integer(non_neg_integer(), pos_integer()) :: t()
```

Encode an integer as a bit vector with a given length.

# `call`

```elixir
@spec call(binary(), [smt2_like()]) :: t()
```

An `Smt2` function call. If some of the arguments
of the function call are literals, they are
converted into `Smt2` values.

# `from_ex`
*macro* 

Create a `Smt2` value from a formula in Elixir code.

The code inside this macro call is converted the following way:

* The macro calls `use Zee3.StdLib` before creating the AST,
  which means elixir functions will be interpreted as if they were
  in a `Zee3.program/2` macro body.
* Elixir variables (`a`, `b`, ...) are converted into symbols

## Examples

    iex(1)> require Zee3.Smt2, as: Smt2
    Zee3.Smt2

    iex(2)> Smt2.from_ex(a)
    #Zee3.Smt2.Symbol<a>

    iex(3)> Smt2.from_ex(a + b)
    #Zee3.Smt2.List<(+ a b)>

    iex(4)> Smt2.from_ex(x or y or z)
    #Zee3.Smt2.List<(or x y z)>

    iex(5)> Smt2.from_ex(x <- a and b and c)
    #Zee3.Smt2.List<(=> (and a b c) x)>

# `from_ex_ast`

# `integer`

```elixir
@spec integer(integer()) :: t()
```

An `Smt2` integer.

# `is_smt2`
*macro* 

# `list`

```elixir
@spec list([smt2_like()]) :: t()
```

An `Smt2` list. If some of the arguments
of the list literals, they are
converted into `Smt2` values.

# `serialize`

# `serialize_multiple`

# `string`

```elixir
@spec string(binary()) :: t()
```

An `Smt2` string.

# `symbol`

```elixir
@spec symbol(binary()) :: t()
```

An `Smt2` symbol.

# `to_smt2`

```elixir
@spec to_smt2(smt2_like()) :: t()
```

Convert a literal into a `Smt2` value.
If the value is already an `Smt2` value it is unchanged.

---

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