cprover
Loading...
Searching...
No Matches
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)
 Issues a command to the solving process which is expected to optionally return a success status followed by the actual response of interest.
 
static optionalt< std::string > get_problem_messages (const smt_responset &response)
 
static std::vector< exprtgather_dependent_expressions (const exprt &expr)
 Find all sub expressions of the given expr which need to be expressed as separate smt commands.
 
static optionalt< smt_termtget_identifier (const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
 
static NODISCARD decision_proceduret::resultt lookup_decision_procedure_result (const smt_check_sat_response_kindt &response_kind)
 

Function Documentation

◆ gather_dependent_expressions()

static std::vector< exprt > gather_dependent_expressions ( const exprt 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.

Definition at line 61 of file smt2_incremental_decision_procedure.cpp.

◆ get_identifier()

static optionalt< smt_termt > get_identifier ( const exprt expr,
const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &  expression_handle_identifiers,
const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &  expression_identifiers 
)
static

Definition at line 167 of file smt2_incremental_decision_procedure.cpp.

◆ get_problem_messages()

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

Definition at line 37 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 
)
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 24 of file smt2_incremental_decision_procedure.cpp.

◆ lookup_decision_procedure_result()

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

Definition at line 293 of file smt2_incremental_decision_procedure.cpp.