#include <smt2_parser.h>

Inheritance diagram for smt2_parsert:

Collaboration diagram for smt2_parsert:

Classes
struct	idt

struct	named_termt

struct	signature_with_parameter_idst

Public Types
using	id_mapt = std::map< irep_idt, idt >

using	named_termst = std::map< irep_idt, named_termt >

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

void	parse ()

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

smt2_tokenizert::smt2_errort	error () const

void	skip_to_end_of_list ()
	This skips tokens until all bracketed expressions are closed. More...

Public Attributes
id_mapt	id_map

named_termst	named_terms

bool	exit

Protected Member Functions
smt2_tokenizert::tokent	next_token ()

void	add_unique_id (irep_idt, exprt)

void	setup_expressions ()

exprt	expression ()

exprt	function_application ()

exprt	function_application_ieee_float_op (const irep_idt &, const exprt::operandst &)

exprt	function_application_ieee_float_eq (const exprt::operandst &)

exprt	function_application_fp (const exprt::operandst &)

exprt::operandst	operands ()

typet	function_signature_declaration ()

signature_with_parameter_idst	function_signature_definition ()

void	check_matching_operand_types (const exprt::operandst &) const

exprt	multi_ary (irep_idt, const exprt::operandst &)

exprt	binary_predicate (irep_idt, const exprt::operandst &)

exprt	binary (irep_idt, const exprt::operandst &)

exprt	unary (irep_idt, const exprt::operandst &)

exprt	bv_division (const exprt::operandst &, bool is_signed)

exprt	bv_mod (const exprt::operandst &, bool is_signed)

std::pair< binding_exprt::variablest, exprt >	binding (irep_idt)

exprt	lambda_expression ()

exprt	let_expression ()

exprt	quantifier_expression (irep_idt)

exprt	function_application (const symbol_exprt &function, const exprt::operandst &op)

exprt::operandst	cast_bv_to_signed (const exprt::operandst &)
	Apply typecast to signedbv to expressions in vector. More...

exprt	cast_bv_to_unsigned (const exprt &)
	Apply typecast to unsignedbv to given expression. More...

typet	sort ()

typet	function_sort ()

void	setup_sorts ()

void	command_sequence ()

void	command (const std::string &)

void	ignore_command ()

void	setup_commands ()

Protected Attributes
smt2_tokenizert	smt2_tokenizer

std::size_t	parenthesis_level

std::unordered_map< std::string, std::function< exprt()> >	expressions

std::unordered_map< std::string, std::function< typet()> >	sorts

std::unordered_map< std::string, std::function< void()> >	commands

Detailed Description

Definition at line 20 of file smt2_parser.h.

Member Typedef Documentation

◆ id_mapt

using smt2_parsert::id_mapt = std::map<irep_idt, idt>

Definition at line 57 of file smt2_parser.h.

◆ named_termst

using smt2_parsert::named_termst = std::map<irep_idt, named_termt>

Definition at line 73 of file smt2_parser.h.

Constructor & Destructor Documentation

◆ smt2_parsert()

smt2_parsert::smt2_parsert ( std::istream & _in )

inlineexplicit

Definition at line 23 of file smt2_parser.h.

Member Function Documentation

◆ add_unique_id()

void smt2_parsert::add_unique_id	(	irep_idt	id,
		exprt	expr
	)

protected

Definition at line 134 of file smt2_parser.cpp.

◆ binary()

exprt smt2_parsert::binary	(	irep_idt	id,
		const exprt::operandst &	op
	)

protected

Definition at line 393 of file smt2_parser.cpp.

◆ binary_predicate()

exprt smt2_parsert::binary_predicate	(	irep_idt	id,
		const exprt::operandst &	op
	)

protected

Definition at line 375 of file smt2_parser.cpp.

◆ binding()

std::pair< binding_exprt::variablest, exprt > smt2_parsert::binding ( irep_idt id )

