GenServer that owns the ETS tables for a single proof session.
Creates the shared, public tables listed below on startup and keeps them alive
for the duration of the session tree; they are dropped with this process when
the session is torn down. All other processes obtain the table references via
get_tables/1.
Tables created:
:stats— proof-search counters and timing metadata.:tombs— branch IDs that have been closed; used to poison descendants.:work_queue— ordered set of{priority_key, Branch.t()}entries.:idle_queue— branches parked waiting for iterative deepening.:traces— per-branch rule application history for proof reconstruction.:provenance— per-fresh-variable annotation (γ / prim-subst origin); seeShotTx.Prover.Provenance.:idle_workers—{worker_pid, true}for each worker currently parked on an empty queue. Read byShotTx.Prover.Workerwhen it pushes a branch, so that a push only wakes workers actually waiting for one.:suggestions— instantiation hints published bySuggestionAgent, consumed by workers on splice; seeShotTx.Prover.Suggestion. Rows are{{prefix, recipe, term}, applied_count, %Suggestion{}}so that:ets.update_counter/3can enforce the cascade cap at position 2.
Summary
Functions
Returns a specification to start this module under a supervisor.
Returns the ETS table map for the given session_id.
Starts the ETS keeper for the given session_id.
Functions
Returns a specification to start this module under a supervisor.
See Supervisor.
Returns the ETS table map for the given session_id.
@spec start_link({String.t(), term()}) :: GenServer.on_start()
Starts the ETS keeper for the given session_id.