#include <smt2_conv.h>

Inheritance diagram for smt2_convt:

Collaboration diagram for smt2_convt:

Classes
struct	identifiert

class	smt2_symbolt

Public Types
enum class	solvert { GENERIC , BITWUZLA , BOOLECTOR , CPROVER_SMT2 , CVC3 , CVC4 , CVC5 , MATHSAT , YICES , Z3 }

Public Types inherited from decision_proceduret
enum class	resultt { D_SATISFIABLE , D_UNSATISFIABLE , 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.

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'.

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

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

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

void	push () override
	Unimplemented.

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

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

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

void	set_converter (irep_idt id, std::function< void(const exprt &)> converter)

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 &)
	For a Boolean expression `expr`, add the constraint 'expr'.

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

resultt	operator() ()
	Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt	operator() (const exprt &assumption)
	Run the decision procedure to solve the problem under the given assumption.

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 class	wheret { BEGIN , END }

using	converterst = std::unordered_map< irep_idt, std::function< void(const exprt &)>, irep_id_hash >

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 (const exprt &) override
	Implementation of the decision procedure.

void	write_header ()

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

bool	use_array_theory (const exprt &)

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

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.

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_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)

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 update_exprt &)

void	convert_update_bit (const update_bit_exprt &)

void	convert_update_bits (const update_bits_exprt &)

void	convert_expr (const exprt &)

void	convert_type (const typet &)

void	convert_literal (const literalt)

void	convert_string_literal (const std::string &)

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.

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

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.

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.

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

converterst	converters

std::vector< literalt >	assumptions

boolbv_widtht	boolbv_width

std::size_t	number_of_solver_calls = 0

letifyt	letify

std::unordered_map< irep_idt, irept >	current_bindings

std::set< irep_idt >	bvfp_set

std::set< irep_idt >	state_fkt_declared

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.

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 40 of file smt2_conv.h.

Member Typedef Documentation

◆ converterst

using smt2_convt::converterst = std:: unordered_map<irep_idt, std::function<void(const exprt &)>, irep_id_hash>

protected

Definition at line 104 of file smt2_conv.h.

◆ datatype_mapt

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

protected

Definition at line 271 of file smt2_conv.h.

◆ defined_expressionst

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

protected

Definition at line 280 of file smt2_conv.h.

◆ identifier_mapt

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

protected

Definition at line 263 of file smt2_conv.h.

◆ smt2_identifierst

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

protected

Definition at line 289 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

enum class smt2_convt::solvert

strong

Enumerator
GENERIC
BITWUZLA
BOOLECTOR
CPROVER_SMT2
CVC3
CVC4
CVC5
MATHSAT
YICES
Z3

Definition at line 43 of file smt2_conv.h.

◆ wheret

enum class smt2_convt::wheret

strongprotected

Enumerator
BEGIN
END

Definition at line 235 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 56 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 901 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 788 of file smt2_conv.cpp.

◆ convert_constant()

void smt2_convt::convert_constant ( const constant_exprt & expr )

protected

Definition at line 3444 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt & expr )

protected

Definition at line 4127 of file smt2_conv.cpp.

◆ convert_euclidean_mod()

void smt2_convt::convert_euclidean_mod ( const euclidean_mod_exprt & expr )

protected

Definition at line 3603 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt & expr )

protected

Definition at line 1170 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt & expr )

protected

Definition at line 1123 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt & expr )

protected

Definition at line 4171 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt & expr )

protected

Definition at line 4107 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt & expr )

protected

Definition at line 4266 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt & expr )

protected

Definition at line 3977 of file smt2_conv.cpp.

◆ convert_floatbv_rem()

void smt2_convt::convert_floatbv_rem ( const binary_exprt & expr )

protected

Definition at line 4286 of file smt2_conv.cpp.

◆ convert_floatbv_round_to_integral()

void smt2_convt::convert_floatbv_round_to_integral ( const floatbv_round_to_integral_exprt & expr )

protected

Definition at line 3293 of file smt2_conv.cpp.

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt & expr )

protected

Definition at line 3149 of file smt2_conv.cpp.

◆ convert_identifier()

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

static

Definition at line 1025 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt & expr )

protected

Definition at line 4534 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const unary_exprt & expr )

protected

Definition at line 3637 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt l )

protected

Definition at line 966 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt & expr )

protected

Definition at line 4604 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt & expr )

protected

Definition at line 4012 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt & expr )

protected

Definition at line 3618 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt & expr )

protected

Definition at line 4191 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt & expr )

protected

Definition at line 3783 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const binary_relation_exprt & expr )

protected

Definition at line 3674 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 3914 of file smt2_conv.cpp.

◆ convert_string_literal()

void smt2_convt::convert_string_literal ( const std::string & s )

protected

Definition at line 1157 of file smt2_conv.cpp.

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt & expr )

protected

Definition at line 3310 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet & type )

protected

Definition at line 5688 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt & expr )

protected

Definition at line 2607 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt & expr )

protected

Definition at line 3416 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const update_exprt & expr )

protected

Definition at line 4517 of file smt2_conv.cpp.

