Optimise size to have approximate bound

This optimises the size function that was only used when
checking for a bound. The new bounded_size takes an
explicit bound argument and reduces the search when
this bound is (approximately) reached.

Author: TGWDB

src/goto-symex/complexity_limiter.cpp

@@ -136,7 +136,7 @@ complexity_limitert::check_complexity(goto_symex_statet &state)
   if(!complexity_limits_active() || !state.reachable)
     return complexity_violationt::NONE;
 
-  std::size_t complexity = state.complexity();
+  std::size_t complexity = state.guard.as_expr().bounded_size(max_complexity);
   if(complexity == 0)
     return complexity_violationt::NONE;
 

src/goto-symex/goto_state.h

@@ -71,15 +71,6 @@ class goto_statet
   /// Threads
   unsigned atomic_section_id = 0;
 
-  /// Get the complexity for this state. Used to short-circuit states if they
-  /// have become too computationally complex.
-  inline std::size_t complexity()
-  {
-    // TODO: This isn't too efficent for BDDs, try using a different size
-    // like DAG size.
-    return guard.as_expr().size();
-  }
-
   /// Constructors
   goto_statet() = delete;
   goto_statet &operator=(const goto_statet &other) = delete;

src/util/expr.cpp

@@ -24,16 +24,28 @@ Author: Daniel Kroening, [email protected]
 
 #include <stack>
 
-std::size_t exprt::size() const
+/// Returns the size of the exprt added to count without searching significantly
+/// beyond the supplied limit.
+std::size_t exprt::bounded_size(std::size_t count, std::size_t limit) const
 {
-  // Initial size of 1 to count self.
-  std::size_t size = 1;
-  for(const auto &op : operands())
+  const auto &ops = operands();
+  count += ops.size();
+  for(const auto &op : ops)
   {
-    size += op.size();
+    if(count >= limit)
+    {
+      return count;
+    }
+    count = op.bounded_size(count, limit);
   }
+  return count;
+}
 
-  return size;
+/// Returns the size of the exprt without significantly searching beyond the
+/// supplied limit.
+std::size_t exprt::bounded_size(std::size_t limit) const
+{
+  return bounded_size(1, limit);
 }
 
 /// Return whether the expression is a constant.

src/util/expr.h

@@ -85,9 +85,9 @@ class exprt:public irept
     return static_cast<const typet &>(find(ID_type));
   }
 
-  /// Amount of nodes this expression tree contains. This is the size of the
-  /// actual tree, ignoring memory/sub-tree sharing.
-  std::size_t size() const;
+  /// Amount of nodes in this expression tree approximately bounded by limit.
+  /// This is the size of the actual tree, ignoring memory/sub-tree sharing.
+  std::size_t bounded_size(std::size_t limit) const;
 
   /// Return true if there is at least one operand.
   bool has_operands() const
@@ -124,6 +124,10 @@ class exprt:public irept
   const exprt &op3() const
   { return operands()[3]; }
 
+  /// Amount of nodes this expression tree contains, with a bound on how far
+  /// to search. Starts with an existing count.
+  std::size_t bounded_size(std::size_t count, std::size_t limit) const;
+
 public:
   void reserve_operands(operandst::size_type n)
   { operands().reserve(n) ; }