cprover
Loading...
Searching...
No Matches
smt2_incremental_decision_procedure.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
5#include <util/arith_tools.h>
8#include <util/c_types.h>
9#include <util/range.h>
10#include <util/simplify_expr.h>
11#include <util/std_expr.h>
13
25
26#include <stack>
27#include <unordered_set>
28
32 smt_base_solver_processt &solver_process,
33 const smt_commandt &command,
34 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
35{
36 solver_process.send(command);
37 auto response = solver_process.receive_response(identifier_table);
38 if(response.cast<smt_success_responset>())
39 return solver_process.receive_response(identifier_table);
40 else
41 return response;
42}
43
46static std::optional<std::string>
48{
49 if(const auto error = response.cast<smt_error_responset>())
50 {
51 return "SMT solver returned an error message - " +
52 id2string(error->message());
53 }
54 if(response.cast<smt_unsupported_responset>())
55 {
56 return {"SMT solver does not support given command."};
57 }
58 return {};
59}
60
73static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
74{
75 std::vector<exprt> dependent_expressions;
76
77 std::stack<const exprt *> stack;
78 stack.push(&root_expr);
79
80 while(!stack.empty())
81 {
82 const exprt &expr_node = *stack.top();
83 stack.pop();
84 if(
85 can_cast_expr<symbol_exprt>(expr_node) ||
86 can_cast_expr<array_exprt>(expr_node) ||
90 {
91 dependent_expressions.push_back(expr_node);
92 }
93 // The decision procedure does not depend on the values inside address of
94 // code typed expressions. We can build the address without knowing the
95 // value at that memory location. In this case the hypothetical compiled
96 // machine instructions at the address are not relevant to solving, only
97 // representing *which* function a pointer points to is needed.
98 const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
99 if(address_of && can_cast_type<code_typet>(address_of->object().type()))
100 continue;
101 for(auto &operand : expr_node.operands())
102 stack.push(&operand);
103 }
104 return dependent_expressions;
105}
106
108 const array_exprt &array,
109 const smt_identifier_termt &array_identifier)
110{
111 identifier_table.emplace(array_identifier.identifier(), array_identifier);
112 const std::vector<exprt> &elements = array.operands();
113 const typet &index_type = array.type().index_type();
114 for(std::size_t i = 0; i < elements.size(); ++i)
115 {
116 const smt_termt index = convert_expr_to_smt(from_integer(i, index_type));
117 const smt_assert_commandt element_definition{smt_core_theoryt::equal(
118 smt_array_theoryt::select(array_identifier, index),
119 convert_expr_to_smt(elements.at(i)))};
120 solver_process->send(element_definition);
121 }
122}
123
125 const array_of_exprt &array,
126 const smt_identifier_termt &array_identifier)
127{
128 const smt_sortt index_type =
130 const smt_identifier_termt array_index_identifier{
131 id2string(array_identifier.identifier()) + "_index", index_type};
132 const smt_termt element_value = convert_expr_to_smt(array.what());
133
134 const smt_assert_commandt elements_definition{smt_forall_termt{
135 {array_index_identifier},
137 smt_array_theoryt::select(array_identifier, array_index_identifier),
138 element_value)}};
139 solver_process->send(elements_definition);
140}
141
143 const string_constantt &string,
144 const smt_identifier_termt &array_identifier)
145{
146 initialize_array_elements(string.to_array_expr(), array_identifier);
147}
148
149template <typename t_exprt>
151 const t_exprt &array)
152{
153 const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
154 INVARIANT(
155 array_sort.cast<smt_array_sortt>(),
156 "Converting array typed expression to SMT should result in a term of array "
157 "sort.");
158 const smt_identifier_termt array_identifier{
159 "array_" + std::to_string(array_sequence()), array_sort};
160 solver_process->send(smt_declare_function_commandt{array_identifier, {}});
161 initialize_array_elements(array, array_identifier);
162 expression_identifiers.emplace(array, array_identifier);
163}
164
166 const exprt &expr,
167 const irep_idt &symbol_identifier,
168 const std::unique_ptr<smt_base_solver_processt> &solver_process,
169 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
170 &expression_identifiers,
171 std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
172{
173 const smt_declare_function_commandt function{
175 symbol_identifier, convert_type_to_smt_sort(expr.type())),
176 {}};
177 expression_identifiers.emplace(expr, function.identifier());
178 identifier_table.emplace(symbol_identifier, function.identifier());
179 solver_process->send(function);
180}
181
185 const exprt &expr)
186{
187 std::unordered_set<exprt, irep_hash> seen_expressions =
189 .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
190 return expr_identifier.first;
191 });
192 std::stack<exprt> to_be_defined;
193 const auto push_dependencies_needed = [&](const exprt &expr) {
194 bool result = false;
195 for(const auto &dependency : gather_dependent_expressions(expr))
196 {
197 if(!seen_expressions.insert(dependency).second)
198 continue;
199 result = true;
200 to_be_defined.push(dependency);
201 }
202 return result;
203 };
204 push_dependencies_needed(expr);
205 while(!to_be_defined.empty())
206 {
207 const exprt current = to_be_defined.top();
208 if(push_dependencies_needed(current))
209 continue;
210 if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
211 {
213 *symbol_expr,
214 symbol_expr->get_identifier(),
218 }
219 else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
220 define_array_function(*array_expr);
221 else if(
222 const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
223 {
224 define_array_function(*array_of_expr);
225 }
226 else if(
227 const auto string = expr_try_dynamic_cast<string_constantt>(current))
228 {
229 define_array_function(*string);
230 }
231 else if(
232 const auto nondet_symbol =
234 {
236 *nondet_symbol,
237 nondet_symbol->get_identifier(),
241 }
242 to_be_defined.pop();
243 }
244}
245
249 exprt expr,
250 const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
251 &expression_identifiers)
252{
253 expr.visit_pre([&](exprt &node) -> void {
254 auto find_result = expression_identifiers.find(node);
255 if(find_result == expression_identifiers.cend())
256 return;
257 const auto type = find_result->first.type();
258 node = symbol_exprt{find_result->second.identifier(), type};
259 });
260 return expr;
261}
262
264 const namespacet &_ns,
265 std::unique_ptr<smt_base_solver_processt> _solver_process,
266 message_handlert &message_handler)
267 : ns{_ns},
269 solver_process(std::move(_solver_process)),
270 log{message_handler},
272 struct_encoding{_ns}
273{
274 solver_process->send(
276 solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
277 solver_process->send(object_size_function.declaration);
279}
280
282{
283 expr.visit_pre([&ns](exprt &expr) {
284 if(
285 auto prophecy_r_or_w_ok =
287 {
288 expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns);
289 }
290 else if(
291 auto prophecy_pointer_in_range =
293 {
294 expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns);
295 }
296 });
297 return expr;
298}
299
301{
302 expr.visit_pre([](exprt &expr) {
303 if(auto zero_extend = expr_try_dynamic_cast<zero_extend_exprt>(expr))
304 {
305 expr = zero_extend->lower();
306 }
307 });
308 return expr;
309}
310
312 const exprt &in_expr)
313{
314 if(
315 expression_handle_identifiers.find(in_expr) !=
317 {
318 return;
319 }
320
321 const exprt lowered_expr = lower(in_expr);
322
323 define_dependent_functions(lowered_expr);
325 "B" + std::to_string(handle_sequence()),
326 {},
327 convert_expr_to_smt(lowered_expr)};
328 expression_handle_identifiers.emplace(in_expr, function.identifier());
329 identifier_table.emplace(
330 function.identifier().identifier(), function.identifier());
331 solver_process->send(function);
332}
333
335 const exprt &expr)
336{
337 expr.visit_post(
338 [&](const exprt &expr_node)
339 {
340 if(!can_cast_type<array_typet>(expr_node.type()))
341 return;
342 if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
343 {
344 const auto index_expr = with_expr->where();
345 const auto index_term = convert_expr_to_smt(index_expr);
346 const auto index_identifier =
347 "index_" + std::to_string(index_sequence());
348 const auto index_definition =
349 smt_define_function_commandt{index_identifier, {}, index_term};
351 index_expr, index_definition.identifier());
352 identifier_table.emplace(
353 index_identifier, index_definition.identifier());
354 solver_process->send(
355 smt_define_function_commandt{index_identifier, {}, index_term});
356 }
357 });
358}
359
361 exprt root_expr)
362{
363 root_expr.visit_pre([&](exprt &node) {
365 {
366 const auto instance = "padding_" + std::to_string(padding_sequence());
367 const auto term =
370 node = symbol_exprt{instance, node.type()};
371 }
372 });
373 return root_expr;
374}
375
378{
380 const exprt substituted = substitute_defined_padding(
384 substituted,
385 ns,
388 object_size_function.make_application,
389 is_dynamic_object_function.make_application);
390 return ::convert_expr_to_smt(
391 substituted,
394 object_size_function.make_application,
395 is_dynamic_object_function.make_application);
396}
397
399{
400 log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
401 debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
402 });
404 return expr;
405}
406
407std::optional<smt_termt>
409{
410 // Lookup the non-lowered form first.
411 const auto handle_find_result = expression_handle_identifiers.find(expr);
412 if(handle_find_result != expression_handle_identifiers.cend())
413 return handle_find_result->second;
414 const auto expr_find_result = expression_identifiers.find(expr);
415 if(expr_find_result != expression_identifiers.cend())
416 return expr_find_result->second;
417
418 // If that didn't yield any results, then try the lowered form.
419 const exprt lowered_expr = lower(expr);
420 const auto lowered_handle_find_result =
421 expression_handle_identifiers.find(lowered_expr);
422 if(lowered_handle_find_result != expression_handle_identifiers.cend())
423 return lowered_handle_find_result->second;
424 const auto lowered_expr_find_result =
425 expression_identifiers.find(lowered_expr);
426 if(lowered_expr_find_result != expression_identifiers.cend())
427 return lowered_expr_find_result->second;
428 return {};
429}
430
432 const smt_termt &array,
433 const array_typet &type) const
434{
435 INVARIANT(
436 type.is_complete(), "Array size is required for getting array values.");
437 const auto size = numeric_cast<std::size_t>(get(type.size()));
438 INVARIANT(
439 size,
440 "Size of array must be convertible to std::size_t for getting array value");
441 std::vector<exprt> elements;
442 const auto index_type = type.index_type();
443 elements.reserve(*size);
444 for(std::size_t index = 0; index < size; ++index)
445 {
446 const auto index_term = ::convert_expr_to_smt(
447 from_integer(index, index_type),
450 object_size_function.make_application,
451 is_dynamic_object_function.make_application);
452 auto element = get_expr(
453 smt_array_theoryt::select(array, index_term), type.element_type());
454 if(!element)
455 return {};
456 elements.push_back(std::move(*element));
457 }
458 return array_exprt{elements, type};
459}
460
462 const smt_termt &struct_term,
463 const struct_tag_typet &type) const
464{
465 const auto encoded_result =
466 get_expr(struct_term, struct_encoding.encode(type));
467 if(!encoded_result)
468 return {};
469 return {struct_encoding.decode(*encoded_result, type)};
470}
471
473 const smt_termt &union_term,
474 const union_tag_typet &type) const
475{
476 const auto encoded_result =
477 get_expr(union_term, struct_encoding.encode(type));
478 if(!encoded_result)
479 return {};
480 return {struct_encoding.decode(*encoded_result, type)};
481}
482
484 const smt_termt &descriptor,
485 const typet &type) const
486{
487 if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
488 {
489 if(array_type->is_incomplete())
490 return {};
491 return get_expr(descriptor, *array_type);
492 }
493 if(const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
494 {
495 return get_expr(descriptor, *struct_type);
496 }
497 if(const auto union_type = type_try_dynamic_cast<union_tag_typet>(type))
498 {
499 return get_expr(descriptor, *union_type);
500 }
501 const smt_get_value_commandt get_value_command{descriptor};
502 const smt_responset response = get_response_to_command(
503 *solver_process, get_value_command, identifier_table);
504 const auto get_value_response = response.cast<smt_get_value_responset>();
505 if(!get_value_response)
506 {
508 "Expected get-value response from solver, but received - " +
509 response.pretty()};
510 }
511 if(get_value_response->pairs().size() > 1)
512 {
514 "Expected single valuation pair in get-value response from solver, but "
515 "received multiple pairs - " +
516 response.pretty()};
517 }
519 get_value_response->pairs()[0].get().value(), type, ns);
520}
521
522// This is a fall back which builds resulting expression based on getting the
523// values of its operands. It is used during trace building in the case where
524// certain kinds of expression appear on the left hand side of an
525// assignment. For example in the following trace assignment -
526// `byte_extract_little_endian(x, offset) = 1`
527// `::get` will be called on `byte_extract_little_endian(x, offset)` and
528// we build a resulting expression where `x` and `offset` are substituted
529// with their values.
531 const exprt &expr,
532 const stack_decision_proceduret &decision_procedure)
533{
534 exprt copy = expr;
535 for(auto &op : copy.operands())
536 {
537 exprt eval_op = decision_procedure.get(op);
538 if(eval_op.is_nil())
539 return nil_exprt{};
540 op = std::move(eval_op);
541 }
542 return copy;
543}
544
546{
547 log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
548 debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
549 });
550 auto descriptor = [&]() -> std::optional<smt_termt> {
551 if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
552 {
553 const auto array = get_identifier(index_expr->array());
554 const auto index = get_identifier(index_expr->index());
555 if(!array || !index)
556 return {};
557 return smt_array_theoryt::select(*array, *index);
558 }
559 if(auto identifier_descriptor = get_identifier(expr))
560 {
561 return identifier_descriptor;
562 }
563 const exprt lowered = lower(expr);
564 if(gather_dependent_expressions(lowered).empty())
565 {
566 INVARIANT(
568 "Objects in expressions being read should already be tracked from "
569 "point of being set/handled.");
570 return ::convert_expr_to_smt(
571 lowered,
574 object_size_function.make_application,
575 is_dynamic_object_function.make_application);
576 }
577 return {};
578 }();
579 if(!descriptor)
580 {
583 "symbol expressions must have a known value",
585 return build_expr_based_on_getting_operands(expr, *this);
586 }
587 if(auto result = get_expr(*descriptor, expr.type()))
588 return std::move(*result);
589 return expr;
590}
591
593 std::ostream &out) const
594{
595 UNIMPLEMENTED_FEATURE("printing of assignments.");
596}
597
598std::string
600{
601 return "incremental SMT2 solving via " + solver_process->description();
602}
603
604std::size_t
609
611 const exprt &in_expr,
612 bool value)
613{
614 log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
615 debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
616 << in_expr.pretty(2, 0) << messaget::eom;
617 });
618 const exprt lowered_expr = lower(in_expr);
620
621 define_dependent_functions(lowered_expr);
622 auto converted_term = [&]() -> smt_termt {
623 const auto expression_handle_identifier =
624 expression_handle_identifiers.find(lowered_expr);
625 if(expression_handle_identifier != expression_handle_identifiers.cend())
626 return expression_handle_identifier->second;
627 else
628 return convert_expr_to_smt(lowered_expr);
629 }();
630 if(!value)
631 converted_term = smt_core_theoryt::make_not(converted_term);
632 solver_process->send(smt_assert_commandt{converted_term});
633}
634
636 const std::vector<exprt> &assumptions)
637{
638 for(const auto &assumption : assumptions)
639 {
641 "pushing of assumption:\n " + assumption.pretty(2, 0));
642 }
643 UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
644}
645
650
655
656[[nodiscard]] static decision_proceduret::resultt
668
670{
672 for(const auto &key_value : object_map)
673 {
674 const decision_procedure_objectt &object = key_value.second;
675 if(object_properties_defined[object.unique_id])
676 continue;
677 else
678 object_properties_defined[object.unique_id] = true;
679 define_dependent_functions(object.size);
680 solver_process->send(object_size_function.make_definition(
681 object.unique_id, convert_expr_to_smt(object.size)));
682 solver_process->send(is_dynamic_object_function.make_definition(
683 object.unique_id, object.is_dynamic));
684 }
685}
686
688{
689 const exprt lowered = struct_encoding.encode(lower_zero_extend(
692 ns),
693 ns));
694 log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
695 if(lowered != expression)
696 debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom;
697 });
698 return lowered;
699}
700
703{
708 if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
709 {
710 if(check_sat_response->kind().cast<smt_unknown_responset>())
711 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
712 return lookup_decision_procedure_result(check_sat_response->kind());
713 }
714 if(const auto problem = get_problem_messages(result))
715 throw analysis_exceptiont{*problem};
716 throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
717}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
API to expression classes for bitvectors.
Expression classes for byte-level operators.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Array constructor from list of elements.
Definition std_expr.h:1621
const array_typet & type() const
Definition std_expr.h:1628
Array constructor from single element.
Definition std_expr.h:1558
const array_typet & type() const
Definition std_expr.h:1565
exprt & what()
Definition std_expr.h:1575
Arrays with given size.
Definition std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:34
bool is_complete() const
Definition std_types.h:852
const exprt & size() const
Definition std_types.h:840
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
resultt
Result of running the decision procedure.
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
Definition expr.cpp:198
operandst & operands()
Definition expr.h:94
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
bool is_nil() const
Definition irep.h:368
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3209
smt_object_sizet object_size_function
Implementation of the SMT formula for the object size function.
size_t number_of_solver_calls
The number of times dec_solve() has been called.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_identifiers
As part of the decision procedure's overall translation of CBMCs exprts into SMT terms,...
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...
exprt lower(exprt expression) const
Performs a combination of transformations which reduces the set of possible expression forms by expre...
exprt substitute_defined_padding(exprt expr)
In the case where lowering passes insert instances of the anonymous nondet_padding_exprt,...
std::optional< exprt > get_expr(const smt_termt &descriptor, const typet &type) const
Gets the value of descriptor from the solver and returns the solver response expressed as an exprt of...
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.
smt_is_dynamic_objectt is_dynamic_object_function
Implementation of the SMT formula for the dynamic object status lookup function.
void ensure_handle_for_expr_defined(const exprt &expr)
If a function has not been defined for handling expr, then a new function is defined.
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 initialize_array_elements(const array_exprt &array, const smt_identifier_termt &array_identifier)
Generate and send to the SMT solver clauses asserting that each array element is as specified by arra...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
messaget log
For reporting errors, warnings and debugging information back to the user.
void pop() override
Pop whatever is on top of the stack.
std::optional< smt_termt > get_identifier(const exprt &expr) const
std::unordered_map< irep_idt, smt_identifier_termt > identifier_table
This maps from the unsorted/untyped string/symbol for the identifiers which we have declared in SMT s...
smt_object_mapt object_map
This map is used to track object related state.
std::vector< bool > object_properties_defined
The size of each object and the dynamic object stus is separately defined as a pre-solving step.
void define_object_properties()
Sends the solver the definitions of the object sizes and dynamic memory statuses.
smt_termt convert_expr_to_smt(const exprt &expr)
Add objects in expr to object_map if needed and convert to smt.
const namespacet & ns
Namespace for looking up the expressions which symbol_exprts relate to.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
type_size_mapt pointer_sizes_map
Precalculated type sizes used for pointer arithmetic.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_handle_identifiers
When the handle(exprt) member function is called, the decision procedure commands the SMT solver to d...
std::unique_ptr< smt_base_solver_processt > solver_process
For handling the lifetime of and communication with the separate SMT 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'.
smt2_incremental_decision_proceduret(const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)
void define_array_function(const t_exprt &array)
Defines a function of array sort and asserts the element values from array_exprt or array_of_exprt.
static const smt_function_application_termt::factoryt< selectt > select
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
virtual smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)=0
const sub_classt * cast() const &
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< nott > make_not
const smt_identifier_termt & identifier() const
const smt_identifier_termt & identifier() const
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:93
irep_idt identifier() const
Definition smt_terms.cpp:81
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const sub_classt * cast() const &
const sub_classt * cast() const &
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Expression to hold a symbol (variable)
Definition std_expr.h:131
The type of an expression, extends irept.
Definition type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
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)
exprt lower_enum(exprt expr, const namespacet &ns)
Function to lower expr and its sub-expressions containing enum types.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
STL namespace.
Expressions for use in incremental SMT2 decision procedure.
void track_expression_objects(const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)
Finds all the object expressions in the given expression and adds them to the object map for cases wh...
bool objects_are_already_tracked(const exprt &expression, const smt_object_mapt &object_map)
Finds whether all base object expressions in the given expression are already tracked in the given ob...
smt_object_mapt initial_smt_object_map()
Constructs an initial object map containing the null object.
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition padding.cpp:154
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
exprt simplify_expr(exprt src, const namespacet &ns)
static exprt lower_rw_ok_pointer_in_range(exprt expr, const namespacet &ns)
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 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 ...
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,...
static decision_proceduret::resultt lookup_decision_procedure_result(const smt_check_sat_response_kindt &response_kind)
static exprt build_expr_based_on_getting_operands(const exprt &expr, const stack_decision_proceduret &decision_procedure)
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.
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 follo...
static exprt lower_zero_extend(exprt expr, const namespacet &ns)
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition invariant.h:549
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
Information the decision procedure holds about each object.
void associate_pointer_sizes(const exprt &expression, const namespacet &ns, type_size_mapt &type_size_map, const smt_object_mapt &object_map, const smt_object_sizet::make_applicationt &object_size, const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object)
This function populates the (pointer) type -> size map.
Utilities for making a map of types to associated sizes.
dstringt irep_idt