#include <smt2_conv.h>

Inheritance diagram for smt2_convt:

Collaboration diagram for smt2_convt:

Classes
struct	identifiert

class	smt2_symbolt

Public Types
enum	solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 }

Public Types inherited from decision_proceduret
enum	resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
	Result of running the decision procedure. More...

Public Member Functions
	smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)

	~smt2_convt () override=default

exprt	handle (const exprt &expr) override
	Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More...

void	set_to (const exprt &expr, bool value) override
	For a Boolean expression `expr`, add the constraint 'expr' if `value` is `true`, otherwise add 'not expr'. More...

exprt	get (const exprt &expr) const override
	Return `expr` with variables replaced by values from satisfying assignment if available. More...

std::string	decision_procedure_text () const override
	Return a textual description of the decision procedure. More...

void	print_assignment (std::ostream &out) const override
	Print satisfying assignment to `out`. More...

void	push () override
	Unimplemented. More...

void	push (const std::vector< exprt > &_assumptions) override
	Currently, only implements a single stack element (no nested contexts) More...

void	pop () override
	Currently, only implements a single stack element (no nested contexts) More...

std::size_t	get_number_of_solver_calls () const override
	Return the number of incremental solver calls. More...

Public Member Functions inherited from stack_decision_proceduret
virtual	~stack_decision_proceduret ()=default

Public Member Functions inherited from decision_proceduret
void	set_to_true (const exprt &expr)
	For a Boolean expression `expr`, add the constraint 'expr'. More...

void	set_to_false (const exprt &expr)
	For a Boolean expression `expr`, add the constraint 'not expr'. More...

resultt	operator() ()
	Run the decision procedure to solve the problem. More...

virtual	~decision_proceduret ()

Static Public Member Functions
static std::string	convert_identifier (const irep_idt &identifier)

Public Attributes
bool	use_FPA_theory

bool	use_array_of_bool

bool	use_as_const

bool	use_check_sat_assuming

bool	use_datatypes

bool	use_lambda_for_array

bool	emit_set_logic

Protected Types
enum	wheret { wheret::BEGIN, wheret::END }

typedef std::unordered_map< irep_idt, identifiert >	identifier_mapt

typedef std::map< typet, std::string >	datatype_mapt

typedef std::map< exprt, irep_idt >	defined_expressionst

typedef std::set< std::string >	smt2_identifierst

Protected Member Functions
resultt	dec_solve () override
	Run the decision procedure to solve the problem. More...

void	write_header ()

void	write_footer ()
	Writes the end of the SMT file to the `smt_convt::out` stream. More...

bool	use_array_theory (const exprt &)

void	flatten_array (const exprt &)
	produce a flat bit-vector for a given array of fixed size More...

void	convert_typecast (const typecast_exprt &expr)

void	convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

void	convert_struct (const struct_exprt &expr)

void	convert_union (const union_exprt &expr)

void	convert_constant (const constant_exprt &expr)

void	convert_relation (const binary_relation_exprt &)

void	convert_is_dynamic_object (const unary_exprt &)

void	convert_plus (const plus_exprt &expr)

void	convert_minus (const minus_exprt &expr)

void	convert_div (const div_exprt &expr)

void	convert_mult (const mult_exprt &expr)

void	convert_rounding_mode_FPA (const exprt &expr)
	Converting a constant or symbolic rounding mode to SMT-LIB. More...

void	convert_floatbv_plus (const ieee_float_op_exprt &expr)

void	convert_floatbv_minus (const ieee_float_op_exprt &expr)

void	convert_floatbv_div (const ieee_float_op_exprt &expr)

void	convert_floatbv_mult (const ieee_float_op_exprt &expr)

void	convert_floatbv_rem (const binary_exprt &expr)

void	convert_mod (const mod_exprt &expr)

void	convert_euclidean_mod (const euclidean_mod_exprt &expr)

void	convert_index (const index_exprt &expr)

void	convert_member (const member_exprt &expr)

void	convert_with (const with_exprt &expr)

void	convert_update (const exprt &expr)

void	convert_expr (const exprt &)

void	convert_type (const typet &)

void	convert_literal (const literalt)

literalt	convert (const exprt &expr)

tvt	l_get (literalt l) const

