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>
 
@@ -191,6 +192,17 @@ void bmc_with_iterative_constraint_strengthening(
   }
 }
 
+/// Extension of solver.handle(...) from expressions to vectors of expressions
+static exprt::operandst
+handles(const exprt::operandst &exprs, decision_proceduret &solver)
+{
+  exprt::operandst result;
+  result.reserve(exprs.size());
+  for(auto &expr : exprs)
+    result.push_back(solver.handle(expr));
+  return result;
+}
+
 property_checker_resultt bmc(
   std::size_t bound,
   bool convert_only,
@@ -211,13 +223,21 @@ property_checker_resultt bmc(
 
   auto solver_wrapper = solver_factory(ns, message_handler);
   auto &solver = solver_wrapper.decision_procedure();
+  auto no_timeframes = bound + 1;
 
   ::unwind(
-    transition_system.trans_expr, message_handler, solver, bound + 1, ns, true);
+    transition_system.trans_expr,
+    message_handler,
+    solver,
+    no_timeframes,
+    ns,
+    true);
 
   // 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())
@@ -230,20 +250,25 @@ property_checker_resultt bmc(
       continue;
     }
 
-    property.timeframe_handles = ::property(
-      property.normalized_expr, message_handler, solver, bound + 1, ns);
+    auto obligations =
+      ::property(property.normalized_expr, message_handler, no_timeframes);
+
+    if(uses_lasso_symbol(obligations))
+      requires_lasso_constraints = true;
+
+    property.timeframe_handles = handles(obligations, solver);
 
     // 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(
-      solver, bound + 1, ns, transition_system.main_symbol->name);
+      solver, no_timeframes, ns, transition_system.main_symbol->name);
   }
 
   if(convert_only)

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

@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ebmc_util.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
-#include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -24,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <verilog/sva_expr.h>
 
 #include "instantiate_word_level.h"
+#include "lasso.h"
 #include "obligations.h"
 #include "sequence.h"
 
@@ -797,9 +797,7 @@ Function: property
 exprt::operandst property(
   const exprt &property_expr,
   message_handlert &message_handler,
-  decision_proceduret &solver,
-  std::size_t no_timeframes,
-  const namespacet &)
+  std::size_t no_timeframes)
 {
   // The first element of the pair is the length of the
   // counterexample, and the second is the condition that
@@ -815,7 +813,7 @@ exprt::operandst property(
     DATA_INVARIANT(
       t >= 0 && t < no_timeframes, "obligation must have valid timeframe");
     auto t_int = numeric_cast_v<std::size_t>(t);
-    prop_handles[t_int] = solver.handle(conjunction(obligation_it.second));
+    prop_handles[t_int] = conjunction(obligation_it.second);
   }
 
   return prop_handles;

src/trans-word-level/property.h

@@ -12,35 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr.h>
 #include <util/message.h>
 #include <util/mp_arith.h>
-#include <util/namespace.h>
-
-#include <solvers/decision_procedure.h>
 
+/// returns a vector of obligation expressions, one per timeframe
 exprt::operandst property(
   const exprt &property_expr,
   message_handlert &,
-  decision_proceduret &solver,
-  std::size_t no_timeframes,
-  const namespacet &);
+  std::size_t no_timeframes);
 
 /// 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(