ShotTx.Prover (ShotTx v0.1.0)

Copy Markdown View Source

Public entry point for the ShotTx tableau prover.

Three related APIs live here:

release_term_pool/0 sits alongside them for callers that run many proofs in one node.

Every call spins up a fresh ShotTx.Prover.SessionSupervisor and blocks synchronously on the Manager until the search terminates (theorem, countermodel, timeout, or exhausted iterative deepening). The session tree is torn down on every exit path, including a caller that is killed outright. Configuration is threaded through as a keyword list that is merged into a ShotTx.Data.Parameters struct — see that module for the full list of knobs, and ShotTx.Config for session-wide defaults.

Summary

Types

proof_result()

Functions

compile_stats(stats)

Compiles a raw stats snapshot (as returned by prove/3 with stats: true) into a structured report grouped by :timing, :search, :rules, :branches, and :csp. Idempotent on already-compiled reports.

format_result(arg1)

Formats a proof_result() as a short human-readable string for quick inspection.

format_stats(stats, opts \\ [])

Pretty-prints a stats snapshot or compiled report. Pass verbose: true to include zero-valued rule/branch counters, or sections: [:timing, :csp] to render a subset.

prove(problem)

Shorthand delegating to the three-argument form.

prove(conclusion, opts)
prove(conclusion, assumptions, opts)

Attempts to prove conclusion from assumptions.

prove_string(target, assumptions \\ [], opts \\ [])

Convenience wrapper that returns a human-readable string result, preserving the original prove interface for quick testing.

release_term_pool()

Drops every term memoized in the node-wide :term_pool.

sat(formulas, defs \\ %{}, opts \\ [])

Checks the satisfiability of a list of formulas. Delegates the execution to the Manager GenServer.

Types

proof_result()

@type proof_result() ::
  {:thm, ShotTx.Proof.t()}
  | {:csa, String.t(), ShotTx.Proof.t()}
  | :unknown
  | {:timeout, ShotTx.Proof.t()}
  | {:error, term()}

Functions

compile_stats(stats)

@spec compile_stats(map()) :: map()

Compiles a raw stats snapshot (as returned by prove/3 with stats: true) into a structured report grouped by :timing, :search, :rules, :branches, and :csp. Idempotent on already-compiled reports.

format_result(arg1)

@spec format_result(proof_result()) :: String.t()

Formats a proof_result() as a short human-readable string for quick inspection.

format_stats(stats, opts \\ [])

@spec format_stats(
  map(),
  keyword()
) :: String.t()

Pretty-prints a stats snapshot or compiled report. Pass verbose: true to include zero-valued rule/branch counters, or sections: [:timing, :csp] to render a subset.

prove(problem)

@spec prove(ShotDs.Data.Problem.t() | ShotDs.Data.Term.term_id()) :: proof_result()

Shorthand delegating to the three-argument form.

Accepts either a ShotDs.Data.Problem (prove(problem) — no options), a single ShotDs.Data.Term.term_id/0 conclusion (prove(conclusion)), or a conclusion plus either an assumption list or options list.

See prove/3 for the primary interface and return type.

prove(conclusion, opts)

@spec prove(
  ShotDs.Data.Problem.t(),
  keyword()
) :: proof_result() | {proof_result(), map()}
@spec prove(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()] | keyword()) ::
  proof_result() | {proof_result(), map()}

prove(conclusion, assumptions, opts)

@spec prove(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()], keyword()) ::
  proof_result() | {proof_result(), map()}

Attempts to prove conclusion from assumptions.

Accepts three call shapes:

  • prove(problem) — a Problem struct with a conjecture and axioms.
  • prove(conclusion) / prove(conclusion, assumptions) — term IDs.
  • prove(conclusion, assumptions, opts) — full form; opts are forwarded to Parameters except for the :defs key (a definition map).

Returns a proof_result().

prove_string(target, assumptions \\ [], opts \\ [])

@spec prove_string(
  ShotDs.Data.Problem.t() | ShotDs.Data.Term.term_id(),
  [ShotDs.Data.Term.term_id()],
  keyword()
) :: String.t()

Convenience wrapper that returns a human-readable string result, preserving the original prove interface for quick testing.

release_term_pool()

@spec release_term_pool() :: :ok

Drops every term memoized in the node-wide :term_pool.

Sessions release their own ETS tables when they terminate, but the term pool is shared and only ever grows: a sweep accumulates every term of every problem it has seen, and the hash-consing lookups on the hot path pay for it.

Term IDs do not survive a release. Any ShotTx.Proof, ShotDs.Data.Problem or bare term ID still held becomes unreadable, so call this only between problems, once the previous result has been consumed.

sat(formulas, defs \\ %{}, opts \\ [])

@spec sat([ShotDs.Data.Term.term_id()] | ShotDs.Data.Term.term_id(), map(), keyword()) ::
  {:sat, map()}
  | {:unsat, map(), list(), map()}
  | {:unknown, term()}
  | {:timeout, ShotTx.Proof.t()}
  | {sat_result :: term(), stats :: map()}

Checks the satisfiability of a list of formulas. Delegates the execution to the Manager GenServer.