exprt	prepare_for_convert_expr (const exprt &expr)
	Perform steps necessary before an expression is passed to convert_expr. More...

exprt	lower_byte_operators (const exprt &expr)
	Lower byte_update and byte_extract operations within `expr`. More...

void	find_symbols (const exprt &expr)

void	find_symbols (const typet &type)

void	find_symbols_rec (const typet &type, std::set< irep_idt > &recstack)

constant_exprt	parse_literal (const irept &, const typet &type)

struct_exprt	parse_struct (const irept &s, const struct_typet &type)

exprt	parse_union (const irept &s, const union_typet &type)

exprt	parse_array (const irept &s, const array_typet &type)
	This function is for parsing array output from SMT solvers when "(get-value \|???\|)" returns an array object. More...

exprt	parse_rec (const irept &s, const typet &type)

void	walk_array_tree (std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
	This function walks the SMT output and populates a map with index/value pairs for the array. More...

void	convert_floatbv (const exprt &expr)

std::string	type2id (const typet &) const

std::string	floatbv_suffix (const exprt &) const

const smt2_symbolt &	to_smt2_symbol (const exprt &expr)

void	flatten2bv (const exprt &)

void	unflatten (wheret, const typet &, unsigned nesting=0)

void	convert_address_of_rec (const exprt &expr, const pointer_typet &result_type)

void	define_object_size (const irep_idt &id, const object_size_exprt &expr)

Protected Attributes
const namespacet &	ns

std::ostream &	out

std::string	benchmark

std::string	notes

std::string	logic

solvert	solver

std::vector< exprt >	assumptions

boolbv_widtht	boolbv_width

std::size_t	number_of_solver_calls = 0

letifyt	letify

std::set< irep_idt >	bvfp_set

pointer_logict	pointer_logic

identifier_mapt	identifier_map

datatype_mapt	datatype_map

defined_expressionst	defined_expressions

std::unordered_map< irep_idt, bool >	set_values
	The values which boolean identifiers have been `smt2_convt::set_to` or in other words those which are asserted as true / false in the output smt2 formula. More...

std::map< object_size_exprt, irep_idt >	object_sizes

smt2_identifierst	smt2_identifiers

std::size_t	no_boolean_variables

std::vector< bool >	boolean_assignment

Detailed Description

Definition at line 36 of file smt2_conv.h.

Member Typedef Documentation

◆ datatype_mapt

typedef std::map<typet, std::string> smt2_convt::datatype_mapt

protected

Definition at line 244 of file smt2_conv.h.

◆ defined_expressionst

typedef std::map<exprt, irep_idt> smt2_convt::defined_expressionst

protected

Definition at line 253 of file smt2_conv.h.

◆ identifier_mapt

typedef std::unordered_map<irep_idt, identifiert> smt2_convt::identifier_mapt

protected

Definition at line 236 of file smt2_conv.h.

◆ smt2_identifierst

typedef std::set<std::string> smt2_convt::smt2_identifierst

protected

Definition at line 262 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

enum smt2_convt::solvert

strong

Enumerator
GENERIC
BOOLECTOR
CPROVER_SMT2
CVC3
CVC4
MATHSAT
YICES
Z3

Definition at line 39 of file smt2_conv.h.

◆ wheret

enum smt2_convt::wheret

strongprotected

Enumerator
BEGIN
END

Definition at line 211 of file smt2_conv.h.

Constructor & Destructor Documentation

◆ smt2_convt()

smt2_convt::smt2_convt	(	const namespacet &	_ns,
		const std::string &	_benchmark,
		const std::string &	_notes,
		const std::string &	_logic,
		solvert	_solver,
		std::ostream &	_out
	)

Definition at line 55 of file smt2_conv.cpp.

◆ ~smt2_convt()

smt2_convt::~smt2_convt ( )

overridedefault

Member Function Documentation

◆ convert()

literalt smt2_convt::convert ( const exprt & expr )

protected

Definition at line 804 of file smt2_conv.cpp.

◆ convert_address_of_rec()

void smt2_convt::convert_address_of_rec	(	const exprt &	expr,
		const pointer_typet &	result_type
	)

protected

Definition at line 702 of file smt2_conv.cpp.

◆ convert_constant()

void smt2_convt::convert_constant ( const constant_exprt & expr )

protected

Definition at line 3146 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt & expr )

