bv_varidt now has next member

This adds a 'next' member to bv_varidt.

Author: kroening

src/ebmc/bdd_engine.cpp

@@ -286,7 +286,7 @@ void bdd_enginet::allocate_vars(const var_mapt &var_map)
           bit_nr<it.second.bits.size();
           bit_nr++)
       {
-        bv_varidt bv_varid(it.first, bit_nr);
+        bv_varidt bv_varid{it.first, bit_nr, false};
         vars[bv_varid].is_input=
           it.second.is_input() || it.second.is_nondet();
       }

src/trans-netlist/bv_varid.h

@@ -18,22 +18,28 @@ class bv_varidt
 public:
   irep_idt id;
   std::size_t bit_nr;
+  bool next;
 
   friend bool operator==(const bv_varidt &i1, const bv_varidt &i2)
   {
-    return i1.id==i2.id && i1.bit_nr==i2.bit_nr;
+    return i1.id == i2.id && i1.bit_nr == i2.bit_nr && i1.next == i2.next;
   }
 
   friend bool operator<(const bv_varidt &i1, const bv_varidt &i2)
   {
     if(i1.id==i2.id)
-      return i1.bit_nr<i2.bit_nr;
-
-    return i1.id<i2.id;
+    {
+      if(i1.bit_nr == i2.bit_nr)
+        return i1.next < i2.next;
+      else
+        return i1.bit_nr < i2.bit_nr;
+    }
+    else
+      return i1.id < i2.id;
   }
 
-  inline bv_varidt(const irep_idt &_id, std::size_t _bit_nr)
-    : id(_id), bit_nr(_bit_nr)
+  inline bv_varidt(const irep_idt &_id, std::size_t _bit_nr, bool _next)
+    : id(_id), bit_nr(_bit_nr), next(_next)
   { }
 
   std::string as_string() const;
@@ -47,7 +53,9 @@ static inline std::ostream & operator<< (std::ostream &out, const bv_varidt &v)
 struct bv_varidt_hash
 {
   size_t operator()(const bv_varidt &bv_varid) const
-  { return hash_string(bv_varid.id)^bv_varid.bit_nr; }
+  {
+    return hash_string(bv_varid.id) ^ bv_varid.bit_nr ^ bv_varid.next;
+  }
 };
 
 #endif

src/trans-netlist/trans_to_netlist.cpp

@@ -335,7 +335,7 @@ void convert_trans_to_netlistt::operator()(
 
     for(std::size_t bit_nr = 0; bit_nr < var.bits.size(); bit_nr++)
     {
-      bv_varidt bv_varid{v_it->first, bit_nr};
+      bv_varidt bv_varid{v_it->first, bit_nr, false};
       var_mapt::vart::bitt &bit=var.bits[bv_varid.bit_nr];
       lhs_entryt &entry=lhs_map[bv_varid];
       entry.bit=&bit;
@@ -392,7 +392,7 @@ void convert_trans_to_netlistt::operator()(
 
       if(it==dest.var_map.reverse_map.end())
       {
-        bv_varidt varid{"nondet", dest.var_map.nondets.size()};
+        bv_varidt varid{"nondet", dest.var_map.nondets.size(), false};
         var_mapt::vart &var=dest.var_map.map[varid.id];
         var.add_bit().current=literalt(n, false);
         var.vartype=var_mapt::vart::vartypet::NONDET;
@@ -603,7 +603,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
 
     for(std::size_t bit_nr = from; bit_nr <= to; bit_nr++)
     {
-      bv_varidt bv_varid{identifier, bit_nr};
+      bv_varidt bv_varid{identifier, bit_nr, false};
       lhs_mapt::iterator it=lhs_map.find(bv_varid);
 
       if(it==lhs_map.end())
@@ -768,7 +768,7 @@ void convert_trans_to_netlistt::add_equality_rec(
 
     for(std::size_t bit_nr = lhs_from; bit_nr != (lhs_to + 1); bit_nr++)
     {
-      bv_varidt bv_varid{identifier, bit_nr};
+      bv_varidt bv_varid{identifier, bit_nr, false};
       lhs_mapt::iterator it=
         lhs_map.find(bv_varid);
 

src/trans-netlist/var_map.cpp

@@ -59,7 +59,7 @@ void var_mapt::add(
 
   if(var.is_latch() || var.is_input())
   {
-    reverse_map.emplace(v_current, bv_varidt{id, bit_nr});
+    reverse_map.emplace(v_current, bv_varidt{id, bit_nr, false});
   }
 }