BMC: support full LTL

Full LTL is supported by the word-level BMC engine.

regression/ebmc/smv/smv_ltlspec_F1.desc

@@ -8,8 +8,8 @@ smv_ltlspec_F1.smv
 ^\[.*\] F x = 2: PROVED up to bound 10$
 ^\[.*\] F x = 1 & F x = 2: PROVED up to bound 10$
 ^\[.*\] F x = 0 & F x = 1: REFUTED$
-^\[.*\] F x = 0 \| F x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] F x = 0 -> FALSE: FAILURE: property not supported by BMC engine$
-^\[.*\] F x = 1 -> F x = 0: FAILURE: property not supported by BMC engine$
+^\[.*\] F x = 0 \| F x = 1: PROVED up to bound 10$
+^\[.*\] F x = 0 -> FALSE: PROVED up to bound 10$
+^\[.*\] F x = 1 -> F x = 0: REFUTED$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_F2.desc

@@ -6,10 +6,10 @@ smv_ltlspec_F2.smv
 ^\[.*\] !F x = 0: PROVED up to bound 10$
 ^\[.*\] !F x = 1: REFUTED$
 ^\[.*\] !F x = 2: REFUTED$
-^\[.*\] !\(F x = 1 & F x = 2\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(F x = 0 & F x = 1\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 1 & F x = 2\): REFUTED$
+^\[.*\] !\(F x = 0 & F x = 1\): PROVED up to bound 10$
 ^\[.*\] !\(F x = 0 \| F x = 1\): REFUTED$
-^\[.*\] !\(F x = 0 -> FALSE\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(F x = 1 -> F x = 0\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(F x = 0 -> FALSE\): REFUTED$
+^\[.*\] !\(F x = 1 -> F x = 0\): PROVED up to bound 10$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G1.desc

@@ -8,8 +8,8 @@ smv_ltlspec_G1.smv
 ^\[.*\] G x != 2: REFUTED$
 ^\[.*\] G x != 5 & G x != 6: PROVED up to bound 10$
 ^\[.*\] G x != 2 & G x != 5: REFUTED$
-^\[.*\] G x != 5 \| G x != 2: FAILURE: property not supported by BMC engine$
-^\[.*\] G x != 2 -> FALSE: FAILURE: property not supported by BMC engine$
-^\[.*\] G x != 5 -> G x != 2: FAILURE: property not supported by BMC engine$
+^\[.*\] G x != 5 \| G x != 2: PROVED up to bound 10$
+^\[.*\] G x != 2 -> FALSE: PROVED up to bound 10$
+^\[.*\] G x != 5 -> G x != 2: REFUTED$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_G2.desc

@@ -6,10 +6,10 @@ smv_ltlspec_G2.smv
 ^\[.*\] !G x != 5: REFUTED$
 ^\[.*\] !G x != 6: REFUTED$
 ^\[.*\] !G x != 2: PROVED up to bound 10$
-^\[.*\] !\(G x != 5 & G x != 6\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(G x != 2 & G x != 5\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 5 & G x != 6\): REFUTED$
+^\[.*\] !\(G x != 2 & G x != 5\): PROVED up to bound 10$
 ^\[.*\] !\(G x != 5 \| G x != 2\): REFUTED$
-^\[.*\] !\(G x != 2 -> FALSE\): FAILURE: property not supported by BMC engine$
-^\[.*\] !\(G x != 5 -> G x != 2\): FAILURE: property not supported by BMC engine$
+^\[.*\] !\(G x != 2 -> FALSE\): REFUTED$
+^\[.*\] !\(G x != 5 -> G x != 2\): PROVED up to bound 10$
 --
 ^warning: ignoring

regression/ebmc/smv/smv_ltlspec_R1.desc

@@ -1,12 +1,12 @@
 CORE broken-smt-backend
 smv_ltlspec_R1.smv
 --bound 10
-^\[.*\] x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] FALSE R x != 4: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
-^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: FAILURE: property not supported by BMC engine$
+^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
+^\[.*\] FALSE R x != 4: REFUTED$
+^\[.*\] x = 2 R x = 1: REFUTED$
+^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: REFUTED$
+^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$
+^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/smv/smv_ltlspec_U1.desc

@@ -1,11 +1,11 @@
 CORE broken-smt-backend
 smv_ltlspec_U1.smv
 --bound 10
-\[.*\] x = 1 U x = 2: FAILURE: property not supported by BMC engine$
-\[.*\] x != 0 U FALSE: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 3: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: FAILURE: property not supported by BMC engine$
-\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: FAILURE: property not supported by BMC engine$
+\[.*\] x = 1 U x = 2: PROVED up to bound 10$
+\[.*\] x != 0 U FALSE: PROVED up to bound 10$
+\[.*\] x = 1 U x = 3: REFUTED$
+\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: PROVED up to bound 10$
+\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/temporal-logic/normalize_property.cpp

@@ -64,13 +64,21 @@ exprt normalize_pre_not(not_exprt expr)
     // ¬ sva_s_eventually φ --> sva_always ¬φ
     return sva_always_exprt{not_exprt{to_sva_eventually_expr(op).op()}};
   }
+  else if(op.id() == ID_implies)
+  {
+    // ¬(a->b) --> a && ¬b
+    auto &implies_expr = to_implies_expr(op);
+    return and_exprt{
+      implies_expr.lhs(), normalize_pre_not(not_exprt{implies_expr.rhs()})};
+  }
 
   return std::move(expr);
 }
 
 exprt normalize_pre_implies(implies_exprt expr)
 {
-  return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
+  auto lhs_normalized = normalize_pre_not(not_exprt{expr.lhs()});
+  return or_exprt{lhs_normalized, expr.rhs()};
 }
 
 exprt normalize_pre_sva_overlapped_implication(

src/trans-word-level/instantiate_word_level.cpp

@@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <verilog/sva_expr.h>
 #include <verilog/verilog_expr.h>
 
-#include "property.h"
-
 /*******************************************************************\
 
 Function: timeframe_identifier

src/trans-word-level/property.cpp

@@ -40,44 +40,7 @@ Function: bmc_supports_LTL_property
 
 bool bmc_supports_LTL_property(const exprt &expr)
 {
-  // We support
-  // * formulas that contain no temporal operator besides X
-  // * Gφ, where φ contains no temporal operator besides X
-  // * Fφ, where φ contains no temporal operator besides X
-  // * GFφ, where φ contains no temporal operator besides X
-  // * conjunctions of supported LTL properties
-  auto non_X_LTL_operator = [](const exprt &expr)
-  { return is_LTL_operator(expr) && expr.id() != ID_X; };
-
-  if(!has_subexpr(expr, non_X_LTL_operator))
-  {
-    return true;
-  }
-  else if(expr.id() == ID_F)
-  {
-    return !has_subexpr(to_F_expr(expr).op(), non_X_LTL_operator);
-  }
-  else if(expr.id() == ID_G)
-  {
-    auto &op = to_G_expr(expr).op();
-    if(op.id() == ID_F)
-    {
-      return !has_subexpr(to_F_expr(op).op(), non_X_LTL_operator);
-    }
-    else
-    {
-      return !has_subexpr(op, non_X_LTL_operator);
-    }
-  }
-  else if(expr.id() == ID_and)
-  {
-    for(auto &op : expr.operands())
-      if(!bmc_supports_LTL_property(op))
-        return false;
-    return true;
-  }
-  else
-    return false;
+  return true;
 }
 
 /*******************************************************************\
@@ -432,7 +395,8 @@ static obligationst property_obligations_rec(
     }
   }
   else if(
-    property_expr.id() == ID_sva_until || property_expr.id() == ID_sva_s_until)
+    property_expr.id() == ID_sva_until ||
+    property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
   {
     // non-overlapping until
     // we need a lasso to refute these
@@ -461,6 +425,32 @@ static obligationst property_obligations_rec(
     DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
     return obligationst{no_timeframes - 1, or_exprt(tmp_q, expansion)};
   }
+  else if(property_expr.id() == ID_R)
+  {
+    // we expand: p R q <=> q && (p || X(p R q))
+    auto &R_expr = to_R_expr(property_expr);
+    exprt tmp_q = R_expr.rhs();
+    tmp_q = property_obligations_rec(tmp_q, solver, current, no_timeframes, ns)
+              .conjunction()
+              .second;
+
+    auto expansion =
+      property_obligations_rec(R_expr.lhs(), solver, current, no_timeframes, ns)
+        .conjunction()
+        .second;
+
+    const auto next = current + 1;
+
+    if(next < no_timeframes)
+    {
+      auto obligations_rec = property_obligations_rec(
+        property_expr, solver, next, no_timeframes, ns);
+      expansion = or_exprt(expansion, obligations_rec.conjunction().second);
+    }
+
+    DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
+    return obligationst{no_timeframes - 1, and_exprt(tmp_q, expansion)};
+  }
   else if(
     property_expr.id() == ID_sva_until_with ||
     property_expr.id() == ID_sva_s_until_with)
@@ -546,8 +536,46 @@ static obligationst property_obligations_rec(
   }
   else if(property_expr.id() == ID_not)
   {
-    return obligationst{
-      instantiate_property(property_expr, current, no_timeframes, ns)};
+    auto &op = to_not_expr(property_expr).op();
+
+    if(op.id() == ID_U)
+    {
+      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+      auto &U = to_U_expr(op);
+      auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+      return property_obligations_rec(R, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_R)
+    {
+      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+      auto &R = to_R_expr(op);
+      auto U = U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+      return property_obligations_rec(U, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_G)
+    {
+      // ¬G φ ≡ F ¬φ
+      auto &G = to_G_expr(op);
+      auto F = F_exprt{not_exprt{G.op()}};
+      return property_obligations_rec(F, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_F)
+    {
+      // ¬F φ ≡ G ¬φ
+      auto &F = to_F_expr(op);
+      auto G = G_exprt{not_exprt{F.op()}};
+      return property_obligations_rec(G, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_X)
+    {
+      // ¬X φ ≡ X ¬φ
+      auto &X = to_X_expr(op);
+      auto negX = X_exprt{not_exprt{X.op()}};
+      return property_obligations_rec(negX, solver, current, no_timeframes, ns);
+    }
+    else
+      return obligationst{
+        instantiate_property(property_expr, current, no_timeframes, ns)};
   }
   else
   {