protected

Definition at line 3831 of file smt2_conv.cpp.

◆ convert_euclidean_mod()

void smt2_convt::convert_euclidean_mod ( const euclidean_mod_exprt & expr )

protected

Definition at line 3290 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt & expr )

protected

Definition at line 1046 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt & expr )

protected

Definition at line 1012 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt & expr )

protected

Definition at line 3875 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt & expr )

protected

Definition at line 3811 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt & expr )

protected

Definition at line 3970 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt & expr )

protected

Definition at line 3661 of file smt2_conv.cpp.

◆ convert_floatbv_rem()

void smt2_convt::convert_floatbv_rem ( const binary_exprt & expr )

protected

Definition at line 3990 of file smt2_conv.cpp.

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt & expr )

protected

Definition at line 2876 of file smt2_conv.cpp.

◆ convert_identifier()

std::string smt2_convt::convert_identifier ( const irep_idt & identifier )

static

Definition at line 926 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt & expr )

protected

Definition at line 4258 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const unary_exprt & expr )

protected

Definition at line 3324 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt l )

protected

Definition at line 869 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt & expr )

protected

Definition at line 4355 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt & expr )

protected

Definition at line 3702 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt & expr )

protected

Definition at line 3305 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt & expr )

protected

Definition at line 3895 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt & expr )

protected

Definition at line 3468 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const binary_relation_exprt & expr )

protected

Definition at line 3361 of file smt2_conv.cpp.

◆ convert_rounding_mode_FPA()

void smt2_convt::convert_rounding_mode_FPA ( const exprt & expr )

protected

Converting a constant or symbolic rounding mode to SMT-LIB.

Only called when use_FPA_theory is enabled. SMT-LIB output to is sent to out.

parameters: The expression representing the rounding mode.

Definition at line 3604 of file smt2_conv.cpp.

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt & expr )

protected

Definition at line 3020 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet & type )

protected

Definition at line 5124 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt & expr )

protected

Definition at line 2343 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt & expr )

protected

Definition at line 3117 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const exprt & expr )

protected

Definition at line 4251 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt & expr )

protected

Definition at line 4013 of file smt2_conv.cpp.

◆ dec_solve()

decision_proceduret::resultt smt2_convt::dec_solve ( )

overrideprotectedvirtual

Run the decision procedure to solve the problem.

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 272 of file smt2_conv.cpp.

◆ decision_procedure_text()

std::string smt2_convt::decision_procedure_text ( ) const

overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 126 of file smt2_conv.cpp.

◆ define_object_size()

void smt2_convt::define_object_size	(	const irep_idt &	id,
		const object_size_exprt &	expr
	)

protected

Definition at line 235 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt & expr )

protected

Definition at line 4800 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet & type )

protected

Definition at line 5257 of file smt2_conv.cpp.

◆ find_symbols_rec()

void smt2_convt::find_symbols_rec	(	const typet &	type,
		std::set< irep_idt > &	recstack
	)

protected

Definition at line 5263 of file smt2_conv.cpp.

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt & expr )

protected

Definition at line 4416 of file smt2_conv.cpp.

◆ flatten_array()

void smt2_convt::flatten_array ( const exprt & expr )

protected

produce a flat bit-vector for a given array of fixed size

Definition at line 3086 of file smt2_conv.cpp.

◆ floatbv_suffix()

std::string smt2_convt::floatbv_suffix ( const exprt & expr ) const

protected

Definition at line 1005 of file smt2_conv.cpp.

◆ get()

exprt smt2_convt::get ( const exprt & expr ) const

overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Definition at line 279 of file smt2_conv.cpp.

◆ get_number_of_solver_calls()

std::size_t smt2_convt::get_number_of_solver_calls ( ) const

overridevirtual

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 5478 of file smt2_conv.cpp.

◆ handle()

exprt smt2_convt::handle ( const exprt & expr )

overridevirtual

Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 860 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt l ) const

protected

Definition at line 141 of file smt2_conv.cpp.

◆ lower_byte_operators()

exprt smt2_convt::lower_byte_operators ( const exprt & expr )

protected

Lower byte_update and byte_extract operations within expr.

