Merge pull request #6806 from diffblue/division

convenience methods for division expressions

Author: kroening

src/util/std_expr.h

@@ -1171,6 +1171,30 @@ class mod_exprt:public binary_exprt
     : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
   {
   }
+
+  /// The dividend of a division is the number that is being divided
+  exprt &dividend()
+  {
+    return op0();
+  }
+
+  /// The dividend of a division is the number that is being divided
+  const exprt &dividend() const
+  {
+    return op0();
+  }
+
+  /// The divisor of a division is the number the dividend is being divided by
+  exprt &divisor()
+  {
+    return op1();
+  }
+
+  /// The divisor of a division is the number the dividend is being divided by
+  const exprt &divisor() const
+  {
+    return op1();
+  }
 };
 
 template <>
@@ -1215,6 +1239,30 @@ class euclidean_mod_exprt : public binary_exprt
     : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
   {
   }
+
+  /// The dividend of a division is the number that is being divided
+  exprt &dividend()
+  {
+    return op0();
+  }
+
+  /// The dividend of a division is the number that is being divided
+  const exprt &dividend() const
+  {
+    return op0();
+  }
+
+  /// The divisor of a division is the number the dividend is being divided by
+  exprt &divisor()
+  {
+    return op1();
+  }
+
+  /// The divisor of a division is the number the dividend is being divided by
+  const exprt &divisor() const
+  {
+    return op1();
+  }
 };
 
 template <>