protected

Definition at line 218 of file smt2_parser.cpp.

◆ bv_division()

exprt smt2_parsert::bv_division	(	const exprt::operandst &	operands,
		bool	is_signed
	)

protected

Definition at line 953 of file smt2_parser.cpp.

◆ bv_mod()

exprt smt2_parsert::bv_mod	(	const exprt::operandst &	operands,
		bool	is_signed
	)

protected

Definition at line 982 of file smt2_parser.cpp.

◆ cast_bv_to_signed()

exprt::operandst smt2_parsert::cast_bv_to_signed ( const exprt::operandst & op )

protected

Apply typecast to signedbv to expressions in vector.

Definition at line 313 of file smt2_parser.cpp.

◆ cast_bv_to_unsigned()

exprt smt2_parsert::cast_bv_to_unsigned ( const exprt & expr )

protected

Apply typecast to unsignedbv to given expression.

Definition at line 336 of file smt2_parser.cpp.

◆ check_matching_operand_types()

void smt2_parsert::check_matching_operand_types ( const exprt::operandst & op ) const

protected

Definition at line 348 of file smt2_parser.cpp.

◆ command()

void smt2_parsert::command ( const std::string & c )

protected

Definition at line 1608 of file smt2_parser.cpp.

◆ command_sequence()

void smt2_parsert::command_sequence ( )

protected

Definition at line 44 of file smt2_parser.cpp.

◆ error() [1/2]

smt2_tokenizert::smt2_errort smt2_parsert::error ( ) const

inline

Definition at line 83 of file smt2_parser.h.

◆ error() [2/2]

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

inline

Definition at line 78 of file smt2_parser.h.

◆ expression()

exprt smt2_parsert::expression ( )

protected

Definition at line 1011 of file smt2_parser.cpp.

◆ function_application() [1/2]

exprt smt2_parsert::function_application ( )

protected

Definition at line 488 of file smt2_parser.cpp.

◆ function_application() [2/2]

exprt smt2_parsert::function_application	(	const symbol_exprt &	function,
		const exprt::operandst &	op
	)

protected

Definition at line 294 of file smt2_parser.cpp.

◆ function_application_fp()

exprt smt2_parsert::function_application_fp ( const exprt::operandst & op )

protected

Definition at line 451 of file smt2_parser.cpp.

◆ function_application_ieee_float_eq()

exprt smt2_parsert::function_application_ieee_float_eq ( const exprt::operandst & op )

protected

Definition at line 403 of file smt2_parser.cpp.

◆ function_application_ieee_float_op()

exprt smt2_parsert::function_application_ieee_float_op	(	const irep_idt &	id,
		const exprt::operandst &	op
	)

protected

Definition at line 422 of file smt2_parser.cpp.

◆ function_signature_declaration()

typet smt2_parsert::function_signature_declaration ( )

protected

Definition at line 1585 of file smt2_parser.cpp.

◆ function_signature_definition()

smt2_parsert::signature_with_parameter_idst smt2_parsert::function_signature_definition ( )

protected

Definition at line 1546 of file smt2_parser.cpp.

◆ function_sort()

typet smt2_parsert::function_sort ( )

protected

Definition at line 1404 of file smt2_parser.cpp.

◆ ignore_command()

void smt2_parsert::ignore_command ( )

protected

Definition at line 89 of file smt2_parser.cpp.

◆ lambda_expression()

exprt smt2_parsert::lambda_expression ( )

protected

Definition at line 278 of file smt2_parser.cpp.

◆ let_expression()

exprt smt2_parsert::let_expression ( )

protected

Definition at line 148 of file smt2_parser.cpp.

◆ multi_ary()

exprt smt2_parsert::multi_ary	(	irep_idt	id,
		const exprt::operandst &	op
	)

protected

Definition at line 363 of file smt2_parser.cpp.

◆ next_token()

