cprover
|
#include "smt2_incremental_decision_procedure.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_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 <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 <stack>
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< exprt > | gather_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_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 NODISCARD decision_proceduret::resultt | lookup_decision_procedure_result (const smt_check_sat_response_kindt &response_kind) |
Find all sub expressions of the given expr
which need to be expressed as separate smt commands.
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.
|
static |
Definition at line 167 of file smt2_incremental_decision_procedure.cpp.
|
static |
Definition at line 37 of file smt2_incremental_decision_procedure.cpp.
|
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.
|
static |
Definition at line 293 of file smt2_incremental_decision_procedure.cpp.