CBMC
smt2_incremental_decision_procedure.cpp File Reference
+ Include dependency graph for smt2_incremental_decision_procedure.cpp:

Go to the source code of this file.

Functions

static smt_responset get_response_to_command (smt_base_solver_processt &solver_process, const smt_commandt &command, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
 Issues a command to the solving process which is expected to optionally return a success status followed by the actual response of interest. More...
 
static std::optional< std::string > get_problem_messages (const smt_responset &response)
 Returns a message string describing the problem in the case where the response from the solver is an error status. More...
 
static std::vector< exprtgather_dependent_expressions (const exprt &root_expr)
 Find all sub expressions of the given expr which need to be expressed as separate smt commands. More...
 
void send_function_definition (const exprt &expr, const irep_idt &symbol_identifier, const std::unique_ptr< smt_base_solver_processt > &solver_process, std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers, std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
 
static exprt substitute_identifiers (exprt expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
 Replaces the sub expressions of expr which have been defined as separate functions in the smt solver, using the expression_identifiers map. More...
 
static exprt lower_rw_ok_pointer_in_range (exprt expr, const namespacet &ns)
 
static exprt build_expr_based_on_getting_operands (const exprt &expr, const stack_decision_proceduret &decision_procedure)
 
static decision_proceduret::resultt lookup_decision_procedure_result (const smt_check_sat_response_kindt &response_kind)
 

Function Documentation

◆ build_expr_based_on_getting_operands()

static exprt build_expr_based_on_getting_operands ( const exprt expr,
const stack_decision_proceduret decision_procedure 
)
static

Definition at line 521 of file smt2_incremental_decision_procedure.cpp.

◆ gather_dependent_expressions()

static std::vector<exprt> gather_dependent_expressions ( const exprt root_expr)
static

Find all sub expressions of the given expr which need to be expressed as separate smt commands.

Returns
A collection of sub expressions, which need to be expressed as separate smt commands. This collection is in traversal order. It will include duplicate subexpressions, which need to be removed by the caller in order to avoid duplicate definitions.
Note
This pass over expr is tightly coupled to the implementation of convert_expr_to_smt. This is because any sub expressions which convert_expr_to_smt translates into function applications, must also be returned by thisgather_dependent_expressions function.

symbol_exprt, array_exprt and nondet_symbol_exprt add dependant expressions.

Definition at line 72 of file smt2_incremental_decision_procedure.cpp.

◆ get_problem_messages()

static std::optional<std::string> get_problem_messages ( const smt_responset response)
static

Returns a message string describing the problem in the case where the response from the solver is an error status.

Returns empty otherwise.

Definition at line 46 of file smt2_incremental_decision_procedure.cpp.

◆ get_response_to_command()

static smt_responset get_response_to_command ( smt_base_solver_processt solver_process,
const smt_commandt command,
const std::unordered_map< irep_idt, smt_identifier_termt > &  identifier_table 
)
static

Issues a command to the solving process which is expected to optionally return a success status followed by the actual response of interest.

Definition at line 30 of file smt2_incremental_decision_procedure.cpp.

◆ lookup_decision_procedure_result()

static decision_proceduret::resultt lookup_decision_procedure_result ( const smt_check_sat_response_kindt response_kind)
static

Definition at line 648 of file smt2_incremental_decision_procedure.cpp.

◆ lower_rw_ok_pointer_in_range()

static exprt lower_rw_ok_pointer_in_range ( exprt  expr,
const namespacet ns 
)
static

Definition at line 280 of file smt2_incremental_decision_procedure.cpp.

◆ send_function_definition()

void send_function_definition ( const exprt expr,
const irep_idt symbol_identifier,
const std::unique_ptr< smt_base_solver_processt > &  solver_process,
std::unordered_map< exprt, smt_identifier_termt, irep_hash > &  expression_identifiers,
std::unordered_map< irep_idt, smt_identifier_termt > &  identifier_table 
)

Definition at line 164 of file smt2_incremental_decision_procedure.cpp.

◆ substitute_identifiers()

static exprt substitute_identifiers ( exprt  expr,
const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &  expression_identifiers 
)
static

Replaces the sub expressions of expr which have been defined as separate functions in the smt solver, using the expression_identifiers map.

Definition at line 247 of file smt2_incremental_decision_procedure.cpp.