# `Zee3`

Documentation for `Zee3`.

# `assert`

```elixir
@spec assert(pid(), binary()) :: :ok
```

Asserts a constraint inside a stateful solver.

# `check_sat`

Check for satisfiability and get the model in case it is
actually satisfiable.

# `check_sat!`

Check for satisfiability and get the model in case it is
actually satisfiable. *Raises on error*.

# `check_sat_and_get_model`

Check for satisfiability and get the model in case it is
actually satisfiable.

# `check_sat_and_get_model!`

Check for satisfiability and get the model in case it is
actually satisfiable. *Raises on error*.

# `declare_const`

```elixir
@spec declare_const(pid(), binary(), binary()) :: :ok
```

Declares a constant inside a stateful solver.

# `declare_datatypes`

```elixir
@spec declare_datatypes(pid(), binary(), [atom()]) :: :ok
```

Declares datatypes inside a stateful solver.

# `declare_fun`

```elixir
@spec declare_fun(pid(), binary(), [binary()], binary()) :: :ok
```

Declares an uninterpreted function inside a stateful solver.

# `pop`

Pops the last context from a stateful solver.

# `program`
*macro* 

Runs code inside the Z3 solver with the given `solver_pid`
using an optimized elixir DSL.

This macro doen't assume its contents are special in any way
and it does not assume we want to push a new context.
If you want to create or remove a context, you must call `push()`
and `pop()` inside the body of the macro.

# `push`

```elixir
@spec push(pid()) :: :ok
@spec push(pid()) :: :ok
```

Pushes a new context into a stateful solver.

# `start_solver`

```elixir
@spec start_solver() :: GenServer.on_start()
```

Starts a new stateful solver process.

When the solver is started, it automatically
`push`es a new context.

# `stop_solver`

```elixir
@spec stop_solver(pid()) :: :ok
```

Starts the stateful solver process.

---

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