#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 , BOOLECTOR , CPROVER_SMT2 , CVC3 , CVC4 , 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.

Public Member Functions inherited from stack_decision_proceduret
virtual void	push (const std::vector< exprt > &assumptions)=0
	Pushes a new context on the stack that consists of the given (possibly empty vector of) `assumptions`.

virtual void	push ()=0
	Push a new context on the stack This context becomes a child context nested in the current context.

virtual void	pop ()=0
	Pop whatever is on top of the stack.

virtual	~stack_decision_proceduret ()=default

Public Member Functions inherited from decision_proceduret
virtual void	set_to (const exprt &expr, bool value)=0
	For a Boolean expression `expr`, add the constraint 'expr' if `value` is `true`, otherwise add 'not expr'.

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

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

virtual exprt	handle (const exprt &expr)=0
	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.

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

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

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

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

virtual std::size_t	get_number_of_solver_calls () const =0
	Return the number of incremental solver calls.

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 }

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.

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

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 exprt &expr)

virtual resultt	dec_solve ()=0
	Run the decision procedure to solve the problem.

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.

defined_expressionst	object_sizes

smt2_identifierst	smt2_identifiers

std::size_t	no_boolean_variables

std::vector< bool >	boolean_assignment

Detailed Description

Definition at line 35 of file smt2_conv.h.

Member Typedef Documentation

◆ datatype_mapt

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

protected

Definition at line 243 of file smt2_conv.h.

◆ defined_expressionst

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

protected

Definition at line 252 of file smt2_conv.h.

◆ identifier_mapt

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

protected

Definition at line 235 of file smt2_conv.h.

◆ smt2_identifierst

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

protected

Definition at line 261 of file smt2_conv.h.

Member Enumeration Documentation

◆ solvert

enum class smt2_convt::solvert

strong

Enumerator
GENERIC
BOOLECTOR
CPROVER_SMT2
CVC3
CVC4
MATHSAT
YICES
Z3

Definition at line 38 of file smt2_conv.h.

◆ wheret

enum class smt2_convt::wheret

strongprotected

Enumerator
BEGIN
END

Definition at line 210 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 794 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 2955 of file smt2_conv.cpp.

◆ convert_div()

void smt2_convt::convert_div ( const div_exprt & expr )

protected

Definition at line 3629 of file smt2_conv.cpp.

◆ convert_euclidean_mod()

void smt2_convt::convert_euclidean_mod ( const euclidean_mod_exprt & expr )

protected

Definition at line 3100 of file smt2_conv.cpp.

◆ convert_expr()

void smt2_convt::convert_expr ( const exprt & expr )

protected

Definition at line 989 of file smt2_conv.cpp.

◆ convert_floatbv()

void smt2_convt::convert_floatbv ( const exprt & expr )

protected

Definition at line 955 of file smt2_conv.cpp.

◆ convert_floatbv_div()

void smt2_convt::convert_floatbv_div ( const ieee_float_op_exprt & expr )

protected

Definition at line 3673 of file smt2_conv.cpp.

◆ convert_floatbv_minus()

void smt2_convt::convert_floatbv_minus ( const ieee_float_op_exprt & expr )

protected

Definition at line 3609 of file smt2_conv.cpp.

◆ convert_floatbv_mult()

void smt2_convt::convert_floatbv_mult ( const ieee_float_op_exprt & expr )

protected

Definition at line 3768 of file smt2_conv.cpp.

◆ convert_floatbv_plus()

void smt2_convt::convert_floatbv_plus ( const ieee_float_op_exprt & expr )

protected

Definition at line 3471 of file smt2_conv.cpp.

◆ convert_floatbv_rem()

void smt2_convt::convert_floatbv_rem ( const binary_exprt & expr )

protected

Definition at line 3788 of file smt2_conv.cpp.

◆ convert_floatbv_typecast()

