simple-netlist: do not label next-state value of nondet nodes

Nondet nodes do not have a next-state value; hence, do not label those.

Author: kroening

src/trans-netlist/aig.h

@@ -118,6 +118,7 @@ class aigt {
   // label a node
   void label(literalt l, const std::string &label)
   {
+    PRECONDITION(l.is_constant() || l.var_no() < number_of_nodes());
     labeling[label] = l;
   }
 

src/trans-netlist/trans_to_netlist_simple.cpp

@@ -123,7 +123,9 @@ void convert_trans_to_netlist_simplet::operator()(
         label += '[' + std::to_string(bit_nr) + ']';
 
       dest.label(var.bits[bit_nr].current, label);
-      dest.label(var.bits[bit_nr].next, label + '\'');
+
+      if(var.has_next())
+        dest.label(var.bits[bit_nr].next, label + '\'');
     }
   }
 }
@@ -140,8 +142,11 @@ void convert_trans_to_netlist_simplet::allocate_nodes(netlistt &dest)
       bit.current = dest.new_var_node();
 
       // use a primary input as AIG node for the next state value
-      bit.next = dest.new_var_node();
-      dest.var_map.record_as_nondet(bit.next.var_no());
+      if(var.has_next())
+      {
+        bit.next = dest.new_var_node();
+        dest.var_map.record_as_nondet(bit.next.var_no());
+      }
     }
   }
 }

src/trans-netlist/var_map.cpp

@@ -294,19 +294,22 @@ void var_mapt::output(std::ostream &out) const
         out << l_c.var_no();
       }
 
-      out << "->";
-
-      literalt l_n = var.bits[i].next;
-
-      if(l_n.is_true())
-        out << "true";
-      else if(l_n.is_false())
-        out << "false";
-      else
+      if(var.has_next())
       {
-        if(l_n.sign())
-          out << "!";
-        out << l_n.var_no();
+        out << "->";
+
+        literalt l_n = var.bits[i].next;
+
+        if(l_n.is_true())
+          out << "true";
+        else if(l_n.is_false())
+          out << "false";
+        else
+        {
+          if(l_n.sign())
+            out << "!";
+          out << l_n.var_no();
+        }
       }
 
       out << " ";

src/trans-netlist/var_map.h

@@ -33,9 +33,17 @@ class var_mapt
 
     inline bool is_latch() const { return vartype==vartypet::LATCH; }
     inline bool is_input() const { return vartype==vartypet::INPUT; }
+    inline bool is_output() const
+    {
+      return vartype == vartypet::OUTPUT;
+    }
     inline bool is_wire() const { return vartype==vartypet::WIRE; }
     inline bool is_nondet() const { return vartype==vartypet::NONDET; }
-    
+    bool has_next() const
+    {
+      return is_latch() || is_input() || is_wire() || is_output();
+    }
+
     struct bitt
     {
       // these are not guaranteed to be positive