smt2_incremental_decision_procedure.cpp File Reference

#include "smt2_incremental_decision_procedure.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <solvers/smt2_incremental/ast/smt_commands.h>
#include <solvers/smt2_incremental/ast/smt_responses.h>
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
#include <solvers/smt2_incremental/convert_expr_to_smt.h>
#include <solvers/smt2_incremental/encoding/enum_encoding.h>
#include <solvers/smt2_incremental/encoding/nondet_padding.h>
#include <solvers/smt2_incremental/smt_solver_process.h>
#include <solvers/smt2_incremental/theories/smt_array_theory.h>
#include <solvers/smt2_incremental/theories/smt_core_theory.h>
#include <solvers/smt2_incremental/type_size_mapping.h>
#include <stack>
#include <unordered_set>

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< exprt >	gather_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	lower_zero_extend (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 533 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 73 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 47 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 31 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 660 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 281 of file smt2_incremental_decision_procedure.cpp.

lower_zero_extend()

static exprt lower_zero_extend ( exprt  expr, const namespacet &  ns  )

static

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