smt2_tokenizert::tokent smt2_parsert::next_token ( )

protected

Definition at line 25 of file smt2_parser.cpp.

◆ operands()

exprt::operandst smt2_parsert::operands ( )

protected

Definition at line 122 of file smt2_parser.cpp.

◆ parse()

void smt2_parsert::parse ( )

inline

Definition at line 31 of file smt2_parser.h.

◆ quantifier_expression()

exprt smt2_parsert::quantifier_expression ( irep_idt id )

protected

Definition at line 284 of file smt2_parser.cpp.

◆ setup_commands()

void smt2_parsert::setup_commands ( )

protected

Definition at line 1620 of file smt2_parser.cpp.

◆ setup_expressions()

void smt2_parsert::setup_expressions ( )

protected

Definition at line 1081 of file smt2_parser.cpp.

◆ setup_sorts()

void smt2_parsert::setup_sorts ( )

protected

Definition at line 1475 of file smt2_parser.cpp.

◆ skip_to_end_of_list()

void smt2_parsert::skip_to_end_of_list ( )

This skips tokens until all bracketed expressions are closed.

Definition at line 37 of file smt2_parser.cpp.

◆ sort()

typet smt2_parsert::sort ( )

protected

Definition at line 1430 of file smt2_parser.cpp.

◆ unary()

exprt smt2_parsert::unary	(	irep_idt	id,
		const exprt::operandst &	op
	)

protected

Definition at line 385 of file smt2_parser.cpp.

Member Data Documentation

◆ commands

std::unordered_map<std::string, std::function<void()> > smt2_parsert::commands

protected

Definition at line 190 of file smt2_parser.h.

◆ exit

bool smt2_parsert::exit

Definition at line 76 of file smt2_parser.h.

◆ expressions

std::unordered_map<std::string, std::function<exprt()> > smt2_parsert::expressions

protected

Definition at line 149 of file smt2_parser.h.

◆ id_map

id_mapt smt2_parsert::id_map

Definition at line 58 of file smt2_parser.h.

◆ named_terms

named_termst smt2_parsert::named_terms

Definition at line 74 of file smt2_parser.h.

◆ parenthesis_level

std::size_t smt2_parsert::parenthesis_level

protected

Definition at line 94 of file smt2_parser.h.

◆ smt2_tokenizer

smt2_tokenizert smt2_parsert::smt2_tokenizer

protected

Definition at line 92 of file smt2_parser.h.

◆ sorts

std::unordered_map<std::string, std::function<typet()> > smt2_parsert::sorts

protected

Definition at line 186 of file smt2_parser.h.

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

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

Classes

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ id_mapt

◆ named_termst

Constructor & Destructor Documentation

◆ smt2_parsert()

Member Function Documentation

◆ add_unique_id()

◆ binary()

◆ binary_predicate()

◆ binding()

◆ bv_division()

◆ bv_mod()

◆ cast_bv_to_signed()

◆ cast_bv_to_unsigned()

◆ check_matching_operand_types()

◆ command()

◆ command_sequence()

◆ error() [1/2]

◆ error() [2/2]

◆ expression()

◆ function_application() [1/2]

◆ function_application() [2/2]

◆ function_application_fp()

◆ function_application_ieee_float_eq()

◆ function_application_ieee_float_op()

◆ function_signature_declaration()

◆ function_signature_definition()

◆ function_sort()

◆ ignore_command()

◆ lambda_expression()

◆ let_expression()

◆ multi_ary()

◆ next_token()

◆ operands()

◆ parse()

◆ quantifier_expression()

◆ setup_commands()

◆ setup_expressions()

◆ setup_sorts()

◆ skip_to_end_of_list()

◆ sort()

◆ unary()

Member Data Documentation

◆ commands

◆ exit

◆ expressions

◆ id_map

◆ named_terms

◆ parenthesis_level

◆ smt2_tokenizer

◆ sorts