use netlist_boolbvt for the property

This enables sharing common subexpressions in the property, reducing the
size of the netlist.

Author: kroening

regression/ebmc/smv-netlist/always_with_range1.desc

@@ -1,10 +1,10 @@
 CORE
 always_with_range1.sv
 --smv-netlist
-^LTLSPEC node275 & X node363 & X X node451 .*
-^LTLSPEC G node1155$
-^LTLSPEC node1243 & X node1331 & X X node1419 .*
-^LTLSPEC G \(\!node2066 \| X node2097\)$
+^LTLSPEC node275 & X node275 & X X node275 .*
+^LTLSPEC G node275$
+^LTLSPEC node275 & X node275 & X X node275 .*
+^LTLSPEC G \(\!node306 \| X node337\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-netlist/cycle_delay2.desc

@@ -1,7 +1,7 @@
 CORE
 cycle_delay2.sv
 --smv-netlist
-^LTLSPEC X node22 \| X X node25$
+^LTLSPEC X node22 \| X X node22$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/trans-netlist/trans_to_netlist.cpp

@@ -17,13 +17,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
+#include <solvers/prop/literal_expr.h>
 #include <temporal-logic/ctl.h>
 #include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
 #include "aig_prop.h"
-#include "instantiate_netlist.h"
 #include "netlist.h"
 #include "netlist_boolbv.h"
 
@@ -145,6 +145,8 @@ class convert_trans_to_netlistt:public messaget
 
   void convert_constraints();
 
+  std::optional<exprt> convert_property(const exprt &);
+
   void map_vars(
     const irep_idt &module,
     netlistt &dest);
@@ -328,9 +330,7 @@ void convert_trans_to_netlistt::operator()(
   // properties
   for(const auto &[id, property_expr] : properties)
   {
-    auto netlist_expr_opt = netlist_property(
-      aig_prop, dest.var_map, property_expr, ns, get_message_handler());
-
+    auto netlist_expr_opt = convert_property(property_expr);
     dest.properties.emplace(id, netlist_expr_opt);
   }
 
@@ -359,6 +359,75 @@ void convert_trans_to_netlistt::operator()(
 
 /*******************************************************************\
 
+Function: convert_trans_to_netlistt::convert_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::optional<exprt>
+convert_trans_to_netlistt::convert_property(const exprt &expr)
+{
+  if(is_temporal_operator(expr))
+  {
+    if(is_LTL_operator(expr) || is_CTL_operator(expr))
+    {
+      exprt copy = expr;
+      for(auto &op : copy.operands())
+      {
+        auto op_opt = convert_property(op);
+        if(op_opt.has_value())
+          op = op_opt.value();
+        else
+          return {};
+      }
+      return copy;
+    }
+    else if(is_SVA_operator(expr))
+    {
+      // Try to turn into LTL
+      auto LTL_opt = SVA_to_LTL(expr);
+      if(LTL_opt.has_value())
+        return convert_property(*LTL_opt);
+      else
+        return {};
+    }
+    else
+      return {};
+  }
+  else if(!has_temporal_operator(expr))
+  {
+    auto l = solver.convert(expr);
+    return literal_exprt{l};
+  }
+  else if(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not ||
+    expr.id() == ID_implies || expr.id() == ID_xor || expr.id() == ID_xnor)
+  {
+    exprt copy = expr;
+    for(auto &op : copy.operands())
+    {
+      auto op_opt = convert_property(op);
+      if(op_opt.has_value())
+        op = op_opt.value();
+      else
+        return {};
+    }
+    return copy;
+  }
+  else
+  {
+    // contains temporal operator, but not propositional skeleton
+    return {};
+  }
+}
+
+/*******************************************************************\
+
 Function: convert_trans_to_netlistt::convert_constraints
 
   Inputs: