Decision procedure interface for various SMT 2.x solvers. More...

#include <smt2_dec.h>

Inheritance diagram for smt2_dect:

Collaboration diagram for smt2_dect:

Public Member Functions
	smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, message_handlert &_message_handler)

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

Public Member Functions inherited from smt2_convt
	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.

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

Protected Member Functions
resultt	dec_solve (const exprt &) override
	Implementation of the decision procedure.

resultt	read_result (std::istream &in)

Protected Member Functions inherited from smt2_convt
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)

	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.

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)

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

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

Protected Attributes
message_handlert &	message_handler

std::stringstream	cached_output
	Everything except the footer is cached, so that output files can be rewritten with varying footers.

Protected Attributes inherited from smt2_stringstreamt
std::stringstream	stringstream

Protected Attributes inherited from smt2_convt
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

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

Additional Inherited Members
Public Types inherited from smt2_convt
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...

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

Public Attributes inherited from smt2_convt
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 inherited from smt2_convt
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

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

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

Static Protected Member Functions inherited from smt2_convt
static std::string	convert_identifier (const irep_idt &identifier)

Detailed Description

Decision procedure interface for various SMT 2.x solvers.

Definition at line 25 of file smt2_dec.h.

Constructor & Destructor Documentation

◆ smt2_dect()

smt2_dect::smt2_dect	(	const namespacet &	_ns,
		const std::string &	_benchmark,
		const std::string &	_notes,
		const std::string &	_logic,
		solvert	_solver,
		message_handlert &	_message_handler
	)

inline

Definition at line 28 of file smt2_dec.h.

Member Function Documentation

◆ dec_solve()

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

overrideprotectedvirtual

Implementation of the decision procedure.

Reimplemented from smt2_convt.

Definition at line 38 of file smt2_dec.cpp.

◆ decision_procedure_text()

std::string smt2_dect::decision_procedure_text ( ) const

overridevirtual

Return a textual description of the decision procedure.

Reimplemented from smt2_convt.

Definition at line 20 of file smt2_dec.cpp.

◆ read_result()

decision_proceduret::resultt smt2_dect::read_result ( std::istream & in )

protected

Definition at line 162 of file smt2_dec.cpp.

Member Data Documentation

◆ cached_output

std::stringstream smt2_dect::cached_output

protected

Everything except the footer is cached, so that output files can be rewritten with varying footers.

Definition at line 48 of file smt2_dec.h.

◆ message_handler

message_handlert& smt2_dect::message_handler

protected

Definition at line 43 of file smt2_dec.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ smt2_dect()

Member Function Documentation

◆ dec_solve()

◆ decision_procedure_text()

◆ read_result()

Member Data Documentation

◆ cached_output

◆ message_handler