Make the order of SMT commands for sub-expressions deterministic

This makes the behaviour of the conversion predictable. This has the
advantage of being easier to unit test and reducing the possiblity of
hard to re-produce bugs.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -18,18 +18,21 @@
 
 /// \brief Find all sub expressions of the given \p expr which need to be
 ///   expressed as separate smt commands.
+/// \return A collection of sub expressions, which need to be expressed as
+///   separate smt commands. This collection is in traversal order. It will
+///   include duplicate subexpressions, which need to be removed by the caller
+///   in order to avoid duplicate definitions.
 /// \note This pass over \p expr is tightly coupled to the implementation of
 ///   `convert_expr_to_smt`. This is because any sub expressions which
 ///   `convert_expr_to_smt` translates into function applications, must also be
 ///   returned by this`gather_dependent_expressions` function.
-static std::unordered_set<exprt, irep_hash>
-gather_dependent_expressions(const exprt &expr)
+static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
 {
-  std::unordered_set<exprt, irep_hash> dependent_expressions;
+  std::vector<exprt> dependent_expressions;
   expr.visit_pre([&](const exprt &expr_node) {
     if(can_cast_expr<symbol_exprt>(expr_node))
     {
-      dependent_expressions.insert(expr_node);
+      dependent_expressions.push_back(expr_node);
     }
   });
   return dependent_expressions;

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -143,23 +143,23 @@ TEST_CASE(
       REQUIRE(
         sent_commands ==
         std::vector<smt_commandt>{
-          smt_declare_function_commandt{nondet_int_b_term, {}},
           smt_declare_function_commandt{nondet_int_a_term, {}},
-          smt_define_function_commandt{
-            "third_comparison",
-            {},
-            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
           smt_define_function_commandt{
             "forty_two", {}, smt_bit_vector_constant_termt{42, 16}},
+          smt_define_function_commandt{
+            "first_comparison",
+            {},
+            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
+          smt_declare_function_commandt{nondet_int_b_term, {}},
           smt_define_function_commandt{
             "second_comparison",
             {},
             smt_core_theoryt::make_not(
               smt_core_theoryt::equal(nondet_int_b_term, forty_two_term))},
           smt_define_function_commandt{
-            "first_comparison",
+            "third_comparison",
             {},
-            smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
+            smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
           smt_define_function_commandt{
             "comparison_conjunction",
             {},