SVA: strengthen typing of sva_sequence_concatenation_exprt

The RHS of a sva_sequence_concatenation_exprt is always a sva_cycle_delay
expression.  This strengthens the typing of the rhs() method accordingly.

Author: kroening

src/temporal-logic/ltl_sva_to_string.cpp

@@ -337,56 +337,50 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // f ##1 g  --> f ; g
     // f ##n g  --> f ; 1[*n-1] ; b
     auto &concatenation = to_sva_sequence_concatenation_expr(expr);
-    if(concatenation.rhs().id() == ID_sva_cycle_delay)
-    {
-      auto &delay = to_sva_cycle_delay_expr(concatenation.rhs());
+    auto &delay = concatenation.rhs();
 
-      auto new_expr = concatenation;
-      new_expr.rhs() = delay.op();
+    binary_exprt new_expr = concatenation;
+    new_expr.rhs() = delay.op();
 
-      if(delay.is_range())
-      {
-        auto from = numeric_cast_v<mp_integer>(delay.from());
+    if(delay.is_range())
+    {
+      auto from = numeric_cast_v<mp_integer>(delay.from());
 
-        if(from == 0)
-        {
-          // requires treatment of empty sequences on lhs
-          throw ebmc_errort{}
-            << "cannot convert 0.. ranged sequence concatenation to Buechi";
-        }
-        else if(delay.is_unbounded())
-        {
-          return infix(
-            " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
-        }
-        else
-        {
-          auto to = numeric_cast_v<mp_integer>(delay.to());
-          PRECONDITION(to >= 0);
-          return infix(
-            " ; 1[*" + integer2string(from - 1) + ".." +
-              integer2string(to - 1) + "] ; ",
-            new_expr,
-            mode);
-        }
+      if(from == 0)
+      {
+        // requires treatment of empty sequences on lhs
+        throw ebmc_errort{}
+          << "cannot convert 0.. ranged sequence concatenation to Buechi";
+      }
+      else if(delay.is_unbounded())
+      {
+        return infix(
+          " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
       }
       else
       {
-        auto n = numeric_cast_v<mp_integer>(delay.from());
-        PRECONDITION(n >= 0);
-        if(n == 0)
-          return infix(" : ", new_expr, mode);
-        else if(n == 1)
-          return infix(" ; ", new_expr, mode);
-        else
-        {
-          return infix(
-            " ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode);
-        }
+        auto to = numeric_cast_v<mp_integer>(delay.to());
+        PRECONDITION(to >= 0);
+        return infix(
+          " ; 1[*" + integer2string(from - 1) + ".." + integer2string(to - 1) +
+            "] ; ",
+          new_expr,
+          mode);
       }
     }
     else
-      return infix(":", expr, mode);
+    {
+      auto n = numeric_cast_v<mp_integer>(delay.from());
+      PRECONDITION(n >= 0);
+      if(n == 0)
+        return infix(" : ", new_expr, mode);
+      else if(n == 1)
+        return infix(" ; ", new_expr, mode);
+      else
+      {
+        return infix(" ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode);
+      }
+    }
   }
   else if(expr.id() == ID_sva_cycle_delay)
   {

src/verilog/sva_expr.h

@@ -861,35 +861,6 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
   return static_cast<sva_and_exprt &>(expr);
 }
 
-class sva_sequence_concatenation_exprt : public binary_exprt
-{
-public:
-  explicit sva_sequence_concatenation_exprt(exprt op0, exprt op1)
-    : binary_exprt(
-        std::move(op0),
-        ID_sva_sequence_concatenation,
-        std::move(op1),
-        verilog_sva_sequence_typet{})
-  {
-  }
-};
-
-static inline const sva_sequence_concatenation_exprt &
-to_sva_sequence_concatenation_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
-  sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const sva_sequence_concatenation_exprt &>(expr);
-}
-
-static inline sva_sequence_concatenation_exprt &
-to_sva_sequence_concatenation_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
-  sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<sva_sequence_concatenation_exprt &>(expr);
-}
-
 class sva_iff_exprt : public binary_predicate_exprt
 {
 public:
@@ -1084,6 +1055,48 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
   return static_cast<sva_cycle_delay_exprt &>(expr);
 }
 
+class sva_sequence_concatenation_exprt : public binary_exprt
+{
+public:
+  // The lhs is a sequence, the rhs is a sva_cycle_delay expression
+  explicit sva_sequence_concatenation_exprt(
+    exprt __lhs,
+    sva_cycle_delay_exprt __rhs)
+    : binary_exprt(
+        std::move(__lhs),
+        ID_sva_sequence_concatenation,
+        std::move(__rhs),
+        verilog_sva_sequence_typet{})
+  {
+  }
+
+  const sva_cycle_delay_exprt &rhs() const
+  {
+    return static_cast<const sva_cycle_delay_exprt &>(binary_exprt::rhs());
+  }
+
+  sva_cycle_delay_exprt &rhs()
+  {
+    return static_cast<sva_cycle_delay_exprt &>(binary_exprt::rhs());
+  }
+};
+
+static inline const sva_sequence_concatenation_exprt &
+to_sva_sequence_concatenation_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
+  sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_sequence_concatenation_exprt &>(expr);
+}
+
+static inline sva_sequence_concatenation_exprt &
+to_sva_sequence_concatenation_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
+  sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_sequence_concatenation_exprt &>(expr);
+}
+
 class sva_cycle_delay_plus_exprt : public unary_exprt
 {
 public: