Add SMT data processing / flow sequence documentation

Author: thomasspriggs

src/solvers/smt2_incremental/README.md

@@ -1,5 +1,7 @@
 # Incremental SMT backend
 
+## General usage
+
 CBMC comes with a solver-agnostic incremental SMT backend.
 
 The SMT incremental backend supports the following `C` features:
@@ -40,3 +42,60 @@ removed from the formula to be converted.
 
 As we move forward with our array-support implementation, we anticipate that the
 need for this extra flag will be diminished.
+
+## Internal code architecture
+
+### Overview of the sequence of data processing and data flow -
+
+1. Other parts of the cbmc code base send `exprt` based expressions to the
+decision procedure through the `handle`, `set_to` and `get` member functions.
+See the base class `decision_proceduret` for doxygen of these functions.
+
+2. The `smt2_incremental_decision_proceduret` is responsible for holding state
+and building commands to send to the solver. It uses `convert_expr_to_smt` for
+the state free (pure) portion of the `exprt` to `termt` conversions.
+
+3. `smt2_incremental_decision_proceduret` sends `smt_commandt` to
+`smt_piped_solver_processt`. Although `exprt` is broadly equivalent to `termt`,
+the terms must be part of a command giving them a broader meaning before they
+are sent to the solver.
+
+4. `smt_piped_solver_processt` uses the `smt_to_smt2_string` function to perform
+the conversion from the tree structure of the `smt_commandt` into the linear
+structure of the string for sending to the solver.
+
+5. `smt_piped_solver_processt` sends `std::string` to `piped_processt`.
+
+6. `piped_processt` has operating system specific implementations which use
+POSIX / Windows API calls to send the strings to the solver process via a pipe.
+Note that the solver is kept in a operating system separated process, not a
+thread. This supports multiprocessing with the solver ingesting commands whilst
+the cbmc process continues symex to generate the following commands.
+
+7. `piped_processt` receives output strings from the solver process using OS API
+calls and a buffer, when the `smt_piped_solver_processt` requests them.
+
+8. The response strings returned to `smt_solve_processt` are converted into type
+less parse trees in the form of raw `irept`s using `smt2irep`. `smt2irep` is
+essentially just an S-expression parser.
+
+9. `smt_piped_solver_processt` uses `validate_smt_response` to convert the
+`irept` parse tree into either a set of validation errors or a `smt_responset`.
+The case of validation errors is considered to be an error with the solver.
+Therefore an exception may be thrown for use as user feedback rather than
+violating an `INVARIANT` as would be the case for an internal cbmc error.
+
+10. The well sorted `smt_reponset` is then returned to the
+`smt2_incremental_decision_proceduret`.
+
+11. In the case of `smt2_incremental_decision_proceduret::get` the response is
+expected to be an `smt_get_value_responset`. The decision procedure uses
+`construct_value_expr_from_smt` to convert the value term in the response from
+the solver into an expression value. This requires information from the decision
+procedure about the kind of type the constructed expression should have. The
+reason for this is that the smt formula (although well sorted) does not encode
+cbmc's notion of types and a given value in SMT terms could correspond to
+multiple different types of cbmc expression.
+
+12. The constructed expression can then be returned to the rest of the cbmc code
+base outside the decision procedure.