#include <smt2_tokenizer.h>

Inheritance diagram for smt2_tokenizert:

Collaboration diagram for smt2_tokenizert:

Classes
class	smt2_errort
	Exception thrown by the tokenizer (and the parser built on top of it) to report a syntactic error at a known source line. More...

class	tokent
	One SMT-LIB v2.6 token. More...

Public Types
using	token_kindt = enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE }

Public Member Functions
	smt2_tokenizert (std::istream &_in)

tokent	next_token ()
	Consume and return the next token.

const tokent &	peek ()
	Return the next token without consuming it.

smt2_errort	error (const std::string &message) const
	generate an error exception, pre-filled with a message

smt2_errort	error () const
	generate an error exception

Protected Member Functions
void	skip_to_end_of_list ()
	skip any tokens until all parentheses are closed or the end of file is reached

Protected Attributes
std::istream *	in

Private Member Functions
unsigned	current_line_no () const
	Line number to attribute a diagnostic to: the line of the peeked token if there is one, otherwise the current input line.

tokent	get_decimal_numeral ()
	Read a NUMERAL of the form "[0-9.]+" from the stream.

tokent	get_hex_numeral ()
	Read a NUMERAL of the form "#x[0-9a-fA-F]+" from the stream.

tokent	get_bin_numeral ()
	Read a NUMERAL of the form "#b[01]+" from the stream.

tokent	get_simple_symbol ()
	Read a SYMBOL of the form "[A-Za-z~!@$%^&_\-+=<>.?/][...]" from the stream.

tokent	get_quoted_symbol ()
	Read a quoted SYMBOL of the form `\|...\|` from the stream.

tokent	get_string_literal ()
	Read a STRING_LITERAL of the form `"..."` from the stream, applying SMT-LIB v2.6 quote-doubling: a `""` inside the literal is interpreted as a single `"</tt>. Called after the opening <tt>"` has been consumed.

tokent	read_token ()
	Read a single token directly from the input stream.

Private Attributes
unsigned	line_no = 1
	Number of the source line currently being read.

std::optional< tokent >	peeked
	Token that has been peeked but not yet consumed.

Detailed Description

Definition at line 22 of file smt2_tokenizer.h.

Member Typedef Documentation

◆ token_kindt

using smt2_tokenizert::token_kindt = enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE }

Definition at line 75 of file smt2_tokenizer.h.

Constructor & Destructor Documentation

◆ smt2_tokenizert()

smt2_tokenizert::smt2_tokenizert ( std::istream & _in )

inlineexplicit

Definition at line 25 of file smt2_tokenizer.h.

Member Function Documentation

◆ current_line_no()

unsigned smt2_tokenizert::current_line_no ( ) const

inlineprivate

Line number to attribute a diagnostic to: the line of the peeked token if there is one, otherwise the current input line.

Definition at line 165 of file smt2_tokenizer.h.

◆ error() [1/2]

smt2_errort smt2_tokenizert::error ( ) const

inline

generate an error exception

Definition at line 142 of file smt2_tokenizer.h.

◆ error() [2/2]

smt2_errort smt2_tokenizert::error ( const std::string & message ) const

inline

generate an error exception, pre-filled with a message

Definition at line 136 of file smt2_tokenizer.h.

◆ get_bin_numeral()

smt2_tokenizert::tokent smt2_tokenizert::get_bin_numeral ( )

private

Read a NUMERAL of the form "#b[01]+" from the stream.

Called after the leading #b has been consumed.

Definition at line 86 of file smt2_tokenizer.cpp.

◆ get_decimal_numeral()

smt2_tokenizert::tokent smt2_tokenizert::get_decimal_numeral ( )

private

Read a NUMERAL of the form "[0-9.]+" from the stream.

Called after the leading digit has been seen and unget'd back onto the stream.

Definition at line 58 of file smt2_tokenizer.cpp.

◆ get_hex_numeral()

smt2_tokenizert::tokent smt2_tokenizert::get_hex_numeral ( )

private

Read a NUMERAL of the form "#x[0-9a-fA-F]+" from the stream.

Called after the leading #x has been consumed.

Definition at line 113 of file smt2_tokenizer.cpp.

◆ get_quoted_symbol()

smt2_tokenizert::tokent smt2_tokenizert::get_quoted_symbol ( )

private

Read a quoted SYMBOL of the form |...| from the stream.

Called after the opening | has been consumed. Throws smt2_errort if EOF is reached before the closing |. Newlines inside |...| are legal and increment line_no.

Definition at line 140 of file smt2_tokenizer.cpp.

◆ get_simple_symbol()

smt2_tokenizert::tokent smt2_tokenizert::get_simple_symbol ( )

private

Read a SYMBOL of the form "[A-Za-z~!@$%^&*_\-+=<>.?/][...]*" from the stream.

Called after the leading character has been seen and unget'd back onto the stream. Returns an END_OF_FILE token if the stream is at end-of-file with an empty buffer.

Definition at line 28 of file smt2_tokenizer.cpp.

◆ get_string_literal()

smt2_tokenizert::tokent smt2_tokenizert::get_string_literal ( )

private

Read a STRING_LITERAL of the form "..." from the stream, applying SMT-LIB v2.6 quote-doubling: a "" inside the literal is interpreted as a single "</tt>. Called after the opening <tt>" has been consumed.

Throws smt2_errort if EOF is reached before the closing ".

Definition at line 169 of file smt2_tokenizer.cpp.

◆ next_token()

smt2_tokenizert::tokent smt2_tokenizert::next_token ( )

Consume and return the next token.

If a token has been peeked (see peek) it is returned; otherwise the next token is read from the input stream.

Definition at line 204 of file smt2_tokenizer.cpp.

◆ peek()

const tokent & smt2_tokenizert::peek ( )

inline

Return the next token without consuming it.

A subsequent call to next_token will return the same token. Repeated calls to peek return the same token without re-reading from the stream.

Definition at line 128 of file smt2_tokenizer.h.

◆ read_token()

smt2_tokenizert::tokent smt2_tokenizert::read_token ( )

private

Read a single token directly from the input stream.

Does not consult or update peeked – callers handle that.

Definition at line 215 of file smt2_tokenizer.cpp.

◆ skip_to_end_of_list()

void smt2_tokenizert::skip_to_end_of_list ( )

protected

skip any tokens until all parentheses are closed or the end of file is reached

Member Data Documentation

◆ in

std::istream* smt2_tokenizert::in

protected

Definition at line 148 of file smt2_tokenizer.h.

◆ line_no

unsigned smt2_tokenizert::line_no = 1

private

Number of the source line currently being read.

Is incremented as \n characters are consumed from the input stream and then stamped onto each tokent emitted by the helpers below.

Definition at line 158 of file smt2_tokenizer.h.

◆ peeked

std::optional<tokent> smt2_tokenizert::peeked

private

Token that has been peeked but not yet consumed.

Definition at line 161 of file smt2_tokenizer.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/solvers/smt2/smt2_tokenizer.h
/home/runner/work/cbmc/cbmc/src/solvers/smt2/smt2_tokenizer.cpp

Classes

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ token_kindt

Constructor & Destructor Documentation

◆ smt2_tokenizert()

Member Function Documentation

◆ current_line_no()

◆ error() [1/2]

◆ error() [2/2]

◆ get_bin_numeral()

◆ get_decimal_numeral()

◆ get_hex_numeral()

◆ get_quoted_symbol()

◆ get_simple_symbol()

◆ get_string_literal()

◆ next_token()

◆ peek()

◆ read_token()

◆ skip_to_end_of_list()

Member Data Documentation

◆ in

◆ line_no

◆ peeked