#include <smt2_conv.h>

Inheritance diagram for smt2_convt:

Collaboration diagram for smt2_convt:

Classes
class	smt2_symbolt
struct	identifiert

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
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_fma (const floatbv_fma_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)
	Find and declare symbols used in an expression This function traverses the expression tree and creates SMT2 declarations for all symbols (variables) found.
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 41 of file smt2_conv.h.

Member Typedef Documentation

◆ converterst

using smt2_convt::converterst

protected

Initial value:

std::

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

exprt

Base class for all expressions.

Definition expr.h:57

irep_id_hash

dstring_hash irep_id_hash

Definition irep.h:38

irep_idt

dstringt irep_idt

Definition verification_result.h:16

Definition at line 105 of file smt2_conv.h.

◆ datatype_mapt

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

protected

Definition at line 273 of file smt2_conv.h.

◆ defined_expressionst

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

protected

Definition at line 282 of file smt2_conv.h.

◆ identifier_mapt

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

protected

Definition at line 265 of file smt2_conv.h.

◆ smt2_identifierst

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

protected

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

◆ wheret

enum class smt2_convt::wheret

strongprotected

Enumerator
BEGIN
END

Definition at line 237 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 59 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 987 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 874 of file smt2_conv.cpp.

◆ convert_constant()

void smt2_convt::convert_constant ( const constant_exprt & expr )

protected

Definition at line 3606 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt & expr )

protected

Definition at line 4306 of file smt2_conv.cpp.

◆ convert_euclidean_mod()

void smt2_convt::convert_euclidean_mod ( const euclidean_mod_exprt & expr )

protected

Definition at line 3779 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt & expr )

protected

Definition at line 1256 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt & expr )

protected

Definition at line 1209 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt & expr )

protected

Definition at line 4360 of file smt2_conv.cpp.

◆ convert_floatbv_fma()

void smt2_convt::convert_floatbv_fma ( const floatbv_fma_exprt & expr )

protected

Definition at line 4498 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt & expr )

protected

Definition at line 4286 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt & expr )

protected

Definition at line 4455 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt & expr )

protected

Definition at line 4154 of file smt2_conv.cpp.

◆ convert_floatbv_rem()

void smt2_convt::convert_floatbv_rem ( const binary_exprt & expr )

protected

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

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt & expr )

protected

Definition at line 3311 of file smt2_conv.cpp.

◆ convert_identifier()

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

static

Definition at line 1111 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt & expr )

protected

Definition at line 4740 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const unary_exprt & expr )

protected

Definition at line 3813 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt l )

protected

Definition at line 1052 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt & expr )

protected

Definition at line 4810 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt & expr )

protected

Definition at line 4189 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt & expr )

protected

Definition at line 3794 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt & expr )

protected

Definition at line 4380 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt & expr )

protected

Definition at line 3960 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const binary_relation_exprt & expr )

protected

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

◆ convert_string_literal()

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

protected

Definition at line 1243 of file smt2_conv.cpp.

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt & expr )

protected

Definition at line 3472 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet & type )

protected

Definition at line 5904 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt & expr )

protected

Definition at line 2749 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt & expr )

protected

Definition at line 3578 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const update_exprt & expr )

protected

Definition at line 4723 of file smt2_conv.cpp.

◆ convert_update_bit()

void smt2_convt::convert_update_bit ( const update_bit_exprt & expr )

protected

Definition at line 4730 of file smt2_conv.cpp.

◆ convert_update_bits()

void smt2_convt::convert_update_bits ( const update_bits_exprt & expr )

protected

Definition at line 4735 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt & expr )

protected

Definition at line 4520 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 328 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 148 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 292 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt & expr )

protected

Find and declare symbols used in an expression This function traverses the expression tree and creates SMT2 declarations for all symbols (variables) found.

Symbols are added to identifier_map to avoid duplication declarations.

Determinism: The traversal of expression trees is deterministic, and solely depends on syntactic expression structure, not expression hash codes.

Parameters

expr	expression to scan for symbols

Definition at line 5324 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet & type )

protected

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

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt & expr )

protected

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

◆ floatbv_suffix()

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

protected

Definition at line 1202 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 343 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 6248 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 1043 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt l ) const

protected

Definition at line 163 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 5244 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 622 of file smt2_conv.cpp.

◆ parse_literal()

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

protected

Definition at line 402 of file smt2_conv.cpp.

◆ parse_rec()

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

protected

Definition at line 789 of file smt2_conv.cpp.

◆ parse_struct()

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

protected

Definition at line 720 of file smt2_conv.cpp.

◆ parse_union()

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

protected

Definition at line 704 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 1089 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 5276 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 153 of file smt2_conv.cpp.

◆ push() [1/2]

void smt2_convt::push ( )

overridevirtual

Unimplemented.

Implements stack_decision_proceduret.

Definition at line 1075 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 1080 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 95 of file smt2_conv.h.

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

◆ to_smt2_symbol()

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

inlineprotected

Definition at line 227 of file smt2_conv.h.

◆ type2id()

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

protected

Definition at line 1146 of file smt2_conv.cpp.

◆ unflatten()

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

protected

Definition at line 4972 of file smt2_conv.cpp.

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt & expr )

protected

Definition at line 5892 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 666 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 208 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )

protected

Definition at line 176 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

std::vector<literalt> smt2_convt::assumptions

protected

Definition at line 109 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark

protected

Definition at line 103 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width

protected

Definition at line 110 of file smt2_conv.h.

◆ boolean_assignment

std::vector<bool> smt2_convt::boolean_assignment

protected

Definition at line 296 of file smt2_conv.h.

◆ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set

protected

Definition at line 208 of file smt2_conv.h.

◆ converters

converterst smt2_convt::converters

protected

Definition at line 107 of file smt2_conv.h.

◆ current_bindings

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

protected

Definition at line 202 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map

protected

Definition at line 274 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions

protected

Definition at line 283 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 74 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map

protected

Definition at line 267 of file smt2_conv.h.

◆ letify

letifyt smt2_convt::letify

protected

Definition at line 179 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic

protected

Definition at line 103 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables

protected

Definition at line 295 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes

protected

Definition at line 103 of file smt2_conv.h.

◆ ns

const namespacet& smt2_convt::ns

protected

Definition at line 101 of file smt2_conv.h.

◆ number_of_solver_calls

std::size_t smt2_convt::number_of_solver_calls = 0

protected

Definition at line 112 of file smt2_conv.h.

◆ object_sizes

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

protected

Definition at line 289 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out

protected

Definition at line 102 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic

protected

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

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers

protected

Definition at line 292 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver

protected

Definition at line 104 of file smt2_conv.h.

◆ state_fkt_declared

std::set<irep_idt> smt2_convt::state_fkt_declared

protected

Definition at line 212 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 69 of file smt2_conv.h.

◆ use_as_const

bool smt2_convt::use_as_const

Definition at line 70 of file smt2_conv.h.

◆ use_check_sat_assuming

bool smt2_convt::use_check_sat_assuming

Definition at line 71 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 72 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 68 of file smt2_conv.h.

◆ use_lambda_for_array

bool smt2_convt::use_lambda_for_array

Definition at line 73 of file smt2_conv.h.

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

solvers/smt2/smt2_conv.h
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_fma()

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