#include <smt2_incremental_decision_procedure.h>

Inheritance diagram for smt2_incremental_decision_proceduret:

Collaboration diagram for smt2_incremental_decision_proceduret:

Classes
class	sequencet
	Generators of sequences of uniquely identifying numbers used for naming SMT functions introduced by the decision procedure. More...

Public Member Functions
	smt2_incremental_decision_proceduret (const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)

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

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

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

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

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

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

void	push (const std::vector< exprt > &assumptions) override
	Pushes a new context on the stack that consists of the given (possibly empty vector of) `assumptions`. More...

void	push () override
	Push a new context on the stack This context becomes a child context nested in the current context. More...

void	pop () override
	Pop whatever is on top of the stack. More...

std::optional< exprt >	get_expr (const smt_termt &descriptor, const typet &type) const
	Gets the value of `descriptor` from the solver and returns the solver response expressed as an exprt of type `type`. More...

std::optional< exprt >	get_expr (const smt_termt &struct_term, const struct_tag_typet &type) const

std::optional< exprt >	get_expr (const smt_termt &union_term, const union_tag_typet &type) const

std::optional< exprt >	get_expr (const smt_termt &array, const array_typet &type) const

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

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

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

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

virtual	~decision_proceduret ()

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

template<typename t_exprt >
void	define_array_function (const t_exprt &array)
	Defines a function of array sort and asserts the element values from `array_exprt` or `array_of_exprt`. More...

void	initialize_array_elements (const array_exprt &array, const smt_identifier_termt &array_identifier)
	Generate and send to the SMT solver clauses asserting that each array element is as specified by `array`. More...

void	initialize_array_elements (const array_of_exprt &array, const smt_identifier_termt &array_identifier)
	Generate and send to the SMT solver clauses asserting that each array element is as specified by `array`. More...

void	initialize_array_elements (const string_constantt &string, const smt_identifier_termt &array_identifier)

void	define_dependent_functions (const exprt &expr)
	Defines any functions which `expr` depends on, which have not yet been defined, along with their dependencies in turn. More...

void	ensure_handle_for_expr_defined (const exprt &expr)
	If a function has not been defined for handling `expr`, then a new function is defined. More...

smt_termt	convert_expr_to_smt (const exprt &expr)
	Add objects in `expr` to object_map if needed and convert to smt. More...

void	define_index_identifiers (const exprt &expr)

exprt	substitute_defined_padding (exprt expr)
	In the case where lowering passes insert instances of the anonymous `nondet_padding_exprt`, these need functions declaring for each instance. More...

void	define_object_properties ()
	Sends the solver the definitions of the object sizes and dynamic memory statuses. More...

exprt	lower (exprt expression) const
	Performs a combination of transformations which reduces the set of possible expression forms by expressing these in terms of the remaining language features. More...

std::optional< smt_termt >	get_identifier (const exprt &expr) const

Protected Attributes
const namespacet &	ns
	Namespace for looking up the expressions which symbol_exprts relate to. More...

size_t	number_of_solver_calls
	The number of times `dec_solve()` has been called. More...

std::unique_ptr< smt_base_solver_processt >	solver_process
	For handling the lifetime of and communication with the separate SMT solver process. More...

messaget	log
	For reporting errors, warnings and debugging information back to the user. More...

class smt2_incremental_decision_proceduret::sequencet	handle_sequence

class smt2_incremental_decision_proceduret::sequencet	array_sequence

class smt2_incremental_decision_proceduret::sequencet	index_sequence

class smt2_incremental_decision_proceduret::sequencet	padding_sequence

std::unordered_map< exprt, smt_identifier_termt, irep_hash >	expression_handle_identifiers
	When the `handle(exprt)` member function is called, the decision procedure commands the SMT solver to define a new function corresponding to the given expression. More...

std::unordered_map< exprt, smt_identifier_termt, irep_hash >	expression_identifiers
	As part of the decision procedure's overall translation of CBMCs `exprt`s into SMT terms, some subexpressions are substituted for separate SMT functions. More...

std::unordered_map< irep_idt, smt_identifier_termt >	identifier_table
	This maps from the unsorted/untyped string/symbol for the identifiers which we have declared in SMT solver to the corresponding sorted/typed `smt_identifier_termt`. More...

smt_object_mapt	object_map
	This map is used to track object related state. More...

std::vector< bool >	object_properties_defined
	The size of each object and the dynamic object stus is separately defined as a pre-solving step. More...

smt_object_sizet	object_size_function
	Implementation of the SMT formula for the object size function. More...

smt_is_dynamic_objectt	is_dynamic_object_function
	Implementation of the SMT formula for the dynamic object status lookup function. More...

