BMC: add support for LTL X operator

This adds support for the LTL X operator to the BMC engine.

Author: kroening

regression/ebmc/smv/smv_ltlspec3.desc

@@ -0,0 +1,8 @@
+CORE
+smv_ltlspec3.smv
+--bound 2
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] X X main::var::x = 1: REFUTED$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ltlspec3.smv

@@ -0,0 +1,10 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 0;
+  next(x) := x;
+
+-- we want to see a trace with three states
+LTLSPEC X X x=1

src/temporal-logic/temporal_expr.h

@@ -235,11 +235,11 @@ static inline A_exprt &to_A_expr(exprt &expr)
   return static_cast<A_exprt &>(expr);
 }
 
-class X_exprt : public binary_predicate_exprt
+class X_exprt : public unary_predicate_exprt
 {
 public:
-  explicit X_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_X, std::move(op1))
+  explicit X_exprt(exprt op)
+    : unary_predicate_exprt(ID_X, std::move(op))
   {
   }
 };

src/trans-word-level/instantiate_word_level.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <verilog/sva_expr.h>
 
+#include <temporal-logic/temporal_expr.h>
+
 #include "property.h"
 
 #include <cassert>
@@ -235,6 +237,17 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
     else
       return true_exprt(); // works on NNF only
   }
+  else if(expr.id()==ID_X)
+  {
+    const auto next = t + 1;
+
+    if(next < no_timeframes)
+    {
+      return instantiate_rec(to_X_expr(expr).op(), next);
+    }
+    else
+      return true_exprt(); // works on NNF only
+  }
   else if(expr.id() == ID_sva_eventually)
   {
     const auto &eventually_expr = to_sva_eventually_expr(expr);

src/trans-word-level/property.cpp

@@ -52,6 +52,8 @@ bool bmc_supports_property(const exprt &expr)
     return true;
   else if(expr.id() == ID_G)
     return true;
+  else if(expr.id() == ID_X)
+    return bmc_supports_property(to_X_expr(expr).op());
   else if(expr.id() == ID_sva_always)
     return true;
   else
@@ -83,12 +85,13 @@ std::map<std::size_t, exprt::operandst> property_obligations(
 
   messaget message(message_handler);
 
-  // Initial state only property?
+  // Initial state property?
   if(
     !is_temporal_operator(property_expr) ||
     property_expr.id() == ID_sva_cycle_delay ||
     property_expr.id() == ID_sva_nexttime ||
-    property_expr.id() == ID_sva_s_nexttime)
+    property_expr.id() == ID_sva_s_nexttime ||
+    property_expr.id() == ID_X)
   {
     exprt tmp = instantiate(property_expr, 0, no_timeframes, ns);
     obligations[0].push_back(solver.handle(tmp));