Add is_always_simplified field in guard implementations

Expressions obtained from BDDs are already simple. Trying to simplify
them is redundant and can slow down the execution.
We add this field so that symex code can take the decision to simplify
or not an expression based on this information.

Author: romainbrenguier

src/analyses/guard_bdd.h

@@ -35,6 +35,11 @@ class guard_bddt
   guard_bddt &append(const guard_bddt &guard);
   exprt as_expr() const;
 
+  /// BDDs are always in a simplified form and thus no further simplification
+  /// is required after calls to \ref as_expr().
+  /// This can vary according to the guard implementation.
+  static constexpr bool is_always_simplified = true;
+
   /// Assign dest to `guard => dest` unless guard or dest are trivial.
   void guard_expr(exprt &dest) const;
 

src/analyses/guard_expr.h

@@ -50,6 +50,11 @@ class guard_exprt
     return expr;
   }
 
+  /// The result of \ref as_expr is not always in a simplified form
+  /// and may requires some simplification.
+  /// This can vary according to the guard implementation.
+  static constexpr bool is_always_simplified = false;
+
   void guard_expr(exprt &dest) const;
 
   bool is_true() const