diff --git a/src/util/std_expr.h b/src/util/std_expr.h index eb58cb0ad0d..6e041aecb0e 100644 --- a/src/util/std_expr.h +++ b/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 ÷nd() + { + return op0(); + } + + /// The dividend of a division is the number that is being divided + const exprt ÷nd() 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 ÷nd() + { + return op0(); + } + + /// The dividend of a division is the number that is being divided + const exprt ÷nd() 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 <>