void smt2_convt::convert_floatbv_typecast ( const floatbv_typecast_exprt & expr )

protected

Definition at line 2683 of file smt2_conv.cpp.

◆ convert_identifier()

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

static

Definition at line 880 of file smt2_conv.cpp.

◆ convert_index()

void smt2_convt::convert_index ( const index_exprt & expr )

protected

Definition at line 4065 of file smt2_conv.cpp.

◆ convert_is_dynamic_object()

void smt2_convt::convert_is_dynamic_object ( const unary_exprt & expr )

protected

Definition at line 3134 of file smt2_conv.cpp.

◆ convert_literal()

void smt2_convt::convert_literal ( const literalt l )

protected

Definition at line 843 of file smt2_conv.cpp.

◆ convert_member()

void smt2_convt::convert_member ( const member_exprt & expr )

protected

Definition at line 4163 of file smt2_conv.cpp.

◆ convert_minus()

void smt2_convt::convert_minus ( const minus_exprt & expr )

protected

Definition at line 3512 of file smt2_conv.cpp.

◆ convert_mod()

void smt2_convt::convert_mod ( const mod_exprt & expr )

protected

Definition at line 3115 of file smt2_conv.cpp.

◆ convert_mult()

void smt2_convt::convert_mult ( const mult_exprt & expr )

protected

Definition at line 3693 of file smt2_conv.cpp.

◆ convert_plus()

void smt2_convt::convert_plus ( const plus_exprt & expr )

protected

Definition at line 3278 of file smt2_conv.cpp.

◆ convert_relation()

void smt2_convt::convert_relation ( const binary_relation_exprt & expr )

protected

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

◆ convert_struct()

void smt2_convt::convert_struct ( const struct_exprt & expr )

protected

Definition at line 2827 of file smt2_conv.cpp.

◆ convert_type()

void smt2_convt::convert_type ( const typet & type )

protected

Definition at line 4876 of file smt2_conv.cpp.

◆ convert_typecast()

void smt2_convt::convert_typecast ( const typecast_exprt & expr )

protected

Definition at line 2150 of file smt2_conv.cpp.

◆ convert_union()

void smt2_convt::convert_union ( const union_exprt & expr )

protected

Definition at line 2922 of file smt2_conv.cpp.

◆ convert_update()

void smt2_convt::convert_update ( const exprt & expr )

protected

Definition at line 4058 of file smt2_conv.cpp.

◆ convert_with()

void smt2_convt::convert_with ( const with_exprt & expr )

protected

Definition at line 3811 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 274 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 127 of file smt2_conv.cpp.

◆ define_object_size()

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

protected

Definition at line 236 of file smt2_conv.cpp.

◆ find_symbols() [1/2]

void smt2_convt::find_symbols ( const exprt & expr )

protected

Definition at line 4572 of file smt2_conv.cpp.

◆ find_symbols() [2/2]

void smt2_convt::find_symbols ( const typet & type )

protected

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

◆ flatten2bv()

void smt2_convt::flatten2bv ( const exprt & expr )

protected

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

◆ floatbv_suffix()

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

protected

Definition at line 948 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 281 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 5226 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 834 of file smt2_conv.cpp.

◆ l_get()

tvt smt2_convt::l_get ( literalt l ) const

protected

Definition at line 142 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 4525 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 479 of file smt2_conv.cpp.

◆ parse_literal()

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

protected

Definition at line 341 of file smt2_conv.cpp.

◆ parse_rec()

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

protected

Definition at line 638 of file smt2_conv.cpp.

◆ parse_struct()

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

protected

Definition at line 579 of file smt2_conv.cpp.

◆ parse_union()

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

protected

Definition at line 563 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 875 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 4557 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 132 of file smt2_conv.cpp.

◆ push() [1/2]

void smt2_convt::push ( )

overridevirtual

Unimplemented.

Implements stack_decision_proceduret.

