SVA_to_LTL now throws exception

SVA_to_LTL(expr) now throws an exception when given an expression that does
not map to LTL.  The exception includes a subexpression that is not
convertible.

Author: kroening

src/ebmc/bdd_engine.cpp

@@ -475,11 +475,15 @@ std::optional<exprt> bdd_enginet::property_supported(const exprt &expr)
   if(is_SVA(expr))
   {
     // We can map some SVA to LTL. In turn, some of that can be mapped to CTL.
-    auto ltl_opt = SVA_to_LTL(expr);
-    if(ltl_opt.has_value())
-      return property_supported(ltl_opt.value());
-    else
+    try
+    {
+      auto ltl = SVA_to_LTL(expr);
+      return property_supported(ltl);
+    }
+    catch(sva_to_ltl_unsupportedt)
+    {
       return {};
+    }
   }
 
   return {};

src/ebmc/output_smv_word_level.cpp

@@ -192,11 +192,16 @@ static void smv_properties(
     else if(is_SVA(property.normalized_expr))
     {
       // we can turn some SVA properties into LTL
-      auto ltl_opt = SVA_to_LTL(property.normalized_expr);
-      if(ltl_opt.has_value())
-        out << "LTLSPEC " << expr2smv(ltl_opt.value(), ns);
-      else
-        out << "-- " << property.identifier << ": SVA not converted\n";
+      try
+      {
+        auto ltl = SVA_to_LTL(property.normalized_expr);
+        out << "LTLSPEC " << expr2smv(ltl, ns);
+      }
+      catch(sva_to_ltl_unsupportedt error)
+      {
+        out << "-- " << property.identifier << ": SVA " << error.expr.id()
+            << " not converted\n";
+      }
     }
     else
       out << "-- " << property.identifier << ": not converted\n";

src/temporal-logic/sva_to_ltl.cpp

@@ -39,100 +39,78 @@ static exprt ltl(const sva_sequence_matcht &match)
   return conjunction(conjuncts);
 }
 
-/// takes an SVA property as input, and returns an equivalent LTL property,
-/// or otherwise {}.
-std::optional<exprt> SVA_to_LTL(exprt expr)
+/// takes an SVA property as input, and returns an equivalent LTL property
+exprt SVA_to_LTL(exprt expr)
 {
   // Some SVA is directly mappable to LTL
   if(expr.id() == ID_sva_always)
   {
     auto rec = SVA_to_LTL(to_sva_always_expr(expr).op());
-    if(rec.has_value())
-      return G_exprt{rec.value()};
-    else
-      return {};
+    return G_exprt{rec};
   }
   else if(expr.id() == ID_sva_ranged_always)
   {
     auto &ranged_always = to_sva_ranged_always_expr(expr);
     auto rec = SVA_to_LTL(ranged_always.op());
-    if(rec.has_value())
-    {
-      // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
+    // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+    auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
 
-      // Is there an upper end of the range?
-      if(ranged_always.to().is_constant())
-      {
-        // upper end set
-        auto to_int =
-          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.to()));
-        PRECONDITION(to_int >= from_int);
-        auto diff = to_int - from_int;
+    // Is there an upper end of the range?
+    if(ranged_always.to().is_constant())
+    {
+      // upper end set
+      auto to_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.to()));
+      PRECONDITION(to_int >= from_int);
+      auto diff = to_int - from_int;
 
-        exprt::operandst conjuncts;
+      exprt::operandst conjuncts;
 
-        for(auto i = 0; i <= diff; i++)
-          conjuncts.push_back(n_Xes(i, rec.value()));
+      for(auto i = 0; i <= diff; i++)
+        conjuncts.push_back(n_Xes(i, rec));
 
-        return n_Xes(from_int, conjunction(conjuncts));
-      }
-      else if(ranged_always.to().id() == ID_infinity)
-      {
-        // always [l:$] op ---> X ... X G op
-        return n_Xes(from_int, G_exprt{rec.value()});
-      }
-      else
-        PRECONDITION(false);
+      return n_Xes(from_int, conjunction(conjuncts));
+    }
+    else if(ranged_always.to().id() == ID_infinity)
+    {
+      // always [l:$] op ---> X ... X G op
+      return n_Xes(from_int, G_exprt{rec});
     }
     else
