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

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

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

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

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

virtual	~decision_proceduret ()

Protected Member Functions
resultt	dec_solve () override
	Run the decision procedure to solve the problem. 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	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)

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)

void	define_object_sizes ()
	Sends the solver the definitions of the object sizes. More...

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

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_size_defined
	The size of each object 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...

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

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

Detailed Description

Definition at line 27 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 243 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 300 of file smt2_incremental_decision_procedure.cpp.

◆ dec_solve()

decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve ( )

overrideprotectedvirtual

Run the decision procedure to solve the problem.

Implements decision_proceduret.

Definition at line 551 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 468 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 120 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 154 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 278 of file smt2_incremental_decision_procedure.cpp.

◆ define_object_sizes()

void smt2_incremental_decision_proceduret::define_object_sizes ( )

protected

Sends the solver the definitions of the object sizes.

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

Definition at line 259 of file smt2_incremental_decision_procedure.cpp.

◆ get()

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

◆ get_expr() [1/2]

array_exprt smt2_incremental_decision_proceduret::get_expr	(	const smt_termt &	array,
		const array_typet &	type
	)		const

Definition at line 344 of file smt2_incremental_decision_procedure.cpp.

◆ get_expr() [2/2]

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 372 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 474 of file smt2_incremental_decision_procedure.cpp.

◆ handle()

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

◆ initialize_array_elements() [1/2]

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 84 of file smt2_incremental_decision_procedure.cpp.

◆ initialize_array_elements() [2/2]

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 101 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 517 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 461 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 512 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 501 of file smt2_incremental_decision_procedure.cpp.

◆ set_to()

void smt2_incremental_decision_proceduret::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 479 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 130 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 140 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 148 of file smt2_incremental_decision_procedure.h.

◆ index_sequence

class smt2_incremental_decision_proceduret::sequencet smt2_incremental_decision_proceduret::index_sequence

protected

◆ log

messaget smt2_incremental_decision_proceduret::log

protected

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

Definition at line 110 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 102 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 104 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 151 of file smt2_incremental_decision_procedure.h.

◆ object_size_defined

std::vector<bool> smt2_incremental_decision_proceduret::object_size_defined

protected

The size of each object is separately defined as a pre-solving step.

object_size_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 157 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 161 of file smt2_incremental_decision_procedure.h.

◆ pointer_sizes_map

type_size_mapt smt2_incremental_decision_proceduret::pointer_sizes_map

protected

Precalculated type sizes used for pointer arithmetic.

Definition at line 163 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 108 of file smt2_incremental_decision_procedure.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
/home/runner/work/cbmc-documentation/cbmc-documentation/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_sizes()

◆ ensure_handle_for_expr_defined()

◆ get()

◆ get_expr() [1/2]

◆ get_expr() [2/2]

◆ get_number_of_solver_calls()

◆ handle()

◆ initialize_array_elements() [1/2]

◆ initialize_array_elements() [2/2]

◆ pop()

◆ print_assignment()

◆ push() [1/2]

◆ push() [2/2]

◆ set_to()

Member Data Documentation

◆ array_sequence

◆ expression_handle_identifiers

◆ expression_identifiers

◆ handle_sequence

◆ identifier_table

◆ index_sequence

◆ log

◆ ns

◆ number_of_solver_calls

◆ object_map

◆ object_size_defined

◆ object_size_function

◆ pointer_sizes_map

◆ solver_process