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

Asserts a constraint inside a stateful solver.

@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 for satisfiability and get the model in case it is actually satisfiable. Raises on error.

@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.

@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.

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.

@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.

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

Declares an relation for the fixpoint datalog engine.

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

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

Return an entity id from a value

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.

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

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

Pushes a new context into a stateful solver.

Query a datalog relation to return all valid pairs.

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

Declares a rule for the datalog fixpoint engine.

@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

Stops the stateful solver process.