Reimplemented assume_greater_than in terms of assume_less_than

These operations are symmetric, so we can rewrite x > y as y < x, and
x >= y as y <= x.  As a consequence of rewriting, greater than
assumptions now also prune.

Author: jezhiggins

regression/goto-analyzer/pruning-gt/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int x = 0;
+  if(nondet())
+  {
+    x = 30;
+  }
+
+  if(x > 20)
+  {
+    assert(x > 10);
+  }
+}

regression/goto-analyzer/pruning-gt/test-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x > 10: UNKNOWN
+
+--

regression/goto-analyzer/pruning-gt/test-intervals.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x > 10: SUCCESS
+--

regression/goto-analyzer/pruning-gt/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x > 10: SUCCESS
+--

…gression/goto-analyzer/pruning-le/main.c …gression/goto-analyzer/pruning-lt/main.cregression/goto-analyzer/pruning-le/main.c renamed to regression/goto-analyzer/pruning-lt/main.c regression/goto-analyzer/pruning-le/main.c renamed to regression/goto-analyzer/pruning-lt/main.c

@@ -743,19 +743,19 @@ exprt assume_less_than(
   return result;
 }
 
+static auto symmetric_operations =
+  std::map<irep_idt, irep_idt>{{ID_ge, ID_le}, {ID_gt, ID_lt}};
+
 exprt assume_greater_than(
   abstract_environmentt &env,
   const exprt &expr,
   const namespacet &ns)
 {
-  auto operands = eval_operands_as_values(env, expr, ns);
-  if(!operands.are_good())
-    return nil_exprt();
+  auto const &gt_expr = to_binary_expr(expr);
 
-  auto left_upper = operands.left_interval().get_upper();
-  auto right_lower = operands.right_interval().get_lower();
+  auto symmetric_op = symmetric_operations[gt_expr.id()];
+  auto symmetric_expr =
+    binary_relation_exprt(gt_expr.rhs(), symmetric_op, gt_expr.lhs());
 
-  auto reduced_ge_expr =
-    binary_relation_exprt(left_upper, expr.id(), right_lower);
-  return env.eval(reduced_ge_expr, ns)->to_constant();
+  return assume_less_than(env, symmetric_expr, ns);
 }

…-analyzer/pruning-le/test-constants.desc …-analyzer/pruning-lt/test-constants.descregression/goto-analyzer/pruning-le/test-constants.desc renamed to regression/goto-analyzer/pruning-lt/test-constants.desc regression/goto-analyzer/pruning-le/test-constants.desc renamed to regression/goto-analyzer/pruning-lt/test-constants.desc

@@ -455,6 +455,10 @@ abstract_value_pointert interval_abstract_valuet::constrain(
   auto upper_bound =
     constant_interval_exprt::get_min(upper, interval.get_upper());
 
+  if(constant_interval_exprt::greater_than(lower_bound, upper_bound))
+    return as_value(mutable_clone());
+
+  auto constrained_interval = constant_interval_exprt(lower_bound, upper_bound);
   return as_value(
     make_interval(constant_interval_exprt(lower_bound, upper_bound)));
 }