Return an equivalent expression that doesn't use byte operators. Note this replaces operators post-order (compare lower_byte_operators, which uses a pre-order walk, replacing in child expressions before the parent). Pre-order replacement currently fails regression tests: see https://github.com/diffblue/cbmc/issues/4380

Definition at line 4753 of file smt2_conv.cpp.

◆ parse_array()

exprt smt2_convt::parse_array	(	const irept &	s,
		const array_typet &	type
	)

protected

This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array object.

Parameters

s	is the irept parsed from the SMT output
type	is the expected type

Returns: an exprt that represents the array

Definition at line 477 of file smt2_conv.cpp.

◆ parse_literal()

constant_exprt smt2_convt::parse_literal	(	const irept &	src,
		const typet &	type
	)

protected

Definition at line 339 of file smt2_conv.cpp.

◆ parse_rec()

exprt smt2_convt::parse_rec	(	const irept &	s,
		const typet &	type
	)

protected

Definition at line 636 of file smt2_conv.cpp.

◆ parse_struct()

struct_exprt smt2_convt::parse_struct	(	const irept &	s,
		const struct_typet &	type
	)

protected

Definition at line 577 of file smt2_conv.cpp.

◆ parse_union()

exprt smt2_convt::parse_union	(	const irept &	s,
		const union_typet &	type
	)

protected

Definition at line 561 of file smt2_conv.cpp.

◆ pop()

void smt2_convt::pop ( )

overridevirtual

Currently, only implements a single stack element (no nested contexts)

Implements stack_decision_proceduret.

Definition at line 904 of file smt2_conv.cpp.

◆ prepare_for_convert_expr()

exprt smt2_convt::prepare_for_convert_expr ( const exprt & expr )

protected

Perform steps necessary before an expression is passed to convert_expr.

Replace byte operators (byte_extract, _update) with equivalent expressions
Call find_symbols to create auxiliary symbols, e.g. for array expressions.
Parameters

expr expression to prepare

Returns
equivalent expression suitable for convert_expr.

Definition at line 4785 of file smt2_conv.cpp.

◆ print_assignment()

void smt2_convt::print_assignment ( std::ostream & out ) const

overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 131 of file smt2_conv.cpp.

◆ push() [1/2]

void smt2_convt::push ( )

overridevirtual

Unimplemented.

Implements stack_decision_proceduret.

Definition at line 892 of file smt2_conv.cpp.

◆ push() [2/2]

void smt2_convt::push ( const std::vector< exprt > & _assumptions )

overridevirtual

Currently, only implements a single stack element (no nested contexts)

Implements stack_decision_proceduret.

Definition at line 897 of file smt2_conv.cpp.

◆ set_to()

void smt2_convt::set_to	(	const exprt &	expr,
		bool	value
	)

overridevirtual

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

Implements decision_proceduret.

Definition at line 4609 of file smt2_conv.cpp.

◆ to_smt2_symbol()

const smt2_symbolt& smt2_convt::to_smt2_symbol ( const exprt & expr )

inlineprotected

Definition at line 201 of file smt2_conv.h.

◆ type2id()

std::string smt2_convt::type2id ( const typet & type ) const

protected

Definition at line 961 of file smt2_conv.cpp.

◆ unflatten()

void smt2_convt::unflatten	(	wheret	where,
		const typet &	type,
		unsigned	nesting = `0`
	)

protected

Definition at line 4505 of file smt2_conv.cpp.

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt & expr )

protected

Definition at line 5103 of file smt2_conv.cpp.

◆ walk_array_tree()

void smt2_convt::walk_array_tree	(	std::unordered_map< int64_t, exprt > *	operands_map,
		const irept &	src,
		const array_typet &	type
	)

protected

This function walks the SMT output and populates a map with index/value pairs for the array.

Parameters

operands_map	is a map of the operands to the array being constructed indexed by their index.
src	is the irept source for the SMT output
type	is the type of the array

Definition at line 521 of file smt2_conv.cpp.

◆ write_footer()

void smt2_convt::write_footer ( )

protected

Writes the end of the SMT file to the smt_convt::out stream.

These parts of the output may be changed when using multiple rounds of solving. They include the following parts of the output file -

