Zee3.Smt2.Parser
(zee3 v0.3.0)
Copy Markdown
A NimbleParsec implementation for parsing SMT-LIB2 S-Expressions.
This is exposed as a public module, although most users will not want to parse any S-expressions directly. This module is used internally to parse the values returned by the solver.
Summary
Functions
Parses exactly one S-Expression from the given binary.
Parses multiple S-Expressions from the given binary, skipping any whitespace.
Parses the given binary as parse_multiple.
Parses the given binary as parse_single.
Functions
Parses exactly one S-Expression from the given binary.
Parses multiple S-Expressions from the given binary, skipping any whitespace.
@spec parse_multiple(binary(), keyword()) :: {:ok, [term()], rest, context, line, byte_offset} | {:error, reason, rest, context, line, byte_offset} when line: {pos_integer(), byte_offset}, byte_offset: non_neg_integer(), rest: binary(), reason: String.t(), context: map()
Parses the given binary as parse_multiple.
Returns {:ok, [token], rest, context, position, byte_offset} or
{:error, reason, rest, context, line, byte_offset} where position
describes the location of the parse_multiple (start position) as {line, offset_to_start_of_line}.
To column where the error occurred can be inferred from byte_offset - offset_to_start_of_line.
Options
:byte_offset- the byte offset for the whole binary, defaults to 0:line- the line and the byte offset into that line, defaults to{1, byte_offset}:context- the initial context value. It will be converted to a map
@spec parse_single(binary(), keyword()) :: {:ok, [term()], rest, context, line, byte_offset} | {:error, reason, rest, context, line, byte_offset} when line: {pos_integer(), byte_offset}, byte_offset: non_neg_integer(), rest: binary(), reason: String.t(), context: map()
Parses the given binary as parse_single.
Returns {:ok, [token], rest, context, position, byte_offset} or
{:error, reason, rest, context, line, byte_offset} where position
describes the location of the parse_single (start position) as {line, offset_to_start_of_line}.
To column where the error occurred can be inferred from byte_offset - offset_to_start_of_line.
Options
:byte_offset- the byte offset for the whole binary, defaults to 0:line- the line and the byte offset into that line, defaults to{1, byte_offset}:context- the initial context value. It will be converted to a map