-      return {};
+      PRECONDITION(false);
   }
   else if(expr.id() == ID_sva_s_always)
   {
     auto &ranged_always = to_sva_s_always_expr(expr);
     auto rec = SVA_to_LTL(ranged_always.op());
-    if(rec.has_value())
-    {
-      // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
-      auto to_int = numeric_cast_v<mp_integer>(ranged_always.to());
-      PRECONDITION(to_int >= from_int);
-      auto diff = to_int - from_int;
 
-      exprt::operandst conjuncts;
+    // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
+    auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
+    auto to_int = numeric_cast_v<mp_integer>(ranged_always.to());
+    PRECONDITION(to_int >= from_int);
+    auto diff = to_int - from_int;
 
-      for(auto i = 0; i <= diff; i++)
-        conjuncts.push_back(n_Xes(i, rec.value()));
+    exprt::operandst conjuncts;
 
-      return n_Xes(from_int, conjunction(conjuncts));
-    }
-    else
-      return {};
+    for(auto i = 0; i <= diff; i++)
+      conjuncts.push_back(n_Xes(i, rec));
+
+    return n_Xes(from_int, conjunction(conjuncts));
   }
   else if(expr.id() == ID_sva_s_eventually)
   {
     auto rec = SVA_to_LTL(to_sva_s_eventually_expr(expr).op());
-    if(rec.has_value())
-      return F_exprt{rec.value()};
-    else
-      return {};
+    return F_exprt{std::move(rec)};
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {
     auto rec = SVA_to_LTL(to_sva_s_nexttime_expr(expr).op());
-    if(rec.has_value())
-      return X_exprt{rec.value()};
-    else
-      return {};
+    return X_exprt{std::move(rec)};
   }
   else if(expr.id() == ID_sva_nexttime)
   {
     auto rec = SVA_to_LTL(to_sva_nexttime_expr(expr).op());
-    if(rec.has_value())
-      return X_exprt{rec.value()};
-    else
-      return {};
+    return X_exprt{std::move(rec)};
   }
   else if(
     expr.id() == ID_sva_overlapped_implication ||
@@ -150,9 +128,6 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
 
       auto property_rec = SVA_to_LTL(implication.property());
 
-      if(!property_rec.has_value())
-        return {};
-
       for(auto &match : matches)
       {
         const auto overlapped = expr.id() == ID_sva_overlapped_implication;
@@ -163,7 +138,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
         else
         {
           auto delay = match.length() + (overlapped ? 0 : 1) - 1;
-          auto delayed_property = n_Xes(delay, property_rec.value());
+          auto delayed_property = n_Xes(delay, property_rec);
           conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
         }
       }
@@ -191,9 +166,6 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
 
       auto property_rec = SVA_to_LTL(followed_by.property());
 
-      if(!property_rec.has_value())
-        return {};
-
       for(auto &match : matches)
       {
         const auto overlapped = expr.id() == ID_sva_overlapped_followed_by;
@@ -204,7 +176,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
         else
         {
           auto delay = match.length() + (overlapped ? 0 : 1) - 1;
-          auto delayed_property = n_Xes(delay, property_rec.value());
+          auto delayed_property = n_Xes(delay, property_rec);
           disjuncts.push_back(and_exprt{ltl(match), delayed_property});
         }
       }
@@ -252,21 +224,15 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     auto &until = to_sva_s_until_expr(expr);
     auto rec_lhs = SVA_to_LTL(until.lhs());
     auto rec_rhs = SVA_to_LTL(until.rhs());
-    if(rec_lhs.has_value() && rec_rhs.has_value())
-      return U_exprt{rec_lhs.value(), rec_rhs.value()};
-    else
-      return {};
+    return U_exprt{rec_lhs, rec_rhs};
   }
   else if(expr.id() == ID_sva_s_until_with)
   {
     // This is release with swapped operands
     auto &until_with = to_sva_s_until_with_expr(expr);
     auto rec_lhs = SVA_to_LTL(until_with.lhs());
     auto rec_rhs = SVA_to_LTL(until_with.rhs());
-    if(rec_lhs.has_value() && rec_rhs.has_value())
-      return R_exprt{rec_rhs.value(), rec_lhs.value()}; // swapped
-    else
-      return {};
+    return R_exprt{rec_rhs, rec_lhs}; // swapped
   }
   else if(!has_temporal_operator(expr))
   {
@@ -279,9 +245,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     for(auto &op : expr.operands())
     {
       auto rec = SVA_to_LTL(op);
-      if(!rec.has_value())
-        return {};
-      op = rec.value();
+      op = rec;
     }
     return expr;
   }

src/temporal-logic/sva_to_ltl.h

@@ -11,8 +11,18 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr.h>
 
+class sva_to_ltl_unsupportedt
+{
+public:
+  explicit sva_to_ltl_unsupportedt(exprt __expr) : expr(std::move(__expr))
+  {
+  }
+
+  exprt expr;
+};
+
 /// If possible, this maps an SVA expression to an equivalent LTL
-/// expression, or otherwise returns {}.
-std::optional<exprt> SVA_to_LTL(exprt);
+/// expression, or otherwise throws \ref sva_to_ltl_unsupportedt.
+exprt SVA_to_LTL(exprt);
 
 #endif

src/trans-netlist/instantiate_netlist.cpp

@@ -179,11 +179,15 @@ std::optional<exprt> netlist_property(
     else if(is_SVA_operator(expr))
     {
       // Try to turn into LTL
-      auto LTL_opt = SVA_to_LTL(expr);
-      if(LTL_opt.has_value())
-        return netlist_property(solver, var_map, *LTL_opt, ns, message_handler);
-      else
+      try
+      {
+        auto LTL = SVA_to_LTL(expr);
+        return netlist_property(solver, var_map, LTL, ns, message_handler);
+      }
+      catch(sva_to_ltl_unsupportedt)
+      {
         return {};
+      }
     }
     else
       return {};

src/trans-netlist/trans_to_netlist.cpp

@@ -391,11 +391,15 @@ convert_trans_to_netlistt::convert_property(const exprt &expr)
     else if(is_SVA_operator(expr))
     {
       // Try to turn into LTL
-      auto LTL_opt = SVA_to_LTL(expr);
-      if(LTL_opt.has_value())
-        return convert_property(*LTL_opt);
-      else
+      try
+      {
+        auto LTL = SVA_to_LTL(expr);
+        return convert_property(LTL);
+      }
+      catch(sva_to_ltl_unsupportedt)
+      {
         return {};
+      }
     }
     else
       return {};