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\): PROVED up to bound 10$
+^\[.*\] !\(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\): PROVED up to bound 10$
+^\[.*\] !\(F x = 1 -> F x = 0\): REFUTED$
 --
 ^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\): PROVED up to bound 10$
+^\[.*\] !\(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\): PROVED up to bound 10$
+^\[.*\] !\(G x != 5 -> G x != 2\): REFUTED$
 --
 ^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: PROVED up to bound 10$
+^\[.*\] x = 2 R x = 1: REFUTED$
+^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: PROVED up to bound 10$
+^\[.*\] 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

@@ -70,7 +70,8 @@ exprt normalize_pre_not(not_exprt 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;
 }
 
 /*******************************************************************\