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

Asserts a constraint inside a stateful solver.

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

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

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

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

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

Declares a constant inside a stateful solver.

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

Declares datatypes inside a stateful solver.

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

Declares an uninterpreted function inside a stateful solver.

Pops the last context from a stateful solver.

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.

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

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

Pushes a new context into a stateful solver.

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

Starts a new stateful solver process.

When the solver is started, it automatically pushes a new context.

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

Starts the stateful solver process.