smt2_incremental_decision_procedure.cpp File Reference

#include "smt2_incremental_decision_procedure.h"
#include <util/arith_tools.h>
#include <util/expr.h>
#include <util/namespace.h>
#include <util/nodiscard.h>
#include <util/range.h>
#include <util/std_expr.h>
#include <util/string_utils.h>
#include <util/symbol.h>
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
#include <solvers/smt2_incremental/convert_expr_to_smt.h>
#include <solvers/smt2_incremental/smt_array_theory.h>
#include <solvers/smt2_incremental/smt_commands.h>
#include <solvers/smt2_incremental/smt_core_theory.h>
#include <solvers/smt2_incremental/smt_responses.h>
#include <solvers/smt2_incremental/smt_solver_process.h>
#include <solvers/smt2_incremental/smt_terms.h>
#include <solvers/smt2_incremental/type_size_mapping.h>
#include <stack>

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 optionalt< std::string >	get_problem_messages (const smt_responset &response)
static std::vector< exprt >	gather_dependent_expressions (const exprt &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 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 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.

symbol_exprt, array_exprt and nondet_symbol_exprt add dependant expressions.

Definition at line 68 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 328 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 42 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 28 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 523 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 135 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 228 of file smt2_incremental_decision_procedure.cpp.