BMC: encode properties using timeframe/handle pair

The property encoding interface is changed to return a timeframe/handle
pair, instead of just a condition per timeframe.

This allows determining the appropriate size of the counterexample trace.

Author: kroening

src/trans-word-level/property.cpp

@@ -72,7 +72,7 @@ Function: property
 
 void property(
   const exprt &property_expr,
-  exprt::operandst &prop_handles,
+  std::map<std::size_t, exprt::operandst> &obligations,
   message_handlert &message_handler,
   decision_proceduret &solver,
   std::size_t no_timeframes,
@@ -87,16 +87,14 @@ void property(
     property_expr.id() == ID_sva_nexttime ||
     property_expr.id() == ID_sva_s_nexttime)
   {
-    prop_handles.resize(no_timeframes, true_exprt());
     if(no_timeframes > 0)
     {
       exprt tmp = instantiate(property_expr, 0, no_timeframes, ns);
-      prop_handles.push_back(solver.handle(tmp));
+      obligations[0].push_back(solver.handle(tmp));
     }
 
     return;
   }
-
   // We want AG p.
   auto &p = [](const exprt &expr) -> const exprt & {
     if(expr.id() == ID_AG)
@@ -115,7 +113,45 @@ void property(
       instantiate(p, c, no_timeframes, ns);
 
     auto handle = solver.handle(tmp);
-    prop_handles.push_back(std::move(handle));
+    obligations[c].push_back(std::move(handle));
+  }
+}
+
+/*******************************************************************\
+
+Function: property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void property(
+  const exprt &property_expr,
+  exprt::operandst &prop_handles,
+  message_handlert &message_handler,
+  decision_proceduret &solver,
+  std::size_t no_timeframes,
+  const namespacet &ns)
+{
+  // The first element of the pair is the length of the
+  // counterexample, and the second is the condition that
+  // must be valid for the property to hold.
+  std::map<std::size_t, exprt::operandst> obligations;
+
+  property(
+    property_expr, obligations, message_handler, solver, no_timeframes, ns);
+
+  // Map obligations onto timeframes.
+  prop_handles.resize(no_timeframes, true_exprt());
+  for(auto &obligation_it : obligations)
+  {
+    auto t = obligation_it.first;
+    DATA_INVARIANT(t < no_timeframes, "obligation must have valid timeframe");
+    prop_handles[t] = conjunction(obligation_it.second);
   }
 }