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,11 @@
+CORE
+smv_ltlspec3.smv
+--bound 10 --numbered-trace
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] X X main::var::x = 1: REFUTED$
+^main::var::x@0 = 0$
+^main::var::x@1 = 0$
+^main::var::x@2 = 0$
+--
+^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,10 @@ 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

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ebmc_util.h>
 
+#include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
 
 #include "property.h"
@@ -235,6 +236,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
@@ -60,7 +62,7 @@ bool bmc_supports_property(const exprt &expr)
 
 /*******************************************************************\
 
-Function: property
+Function: property_obligations_rec
 
   Inputs:
 
@@ -70,51 +72,77 @@ Function: property
 
 \*******************************************************************/
 
-std::map<std::size_t, exprt::operandst> property_obligations(
+void property_obligations_rec(
   const exprt &property_expr,
-  message_handlert &message_handler,
   decision_proceduret &solver,
+  std::size_t current,
   std::size_t no_timeframes,
-  const namespacet &ns)
+  const namespacet &ns,
+  std::map<std::size_t, exprt::operandst> &obligations)
 {
-  PRECONDITION(no_timeframes > 0);
+  PRECONDITION(current < no_timeframes);
 
-  std::map<std::size_t, exprt::operandst> obligations;
-
-  messaget message(message_handler);
-
-  // Initial state only 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)
+  if(property_expr.id() == ID_X)
   {
-    exprt tmp = instantiate(property_expr, 0, no_timeframes, ns);
-    obligations[0].push_back(solver.handle(tmp));
-    return obligations;
+    auto next = current + 1;
+    if(next < no_timeframes)
+    {
+      auto &op = to_X_expr(property_expr).op();
+      property_obligations_rec(
+        op, solver, next, no_timeframes, ns, obligations);
+    }
   }
+  else if(
+    property_expr.id() == ID_AG || property_expr.id() == ID_G ||
+    property_expr.id() == ID_sva_always)
+  {
+    // We want AG phi.
+    auto &phi = [](const exprt &expr) -> const exprt & {
+      if(expr.id() == ID_AG)
+        return to_AG_expr(expr).op();
+      else if(expr.id() == ID_G)
+        return to_G_expr(expr).op();
+      else if(expr.id() == ID_sva_always)
+        return to_sva_always_expr(expr).op();
+      else
+        PRECONDITION(false);
+    }(property_expr);
+
+    for(std::size_t c = current; c < no_timeframes; c++)
+    {
+      property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
+    }
+  }
+  else
+  {
+    // current state property
+    exprt tmp = instantiate(property_expr, current, no_timeframes, ns);
+    obligations[current].push_back(solver.handle(tmp));
+  }
+}
 
-  // We want AG p.
-  auto &p = [](const exprt &expr) -> const exprt & {
-    if(expr.id() == ID_AG)
-      return to_AG_expr(expr).op();
-    else if(expr.id() == ID_G)
-      return to_G_expr(expr).op();
-    else if(expr.id() == ID_sva_always)
-      return to_sva_always_expr(expr).op();
-    else
-      PRECONDITION(false);
-  }(property_expr);
+/*******************************************************************\
 
-  for(std::size_t c = 0; c < no_timeframes; c++)
-  {
-    exprt tmp=
-      instantiate(p, c, no_timeframes, ns);
+Function: property_obligations
 
-    auto handle = solver.handle(tmp);
-    obligations[c].push_back(std::move(handle));
-  }
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::map<std::size_t, exprt::operandst> property_obligations(
+  const exprt &property_expr,
+  decision_proceduret &solver,
+  std::size_t no_timeframes,
+  const namespacet &ns)
+{
+  std::map<std::size_t, exprt::operandst> obligations;
+
+  property_obligations_rec(
+    property_expr, solver, 0, no_timeframes, ns, obligations);
 
   return obligations;
 }
@@ -142,8 +170,8 @@ void property(
   // The first element of the pair is the length of the
   // counterexample, and the second is the condition that
   // must be valid for the property to hold.
-  auto obligations = property_obligations(
-    property_expr, message_handler, solver, no_timeframes, ns);
+  auto obligations =
+    property_obligations(property_expr, solver, no_timeframes, ns);
 
   // Map obligations onto timeframes.
   prop_handles.resize(no_timeframes, true_exprt());