SemanticVerifier.Session (semantic_verifier v0.1.0)

Copy Markdown View Source

Stateful GenServer managing a single persistent interactive Z3 Port process (z3 -in -smt2).

Summary

Functions

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

execute_async(session, smt_script, from, pool_pid, timeout \\ 5000)
find_z3_binary(custom_path \\ nil)
query(session, smt_script, timeout \\ 5000)
start_link(opts \\ [])

Functions

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

execute_async(session, smt_script, from, pool_pid, timeout \\ 5000)

@spec execute_async(pid(), String.t(), GenServer.from(), pid(), non_neg_integer()) ::
  :ok

find_z3_binary(custom_path \\ nil)

query(session, smt_script, timeout \\ 5000)

@spec query(pid(), String.t(), non_neg_integer()) ::
  {:ok, :sat, String.t()} | {:ok, :unsat} | {:error, term()}

start_link(opts \\ [])

@spec start_link(keyword()) :: GenServer.on_start()