Allow simplification of singleton interval.

Before this change, an expression like `value >= 255 && value <= 255`
would fail to be simplified to `value == 255` by the expression
simplifier.

While the simplification itself is useful, the *lack* of it was causing
some misbehaviour in one of our backends (the old SMT one under
`src/solvers/smt2`) because the lack of simplification resulted
in less constraints being propagated to the solver, missing some assertions
around the expression that was using `value` as the size of an array.

Author: NlightNFotis

src/util/simplify_expr_boolean.cpp

@@ -99,6 +99,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
     bool no_change = true;
     bool may_be_reducible_to_interval =
       expr.id() == ID_or && expr.operands().size() > 2;
+    bool may_be_reducible_to_singleton_interval =
+      expr.id() == ID_and && expr.operands().size() == 2;
 
     exprt::operandst new_operands = expr.operands();
 
@@ -137,6 +139,102 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
       }
     }
 
+    // This block reduces singleton intervals like (value >= 255 && value <= 255)
+    // to just (value == 255). We also need to be careful with the operands
+    // as some of them are erased in the previous step. We proceed only if
+    // no operands have been erased (i.e. the expression structure has been
+    // preserved by previous simplification rounds.)
+    if(may_be_reducible_to_singleton_interval && new_operands.size() == 2)
+    {
+      struct boundst
+      {
+        mp_integer lower;
+        mp_integer higher;
+      };
+      boundst bounds;
+      bool structure_matched = false;
+
+      // Before we do anything else, we need to "pattern match" against the
+      // expression and make sure that it has the structure we're looking for.
+      // The structure we're looking for is going to be
+      //      (value >= 255 && !(value >= 256))   -- 255, 256 values indicative.
+      // (this is because previous simplification runs will have transformed
+      //  the less_than_or_equal expression to a not(greater_than_or_equal) expression)
+
+      // matching (value >= 255)
+      auto const match_first_operand = [&bounds](const exprt &op) -> bool
+      {
+        if(
+          const auto ge_expr =
+            expr_try_dynamic_cast<greater_than_or_equal_exprt>(op))
+        {
+          // The construction of these expressions ensures that the RHS is constant,
+          // therefore if we don't have a constant, it's a different expression, so
+          // we bail.
+          if(!ge_expr->rhs().is_constant())
+            return false;
+          if(
+            auto int_opt =
+              numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
+          {
+            bounds.lower = *int_opt;
+            return true;
+          }
+          return false;
+        }
+        return false;
+      };
+
+      // matching !(value >= 256)
+      auto const match_second_operand = [&bounds](const exprt &op) -> bool
+      {
+        if(const auto not_expr = expr_try_dynamic_cast<not_exprt>(op))
+        {
+          PRECONDITION(not_expr->operands().size() == 1);
+          if(
+            const auto ge_expr =
+              expr_try_dynamic_cast<greater_than_or_equal_exprt>(
+                not_expr->op()))
+          {
+            // If the rhs() is not constant, it has a different structure (e.g. i >= j)
+            if(!ge_expr->rhs().is_constant())
+              return false;
+            if(
+              auto int_opt =
+                numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
+            {
+              bounds.higher = *int_opt - 1;
+              return true;
+            }
+            return false;
+          }
+          return false;
+        }
+        return false;
+      };
+
+      // We need to match both operands, at the particular sequence we expect.
+      structure_matched |= match_first_operand(new_operands[0]);
+      structure_matched &= match_second_operand(new_operands[1]);
+
+      if(structure_matched && bounds.lower == bounds.higher)
+      {
+        // Go through the expression again and convert >= operand into ==
+        for(const auto &op : new_operands)
+        {
+          if(
+            const auto ge_expr =
+              expr_try_dynamic_cast<greater_than_or_equal_exprt>(op))
+          {
+            equal_exprt new_expr{ge_expr->lhs(), ge_expr->rhs()};
+            return changed(new_expr);
+          }
+          else
+            continue;
+        }
+      }
+    }
+
     if(may_be_reducible_to_interval)
     {
       optionalt<symbol_exprt> symbol_opt;