BMC: instantiate_word_level now side-effect free

This removes the side effect of the methods in instantiate_word_levelt, by
introducing an explicit parameter.

Author: kroening

src/trans-word-level/instantiate_word_level.cpp

@@ -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(std::size_t _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, std::size_t t) const
   {
-    return instantiate_rec(std::move(expr));
+    return instantiate_rec(std::move(expr), t);
   }
 
 protected:
-  std::size_t current, no_timeframes;
+  std::size_t 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, std::size_t t) const;
+  [[nodiscard]] typet instantiate_rec(typet, std::size_t 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 std::size_t 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.to_ulong();
 
         // 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.to_ulong();
 
-          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++)
     {
       exprt::operandst disjuncts = {not_exprt(lasso_symbol(k, i))};
 
       for(std::size_t 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, std::size_t) const
 {
   return type;
 }
@@ -391,10 +357,10 @@ Function: instantiate
 
 exprt instantiate(
   const exprt &expr,
-  std::size_t current,
+  std::size_t t,
   std::size_t 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);
 }