Merge pull request #402 from diffblue/instantiate_wl_functional

BMC: world-level property instantiation refactorings

Author: tautschnig

src/trans-word-level/instantiate_word_level.cpp

@@ -29,9 +29,9 @@ Function: timeframe_identifier
 \*******************************************************************/
 
 std::string
-timeframe_identifier(std::size_t timeframe, const irep_idt &identifier)
+timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier)
 {
-  return id2string(identifier)+"@"+std::to_string(timeframe);
+  return id2string(identifier) + "@" + integer2string(timeframe);
 }
 
 /*******************************************************************\
@@ -46,7 +46,7 @@ Function: timeframe_symbol
 
 \*******************************************************************/
 
-symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt src)
+symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 {
   auto result = std::move(src);
   result.set_identifier(
@@ -69,40 +69,23 @@ symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  wl_instantiatet(
-    std::size_t _current,
-    std::size_t _no_timeframes,
-    const namespacet &_ns)
-    : current(_current), no_timeframes(_no_timeframes), ns(_ns)
+  wl_instantiatet(const mp_integer &_no_timeframes, const namespacet &_ns)
+    : no_timeframes(_no_timeframes), ns(_ns)
   {
   }
 
-  [[nodiscard]] exprt operator()(exprt expr)
+  /// Instantiate the given expression for timeframe t
+  [[nodiscard]] exprt operator()(exprt expr, const mp_integer &t) const
   {
-    return instantiate_rec(std::move(expr));
+    return instantiate_rec(std::move(expr), t);
   }
 
 protected:
-  std::size_t current, no_timeframes;
+  const mp_integer &no_timeframes;
   const namespacet &ns;
 
-  [[nodiscard]] exprt instantiate_rec(exprt);
-  [[nodiscard]] typet instantiate_rec(typet);
-
-  class save_currentt
-  {
-  public:
-    inline explicit save_currentt(std::size_t &_c) : c(_c), saved(c)
-    {
-    }
-    
-    inline ~save_currentt()
-    {
-      c=saved; // restore
-    }
-
-    std::size_t &c, saved;
-  };
+  [[nodiscard]] exprt instantiate_rec(exprt, const mp_integer &t) const;
+  [[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
 };
 
 /*******************************************************************\
@@ -117,26 +100,26 @@ Function: wl_instantiatet::instantiate_rec
 
 \*******************************************************************/
 
-exprt wl_instantiatet::instantiate_rec(exprt expr)
+exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 {
-  expr.type() = instantiate_rec(expr.type());
+  expr.type() = instantiate_rec(expr.type(), t);
 
   if(expr.id() == ID_next_symbol)
   {
     expr.id(ID_symbol);
-    return timeframe_symbol(current + 1, to_symbol_expr(std::move(expr)));
+    return timeframe_symbol(t + 1, to_symbol_expr(std::move(expr)));
   }
   else if(expr.id() == ID_symbol)
   {
-    return timeframe_symbol(current, to_symbol_expr(std::move(expr)));
+    return timeframe_symbol(t, to_symbol_expr(std::move(expr)));
   }
   else if(expr.id()==ID_sva_overlapped_implication)
   {
     // same as regular implication
     expr.id(ID_implies);
 
     for(auto &op : expr.operands())
-      op = instantiate_rec(op);
+      op = instantiate_rec(op, t);
 
     return expr;
   }
@@ -147,18 +130,16 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
     {
       expr.id(ID_implies);
       auto &implies_expr = to_implies_expr(expr);
-      implies_expr.op0() = instantiate_rec(implies_expr.op0());
+      implies_expr.op0() = instantiate_rec(implies_expr.op0(), t);
+
+      const auto next = t + 1;
 
-      save_currentt save_current(current);
-      
-      current++;
-      
       // Do we exceed the bound? Make it 'true',
       // works on NNF only
-      if(current>=no_timeframes)
+      if(next >= no_timeframes)
         implies_expr.op1() = true_exprt();
       else
-        implies_expr.op1() = instantiate_rec(implies_expr.op1());
+        implies_expr.op1() = instantiate_rec(implies_expr.op1(), next);
 
       return std::move(implies_expr);
     }
@@ -171,22 +152,19 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
     {
       auto &ternary_expr = to_ternary_expr(expr);
 
-      // save the current time frame, we'll change it
-      save_currentt save_current(current);
-
       if(ternary_expr.op1().is_nil())
       {
         mp_integer offset;
         if(to_integer_non_constant(ternary_expr.op0(), offset))
           throw "failed to convert sva_cycle_delay offset";
 
-        current = save_current.saved + offset.to_ulong();
+        const auto u = t + offset;
 
         // Do we exceed the bound? Make it 'true'
-        if(current>=no_timeframes)
+        if(u >= no_timeframes)
           return true_exprt();
         else
-          return instantiate_rec(ternary_expr.op2());
+          return instantiate_rec(ternary_expr.op2(), u);
       }
       else
       {
@@ -208,14 +186,14 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
 
         for(mp_integer offset=from; offset<to; ++offset)
         {
-          current = save_current.saved + offset.to_ulong();
+          auto u = t + offset;
 
-          if(current>=no_timeframes)
+          if(u >= no_timeframes)
           {
           }
           else
           {
-            disjuncts.push_back(instantiate_rec(ternary_expr.op2()));
+            disjuncts.push_back(instantiate_rec(ternary_expr.op2(), u));
           }
         }
 
@@ -231,22 +209,19 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
     expr.id(ID_and);
 
     for(auto &op : expr.operands())
-      op = instantiate_rec(op);
+      op = instantiate_rec(op, t);
 
     return expr;
   }
   else if(expr.id()==ID_sva_always)
   {
     auto &op = to_sva_always_expr(expr).op();
 
-    // save the current time frame, we'll change it
-    save_currentt save_current(current);
-    
     exprt::operandst conjuncts;
 
-    for(; current<no_timeframes; current++)
+    for(auto u = t; u < no_timeframes; ++u)
     {
-      conjuncts.push_back(instantiate_rec(op));
+      conjuncts.push_back(instantiate_rec(op, u));
     }
 
     return conjunction(conjuncts);
@@ -255,15 +230,12 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
           expr.id()==ID_sva_s_nexttime)
   {
     assert(expr.operands().size()==1);
-    
-    // save the current time frame, we'll change it
-    save_currentt save_current(current);
-    
-    current++;
-    
-    if(current<no_timeframes)
+
+    const auto next = t + 1;
+
+    if(next < no_timeframes)
     {
-      return instantiate_rec(to_unary_expr(expr).op());
+      return instantiate_rec(to_unary_expr(expr).op(), next);
     }
     else
       return true_exprt(); // works on NNF only
@@ -280,25 +252,22 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
     //     some earlier state k < i.
     // (1) No state j with k<=k<=i on the lasso satisfies 'p'.
     //
-    // We look backwards instead of forwards so that 'current'
+    // We look backwards instead of forwards so that 't'
     // is the last state of the counterexample trace.
     //
-    // Note that this is trivially true when current is zero,
+    // Note that this is trivially true when t is zero,
     // as a single state cannot demonstrate the loop.
 
     exprt::operandst conjuncts = {};
-    const std::size_t i = current;
+    const auto i = t;
 
-    for(std::size_t k = 0; k < i; k++)
+    for(mp_integer k = 0; k < i; ++k)
     {
       exprt::operandst disjuncts = {not_exprt(lasso_symbol(k, i))};
 
-      for(std::size_t j = k; j <= i; j++)
+      for(mp_integer j = k; j <= i; ++j)
       {
-        // save the current time frame, we'll change it
-        save_currentt save_current(current);
-        current = j;
-        disjuncts.push_back(instantiate_rec(p));
+        disjuncts.push_back(instantiate_rec(p, j));
       }
 
       conjuncts.push_back(disjunction(disjuncts));
@@ -314,22 +283,19 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
     assert(expr.operands().size()==2);
 
     // we need a lasso to refute these
-    
-    // save the current time frame, we'll change it
-    save_currentt save_current(current);
-    
+
     // we expand: p U q <=> q || (p && X(p U q))
     exprt tmp_q = to_binary_expr(expr).op1();
-    tmp_q = instantiate_rec(tmp_q);
+    tmp_q = instantiate_rec(tmp_q, t);
 
     exprt expansion = to_binary_expr(expr).op0();
-    expansion = instantiate_rec(expansion);
+    expansion = instantiate_rec(expansion, t);
 
-    current++;
-    
-    if(current<no_timeframes)
+    const auto next = t + 1;
+
+    if(next < no_timeframes)
     {
-      expansion = and_exprt(expansion, instantiate_rec(expr));
+      expansion = and_exprt(expansion, instantiate_rec(expr, next));
     }
 
     return or_exprt(tmp_q, expansion);
@@ -350,12 +316,12 @@ exprt wl_instantiatet::instantiate_rec(exprt expr)
 
     tmp.op1() = sva_nexttime_exprt(tmp.op1());
 
-    return instantiate_rec(tmp);
+    return instantiate_rec(tmp, t);
   }
   else
   {
     for(auto &op : expr.operands())
-      op = instantiate_rec(op);
+      op = instantiate_rec(op, t);
     return expr;
   }
 }
@@ -372,7 +338,7 @@ Function: wl_instantiatet::instantiate_rec
 
 \*******************************************************************/
 
-typet wl_instantiatet::instantiate_rec(typet type)
+typet wl_instantiatet::instantiate_rec(typet type, const mp_integer &) const
 {
   return type;
 }
@@ -391,10 +357,10 @@ Function: instantiate
 
 exprt instantiate(
   const exprt &expr,
-  std::size_t current,
-  std::size_t no_timeframes,
+  const mp_integer &t,
+  const mp_integer &no_timeframes,
   const namespacet &ns)
 {
-  wl_instantiatet wl_instantiate(current, no_timeframes, ns);
-  return wl_instantiate(expr);
+  wl_instantiatet wl_instantiate(no_timeframes, ns);
+  return wl_instantiate(expr, t);
 }

src/trans-word-level/instantiate_word_level.h

@@ -9,19 +9,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 #define CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 
-#include <solvers/prop/prop_conv.h>
-
+#include <util/mp_arith.h>
 #include <util/namespace.h>
 
+#include <solvers/prop/prop_conv.h>
+
 exprt instantiate(
   const exprt &expr,
-  std::size_t current,
-  std::size_t no_timeframes,
+  const mp_integer &current,
+  const mp_integer &no_timeframes,
   const namespacet &);
 
 std::string
-timeframe_identifier(std::size_t timeframe, const irep_idt &identifier);
+timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
 
-symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt);
+symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt);
 
 #endif

src/trans-word-level/property.cpp

@@ -109,8 +109,8 @@ Function: states_equal
 \*******************************************************************/
 
 exprt states_equal(
-  std::size_t k,
-  std::size_t i,
+  const mp_integer &k,
+  const mp_integer &i,
   const std::vector<symbol_exprt> &variables_to_compare)
 {
   // We require k<i to avoid the symmetric constraints.
@@ -141,13 +141,13 @@ Function: lasso_symbol
 
 \*******************************************************************/
 
-symbol_exprt lasso_symbol(std::size_t k, std::size_t i)
+symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i)
 {
   // True when states i and k are equal.
   // We require k<i to avoid the symmetric constraints.
   PRECONDITION(k < i);
   irep_idt lasso_identifier =
-    "lasso::" + std::to_string(i) + "-back-to-" + std::to_string(k);
+    "lasso::" + integer2string(i) + "-back-to-" + integer2string(k);
   return symbol_exprt(lasso_identifier, bool_typet());
 }
 
@@ -165,7 +165,7 @@ Function: lasso_constraints
 
 void lasso_constraints(
   decision_proceduret &solver,
-  std::size_t no_timeframes,
+  const mp_integer &no_timeframes,
   const namespacet &ns,
   const irep_idt &module_identifier)
 {
@@ -204,9 +204,9 @@ void lasso_constraints(
     }
   }
 
-  for(std::size_t i = 1; i < no_timeframes; i++)
+  for(mp_integer i = 1; i < no_timeframes; ++i)
   {
-    for(std::size_t k = 0; k < i; k++)
+    for(mp_integer k = 0; k < i; ++k)
     {
       // Is there a loop back from time frame i back to time frame k?
       auto lasso_symbol = ::lasso_symbol(k, i);