A root file together with everything its include directives reach.
Tptp.from_file/2 reads a single file. This reads a problem: the root and the
axiom sets it includes, with every span identifying the file it originates in, so
that a diagnostic concerning a symbol declared in an axiom file and used in the
problem can refer to both.
{:ok, unit, diagnostics} =
Tptp.Unit.from_file("Problems/PUZ/PUZ001+1.p", resolver: Tptp.Resolver.Fs)
Tptp.Unit.statements(unit) # [{file_id, statement}], includes expanded in place
unit.files[unit.root] # the root %Tptp.File{}Resolution is explicit
The default resolver is Tptp.Resolver.None, which records each directive and
reads nothing. Resolution reads files the caller did not name and, under
Tptp.Resolver.Http, performs network access, so the resolver is supplied by the
caller rather than defaulted.
Two representations
files is the set of files, each read once even where a diamond in the graph
reaches it twice. statements/1 is the sequence, with each include expanded in
position, which is what textual inclusion denotes and what a prover observes. A
file read once may therefore occur twice in the sequence.
Formula selection
include('big.ax', [key_lemma]) retains only the named formulae, and the filter
applies to the whole subtree beneath that directive rather than to big.ax
alone. The TPTP standard does not define the meaning of a selection when the
selected file has includes of its own; this reading makes include(f, [x])
denote the formula x wherever it occurs beneath the directive. A name occurring
nowhere beneath it produces a TPTP0603 warning.
Summary
Types
Options accepted by the entry points.
A root file and everything reachable from it through include, with the resolutions that got there.
Functions
Whether anything error-severity was found, in any file.
The file a span or id belongs to.
Every diagnostic, rendered one per line against the file it belongs to.
Every annotated formula, include directives expanded and filtered by selection.
Read a file from disk and everything it includes.
Read a file and everything it includes, raising Tptp.Error on any error.
Read a file the resolver knows by name, and everything it includes.
Read a file and everything it includes.
Every statement, with include directives expanded where they stand.
The bytes a span names, wherever in the unit it points.
Types
@type option() :: Tptp.option() | {:resolver, Tptp.Resolver.t()} | {:max_depth, pos_integer()} | {:max_concurrency, pos_integer()}
Options accepted by the entry points.
Everything Tptp.option/0 accepts, plus:
:resolver— how anincludename becomes bytes. Defaults toTptp.Resolver.None, which follows nothing.:max_concurrency— how many sibling includes are parsed at once. Defaults toSystem.schedulers_online(); set it to1for a strictly sequential walk, which is what a caller running under its ownmax_heap_sizeneeds, since that ceiling is not inherited by the processesTptp.Includespawns.:max_depth— how deep the include graph may nest before the walk stops and says so. Defaults to 64.
@type t() :: %Tptp.Unit{ diagnostics: [Tptp.Diagnostic.t()], files: %{required(Tptp.Span.file_id()) => Tptp.File.t()}, resolutions: %{ required({Tptp.Span.file_id(), non_neg_integer()}) => Tptp.Span.file_id() }, root: Tptp.Span.file_id() }
A root file and everything reachable from it through include, with the resolutions that got there.
Functions
Whether anything error-severity was found, in any file.
@spec file(t(), Tptp.Span.file_id() | Tptp.Span.t()) :: Tptp.File.t() | nil
The file a span or id belongs to.
Every diagnostic, rendered one per line against the file it belongs to.
@spec formulae(t()) :: [{Tptp.Span.file_id(), Tptp.Statement.Annotated.t()}]
Every annotated formula, include directives expanded and filtered by selection.
@spec from_file(Path.t(), [option()]) :: {:ok, t(), [Tptp.Diagnostic.t()]} | {:error, [Tptp.Diagnostic.t()]}
Read a file from disk and everything it includes.
Fails only when the root file cannot be read; an include that cannot be resolved is a diagnostic on an otherwise usable unit.
Read a file and everything it includes, raising Tptp.Error on any error.
@spec from_name(binary(), [option()]) :: {:ok, t(), [Tptp.Diagnostic.t()]} | {:error, [Tptp.Diagnostic.t()]}
Read a file the resolver knows by name, and everything it includes.
The entry point for a caller who has a TPTP name rather than a path — from a
problem list, a benchmark set, or a user typing PUZ001+1.p. The root goes
through the same resolver as its includes, so pointing $TPTP_ROOT at a local
library or passing Tptp.Resolver.Http changes where everything comes from at
once.
Tptp.Unit.from_name("Problems/PUZ/PUZ001+1.p", resolver: Tptp.Resolver.Fs)@spec from_string(binary(), [option()]) :: {:ok, t(), [Tptp.Diagnostic.t()]}
Read a file and everything it includes.
iex> resolver = {Tptp.Resolver.Map, files: %{"a.ax" => "fof(a, axiom, p)."}}
iex> {:ok, unit, []} = Tptp.Unit.from_string("include('a.ax'). fof(b, conjecture, p).", resolver: resolver)
iex> unit |> Tptp.Unit.statements() |> Enum.map(fn {_id, statement} -> statement.name.text end)
["a", "b"]@spec statements(t()) :: [{Tptp.Span.file_id(), Tptp.Statement.t()}]
Every statement, with include directives expanded where they stand.
Each element is {file_id, statement}, because the statement itself carries only
offsets — the file it belongs to is what turns those into a position. The
directives themselves are not in the result; they have been replaced by what they
name. An unresolved directive contributes nothing, and said so at read time.
@spec text(t(), Tptp.Span.t()) :: binary() | nil
The bytes a span names, wherever in the unit it points.