diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 727dc9fe0ad..23b50799a5b 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -70,13 +70,21 @@ class smt2_incremental_decision_proceduret final /// Sends the solver the definitions of the object sizes. void define_object_sizes(); + /// Namespace for looking up the expressions which symbol_exprts relate to. + /// This includes the symbols defined outside of the decision procedure but + /// does not include any additional SMT function identifiers introduced by the + /// decision procedure. const namespacet &ns; - + /// The number of times `dec_solve()` has been called. size_t number_of_solver_calls; - + /// \brief For handling the lifetime of and communication with the separate + /// SMT solver process. + /// \note This may be mocked for unit testing purposes. std::unique_ptr solver_process; + /// For reporting errors, warnings and debugging information back to the user. messaget log; - + /// Generators of sequences of uniquely identifying numbers used for naming + /// SMT functions introduced by the decision procedure. class sequencet { size_t next_id = 0; @@ -87,14 +95,38 @@ class smt2_incremental_decision_proceduret final return next_id++; } } handle_sequence, array_sequence; - + /// When the `handle(exprt)` member function is called, the decision procedure + /// commands the SMT solver to define a new function corresponding to the + /// given expression. The mapping of the expressions to the function + /// identifiers is stored in this map so that when there is as subsequent + /// `get(exprt)` call for the same expression, the function identifier can be + /// requested from the solver, rather than reconverting the expression. std::unordered_map expression_handle_identifiers; + /// As part of the decision procedure's overall translation of CBMCs `exprt`s + /// into SMT terms, some subexpressions are substituted for separate SMT + /// functions. This map associates these sub-expressions to the identifiers of + /// the separated functions. This applies to `symbol_exprt` where it is fairly + /// natural to define the value of the symbol using a separate function, but + /// also to the expressions which define entire arrays. This includes + /// `array_exprt` for example and will additionally include other similar + /// array expressions when support for them is implemented. std::unordered_map expression_identifiers; + /// This map is used to track object related state. See documentation in + /// object_tracking.h for details. smt_object_mapt object_map; + /// The size of each object is separately defined as a pre-solving step. + /// `object_size_defined[object ID]` is set to true for objects where the size + /// has been defined. This is used to avoid defining the size of the same + /// object multiple times in the case where multiple rounds of solving are + /// carried out. std::vector object_size_defined; + /// Implementation of the SMT formula for the object size function. This is + /// stateful because it depends on the configuration of the number of object + /// bits and how many bits wide the size type is configured to be. smt_object_sizet object_size_function; + /// Precalculated type sizes used for pointer arithmetic. type_size_mapt pointer_sizes_map; };