The object size definitions.
The assertions based on the assumptions member variable.
The (check-sat) or check-sat-assuming command.
A (get-value |identifier|) command for each of the identifiers in smt2_convt::smt2_identifiers.
An (exit) command.

Definition at line 184 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )

protected

Definition at line 154 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

std::vector<exprt> smt2_convt::assumptions

protected

Definition at line 94 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark

protected

Definition at line 91 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width

protected

Definition at line 95 of file smt2_conv.h.

◆ boolean_assignment

std::vector<bool> smt2_convt::boolean_assignment

protected

Definition at line 267 of file smt2_conv.h.

◆ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set

protected

Definition at line 186 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map

protected

Definition at line 245 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions

protected

Definition at line 254 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 67 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map

protected

Definition at line 238 of file smt2_conv.h.

◆ letify

letifyt smt2_convt::letify

protected

Definition at line 158 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic

protected

Definition at line 91 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables

protected

Definition at line 266 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes

protected

Definition at line 91 of file smt2_conv.h.

◆ ns

const namespacet& smt2_convt::ns

protected

Definition at line 89 of file smt2_conv.h.

◆ number_of_solver_calls

std::size_t smt2_convt::number_of_solver_calls = 0

protected

Definition at line 97 of file smt2_conv.h.

◆ object_sizes

std::map<object_size_exprt, irep_idt> smt2_convt::object_sizes

protected

Definition at line 260 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out

protected

Definition at line 90 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic

protected

Definition at line 216 of file smt2_conv.h.

◆ set_values

std::unordered_map<irep_idt, bool> smt2_convt::set_values

protected

The values which boolean identifiers have been smt2_convt::set_to or in other words those which are asserted as true / false in the output smt2 formula.

Definition at line 258 of file smt2_conv.h.

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers

protected

Definition at line 263 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver

protected

Definition at line 92 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 62 of file smt2_conv.h.

◆ use_as_const

bool smt2_convt::use_as_const

Definition at line 63 of file smt2_conv.h.

◆ use_check_sat_assuming

bool smt2_convt::use_check_sat_assuming

Definition at line 64 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 65 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 61 of file smt2_conv.h.

◆ use_lambda_for_array

bool smt2_convt::use_lambda_for_array

Definition at line 66 of file smt2_conv.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2/smt2_conv.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2/smt2_conv.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ datatype_mapt

◆ defined_expressionst

◆ identifier_mapt

◆ smt2_identifierst

Member Enumeration Documentation

◆ solvert

◆ wheret

Constructor & Destructor Documentation

◆ smt2_convt()

◆ ~smt2_convt()

Member Function Documentation

◆ convert()

◆ convert_address_of_rec()

◆ convert_constant()

◆ convert_div()

◆ convert_euclidean_mod()

◆ convert_expr()

◆ convert_floatbv()

◆ convert_floatbv_div()

◆ convert_floatbv_minus()

◆ convert_floatbv_mult()

◆ convert_floatbv_plus()

◆ convert_floatbv_rem()

◆ convert_floatbv_typecast()

◆ convert_identifier()

◆ convert_index()

◆ convert_is_dynamic_object()

◆ convert_literal()

◆ convert_member()

◆ convert_minus()

◆ convert_mod()

◆ convert_mult()

◆ convert_plus()

◆ convert_relation()

◆ convert_rounding_mode_FPA()

◆ convert_struct()

◆ convert_type()

◆ convert_typecast()

◆ convert_union()

◆ convert_update()

◆ convert_with()

◆ dec_solve()

◆ decision_procedure_text()

◆ define_object_size()

◆ find_symbols() [1/2]

◆ find_symbols() [2/2]

◆ find_symbols_rec()

◆ flatten2bv()

◆ flatten_array()

◆ floatbv_suffix()

◆ get()

◆ get_number_of_solver_calls()

◆ handle()

◆ l_get()

◆ lower_byte_operators()

◆ parse_array()

◆ parse_literal()

◆ parse_rec()

◆ parse_struct()

◆ parse_union()

◆ pop()

◆ prepare_for_convert_expr()

◆ print_assignment()

◆ push() [1/2]

◆ push() [2/2]

◆ set_to()

◆ to_smt2_symbol()

◆ type2id()

◆ unflatten()

◆ use_array_theory()