Merge pull request #467 from diffblue/netlist-unwind-property

ebmc: netlist unwinding now uses netlist property node

Author: tautschnig

src/ebmc/bdd_engine.cpp

@@ -364,6 +364,10 @@ void bdd_enginet::compute_counterexample(
   propertyt &property,
   unsigned number_of_timeframes)
 {
+  // Supported by BMC engine?
+  if(!netlist_bmc_supports_property(property.normalized_expr))
+    return;
+
   message.status() << "Computing counterexample with " << number_of_timeframes
                    << " timeframe(s)" << messaget::eom;
 
@@ -372,16 +376,14 @@ void bdd_enginet::compute_counterexample(
   satcheckt solver{message.get_message_handler()};
   bmc_map.map_timeframes(netlist, number_of_timeframes, solver);
 
-  const namespacet ns(transition_system.symbol_table);
-
   ::unwind(netlist, bmc_map, message, solver);
+
+  // find the netlist property
+  auto netlist_property = netlist.properties.find(property.identifier);
+  CHECK_RETURN(netlist_property != netlist.properties.end());
+
   ::unwind_property(
-    property.normalized_expr,
-    property.timeframe_literals,
-    message.get_message_handler(),
-    solver,
-    bmc_map,
-    ns);
+    netlist_property->second, bmc_map, property.timeframe_literals);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;
@@ -402,6 +404,8 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
+  const namespacet ns(transition_system.symbol_table);
+
   property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }

src/ebmc/ebmc_base.cpp

@@ -208,13 +208,12 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
         continue;
       }
 
+      // look up the property in the netlist
+      auto netlist_property = netlist.properties.find(property.identifier);
+      CHECK_RETURN(netlist_property != netlist.properties.end());
+
       ::unwind_property(
-        property.normalized_expr,
-        property.timeframe_literals,
-        message.get_message_handler(),
-        solver,
-        bmc_map,
-        ns);
+        netlist_property->second, bmc_map, property.timeframe_literals);
 
       // freeze for incremental usage
       for(auto l : property.timeframe_literals)

src/ebmc/ebmc_properties.cpp

@@ -67,12 +67,8 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
 
       properties.properties.push_back(propertyt());
       properties.properties.back().number = properties.properties.size() - 1;
-
-      if(symbol.pretty_name.empty())
-        properties.properties.back().name = symbol.name;
-      else
-        properties.properties.back().name = symbol.pretty_name;
-
+      properties.properties.back().identifier = symbol.name;
+      properties.properties.back().name = symbol.display_name();
       properties.properties.back().original_expr = symbol.value;
       properties.properties.back().normalized_expr =
         normalize_property(symbol.value);

src/ebmc/ebmc_properties.h

@@ -26,7 +26,7 @@ class ebmc_propertiest
   {
   public:
     std::size_t number = 0;
-    irep_idt name;
+    irep_idt identifier, name;
     source_locationt location;
     std::string expr_string;
     irep_idt mode;

src/ebmc/report_results.cpp

@@ -55,7 +55,8 @@ void report_results(
         continue;
 
       json_objectt json_property;
-      json_property["identifier"] = json_stringt(id2string(property.name));
+      json_property["identifier"] =
+        json_stringt(id2string(property.identifier));
       json_property["status"] = json_stringt(property.status_as_string());
 
       if(property.has_witness_trace())
@@ -77,7 +78,7 @@ void report_results(
         continue;
 
       xmlt xml_result("result");
-      xml_result.set_attribute("property", id2string(property.name));
+      xml_result.set_attribute("property", id2string(property.identifier));
       xml_result.set_attribute("status", property.status_as_string());
 
       if(property.has_witness_trace())