type_size_mapt	pointer_sizes_map
	Precalculated type sizes used for pointer arithmetic. More...

struct_encodingt	struct_encoding

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

Detailed Description

Definition at line 28 of file smt2_incremental_decision_procedure.h.

Constructor & Destructor Documentation

◆ smt2_incremental_decision_proceduret()

smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret	(	const namespacet &	_ns,
		std::unique_ptr< smt_base_solver_processt >	solver_process,
		message_handlert &	message_handler
	)

explicit

Parameters

_ns	Namespace for looking up the expressions which symbol_exprts relate to.
solver_process	The smt2 solver process communication interface.
message_handler	The messaging system to be used for logging purposes.

Definition at line 263 of file smt2_incremental_decision_procedure.cpp.

Member Function Documentation

◆ convert_expr_to_smt()

smt_termt smt2_incremental_decision_proceduret::convert_expr_to_smt ( const exprt & expr )

protected

Add objects in expr to object_map if needed and convert to smt.

Note: This function is non-const because it mutates the object_map.

Definition at line 380 of file smt2_incremental_decision_procedure.cpp.

◆ dec_solve()

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

overrideprotectedvirtual

Implementation of the decision procedure.

Implements decision_proceduret.

Definition at line 705 of file smt2_incremental_decision_procedure.cpp.

◆ decision_procedure_text()

std::string smt2_incremental_decision_proceduret::decision_procedure_text ( ) const

overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Definition at line 602 of file smt2_incremental_decision_procedure.cpp.

◆ define_array_function()

template<typename t_exprt >

void smt2_incremental_decision_proceduret::define_array_function ( const t_exprt & array )

protected

Defines a function of array sort and asserts the element values from array_exprt or array_of_exprt.

The new array function identifier is added to the expression_identifiers map.

Note: Statically fails if the template type is not a array_exprt or array_of_exprt.

Definition at line 150 of file smt2_incremental_decision_procedure.cpp.

◆ define_dependent_functions()

void smt2_incremental_decision_proceduret::define_dependent_functions ( const exprt & expr )

protected

Defines any functions which expr depends on, which have not yet been defined, along with their dependencies in turn.

Definition at line 184 of file smt2_incremental_decision_procedure.cpp.

◆ define_index_identifiers()

void smt2_incremental_decision_proceduret::define_index_identifiers ( const exprt & expr )

protected

Definition at line 334 of file smt2_incremental_decision_procedure.cpp.

◆ define_object_properties()

void smt2_incremental_decision_proceduret::define_object_properties ( )

protected

Sends the solver the definitions of the object sizes and dynamic memory statuses.

Definition at line 672 of file smt2_incremental_decision_procedure.cpp.

◆ ensure_handle_for_expr_defined()

void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined ( const exprt & expr )

protected

If a function has not been defined for handling expr, then a new function is defined.

If the corresponding function exists already, then no action is taken.

Definition at line 311 of file smt2_incremental_decision_procedure.cpp.

◆ get()

exprt smt2_incremental_decision_proceduret::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 548 of file smt2_incremental_decision_procedure.cpp.

◆ get_expr() [1/4]

std::optional< exprt > smt2_incremental_decision_proceduret::get_expr	(	const smt_termt &	array,
		const array_typet &	type
	)		const

Definition at line 434 of file smt2_incremental_decision_procedure.cpp.

◆ get_expr() [2/4]

std::optional< exprt > smt2_incremental_decision_proceduret::get_expr	(	const smt_termt &	descriptor,
		const typet &	type
	)		const

Gets the value of descriptor from the solver and returns the solver response expressed as an exprt of type type.

This is an implementation detail of the get(exprt) member function.

Definition at line 486 of file smt2_incremental_decision_procedure.cpp.

◆ get_expr() [3/4]

std::optional< exprt > smt2_incremental_decision_proceduret::get_expr	(	const smt_termt &	struct_term,
		const struct_tag_typet &	type
	)		const

Definition at line 464 of file smt2_incremental_decision_procedure.cpp.

◆ get_expr() [4/4]

std::optional< exprt > smt2_incremental_decision_proceduret::get_expr	(	const smt_termt &	union_term,
		const union_tag_typet &	type
	)		const

Definition at line 475 of file smt2_incremental_decision_procedure.cpp.

◆ get_identifier()

std::optional< smt_termt > smt2_incremental_decision_proceduret::get_identifier ( const exprt & expr ) const

protected

Definition at line 411 of file smt2_incremental_decision_procedure.cpp.

◆ get_number_of_solver_calls()

std::size_t smt2_incremental_decision_proceduret::get_number_of_solver_calls ( ) const

overridevirtual

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 608 of file smt2_incremental_decision_procedure.cpp.

◆ handle()

exprt smt2_incremental_decision_proceduret::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 401 of file smt2_incremental_decision_procedure.cpp.

◆ initialize_array_elements() [1/3]

void smt2_incremental_decision_proceduret::initialize_array_elements	(	const array_exprt &	array,
		const smt_identifier_termt &	array_identifier
	)

protected

Generate and send to the SMT solver clauses asserting that each array element is as specified by array.

Definition at line 107 of file smt2_incremental_decision_procedure.cpp.

◆ initialize_array_elements() [2/3]

void smt2_incremental_decision_proceduret::initialize_array_elements	(	const array_of_exprt &	array,
		const smt_identifier_termt &	array_identifier
	)

protected

Generate and send to the SMT solver clauses asserting that each array element is as specified by array.

Note: This function uses a forall SMT2 term. Using it in combination with arrays, bit vectors and uninterpreted functions requires the ALL SMT logic that is not in the SMT 2.6 standard, but that it has been tested working on Z3 and CVC5.

Definition at line 124 of file smt2_incremental_decision_procedure.cpp.

◆ initialize_array_elements() [3/3]

void smt2_incremental_decision_proceduret::initialize_array_elements	(	const string_constantt &	string,
		const smt_identifier_termt &	array_identifier
	)

protected

Definition at line 142 of file smt2_incremental_decision_procedure.cpp.

◆ lower()

exprt smt2_incremental_decision_proceduret::lower ( exprt expression ) const

protected

Performs a combination of transformations which reduces the set of possible expression forms by expressing these in terms of the remaining language features.

Definition at line 690 of file smt2_incremental_decision_procedure.cpp.

◆ pop()

void smt2_incremental_decision_proceduret::pop ( )

overridevirtual

Pop whatever is on top of the stack.

Popping from the empty stack results in an invariant violation.

Implements stack_decision_proceduret.

Definition at line 654 of file smt2_incremental_decision_procedure.cpp.

◆ print_assignment()

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

overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 595 of file smt2_incremental_decision_procedure.cpp.

◆ push() [1/2]

void smt2_incremental_decision_proceduret::push ( )

overridevirtual

Push a new context on the stack This context becomes a child context nested in the current context.

Implements stack_decision_proceduret.

Definition at line 649 of file smt2_incremental_decision_procedure.cpp.

◆ push() [2/2]

void smt2_incremental_decision_proceduret::push ( const std::vector< exprt > & assumptions )

overridevirtual

Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.

This context becomes a child context nested in the current context. An assumption is usually obtained by calling decision_proceduret::handle. Thus it can be a Boolean expression or something more solver-specific such as literal_exprt. An empty vector of assumptions counts as an element on the stack (and therefore needs to be popped), but has no effect beyond that.

Implements stack_decision_proceduret.

Definition at line 638 of file smt2_incremental_decision_procedure.cpp.

◆ set_to()

void smt2_incremental_decision_proceduret::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 613 of file smt2_incremental_decision_procedure.cpp.

◆ substitute_defined_padding()

exprt smt2_incremental_decision_proceduret::substitute_defined_padding ( exprt expr )

protected

In the case where lowering passes insert instances of the anonymous nondet_padding_exprt, these need functions declaring for each instance.

These instances are then substituted for the function identifier in order to free the solver to choose a non-det value.

Definition at line 363 of file smt2_incremental_decision_procedure.cpp.

Member Data Documentation

◆ array_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::array_sequence

protected

◆ expression_handle_identifiers

std::unordered_map<exprt, smt_identifier_termt, irep_hash> smt2_incremental_decision_proceduret::expression_handle_identifiers

protected

When the handle(exprt) member function is called, the decision procedure commands the SMT solver to define a new function corresponding to the given expression.

The mapping of the expressions to the function identifiers is stored in this map so that when there is as subsequent get(exprt) call for the same expression, the function identifier can be requested from the solver, rather than reconverting the expression.

Definition at line 154 of file smt2_incremental_decision_procedure.h.

◆ expression_identifiers

std::unordered_map<exprt, smt_identifier_termt, irep_hash> smt2_incremental_decision_proceduret::expression_identifiers

protected

As part of the decision procedure's overall translation of CBMCs exprts into SMT terms, some subexpressions are substituted for separate SMT functions.

This map associates these sub-expressions to the identifiers of the separated functions. This applies to symbol_exprt where it is fairly natural to define the value of the symbol using a separate function, but also to the expressions which define entire arrays. This includes array_exprt for example and will additionally include other similar array expressions when support for them is implemented.

Definition at line 164 of file smt2_incremental_decision_procedure.h.

◆ handle_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::handle_sequence

protected

◆ identifier_table

std::unordered_map<irep_idt, smt_identifier_termt> smt2_incremental_decision_proceduret::identifier_table