Definition at line 863 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 868 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 4417 of file smt2_conv.cpp.

◆ to_smt2_symbol()

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

inlineprotected

Definition at line 200 of file smt2_conv.h.

◆ type2id()

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

protected

Definition at line 911 of file smt2_conv.cpp.

◆ unflatten()

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

protected

Definition at line 4313 of file smt2_conv.cpp.

◆ use_array_theory()

bool smt2_convt::use_array_theory ( const exprt & expr )

protected

Definition at line 4855 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 523 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 185 of file smt2_conv.cpp.

◆ write_header()

void smt2_convt::write_header ( )

protected

Definition at line 155 of file smt2_conv.cpp.

Member Data Documentation

◆ assumptions

std::vector<exprt> smt2_convt::assumptions

protected

Definition at line 93 of file smt2_conv.h.

◆ benchmark

std::string smt2_convt::benchmark

protected

Definition at line 90 of file smt2_conv.h.

◆ boolbv_width

boolbv_widtht smt2_convt::boolbv_width

protected

Definition at line 94 of file smt2_conv.h.

◆ boolean_assignment

std::vector<bool> smt2_convt::boolean_assignment

protected

Definition at line 266 of file smt2_conv.h.

◆ bvfp_set

std::set<irep_idt> smt2_convt::bvfp_set

protected

Definition at line 185 of file smt2_conv.h.

◆ datatype_map

datatype_mapt smt2_convt::datatype_map

protected

Definition at line 244 of file smt2_conv.h.

◆ defined_expressions

defined_expressionst smt2_convt::defined_expressions

protected

Definition at line 253 of file smt2_conv.h.

◆ emit_set_logic

bool smt2_convt::emit_set_logic

Definition at line 66 of file smt2_conv.h.

◆ identifier_map

identifier_mapt smt2_convt::identifier_map

protected

Definition at line 237 of file smt2_conv.h.

◆ letify

letifyt smt2_convt::letify

protected

Definition at line 157 of file smt2_conv.h.

◆ logic

std::string smt2_convt::logic

protected

Definition at line 90 of file smt2_conv.h.

◆ no_boolean_variables

std::size_t smt2_convt::no_boolean_variables

protected

Definition at line 265 of file smt2_conv.h.

◆ notes

std::string smt2_convt::notes

protected

Definition at line 90 of file smt2_conv.h.

◆ ns

const namespacet& smt2_convt::ns

protected

Definition at line 88 of file smt2_conv.h.

◆ number_of_solver_calls

std::size_t smt2_convt::number_of_solver_calls = 0

protected

Definition at line 96 of file smt2_conv.h.

◆ object_sizes

defined_expressionst smt2_convt::object_sizes

protected

Definition at line 259 of file smt2_conv.h.

◆ out

std::ostream& smt2_convt::out

protected

Definition at line 89 of file smt2_conv.h.

◆ pointer_logic

pointer_logict smt2_convt::pointer_logic

protected

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

◆ smt2_identifiers

smt2_identifierst smt2_convt::smt2_identifiers

protected

Definition at line 262 of file smt2_conv.h.

◆ solver

solvert smt2_convt::solver

protected

Definition at line 91 of file smt2_conv.h.

◆ use_array_of_bool

bool smt2_convt::use_array_of_bool

Definition at line 61 of file smt2_conv.h.

◆ use_as_const

bool smt2_convt::use_as_const

Definition at line 62 of file smt2_conv.h.

◆ use_check_sat_assuming

bool smt2_convt::use_check_sat_assuming

Definition at line 63 of file smt2_conv.h.

◆ use_datatypes

bool smt2_convt::use_datatypes

Definition at line 64 of file smt2_conv.h.

◆ use_FPA_theory

bool smt2_convt::use_FPA_theory

Definition at line 60 of file smt2_conv.h.

◆ use_lambda_for_array

bool smt2_convt::use_lambda_for_array

Definition at line 65 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

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