BMC now checks for use of lasso symbol

Instead of examining the property, the BMC engine now looks for the use of a
lasso symbol in the property encoding.

This prevents a mismatch between the two methods.

Author: kroening

src/ebmc/bmc.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "bmc.h"
 
 #include <solvers/prop/literal_expr.h>
+#include <trans-word-level/lasso.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
@@ -218,6 +219,8 @@ property_checker_resultt bmc(
   // convert the properties
   message.status() << "Properties" << messaget::eom;
 
+  bool requires_lasso_constraints = false;
+
   for(auto &property : properties.properties)
   {
     if(property.is_disabled() || property.is_failure())
@@ -233,13 +236,16 @@ property_checker_resultt bmc(
     property.timeframe_handles = ::property(
       property.normalized_expr, message_handler, solver, bound + 1, ns);
 
+    if(uses_lasso_symbol(property.timeframe_handles))
+      requires_lasso_constraints = true;
+
     // If it's an assumption, then add it as constraint.
     if(property.is_assumed())
       solver.set_to_true(conjunction(property.timeframe_handles));
   }
 
   // lasso constraints, if needed
-  if(properties.requires_lasso_constraints())
+  if(requires_lasso_constraints)
   {
     message.status() << "Adding lasso constraints" << messaget::eom;
     lasso_constraints(

src/ebmc/ebmc_properties.h

@@ -199,11 +199,6 @@ class ebmc_propertiest
 
     propertyt() = default;
 
-    bool requires_lasso_constraints() const
-    {
-      return ::requires_lasso_constraints(normalized_expr);
-    }
-
     bool is_exists_path() const
     {
       return ::is_exists_path(original_expr);
@@ -236,15 +231,6 @@ class ebmc_propertiest
     return false;
   }
 
-  bool requires_lasso_constraints() const
-  {
-    for(const auto &p : properties)
-      if(!p.is_disabled() && p.requires_lasso_constraints())
-        return true;
-
-    return false;
-  }
-
   static ebmc_propertiest from_command_line(
     const cmdlinet &,
     const transition_systemt &,

src/trans-word-level/lasso.cpp

@@ -59,13 +59,15 @@ Function: lasso_symbol
 
 \*******************************************************************/
 
+#define LASSO_PREFIX "lasso::"
+
 symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i)
 {
   // True when states i and k are equal.
   // We require k<i to avoid the symmetric constraints.
   PRECONDITION(k < i);
   irep_idt lasso_identifier =
-    "lasso::" + integer2string(i) + "-back-to-" + integer2string(k);
+    LASSO_PREFIX + integer2string(i) + "-back-to-" + integer2string(k);
   return symbol_exprt(lasso_identifier, bool_typet());
 }
 
@@ -136,7 +138,7 @@ void lasso_constraints(
 
 /*******************************************************************\
 
-Function: requires_lasso_constraints
+Function: uses_lasso_symbol
 
   Inputs:
 
@@ -146,21 +148,38 @@ Function: requires_lasso_constraints
 
 \*******************************************************************/
 
-bool requires_lasso_constraints(const exprt &expr)
+bool uses_lasso_symbol(const exprt &expr)
 {
   for(auto subexpr_it = expr.depth_cbegin(), subexpr_end = expr.depth_cend();
       subexpr_it != subexpr_end;
       subexpr_it++)
   {
-    if(
-      subexpr_it->id() == ID_sva_until || subexpr_it->id() == ID_sva_s_until ||
-      subexpr_it->id() == ID_sva_eventually ||
-      subexpr_it->id() == ID_sva_s_eventually || subexpr_it->id() == ID_AF ||
-      subexpr_it->id() == ID_F || subexpr_it->id() == ID_U)
-    {
-      return true;
-    }
+    if(subexpr_it->id() == ID_symbol)
+      if(to_symbol_expr(*subexpr_it).get_identifier().starts_with(LASSO_PREFIX))
+      {
+        return true;
+      }
   }
 
   return false;
 }
+
+/*******************************************************************\
+
+Function: uses_lasso_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool uses_lasso_symbol(const exprt::operandst &exprs)
+{
+  for(auto &expr : exprs)
+    if(::uses_lasso_symbol(expr))
+      return true;
+  return false;
+}

src/trans-word-level/lasso.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_TRANS_WORD_LEVEL_LASSO_H
 #define CPROVER_TRANS_WORD_LEVEL_LASSO_H
 
+#include <util/expr.h>
 #include <util/mp_arith.h>
 #include <util/namespace.h>
 
@@ -26,7 +27,7 @@ void lasso_constraints(
 /// Precondition: k<i
 symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i);
 
-/// Returns true iff the given property requires lasso constraints for BMC.
-bool requires_lasso_constraints(const exprt &);
+/// Returns true iff the given formula uses a lasso symbol
+bool uses_lasso_symbol(const exprt::operandst &);
 
 #endif

src/trans-word-level/property.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "instantiate_word_level.h"
 #include "obligations.h"
+#include "lasso.h"
 #include "sequence.h"
 
 #include <cstdlib>

src/trans-word-level/property.h

@@ -26,21 +26,6 @@ exprt::operandst property(
 /// Is the given property supported by word-level unwinding?
 bool bmc_supports_property(const exprt &);
 
-/// Adds a constraint that can be used to determine whether the
-/// given state has already been seen earlier in the trace.
-void lasso_constraints(
-  decision_proceduret &,
-  const mp_integer &no_timeframes,
-  const namespacet &,
-  const irep_idt &module_identifier);
-
-/// Is there a loop from i back to k?
-/// Precondition: k<i
-symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i);
-
-/// Returns true iff the given property requires lasso constraints for BMC.
-bool requires_lasso_constraints(const exprt &);
-
 class obligationst;
 
 obligationst property_obligations(