protected

This maps from the unsorted/untyped string/symbol for the identifiers which we have declared in SMT solver to the corresponding sorted/typed smt_identifier_termt.

This enables type checking the parse trees of responses received back from the solver. It is required because without the definitive sorts we would need to attempt to infer the sorts of identifiers from the surrounding terms which would be a looser check with a more complex implementation.

Definition at line 172 of file smt2_incremental_decision_procedure.h.

◆ index_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::index_sequence

protected

◆ is_dynamic_object_function

smt_is_dynamic_objectt smt2_incremental_decision_proceduret::is_dynamic_object_function

protected

Implementation of the SMT formula for the dynamic object status lookup function.

This is stateful because it depends on the configuration of the number of object bits and how many bits wide the size type is configured to be.

Definition at line 190 of file smt2_incremental_decision_procedure.h.

◆ log

messaget smt2_incremental_decision_proceduret::log

protected

For reporting errors, warnings and debugging information back to the user.

Definition at line 134 of file smt2_incremental_decision_procedure.h.

◆ ns

const namespacet& smt2_incremental_decision_proceduret::ns

protected

Namespace for looking up the expressions which symbol_exprts relate to.

This includes the symbols defined outside of the decision procedure but does not include any additional SMT function identifiers introduced by the decision procedure.

Definition at line 126 of file smt2_incremental_decision_procedure.h.

◆ number_of_solver_calls

size_t smt2_incremental_decision_proceduret::number_of_solver_calls

protected

The number of times dec_solve() has been called.

Definition at line 128 of file smt2_incremental_decision_procedure.h.

◆ object_map

smt_object_mapt smt2_incremental_decision_proceduret::object_map

protected

This map is used to track object related state.

See documentation in object_tracking.h for details.

Definition at line 175 of file smt2_incremental_decision_procedure.h.

◆ object_properties_defined

std::vector<bool> smt2_incremental_decision_proceduret::object_properties_defined

protected

The size of each object and the dynamic object stus is separately defined as a pre-solving step.

object_properties_defined[object ID] is set to true for objects where the size has been defined. This is used to avoid defining the size of the same object multiple times in the case where multiple rounds of solving are carried out.

Definition at line 181 of file smt2_incremental_decision_procedure.h.

◆ object_size_function

smt_object_sizet smt2_incremental_decision_proceduret::object_size_function

protected

Implementation of the SMT formula for the object size function.

This is stateful because it depends on the configuration of the number of object bits and how many bits wide the size type is configured to be.

Definition at line 185 of file smt2_incremental_decision_procedure.h.

◆ padding_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::padding_sequence

protected

◆ pointer_sizes_map

type_size_mapt smt2_incremental_decision_proceduret::pointer_sizes_map

protected

Precalculated type sizes used for pointer arithmetic.

Definition at line 192 of file smt2_incremental_decision_procedure.h.

◆ solver_process

std::unique_ptr<smt_base_solver_processt> smt2_incremental_decision_proceduret::solver_process

protected

For handling the lifetime of and communication with the separate SMT solver process.

Note: This may be mocked for unit testing purposes.

Definition at line 132 of file smt2_incremental_decision_procedure.h.

◆ struct_encoding

struct_encodingt smt2_incremental_decision_proceduret::struct_encoding

protected

Definition at line 193 of file smt2_incremental_decision_procedure.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
/home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ smt2_incremental_decision_proceduret()

Member Function Documentation

◆ convert_expr_to_smt()

◆ dec_solve()

◆ decision_procedure_text()

◆ define_array_function()

◆ define_dependent_functions()

◆ define_index_identifiers()

◆ define_object_properties()

◆ ensure_handle_for_expr_defined()

◆ get()

◆ get_expr() [1/4]

◆ get_expr() [2/4]

◆ get_expr() [3/4]

◆ get_expr() [4/4]

◆ get_identifier()

◆ get_number_of_solver_calls()

◆ handle()

◆ initialize_array_elements() [1/3]

◆ initialize_array_elements() [2/3]

◆ initialize_array_elements() [3/3]

◆ lower()

◆ pop()

◆ print_assignment()

◆ push() [1/2]

◆ push() [2/2]

◆ set_to()

◆ substitute_defined_padding()

Member Data Documentation

◆ array_sequence

◆ expression_handle_identifiers

◆ expression_identifiers

◆ handle_sequence

◆ identifier_table

◆ index_sequence

◆ is_dynamic_object_function

◆ log

◆ ns

◆ number_of_solver_calls

◆ object_map

◆ object_properties_defined

◆ object_size_function

◆ padding_sequence

◆ pointer_sizes_map

◆ solver_process

◆ struct_encoding