Merge pull request #934 from diffblue/prop_handles

BMC: return property handles/literals
diffblue · Jan 17, 2025 · f6c38d9 · f6c38d9
2 parents a2cd909 + 4700fa7
commit f6c38d9
Show file tree

Hide file tree

Showing 8 changed files with 19 additions and 26 deletions.
diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
@@ -409,8 +409,8 @@ void bdd_enginet::compute_counterexample(
   auto netlist_property = netlist.properties.find(property.identifier);
   CHECK_RETURN(netlist_property != netlist.properties.end());
 
-  ::unwind_property(
-    netlist_property->second, bmc_map, property.timeframe_literals);
+  property.timeframe_literals =
+    ::unwind_property(netlist_property->second, bmc_map);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;

diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
@@ -230,13 +230,8 @@ property_checker_resultt bmc(
       continue;
     }
 
-    ::property(
-      property.normalized_expr,
-      property.timeframe_handles,
-      message_handler,
-      solver,
-      bound + 1,
-      ns);
+    property.timeframe_handles = ::property(
+      property.normalized_expr, message_handler, solver, bound + 1, ns);
 
     // If it's an assumption, then add it as constraint.
     if(property.is_assumed())

diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp
@@ -78,7 +78,7 @@ void bmc_cegart::unwind(
   for(auto &property_it : netlist.properties)
   {
     auto &prop_bv = prop_bv_map[property_it.first];
-    unwind_property(property_it.second, bmc_map, prop_bv);
+    prop_bv = unwind_property(property_it.second, bmc_map);
 
     disjuncts.push_back(!solver.land(prop_bv));
   }

diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
@@ -257,8 +257,8 @@ property_checker_resultt bit_level_bmc(
       auto netlist_property = netlist.properties.find(property.identifier);
       CHECK_RETURN(netlist_property != netlist.properties.end());
 
-      ::unwind_property(
-        netlist_property->second, bmc_map, property.timeframe_literals);
+      property.timeframe_literals =
+        ::unwind_property(netlist_property->second, bmc_map);
 
       if(property.is_assumed())
       {

diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
@@ -141,21 +141,22 @@ Function: unwind_property
 
 \*******************************************************************/
 
-void unwind_property(
+bvt unwind_property(
   const netlistt::propertyt &property,
-  const bmc_mapt &bmc_map,
-  bvt &prop_bv)
+  const bmc_mapt &bmc_map)
 {
   PRECONDITION(std::holds_alternative<netlistt::Gpt>(property));
   auto property_node = std::get<netlistt::Gpt>(property).p;
 
-  prop_bv.resize(bmc_map.timeframe_map.size());
+  bvt prop_bv{bmc_map.timeframe_map.size()};
 
   for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
   {
     literalt l=bmc_map.translate(t, property_node);
     prop_bv[t]=l;
   }
+
+  return prop_bv;
 }
 
 /*******************************************************************\

diff --git a/src/trans-netlist/unwind_netlist.h b/src/trans-netlist/unwind_netlist.h
@@ -36,9 +36,6 @@ void unwind(
 bool netlist_bmc_supports_property(const class exprt &);
 
 // unwind a netlist property
-void unwind_property(
-  const netlistt::propertyt &,
-  const bmc_mapt &,
-  bvt &prop_bv);
+bvt unwind_property(const netlistt::propertyt &, const bmc_mapt &);
 
 #endif
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
@@ -682,9 +682,8 @@ Function: property
 
 \*******************************************************************/
 
-void property(
+exprt::operandst property(
   const exprt &property_expr,
-  exprt::operandst &prop_handles,
   message_handlert &message_handler,
   decision_proceduret &solver,
   std::size_t no_timeframes,
@@ -696,8 +695,8 @@ void property(
   auto obligations = property_obligations(property_expr, no_timeframes);
 
   // Map obligations onto timeframes.
-  prop_handles.clear();
-  prop_handles.resize(no_timeframes, true_exprt());
+  exprt::operandst prop_handles{no_timeframes, true_exprt()};
+
   for(auto &obligation_it : obligations.map)
   {
     auto t = obligation_it.first;
@@ -706,4 +705,6 @@ void property(
     auto t_int = numeric_cast_v<std::size_t>(t);
     prop_handles[t_int] = solver.handle(conjunction(obligation_it.second));
   }
+
+  return prop_handles;
 }
diff --git a/src/trans-word-level/property.h b/src/trans-word-level/property.h
@@ -16,9 +16,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/decision_procedure.h>
 
-void property(
+exprt::operandst property(
   const exprt &property_expr,
-  exprt::operandst &prop_handles,
   message_handlert &,
   decision_proceduret &solver,
   std::size_t no_timeframes,