Merge pull request #1062 from diffblue/sva_sequence_property_expr_baset

`sva_sequence_property_expr_baset`

Author: tautschnig

src/temporal-logic/trivial_sva.cpp

@@ -111,7 +111,7 @@ exprt trivial_sva(exprt expr)
   {
     // We simplify sequences to boolean expressions, and hence can drop
     // the sva_sequence_property converter
-    auto &op = to_sva_sequence_property_expr(expr).op();
+    auto &op = to_sva_sequence_property_expr(expr).sequence();
     if(op.type().id() == ID_bool)
       return op;
   }

src/trans-word-level/property.cpp

@@ -507,25 +507,6 @@ static obligationst property_obligations_rec(
       std::max(obligations_true.first, obligations_false.first),
       if_exprt{cond, obligations_true.second, obligations_false.second}};
   }
-  else if(property_expr.id() == ID_sva_sequence_property)
-  {
-    // Sequences can be used as property, and evaluate to true
-    // when there is at least one match.
-    auto &sequence = to_sva_sequence_property_expr(property_expr).op();
-    auto matches = instantiate_sequence(sequence, current, no_timeframes);
-
-    exprt::operandst disjuncts;
-    disjuncts.reserve(matches.size());
-    mp_integer max = current;
-
-    for(auto &match : matches)
-    {
-      disjuncts.push_back(match.condition);
-      max = std::max(max, match.end_time);
-    }
-
-    return obligationst{max, disjunction(disjuncts)};
-  }
   else if(
     property_expr.id() == ID_typecast &&
     to_typecast_expr(property_expr).op().type().id() == ID_bool)
@@ -665,9 +646,11 @@ static obligationst property_obligations_rec(
     return obligationst{t, disjunction(disjuncts)};
   }
   else if(
-    property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak)
+    property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak ||
+    property_expr.id() == ID_sva_sequence_property)
   {
-    auto &sequence = to_unary_expr(property_expr).op();
+    auto &sequence =
+      to_sva_sequence_property_expr_base(property_expr).sequence();
 
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches

src/verilog/expr2verilog.cpp

@@ -537,7 +537,8 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary(
   if(op.id() == ID_typecast)
     op_operands = to_typecast_expr(op).op().operands().size();
   else if(src.op().id() == ID_sva_sequence_property)
-    op_operands = to_sva_sequence_property_expr(op).op().operands().size();
+    op_operands =
+      to_sva_sequence_property_expr(op).sequence().operands().size();
   else
     op_operands = op.operands().size();
 
@@ -1816,7 +1817,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_function("weak", src);
 
   else if(src.id() == ID_sva_sequence_property)
-    return convert_rec(to_sva_sequence_property_expr(src).op());
+    return convert_rec(to_sva_sequence_property_expr(src).sequence());
 
   else if(src.id()==ID_sva_sequence_concatenation)
     return convert_sva_sequence_concatenation(

src/verilog/sva_expr.h

@@ -1111,44 +1111,86 @@ static inline sva_if_exprt &to_sva_if_expr(exprt &expr)
   return static_cast<sva_if_exprt &>(expr);
 }
 
-class sva_strong_exprt : public unary_exprt
+/// Base class for sequence property expressions.
+/// 1800-2017 16.12.2 Sequence property
+class sva_sequence_property_expr_baset : public unary_predicate_exprt
+{
+public:
+  sva_sequence_property_expr_baset(irep_idt __id, exprt __op)
+    : unary_predicate_exprt(__id, std::move(__op))
+  {
+  }
+
+  const exprt &sequence() const
+  {
+    return op();
+  }
+
+  exprt &sequence()
+  {
+    return op();
+  }
+
+protected:
+  using unary_predicate_exprt::op;
+};
+
+inline const sva_sequence_property_expr_baset &
+to_sva_sequence_property_expr_base(const exprt &expr)
+{
+  sva_sequence_property_expr_baset::check(expr);
+  return static_cast<const sva_sequence_property_expr_baset &>(expr);
+}
+
+inline sva_sequence_property_expr_baset &
+to_sva_sequence_property_base_expr(exprt &expr)
+{
+  sva_sequence_property_expr_baset::check(expr);
+  return static_cast<sva_sequence_property_expr_baset &>(expr);
+}
+
+class sva_strong_exprt : public sva_sequence_property_expr_baset
 {
 public:
-  sva_strong_exprt(exprt __op, typet __type)
-    : unary_exprt(ID_sva_strong, std::move(__op), std::move(__type))
+  sva_strong_exprt(exprt __op)
+    : sva_sequence_property_expr_baset(ID_sva_strong, std::move(__op))
   {
   }
 };
 
 inline const sva_strong_exprt &to_sva_strong_expr(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_sva_strong);
   sva_strong_exprt::check(expr);
   return static_cast<const sva_strong_exprt &>(expr);
 }
 
 inline sva_strong_exprt &to_sva_strong_expr(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_sva_strong);
   sva_strong_exprt::check(expr);
   return static_cast<sva_strong_exprt &>(expr);
 }
 
-class sva_weak_exprt : public unary_exprt
+class sva_weak_exprt : public sva_sequence_property_expr_baset
 {
 public:
-  sva_weak_exprt(exprt __op, typet __type)
-    : unary_exprt(ID_sva_weak, std::move(__op), std::move(__type))
+  sva_weak_exprt(exprt __op)
+    : sva_sequence_property_expr_baset(ID_sva_weak, std::move(__op))
   {
   }
 };
 
 inline const sva_weak_exprt &to_sva_weak_expr(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_sva_weak);
   sva_weak_exprt::check(expr);
   return static_cast<const sva_weak_exprt &>(expr);
 }
 
 inline sva_weak_exprt &to_sva_weak_expr(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_sva_weak);
   sva_weak_exprt::check(expr);
   return static_cast<sva_weak_exprt &>(expr);
 }
@@ -1517,11 +1559,11 @@ to_sva_sequence_first_match_expr(exprt &expr)
 
 /// 1800-2017 16.12.2 Sequence property
 /// Equivalent to weak(...) or strong(...) depending on context.
-class sva_sequence_property_exprt : public unary_predicate_exprt
+class sva_sequence_property_exprt : public sva_sequence_property_expr_baset
 {
 public:
   explicit sva_sequence_property_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_sequence_property, std::move(op))
+    : sva_sequence_property_expr_baset(ID_sva_sequence_property, std::move(op))
   {
   }
 };