# `Zee3`

The main entry point for the `Zee3` functionality.

# `assert`

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

Asserts a constraint inside a stateful solver.

# `check_sat`

```elixir
@spec check_sat(
  pid(),
  keyword()
) :: {:ok, :sat | :unsat | :unknown} | {:error, any()}
@spec check_sat(
  pid(),
  keyword()
) :: :sat | :unsat | :unknown
```

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`

```elixir
@spec check_sat_and_get_model(
  pid(),
  keyword()
) :: {:ok, any()} | {:error, any()}
```

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

# `check_sat_and_get_model!`

```elixir
@spec check_sat_and_get_model!(
  pid(),
  keyword()
) :: {:sat, any()} | :unsat | :unknown
```

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

# `current_z3_pid!`

Gets the PID for the current Z3 process.
This function only works if called inside a function
that was invokes inside a `Zee3.program/2` block.

# `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.

# `declare_rel`

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

Declares an relation for the fixpoint datalog engine.

# `declare_var`

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

Declares a variable which can be used in rules in the datalog engine.

# `entity_id`

Return an entity id from a value

# `eval_smt2_code`

Runs raw SMT-LIB2 code in the current solver.
Resturns `{:ok, data}` if there are no errors and
`{:error, data}` if there is at least an error.
The payload `data` is the raw output of the solver,
parsed into a list of `%Smt.XXX` values.

# `pop`

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

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
```

Pushes a new context into a stateful solver.

# `query`

Query a datalog relation to return all valid pairs.

# `query!`

Query a datalog relation to return all valid pairs. Raises on error.

# `rule`

Declares a rule for the datalog fixpoint engine.

# `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
```

Stops the stateful solver process.

---

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