◆ convert_update_bit()

void smt2_convt::convert_update_bit ( const update_bit_exprt & expr )

protected

Definition at line 4524 of file smt2_conv.cpp.

◆ convert_update_bits()

void smt2_convt::convert_update_bits ( const update_bits_exprt & expr )

protected

Definition at line 4529 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt & expr )

protected

Definition at line 4309 of file smt2_conv.cpp.

◆ dec_solve()

decision_proceduret::resultt smt2_convt::dec_solve ( const exprt & assumption )

overrideprotectedvirtual

Implementation of the decision procedure.

Implements decision_proceduret.

Reimplemented in smt2_dect.

Definition at line 320 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 145 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 284 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt & expr )

protected

Definition at line 5109 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet & type )

protected

Definition at line 5823 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 5829 of file smt2_conv.cpp.

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt & expr )

protected

Definition at line 4675 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 3385 of file smt2_conv.cpp.

◆ floatbv_suffix()

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

protected

Definition at line 1116 of file smt2_conv.cpp.

◆ get()

exprt smt2_convt::get ( const exprt & ) 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 335 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 6030 of file smt2_conv.cpp.

◆ handle()

exprt smt2_convt::handle ( const exprt & )

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 957 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt l ) const

protected

Definition at line 160 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 5038 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 536 of file smt2_conv.cpp.

◆ parse_literal()

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

protected

Definition at line 394 of file smt2_conv.cpp.

◆ parse_rec()

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

protected

Definition at line 703 of file smt2_conv.cpp.

◆ parse_struct()

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

protected

Definition at line 634 of file smt2_conv.cpp.

◆ parse_union()

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

protected

Definition at line 618 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 1003 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 5070 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 150 of file smt2_conv.cpp.

◆ push() [1/2]

void smt2_convt::push ( )

overridevirtual

Unimplemented.

Implements stack_decision_proceduret.

Definition at line 989 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 994 of file smt2_conv.cpp.

◆ set_converter()

void smt2_convt::set_converter	(	irep_idt	id,
		std::function< void(const exprt &)>	converter
	)

inline

Definition at line 94 of file smt2_conv.h.

◆ set_to()

void smt2_convt::set_to	(	const exprt &	,
		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 4883 of file smt2_conv.cpp.

◆ to_smt2_symbol()

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

inlineprotected

Definition at line 225 of file smt2_conv.h.

◆ type2id()

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

protected

Definition at line 1060 of file smt2_conv.cpp.

◆ unflatten()

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

protected

Definition at line 4766 of file smt2_conv.cpp.

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt & expr )

protected

Definition at line 5676 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 580 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 205 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )

protected

Definition at line 173 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

std::vector<literalt> smt2_convt::assumptions

protected

Definition at line 108 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark

protected

Definition at line 102 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width

protected

Definition at line 109 of file smt2_conv.h.

◆ boolean_assignment

std::vector<bool> smt2_convt::boolean_assignment

protected

Definition at line 294 of file smt2_conv.h.

◆ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set

protected

Definition at line 206 of file smt2_conv.h.

◆ converters

converterst smt2_convt::converters

protected

Definition at line 106 of file smt2_conv.h.

◆ current_bindings

std::unordered_map<irep_idt, irept> smt2_convt::current_bindings

protected

Definition at line 200 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map

protected

Definition at line 272 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions

protected

Definition at line 281 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 73 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map

protected

Definition at line 265 of file smt2_conv.h.

◆ letify

letifyt smt2_convt::letify

protected

Definition at line 177 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic

protected

Definition at line 102 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables

protected

Definition at line 293 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes

protected

Definition at line 102 of file smt2_conv.h.

◆ ns

const namespacet& smt2_convt::ns

protected

Definition at line 100 of file smt2_conv.h.

◆ number_of_solver_calls

std::size_t smt2_convt::number_of_solver_calls = 0

protected

Definition at line 111 of file smt2_conv.h.

◆ object_sizes

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

protected

Definition at line 287 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out

protected

Definition at line 101 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic

protected

Definition at line 240 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 285 of file smt2_conv.h.

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers

protected

Definition at line 290 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver

protected

Definition at line 103 of file smt2_conv.h.

◆ state_fkt_declared

std::set<irep_idt> smt2_convt::state_fkt_declared

protected

Definition at line 210 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 68 of file smt2_conv.h.

◆ use_as_const

bool smt2_convt::use_as_const

Definition at line 69 of file smt2_conv.h.

◆ use_check_sat_assuming

bool smt2_convt::use_check_sat_assuming

Definition at line 70 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 71 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 67 of file smt2_conv.h.

◆ use_lambda_for_array

bool smt2_convt::use_lambda_for_array

Definition at line 72 of file smt2_conv.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/smt2/smt2_conv.h
/home/runner/work/cbmc/cbmc/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

◆ converterst

◆ 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_round_to_integral()

◆ 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_string_literal()

◆ convert_struct()

◆ convert_type()

◆ convert_typecast()

◆ convert_union()

◆ convert_update()

◆ convert_update_bit()

◆ convert_update_bits()

◆ 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]