SVA: replace sva_sequence_concatenation_exprt

regression/ebmc-spot/sva-buechi/sequence_repetition5.desc

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/sequence_repetition5.sv
 --buechi --bound 20
-^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$
-^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/empty_sequence1.desc

@@ -2,7 +2,7 @@ CORE
 empty_sequence1.sv
 --bound 5
 ^\[main\.p0\] 1 \[\*0\]: REFUTED$
-^\[main\.p1\] 1 \[\*0\] ##1 main\.x == 0: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_repetition5.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_repetition5.sv
 --bound 20
-^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$
-^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$
+^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_disable_iff)
-IREP_ID_ONE(sva_sequence_concatenation)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)

src/temporal-logic/ltl_sva_to_string.cpp

@@ -327,22 +327,49 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
     return rec(to_sva_boolean_expr(expr).op(), BOOLEAN);
   }
-  else if(expr.id() == ID_sva_sequence_concatenation)
+  else if(expr.id() == ID_sva_cycle_delay)
   {
     PRECONDITION(mode == SVA_SEQUENCE);
-    // SVA sequence concatenation is overlapping, whereas
-    // the ; operator is nonoverlapping. We special-case
-    // the following for better readability:
-    // f ##0 g  --> f : g
-    // 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(expr);
+
+    if(delay.lhs().is_nil())
     {
-      auto &delay = to_sva_cycle_delay_expr(concatenation.rhs());
+      auto new_expr = unary_exprt{expr.id(), delay.rhs()};
 
-      auto new_expr = concatenation;
-      new_expr.rhs() = delay.op();
+      if(delay.is_range()) // ##[from:to] rhs
+      {
+        auto from = numeric_cast_v<mp_integer>(delay.from());
+
+        if(delay.is_unbounded()) // ##[n:$] rhs
+        {
+          return prefix(
+            "1[*" + integer2string(from) + "..] ; ", new_expr, mode);
+        }
+        else
+        {
+          auto to = numeric_cast_v<mp_integer>(delay.to());
+          PRECONDITION(to >= 0);
+          return prefix(
+            "1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ",
+            new_expr,
+            mode);
+        }
+      }
+      else // ##n rhs
+      {
+        auto i = numeric_cast_v<mp_integer>(delay.from());
+        PRECONDITION(i >= 0);
+        return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode);
+      }
+    }
+    else // lhs is not nil
+    {
+      // We special-case the following for better readability:
+      // f ##0 g  --> f : g
+      // f ##1 g  --> f ; g
+      // f ##n g  --> f ; 1[*n-1] ; b
+      auto new_expr =
+        binary_exprt{delay.lhs(), delay.id(), delay.rhs(), delay.type()};
 
       if(delay.is_range())
       {
@@ -354,12 +381,12 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
           throw ebmc_errort{}
             << "cannot convert 0.. ranged sequence concatenation to Buechi";
         }
-        else if(delay.is_unbounded())
+        else if(delay.is_unbounded()) // f ##[n:$] g
         {
           return infix(
             " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
         }
-        else
+        else // f ##[from:to] g
         {
           auto to = numeric_cast_v<mp_integer>(delay.to());
           PRECONDITION(to >= 0);
@@ -370,7 +397,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
             mode);
         }
       }
-      else
+      else // f ##n g
       {
         auto n = numeric_cast_v<mp_integer>(delay.from());
         PRECONDITION(n >= 0);
@@ -385,39 +412,6 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
         }
       }
     }
-    else
-      return infix(":", expr, mode);
-  }
-  else if(expr.id() == ID_sva_cycle_delay)
-  {
-    PRECONDITION(mode == SVA_SEQUENCE);
-    auto &delay = to_sva_cycle_delay_expr(expr);
-    unary_exprt new_expr{expr.id(), delay.op()};
-
-    if(delay.is_range())
-    {
-      auto from = numeric_cast_v<mp_integer>(delay.from());
-
-      if(delay.is_unbounded())
-      {
-        return prefix("1[*" + integer2string(from) + "..] ; ", new_expr, mode);
-      }
-      else
-      {
-        auto to = numeric_cast_v<mp_integer>(delay.to());
-        PRECONDITION(to >= 0);
-        return prefix(
-          "1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ",
-          new_expr,
-          mode);
-      }
-    }
-    else // singleton
-    {
-      auto i = numeric_cast_v<mp_integer>(delay.from());
-      PRECONDITION(i >= 0);
-      return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode);
-    }
   }
   else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
   {

src/temporal-logic/sva_sequence_match.cpp

@@ -47,7 +47,8 @@ overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b)
   PRECONDITION(!b.empty_match());
   auto a_last = a.cond_vector.back();
   a.cond_vector.pop_back();
