extract code for outputting netlists as SMV

This extracts the code for outputting netlists as SMV files from the class,
and into a separate file.

Author: kroening

src/ebmc/ebmc_parse_options.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/help_formatter.h>
 #include <util/string2int.h>
 
+#include <trans-netlist/smv_netlist.h>
+
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
@@ -288,7 +290,7 @@ int ebmc_parse_optionst::doit()
       outfile.stream() << "-- Generated from "
                        << transition_system.main_symbol->name << '\n';
       outfile.stream() << '\n';
-      netlist.output_smv(outfile.stream());
+      smv_netlist(netlist, outfile.stream());
       return 0;
     }
 

src/trans-netlist/Makefile

@@ -1,19 +1,21 @@
 SRC = aig.cpp \
-      aig_terminals.cpp \
       aig_prop.cpp \
+      aig_terminals.cpp \
       bmc_map.cpp \
+      bv_varid.cpp \
+      compute_ct.cpp \
       counterexample_netlist.cpp \
       instantiate_netlist.cpp \
+      ldg.cpp \
+      map_aigs.cpp \
       netlist.cpp \
+      smv_netlist.cpp \
+      trans_to_netlist.cpp \
+      trans_trace.cpp \
       trans_trace_netlist.cpp \
-      var_map.cpp \
       unwind_netlist.cpp \
-      ldg.cpp \
-      compute_ct.cpp \
-      trans_trace.cpp \
-      trans_to_netlist.cpp \
-      map_aigs.cpp \
-      bv_varid.cpp
+      var_map.cpp \
+      # last line
 
 include ../config.inc
 include ../common

src/trans-netlist/netlist.cpp

@@ -8,14 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "netlist.h"
 
-#include <util/namespace.h>
-#include <util/symbol_table.h>
-
-#include <smvlang/expr2smv.h>
 #include <solvers/flattening/boolbv_width.h>
-#include <solvers/prop/literal_expr.h>
-#include <temporal-logic/temporal_logic.h>
-#include <verilog/sva_expr.h>
 
 #include <ctype.h>
 #include <sstream>
@@ -225,310 +218,3 @@ void netlistt::output_dot(std::ostream &out) const
     }
   }
 }
