smv-netlist: use expr2smv for property

The SMV to netlist conversion now uses expr2smv for outputting the property,
which enables outputting full LTL or CTL.

Author: kroening

regression/ebmc/smv-netlist/smv1.desc

@@ -0,0 +1,10 @@
+CORE
+smv1.smv
+--smv-netlist
+^MODULE main$
+^VAR smv\.main\.var\.x: boolean;$
+^ASSIGN next\(smv\.main\.var\.x\):=\!smv\.main\.var\.x;$
+^INIT !smv\.main\.var\.x$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/smv1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x: boolean;
+
+ASSIGN next(x):=!x;
+ASSIGN init(x):=FALSE;
+
+LTLSPEC G F x
+

regression/ebmc/smv-netlist/verilog1.desc

@@ -0,0 +1,10 @@
+CORE
+verilog1.sv
+--smv-netlist
+^MODULE main$
+^VAR Verilog\.main\.x: boolean;$
+^ASSIGN next\(Verilog\.main\.x\):=\!Verilog\.main\.x;$
+^INIT !Verilog\.main\.x$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-netlist/verilog1.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = !x;
+
+  always assert property (always s_eventually x);
+
+endmodule

src/trans-netlist/smv_netlist.cpp

@@ -88,21 +88,35 @@ void print_smv(const netlistt &netlist, std::ostream &out, const exprt &expr)
   symbol_tablet symbol_table;
   namespacet ns{symbol_table};
 
-  // replace literal expressions by symbols
+  class expr2smv_netlistt : public expr2smvt
+  {
+  public:
+    expr2smv_netlistt(const namespacet &ns, const netlistt &__netlist)
+      : expr2smvt(ns), netlist(__netlist)
+    {
+    }
 
-  exprt replaced = expr;
-  replaced.visit_pre(
-    [&netlist](exprt &node)
+  protected:
+    const netlistt &netlist;
+
+    resultt convert_rec(const exprt &expr) override
     {
-      if(node.id() == ID_literal)
+      if(expr.id() == ID_literal)
       {
         std::ostringstream buffer;
-        print_smv(netlist, buffer, to_literal_expr(node).get_literal());
-        node = symbol_exprt{buffer.str(), node.type()};
+        auto l = to_literal_expr(expr).get_literal();
+        print_smv(netlist, buffer, l);
+        if(l.sign())
+          return {precedencet::NOT, buffer.str()};
+        else
+          return {precedencet::MAX, buffer.str()};
       }
-    });
+      else
+        return expr2smvt::convert_rec(expr);
+    }
+  };
 
-  out << expr2smv(replaced, ns);
+  out << expr2smv_netlistt{ns, netlist}.convert(expr);
 }
 
 void smv_netlist(const netlistt &netlist, std::ostream &out)