Contains utility to parse files from the TPTP problem library (https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.
For reference, the TH0 language is defined in https://doi.org/10.1007/s10817-017-9407-7.
Summary
Functions
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Raises on errors.
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Raises on errors.
Functions
@spec parse_tptp_file(String.t(), :tptp_problem | :tptp_relative | :custom) :: {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
This function serves two purposes: parsing a file from the TPTP problem library (https://tptp.org/TPTP/) or a custom problem file given by the user.
origin indicates whether it is a file from the TPTP problem library and can
be accessed via the environment variable TPTP_ROOT pointing to the root
directory of the TPTP library.
@spec parse_tptp_file!(String.t(), :tptp_problem | :tptp_relative | :custom) :: ShotDs.Data.Problem.t()
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Raises on errors.
This function serves two purposes: parsing a file from the TPTP problem library (https://tptp.org/TPTP/) or a custom problem file given by the user.
origin indicates whether it is a file from the TPTP problem library and can
be accessed via the environment variable TPTP_ROOT pointing to the root
directory of the TPTP library.
@spec parse_tptp_string(String.t(), String.t()) :: {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Info
The parsing of content only supports including files from the TPTP problem
library. If such includes are present, make sure that the TPTP_ROOT
environment variable is set.
@spec parse_tptp_string!(String.t(), String.t()) :: ShotDs.Data.Problem.t()
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Raises on errors.
Info
The parsing of content only supports including files from the TPTP problem
library. If such includes are present, make sure that the TPTP_ROOT
environment variable is set.