extract sva_sequence_matcht

This extracts the class that represents potential SVA sequence matches, and
the function that generates these from SVA sequence expressions into a
separate file.

Author: kroening

src/temporal-logic/Makefile

@@ -2,6 +2,7 @@ SRC = ctl.cpp \
       ltl.cpp \
       nnf.cpp \
       normalize_property.cpp \
+      sva_sequence_match.cpp \
       sva_to_ltl.cpp \
       temporal_logic.cpp \
       trivial_sva.cpp \

src/temporal-logic/sva_to_ltl.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <verilog/sva_expr.h>
 
 #include "ltl.h"
+#include "sva_sequence_match.h"
 #include "temporal_logic.h"
 
 static exprt n_Xes(mp_integer n, exprt op)
@@ -22,153 +23,18 @@ static exprt n_Xes(mp_integer n, exprt op)
     return n_Xes(n - 1, X_exprt{std::move(op)});
 }
 
-// Returns a set of match conditions (given as LTL formula)
-struct ltl_sequence_matcht
+// c0 ∧ X c1 ∧ XX c2 ....
+static exprt ltl(const sva_sequence_matcht &match)
 {
-  // the empty match
-  ltl_sequence_matcht()
+  exprt::operandst conjuncts;
+  conjuncts.reserve(match.cond_vector.size());
+  for(std::size_t i = 0; i < match.cond_vector.size(); i++)
   {
+    auto &c = match.cond_vector[i];
+    if(!c.is_true())
+      conjuncts.push_back(n_Xes(i, c));
   }
-
-  // a match of length 1
-  explicit ltl_sequence_matcht(exprt __cond) : cond_vector{1, std::move(__cond)}
-  {
-  }
-
-  std::vector<exprt> cond_vector;
-
-  std::size_t length()
-  {
-    return cond_vector.size();
-  }
-
-  bool empty_match() const
-  {
-    return cond_vector.empty();
-  }
-
-  // c0 ∧ X c1 ∧ XX c2 ....
-  exprt cond_expr() const
-  {
-    exprt::operandst conjuncts;
-    conjuncts.reserve(cond_vector.size());
-    for(std::size_t i = 0; i < cond_vector.size(); i++)
-    {
-      auto &c = cond_vector[i];
-      if(!c.is_true())
-        conjuncts.push_back(n_Xes(i, c));
-    }
-    return conjunction(conjuncts);
-  }
-
-  // generate true ##1 ... ##1 true with length n
-  static ltl_sequence_matcht true_match(const mp_integer &n)
-  {
-    ltl_sequence_matcht result;
-    for(mp_integer i; i < n; ++i)
-      result.cond_vector.push_back(true_exprt{});
-    return result;
-  }
-};
-
-// nonoverlapping concatenation
-ltl_sequence_matcht concat(ltl_sequence_matcht a, const ltl_sequence_matcht &b)
-{
-  a.cond_vector.insert(
-    a.cond_vector.end(), b.cond_vector.begin(), b.cond_vector.end());
-  return a;
-}
-
-// overlapping concatenation
-ltl_sequence_matcht
-overlapping_concat(ltl_sequence_matcht a, ltl_sequence_matcht b)
-{
-  PRECONDITION(!a.empty_match());
-  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()});
-  return concat(std::move(a), b);
-}
-
-std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
-{
-  if(sequence.id() == ID_sva_boolean)
-  {
-    // atomic proposition
-    return {ltl_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());
-
-    if(matches_lhs.empty() || matches_rhs.empty())
-      return {};
-
-    std::vector<ltl_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_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(matches.empty())
-      return {};
-
-    if(delay.to().is_nil())
-    {
-      // delay as instructed
-      auto delay_sequence = ltl_sequence_matcht::true_match(from_int);
-
-      for(auto &match : matches)
-        match = concat(delay_sequence, match);
-
-      return matches;
-    }
-    else if(delay.to().id() == ID_infinity)
-    {
-      return {}; // can't encode
-    }
-    else if(delay.to().is_constant())
-    {
-      auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
-      std::vector<ltl_sequence_matcht> new_matches;
-
-      for(mp_integer i = from_int; i <= to_int; ++i)
-      {
-        // delay as instructed
-        auto delay_sequence = ltl_sequence_matcht::true_match(i);
-
-        for(const auto &match : matches)
-        {
-          new_matches.push_back(concat(delay_sequence, match));
-        }
-      }
-
-      return new_matches;
-    }
-    else
-      return {};
-  }
-  else
-  {
-    return {}; // unsupported
-  }
+  return conjunction(conjuncts);
 }
 
 /// takes an SVA property as input, and returns an equivalent LTL property,
@@ -296,7 +162,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
       {
         auto delay = match.length() + (overlapped ? 0 : 1) - 1;
         auto delayed_property = n_Xes(delay, property_rec.value());
-        conjuncts.push_back(implies_exprt{match.cond_expr(), delayed_property});
+        conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
       }
     }
 
@@ -332,7 +198,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
       {
         auto delay = match.length() + (overlapped ? 0 : 1) - 1;
         auto delayed_property = n_Xes(delay, property_rec.value());
-        disjuncts.push_back(and_exprt{match.cond_expr(), delayed_property});
+        disjuncts.push_back(and_exprt{ltl(match), delayed_property});
       }
     }
 
@@ -360,7 +226,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     for(auto &match : matches)
     {
       if(!match.empty_match())
-        disjuncts.push_back(match.cond_expr());
+        disjuncts.push_back(ltl(match));
     }
 
     return disjunction(disjuncts);