-
-/*******************************************************************\
-
-Function: netlistt::output_smv
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void netlistt::output_smv(std::ostream &out) const
-{
-  out << "MODULE main" << '\n';
-
-  out << '\n';
-  out << "-- Variables" << '\n';
-  out << '\n';
-
-  for(var_mapt::mapt::const_iterator
-      it=var_map.map.begin();
-      it!=var_map.map.end();
-      it++)
-  {
-    const var_mapt::vart &var=it->second;
-
-    for(unsigned i=0; i<var.bits.size(); i++)
-    {
-      if(var.is_latch())
-      {
-        out << "VAR " << id2smv(it->first);
-        if(var.bits.size()!=1) out << "[" << i << "]";
-        out << ": boolean;" << '\n';
-      }
-    }
-  }
-
-  out << '\n';
-  out << "-- Inputs" << '\n';
-  out << '\n';
-
-  for(var_mapt::mapt::const_iterator
-      it=var_map.map.begin();
-      it!=var_map.map.end();
-      it++)
-  {
-    const var_mapt::vart &var=it->second;
-
-    for(unsigned i=0; i<var.bits.size(); i++)
-    {
-      if(var.is_input())
-      {
-        out << "VAR " << id2smv(it->first);
-        if(var.bits.size()!=1) out << "[" << i << "]";
-        out << ": boolean;" << '\n';
-      }
-    }
-  }
-
-  out << '\n';
-  out << "-- AND Nodes" << '\n';
-  out << '\n';
-
-  for(unsigned node_nr=0; node_nr<nodes.size(); node_nr++)
-  {
-    const aig_nodet &node=nodes[node_nr];
-
-    if(node.is_and())
-    {
-      out << "DEFINE node" << node_nr << ":=";
-      print_smv(out, node.a);
-      out << " & ";
-      print_smv(out, node.b);
-      out << ";" << '\n';
-    }
-  }
-
-  out << '\n';
-  out << "-- Next state functions" << '\n';
-  out << '\n';
-
-  for(var_mapt::mapt::const_iterator
-      it=var_map.map.begin();
-      it!=var_map.map.end();
-      it++)
-  {
-    const var_mapt::vart &var=it->second;
-
-    for(unsigned i=0; i<var.bits.size(); i++)
-    {
-      if(var.is_latch())
-      {
-        out << "ASSIGN next(" << id2smv(it->first);
-        if(var.bits.size()!=1) out << "[" << i << "]";
-        out << "):=";
-        print_smv(out, var.bits[i].next);
-        out << ";" << '\n';
-      }
-    }
-  }
-
-  out << '\n';
-  out << "-- Initial state" << '\n';
-  out << '\n';
-
-  for(auto &initial_l : initial)
-  {
-    if(!initial_l.is_true())
-    {
-      out << "INIT ";
-      print_smv(out, initial_l);
-      out << '\n';
-    }
-  }
-
-  out << '\n';
-  out << "-- TRANS" << '\n';
-  out << '\n';
-
-  for(auto &trans_l : transition)
-  {
-    if(!trans_l.is_true())
-    {
-      out << "TRANS ";
-      print_smv(out, trans_l);
-      out << '\n';
-    }
-  }
-
-  out << '\n';
-  out << "-- Properties" << '\n';
-  out << '\n';
-
-  for(auto &[id, netlist_expr] : properties)
-  {
-    if(is_CTL(netlist_expr))
-    {
-      out << "-- " << id << '\n';
-      out << "CTLSPEC ";
-      print_smv(out, netlist_expr);
-      out << '\n';
-    }
-    else if(is_LTL(netlist_expr))
-    {
-      out << "-- " << id << '\n';
-      out << "LTLSPEC ";
-      print_smv(out, netlist_expr);
-      out << '\n';
-    }
-    else if(is_SVA(netlist_expr))
-    {
-      if(is_SVA_always_p(netlist_expr))
-      {
-        out << "-- " << id << '\n';
-        out << "CTLSPEC AG ";
-        print_smv(out, to_sva_always_expr(netlist_expr).op());
-        out << '\n';
-      }
-      else if(is_SVA_always_s_eventually_p(netlist_expr))
-      {
-        out << "-- " << id << '\n';
-        out << "CTLSPEC AG AF ";
-        print_smv(
-          out,
-          to_sva_s_eventually_expr(to_sva_always_expr(netlist_expr).op()).op());
-        out << '\n';
-      }
-      else
-      {
-        out << "-- " << id << '\n';
-        out << "-- not translated\n";
-        out << '\n';
-      }
-    }
-    else
-    {
-      // neither LTL nor CTL nor SVA
-      out << "-- " << id << '\n';
-      out << "-- not translated\n";
-      out << '\n';
-    }
-  }
-}
-
-/*******************************************************************\
-
-Function: netlistt::id2smv
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-std::string netlistt::id2smv(const irep_idt &id)
-{
-  std::string result;
-  
-  for(unsigned i=0; i<id.size(); i++)
-  {
-    const bool first = i == 0;
-    char ch=id[i];
-    if(
-      isalnum(ch) || ch == '_' || (ch == '.' && !first) ||
-      (ch == '#' && !first) || (ch == '-' && !first))
-    {
-      result+=ch;
-    }
-    else if(ch==':')
-    {
-      result+='.';
-      if((i-1)<id.size() && id[i+1]==':') i++;
-    }
-    else
-    {
-      result+='$';
-      result+=std::to_string(ch);
-      result+='$';
-    }
-  }
-  
-  return result;
-}
-
-/*******************************************************************\
-
-Function: netlistt::print_smv
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void netlistt::print_smv(
-  std::ostream& out,
-  literalt a) const
-{
-  if(a==const_literal(false))
-  {
-    out << "0";
-    return;
-  }
-  else if(a==const_literal(true))
-  {
-    out << "1";
-    return;
-  }
-
-  unsigned node_nr=a.var_no();
-  DATA_INVARIANT(node_nr < number_of_nodes(), "node_nr in range");
-
-  if(a.sign()) out << "!";
-
-  if(nodes[node_nr].is_and())
-    out << "node" << node_nr;
-  else if(nodes[node_nr].is_var())
-  {
-    const bv_varidt &varid=var_map.reverse(node_nr);
-    out << id2smv(varid.id);
-    const var_mapt::mapt::const_iterator v_it=var_map.map.find(varid.id);
-    if(v_it!=var_map.map.end() && v_it->second.bits.size()!=1)
-      out << '[' << varid.bit_nr << ']';
-  }
-  else
-    out << "unknown";
-}
-
-/*******************************************************************\
-
-Function: netlistt::print_smv
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void netlistt::print_smv(std::ostream &out, const exprt &expr) const
-{
-  symbol_tablet symbol_table;
-  namespacet ns{symbol_table};
-
-  // replace literal expressions by symbols
-
-  exprt replaced = expr;
-  replaced.visit_pre(
-    [this](exprt &node)
-    {
-      if(node.id() == ID_literal)
-      {
-        std::ostringstream buffer;
-        print_smv(buffer, to_literal_expr(node).get_literal());
-        node = symbol_exprt{buffer.str(), node.type()};
-      }
-    });
-
-  out << expr2smv(replaced, ns);
-}

src/trans-netlist/netlist.h

@@ -38,7 +38,6 @@ class netlistt:public aig_plus_constraintst
   using aigt::print;
   virtual void print(std::ostream &out) const;
   virtual void output_dot(std::ostream &out) const;
-  virtual void output_smv(std::ostream &out) const;
   virtual std::string label(unsigned n) const;
   virtual std::string dot_label(unsigned n) const;
 
@@ -59,11 +58,6 @@ class netlistt:public aig_plus_constraintst
   // which uses literal_exprt.
   using propertiest = std::map<irep_idt, exprt>;
   propertiest properties;
-
-protected:
-  static std::string id2smv(const irep_idt &id);
-  void print_smv(std::ostream &, literalt) const;
-  void print_smv(std::ostream &, const exprt &) const;
 };
 
 #endif