Fix fragment of SVA supported by word-level BMC

1) The simplifier is changed to stay within SVA when simplifying SVA.

2) The logic that recognises supported SVA is adjusted.

Author: kroening

src/temporal-logic/normalize_property.cpp

@@ -76,7 +76,7 @@ exprt normalize_pre_implies(implies_exprt expr)
 exprt normalize_pre_sva_overlapped_implication(
   sva_overlapped_implication_exprt expr)
 {
-  // Same as regular implication if lhs is not a sequence.
+  // Same as regular implication if the lhs is not a sequence.
   if(!is_SVA_sequence(expr.lhs()))
     return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
   else
@@ -86,9 +86,13 @@ exprt normalize_pre_sva_overlapped_implication(
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
-  // Same as a->nexttime b if lhs is not a sequence.
+  // Same as a->always[1:1] b if lhs is not a sequence.
   if(!is_SVA_sequence(expr.lhs()))
-    return or_exprt{not_exprt{expr.lhs()}, sva_nexttime_exprt{expr.rhs()}};
+  {
+    auto one = natural_typet{}.one_expr();
+    return or_exprt{
+      not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+  }
   else
     return std::move(expr);
 }
@@ -178,7 +182,7 @@ exprt normalize_property(exprt expr)
   else if(expr.id() == ID_sva_s_nexttime)
   {
     auto one = natural_typet{}.one_expr();
-    expr = sva_ranged_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
+    expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_indexed_nexttime)
   {
@@ -193,11 +197,18 @@ exprt normalize_property(exprt expr)
       nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
   }
   else if(expr.id() == ID_sva_cycle_delay)
+  {
     expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
+  }
   else if(expr.id() == ID_sva_cycle_delay_plus)
-    expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+  {
+    expr = sva_s_eventually_exprt{
+      sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+  }
   else if(expr.id() == ID_sva_cycle_delay_star)
-    expr = F_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+  {
+    expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+  }
   else if(expr.id() == ID_sva_sequence_concatenation)
   {
     auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr);

src/temporal-logic/normalize_property.h

@@ -24,14 +24,16 @@ Author: Daniel Kroening, [email protected]
 /// a sva_iff b --> a <-> b
 /// a sva_implies b --> a -> b
 /// sva_not a --> ¬a
-/// a sva_and b --> a ∧ b                                   if a and b are not SVA sequences
-/// a sva_or b --> a ∨ b                                    if a and b are not SVA sequences
-/// sva_overlapped_implication --> ¬a ∨ b                   if a is not an SVA sequence
-/// sva_non_overlapped_implication --> ¬a ∨ sva_nexttime b  if a is not an SVA sequence
-/// sva_nexttime φ --> Xφ
+/// a sva_and b --> a ∧ b                                  if a and b are not SVA sequences
+/// a sva_or b --> a ∨ b                                   if a and b are not SVA sequences
+/// sva_overlapped_implication --> ¬a ∨ b                  if a is not an SVA sequence
+/// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b  if a is not an SVA sequence
+/// sva_nexttime φ --> sva_always[1:1] φ
 /// sva_nexttime[i] φ --> sva_always[i:i] φ
-/// sva_s_nexttime φ --> Xφ
+/// sva_s_nexttime φ --> sva_always[1:1] φ
 /// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ
+/// ##[*] φ --> F φ
+/// ##[+] φ --> X F φ
 /// sva_if --> ? :
 /// ##[0:$] φ --> s_eventually φ
 /// ##[i:$] φ --> s_nexttime[i] s_eventually φ

src/temporal-logic/temporal_logic.h

@@ -45,7 +45,7 @@ bool is_SVA_sequence(const exprt &);
 /// Returns true iff the given expression is an SVA temporal operator
 bool is_SVA_operator(const exprt &);
 
-/// Returns true iff the given expression contains an SVA temporal operator
+/// Returns true iff the given expression is an SVA expression
 bool is_SVA(const exprt &);
 
 #endif

src/trans-word-level/property.cpp

@@ -145,35 +145,15 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
-  if(!is_temporal_operator(expr))
-  {
-    if(!has_temporal_operator(expr))
-      return true; // initial state only
-    else if(
-      expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
-    {
-      for(auto &op : expr.operands())
-        if(!bmc_supports_property(op))
-          return false;
-      return true;
-    }
-    else
-      return false;
-  }
-  else if(expr.id() == ID_sva_cycle_delay)
-    return !has_temporal_operator(to_sva_cycle_delay_expr(expr).op());
-  else if(expr.id() == ID_sva_nexttime)
-    return !has_temporal_operator(to_sva_nexttime_expr(expr).op());
-  else if(expr.id() == ID_sva_s_nexttime)
-    return !has_temporal_operator(to_sva_s_nexttime_expr(expr).op());
-  else if(expr.id() == ID_sva_always)
-    return true;
-  else if(expr.id() == ID_sva_ranged_always)
-    return true;
-  else if(expr.id() == ID_sva_s_eventually)
-    return true;
-  else
+  // sva_nonoverlapped_followed_by is not supported yet
+  if(has_subexpr(expr, ID_sva_nonoverlapped_followed_by))
+    return false;
+
+  // sva_overlapped_followed_by is not supported yet
+  if(has_subexpr(expr, ID_sva_overlapped_followed_by))
     return false;
+
+  return true;
 }
 
 /*******************************************************************\
@@ -194,8 +174,10 @@ bool bmc_supports_property(const exprt &expr)
     return bmc_supports_LTL_property(expr);
   else if(is_CTL(expr))
     return bmc_supports_CTL_property(expr);
-  else
+  else if(is_SVA(expr))
     return bmc_supports_SVA_property(expr);
+  else
+    return false; // unknown category
 }
 
 /*******************************************************************\