cprover
Loading...
Searching...
No Matches
smt2_incremental_decision_procedure.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
12#include <util/expr.h>
13#include <util/namespace.h>
14#include <util/nodiscard.h>
15#include <util/range.h>
16#include <util/std_expr.h>
17#include <util/string_utils.h>
18#include <util/symbol.h>
19
20#include <stack>
21
25 smt_base_solver_processt &solver_process,
26 const smt_commandt &command)
27{
28 solver_process.send(command);
29 auto response = solver_process.receive_response();
30 if(response.cast<smt_success_responset>())
31 return solver_process.receive_response();
32 else
33 return response;
34}
35
38{
39 if(const auto error = response.cast<smt_error_responset>())
40 {
41 return "SMT solver returned an error message - " +
42 id2string(error->message());
43 }
44 if(response.cast<smt_unsupported_responset>())
45 {
46 return {"SMT solver does not support given command."};
47 }
48 return {};
49}
50
61static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
62{
63 std::vector<exprt> dependent_expressions;
64 expr.visit_pre([&](const exprt &expr_node) {
65 if(can_cast_expr<symbol_exprt>(expr_node))
66 {
67 dependent_expressions.push_back(expr_node);
68 }
69 });
70 return dependent_expressions;
71}
72
76 const exprt &expr)
77{
78 std::unordered_set<exprt, irep_hash> seen_expressions =
80 .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
81 return expr_identifier.first;
82 });
83 std::stack<exprt> to_be_defined;
84 const auto push_dependencies_needed = [&](const exprt &expr) {
85 bool result = false;
86 for(const auto &dependency : gather_dependent_expressions(expr))
87 {
88 if(!seen_expressions.insert(dependency).second)
89 continue;
90 result = true;
91 to_be_defined.push(dependency);
92 }
93 return result;
94 };
95 push_dependencies_needed(expr);
96 while(!to_be_defined.empty())
97 {
98 const exprt current = to_be_defined.top();
99 if(push_dependencies_needed(current))
100 continue;
101 if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
102 {
103 const irep_idt &identifier = symbol_expr->get_identifier();
104 const symbolt *symbol = nullptr;
105 if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
106 {
107 const smt_declare_function_commandt function{
109 identifier, convert_type_to_smt_sort(symbol_expr->type())),
110 {}};
111 expression_identifiers.emplace(*symbol_expr, function.identifier());
112 solver_process->send(function);
113 }
114 else
115 {
116 if(push_dependencies_needed(symbol->value))
117 continue;
118 const smt_define_function_commandt function{
119 symbol->name, {}, convert_expr_to_smt(symbol->value)};
120 expression_identifiers.emplace(*symbol_expr, function.identifier());
121 solver_process->send(function);
122 }
123 }
124 to_be_defined.pop();
125 }
126}
127
129 const namespacet &_ns,
130 std::unique_ptr<smt_base_solver_processt> _solver_process,
131 message_handlert &message_handler)
132 : ns{_ns},
133 number_of_solver_calls{0},
134 solver_process(std::move(_solver_process)),
135 log{message_handler}
136{
137 solver_process->send(
140 smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
141}
142
144 const exprt &expr)
145{
146 if(
149 {
150 return;
151 }
152
155 "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
156 expression_handle_identifiers.emplace(expr, function.identifier());
157 solver_process->send(function);
158}
159
161{
162 log.debug() << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
164 return expr;
165}
166
168 const exprt &expr,
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)
173{
174 const auto handle_find_result = expression_handle_identifiers.find(expr);
175 if(handle_find_result != expression_handle_identifiers.cend())
176 return handle_find_result->second;
177 const auto expr_find_result = expression_identifiers.find(expr);
178 if(expr_find_result != expression_identifiers.cend())
179 return expr_find_result->second;
180 return {};
181}
182
184{
185 log.debug() << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
186 optionalt<smt_termt> descriptor =
188 if(!descriptor)
189 {
190 if(gather_dependent_expressions(expr).empty())
191 {
192 descriptor = convert_expr_to_smt(expr);
193 }
194 else
195 {
196 const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
197 INVARIANT(
198 symbol_expr, "Unhandled expressions are expected to be symbols");
199 // Note this case is currently expected to be encountered during trace
200 // generation for -
201 // * Steps which were removed via --slice-formula.
202 // * Getting concurrency clock values.
203 // The below implementation which returns the given expression was chosen
204 // based on the implementation of `smt2_convt::get` in the non-incremental
205 // smt2 decision procedure.
206 log.warning()
207 << "`get` attempted for unknown symbol, with identifier - \n"
208 << symbol_expr->get_identifier() << messaget::eom;
209 return expr;
210 }
211 }
212 const smt_get_value_commandt get_value_command{*descriptor};
213 const smt_responset response =
214 get_response_to_command(*solver_process, get_value_command);
215 const auto get_value_response = response.cast<smt_get_value_responset>();
216 if(!get_value_response)
217 {
219 "Expected get-value response from solver, but received - " +
220 response.pretty()};
221 }
222 if(get_value_response->pairs().size() > 1)
223 {
225 "Expected single valuation pair in get-value response from solver, but "
226 "received multiple pairs - " +
227 response.pretty()};
228 }
230 get_value_response->pairs()[0].get().value(), expr.type());
231}
232
234 std::ostream &out) const
235{
236 UNIMPLEMENTED_FEATURE("printing of assignments.");
237}
238
239std::string
241{
242 return "incremental SMT2 solving via " + solver_process->description();
243}
244
245std::size_t
247{
249}
250
252{
254 log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
255 << ") -\n " << expr.pretty(2, 0) << messaget::eom;
256
258 auto converted_term = [&]() -> smt_termt {
259 const auto expression_handle_identifier =
261 if(expression_handle_identifier != expression_handle_identifiers.cend())
262 return expression_handle_identifier->second;
263 else
264 return convert_expr_to_smt(expr);
265 }();
266 if(!value)
267 converted_term = smt_core_theoryt::make_not(converted_term);
268 solver_process->send(smt_assert_commandt{converted_term});
269}
270
272 const std::vector<exprt> &assumptions)
273{
274 for(const auto &assumption : assumptions)
275 {
277 "pushing of assumption:\n " + assumption.pretty(2, 0));
278 }
279 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
280}
281
283{
284 UNIMPLEMENTED_FEATURE("`push`.");
285}
286
288{
289 UNIMPLEMENTED_FEATURE("`pop`.");
290}
291
294 const smt_check_sat_response_kindt &response_kind)
295{
296 if(response_kind.cast<smt_sat_responset>())
298 if(response_kind.cast<smt_unsat_responset>())
300 if(response_kind.cast<smt_unknown_responset>())
303}
304
306{
308 const smt_responset result =
310 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
311 {
312 if(check_sat_response->kind().cast<smt_unknown_responset>())
313 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
314 return lookup_decision_procedure_result(check_sat_response->kind());
315 }
316 if(const auto problem = get_problem_messages(result))
317 throw analysis_exceptiont{*problem};
318 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
319}
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.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:245
typet & type()
Return the type of the expression.
Definition expr.h:82
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
bool is_nil() const
Definition irep.h:376
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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 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.
const sub_classt * cast() const &
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:81
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const sub_classt * cast() const &
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
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)
Definition irep.h:47
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
nonstd::optional< T > optionalt
Definition optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:524
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)
Definition invariant.h:517
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:173
bool can_cast_type< bool_typet >(const typet &base)
Definition std_types.h:44
Symbol table entry.