generate stable AIGs

To remove nondeterminism when generating AIGs, sort the identifiers before
allocating netlist nodes to them.

Author: kroening

regression/ebmc/smv-netlist/s_until1.desc

@@ -1,8 +1,8 @@
 CORE
 s_until1.sv
 --smv-netlist
-^LTLSPEC \(\!node144\) U node151$
-^LTLSPEC TRUE U node158$
+^LTLSPEC \(\!node144\) U node51$
+^LTLSPEC TRUE U node151$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/trans-netlist/trans_to_netlist.cpp

@@ -264,7 +264,22 @@ void convert_trans_to_netlistt::map_vars(
     }
   };
 
-  for_all_module_symbols(symbol_table, module, update_dest_var_map);
+  // get the symbols in the given module
+  std::vector<const symbolt *> module_symbols;
+
+  for(const auto &symbol_it : symbol_table.symbols)
+    if(symbol_it.second.module == module)
+      module_symbols.push_back(&symbol_it.second);
+
+  // we sort them to get a stable netlist
+  std::sort(
+    module_symbols.begin(),
+    module_symbols.end(),
+    [](const symbolt *a, const symbolt *b)
+    { return a->name.compare(b->name) < 0; });
+
+  for(auto symbol_ptr : module_symbols)
+    update_dest_var_map(*symbol_ptr);
 }
 
 /*******************************************************************\

src/util/ebmc_util.h

@@ -15,18 +15,6 @@
 
 #include <solvers/sat/cnf.h>
 
-template <typename F>
-void for_all_module_symbols(const symbol_tablet &symbol_table,
-                            const irep_idt &module_name, F &&f) {
-  using symbol_pairt = typename symbol_tablet::iteratort::value_type;
-  std::for_each(symbol_table.begin(), symbol_table.end(),
-                [&module_name, &f](const symbol_pairt &symbol_pair) {
-                  const auto &symbol = symbol_pair.second;
-                  if (symbol.module == module_name)
-                    f(symbol);
-                });
-}
-
 // This function is legacy, and will be gradually removed.
 // Consider to_integer(constant_exprt, mp_integer &) or numerical_cast<mp_integer>(...).
 inline bool to_integer_non_constant(const exprt &expr, mp_integer &int_value)