sort AIG variable map before output

To obtain deterministic results, sort the AIG variable map before outputting
it, or before outputting data based on the variable map.

Author: kroening

src/trans-netlist/counterexample_netlist.cpp

@@ -39,9 +39,7 @@ void show_state(
   std::cout << "Transition system state " << timeframe << "\n";
   std::cout << "----------------------------------------------------\n";
 
-  for(var_mapt::mapt::const_iterator
-      it=map.var_map.map.begin();
-      it!=map.var_map.map.end(); it++)
+  for(auto it : map.var_map.sorted())
   {
     const var_mapt::vart &var=it->second;
 

src/trans-netlist/ldg.cpp

@@ -59,11 +59,8 @@ void ldgt::compute(
     nodes[*l_it].is_source_latch=true;
 
   // get the next state nodes
-    
-  for(var_mapt::mapt::const_iterator
-      m_it=netlist.var_map.map.begin();
-      m_it!=netlist.var_map.map.end();
-      m_it++)
+
+  for(auto m_it : netlist.var_map.sorted())
   {
     const var_mapt::vart &var=m_it->second;
     if(var.is_latch())

src/trans-netlist/netlist.cpp

@@ -32,9 +32,8 @@ void netlistt::print(std::ostream &out) const
   out << '\n';
   out << "Next state functions:" << '\n';
 
-  for(var_mapt::mapt::const_iterator
-      it=var_map.map.begin();
-      it!=var_map.map.end(); it++)
+  // use a sorted var_map to get determistic output
+  for(auto it : var_map.sorted())
   {
     const var_mapt::vart &var=it->second;
 
@@ -190,11 +189,9 @@ void netlistt::output_dot(std::ostream &out) const
 {
   aigt::output_dot(out);
 
-  // add the sinks
-  for(var_mapt::mapt::const_iterator
-      it=var_map.map.begin();
-      it!=var_map.map.end();
-      it++)
+  // Add the sinks.
+  // Use a sorted var_map to get deterministic results.
+  for(auto it : var_map.sorted())
   {
     const var_mapt::vart &var=it->second;
 

src/trans-netlist/smv_netlist.cpp

@@ -127,17 +127,19 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   out << "-- Variables" << '\n';
   out << '\n';
 
+  // We use the sorted var map to get deterministic output
   auto &var_map = netlist.var_map;
+  const auto sorted_var_map = var_map.sorted();
 
-  for(auto &var_it : var_map.map)
+  for(auto var_it : sorted_var_map)
   {
-    const var_mapt::vart &var = var_it.second;
+    const var_mapt::vart &var = var_it->second;
 
     for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_latch())
       {
-        out << "VAR " << id2smv(var_it.first);
+        out << "VAR " << id2smv(var_it->first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << ": boolean;" << '\n';
@@ -149,15 +151,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   out << "-- Inputs" << '\n';
   out << '\n';
 
-  for(auto &var_it : var_map.map)
+  for(auto var_it : sorted_var_map)
   {
-    const var_mapt::vart &var = var_it.second;
+    const var_mapt::vart &var = var_it->second;
 
     for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_input())
       {
-        out << "VAR " << id2smv(var_it.first);
+        out << "VAR " << id2smv(var_it->first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << ": boolean;" << '\n';
@@ -189,15 +191,15 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
   out << "-- Next state functions" << '\n';
   out << '\n';
 
-  for(auto &var_it : var_map.map)
+  for(auto var_it : sorted_var_map)
   {
-    const var_mapt::vart &var = var_it.second;
+    const var_mapt::vart &var = var_it->second;
 
     for(std::size_t i = 0; i < var.bits.size(); i++)
     {
       if(var.is_latch())
       {
-        out << "ASSIGN next(" << id2smv(var_it.first);
+        out << "ASSIGN next(" << id2smv(var_it->first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << "):=";

src/trans-netlist/trans_trace_netlist.cpp

@@ -106,16 +106,16 @@ trans_tracet compute_trans_trace(
   trans_tracet dest;
 
   dest.states.reserve(bmc_map.get_no_timeframes());
-  
+
+  // use a sorted var_map to get deterministic results
+  const auto sorted_var_map = bmc_map.var_map.sorted();
+
   for(unsigned t=0; t<bmc_map.get_no_timeframes(); t++)
   {
     dest.states.push_back(trans_tracet::statet());
     trans_tracet::statet &state=dest.states.back();
-  
-    for(var_mapt::mapt::const_iterator
-        it=bmc_map.var_map.map.begin();
-        it!=bmc_map.var_map.map.end();
-        it++)
+
+    for(auto it : sorted_var_map)
     {
       const var_mapt::vart &var=it->second;
 

src/trans-netlist/unwind_netlist.cpp

@@ -83,10 +83,7 @@ void unwind(
   if(!last)
   {     
     // joining the latches between timeframe and timeframe+1
-    for(var_mapt::mapt::const_iterator
-        v_it=netlist.var_map.map.begin();
-        v_it!=netlist.var_map.map.end();
-        v_it++)
+    for(auto v_it : netlist.var_map.sorted())
     {
       const var_mapt::vart &var=v_it->second;
       if(var.is_latch())

src/trans-netlist/var_map.cpp

@@ -179,6 +179,35 @@ const bv_varidt &var_mapt::reverse(unsigned v) const
 
 /*******************************************************************\
 
+Function: var_mapt::sorted
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::vector<var_mapt::mapt::const_iterator> var_mapt::sorted() const
+{
+  using iteratort = mapt::const_iterator;
+  std::vector<iteratort> iterators;
+  iterators.reserve(map.size());
+
+  for(auto it = map.begin(); it != map.end(); it++)
+    iterators.push_back(it);
+
+  std::sort(
+    iterators.begin(),
+    iterators.end(),
+    [](iteratort a, iteratort b) { return a->first.compare(b->first) < 0; });
+
+  return iterators;
+}
+
+/*******************************************************************\
+
 Function: var_mapt::output
 
   Inputs:
@@ -193,14 +222,14 @@ void var_mapt::output(std::ostream &out) const
 {
   out << "Variable map:" << '\n';
 
-  for(mapt::const_iterator it=map.begin();
-      it!=map.end(); it++)
+  // sort by identifier to get stable output
+  for(auto map_it : sorted())
   {
-    const vart &var=it->second;
+    const vart &var = map_it->second;
 
     for(std::size_t i=0; i<var.bits.size(); i++)
     {
-      out << "  " << it->first;
+      out << "  " << map_it->first;
       if(var.bits.size()!=1) out << "[" << i << "]";
       out << "=";
 

src/trans-netlist/var_map.h

@@ -128,6 +128,8 @@ class var_mapt
     wires.clear();
     map.clear();
   }
+
+  std::vector<mapt::const_iterator> sorted() const;
 };
 
 #endif