-  b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
+  if(!a_last.is_true())
+    b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
   return concat(std::move(a), b);
 }
 
@@ -58,26 +59,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
     // atomic proposition
     return {sva_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
   }
-  else if(sequence.id() == ID_sva_sequence_concatenation)
-  {
-    auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
-    auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
-    auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
-
-    std::vector<sva_sequence_matcht> result;
-
-    // cross product
-    for(auto &match_lhs : matches_lhs)
-      for(auto &match_rhs : matches_rhs)
-      {
-        // Sequence concatenation is overlapping
-        auto new_match = overlapping_concat(match_lhs, match_rhs);
-        CHECK_RETURN(
-          new_match.length() == match_lhs.length() + match_rhs.length() - 1);
-        result.push_back(std::move(new_match));
-      }
-    return result;
-  }
   else if(sequence.id() == ID_sva_sequence_repetition_star) // [*n], [*n:m]
   {
     auto &repetition = to_sva_sequence_repetition_star_expr(sequence);
@@ -119,41 +100,61 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
   else if(sequence.id() == ID_sva_cycle_delay)
   {
     auto &delay = to_sva_cycle_delay_expr(sequence);
-    auto matches = LTL_sequence_matches(delay.op());
-    auto from_int = numeric_cast_v<mp_integer>(delay.from());
 
-    if(!delay.is_range())
+    // These have an optional LHS and a RHS.
+    std::vector<sva_sequence_matcht> lhs_matches;
+
+    if(delay.lhs().is_nil())
     {
-      // delay as instructed
-      auto delay_sequence = sva_sequence_matcht::true_match(from_int);
+      // If the LHS is not given, it's equivalent to 'true'.
+      lhs_matches = {sva_sequence_matcht::true_match(1)};
+    }
+    else
+    {
+      lhs_matches = LTL_sequence_matches(delay.lhs());
+    }
 
-      for(auto &match : matches)
-        match = concat(delay_sequence, match);
+    // The delay in between lhs and rhs
+    std::vector<sva_sequence_matcht> delay_matches;
+
+    auto from_int = numeric_cast_v<mp_integer>(delay.from());
 
-      return matches;
+    if(!delay.is_range()) // f ##n g
+    {
+      delay_matches = {sva_sequence_matcht::true_match(from_int)};
     }
-    else if(delay.is_unbounded())
+    else if(delay.is_unbounded()) // f ##[from:$] g
     {
       throw sva_sequence_match_unsupportedt{sequence}; // can't encode
     }
-    else
+    else // f ##[from:to] g
     {
       auto to_int = numeric_cast_v<mp_integer>(delay.to());
-      std::vector<sva_sequence_matcht> new_matches;
 
       for(mp_integer i = from_int; i <= to_int; ++i)
-      {
-        // delay as instructed
-        auto delay_sequence = sva_sequence_matcht::true_match(i);
+        delay_matches.push_back(sva_sequence_matcht::true_match(i));
+    }
+
+    // now do RHS
+    auto rhs_matches = LTL_sequence_matches(delay.rhs());
+
+    // cross product lhs x delay x rhs
+    std::vector<sva_sequence_matcht> result;
 
-        for(const auto &match : matches)
+    for(auto &lhs_match : lhs_matches)
+      for(auto &delay_match : delay_matches)
+        for(auto &rhs_match : rhs_matches)
         {
-          new_matches.push_back(concat(delay_sequence, match));
+          // Sequence concatenation is overlapping
+          auto new_match =
+            overlapping_concat(lhs_match, concat(delay_match, rhs_match));
+          CHECK_RETURN(
+            new_match.length() ==
+            lhs_match.length() + delay_match.length() + rhs_match.length() - 1);
+          result.push_back(std::move(new_match));
         }
-      }
 
-      return new_matches;
-    }
+    return result;
   }
   else if(sequence.id() == ID_sva_and)
   {

src/temporal-logic/temporal_logic.cpp

@@ -107,7 +107,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
   // Note that ID_sva_not does not yield a sequence expression.
   return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay ||
          id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star ||
-         id == ID_sva_sequence_concatenation ||
          id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
          id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
          id == ID_sva_sequence_goto_repetition ||