28 solver_process.
send(command);
41 return "SMT solver returned an error message - " +
46 return {
"SMT solver does not support given command."};
80 .map([](
const std::pair<exprt, smt_identifier_termt> &
expr_identifier) {
103 const irep_idt &identifier = symbol_expr->get_identifier();
104 const symbolt *symbol =
nullptr;
133 number_of_solver_calls{0},
169 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
170 &expression_handle_identifiers,
171 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
172 &expression_identifiers)
198 symbol_expr,
"Unhandled expressions are expected to be symbols");
207 <<
"`get` attempted for unknown symbol, with identifier - \n"
219 "Expected get-value response from solver, but received - " +
225 "Expected single valuation pair in get-value response from solver, but "
226 "received multiple pairs - " +
234 std::ostream &out)
const
242 return "incremental SMT2 solving via " +
solver_process->description();
254 log.
debug() <<
"`set_to` (" << std::string{value ?
"true" :
"false"}
272 const std::vector<exprt> &assumptions)
274 for(
const auto &assumption : assumptions)
277 "pushing of assumption:\n " + assumption.pretty(2, 0));
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
mstreamt & warning() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
size_t number_of_solver_calls
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_identifiers
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
resultt dec_solve() override
Run the decision procedure to solve the problem.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void ensure_handle_for_expr_defined(const exprt &expr)
void define_dependent_functions(const exprt &expr)
Defines any functions which expr depends on, which have not yet been defined, along with their depend...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
void pop() override
Pop whatever is on top of the stack.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_handle_identifiers
std::unique_ptr< smt_base_solver_processt > solver_process
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
class smt2_incremental_decision_proceduret::sequencet handle_sequence
smt2_incremental_decision_proceduret(const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)
virtual smt_responset receive_response()=0
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
const sub_classt * cast() const &
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
const std::string & id2string(const irep_idt &d)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
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 follo...
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 optionalt< std::string > get_problem_messages(const smt_responset &response)
static NODISCARD decision_proceduret::resultt lookup_decision_procedure_result(const smt_check_sat_response_kindt &response_kind)
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.