Introduce euclidean_mod expression

This introduces a variant of the modulo operator, to be used on integers,
which uses Boute's Euclidean definition.  The result is never negative, and
thus differs from the C99 "%" operator.  The semantics match what SMT-LIB2
does in the integer theory.

The operator % is not defined by SMT-LIB2, and is removed from the parser.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1285,6 +1285,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_mod(to_mod_expr(expr));
   }
+  else if(expr.id() == ID_euclidean_mod)
+  {
+    convert_euclidean_mod(to_euclidean_mod_expr(expr));
+  }
   else if(expr.id()==ID_mult)
   {
     convert_mult(to_mult_expr(expr));
@@ -2988,6 +2992,21 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
     UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
 }
 
+void smt2_convt::convert_euclidean_mod(const euclidean_mod_exprt &expr)
+{
+  if(expr.type().id() == ID_integer)
+  {
+    out << "(mod ";
+    convert_expr(expr.op0());
+    out << ' ';
+    convert_expr(expr.op1());
+    out << ')';
+  }
+  else
+    UNEXPECTEDCASE(
+      "unsupported type for euclidean_mod: " + expr.type().id_string());
+}
+
 void smt2_convt::convert_mod(const mod_exprt &expr)
 {
   if(expr.type().id()==ID_unsignedbv ||

src/solvers/smt2/smt2_conv.h

@@ -120,6 +120,7 @@ class smt2_convt : public stack_decision_proceduret
   void convert_floatbv_div(const ieee_float_op_exprt &expr);
   void convert_floatbv_mult(const ieee_float_op_exprt &expr);
   void convert_mod(const mod_exprt &expr);
+  void convert_euclidean_mod(const euclidean_mod_exprt &expr);
   void convert_index(const index_exprt &expr);
   void convert_member(const member_exprt &expr);
 

src/solvers/smt2/smt2_parser.cpp

@@ -1067,7 +1067,12 @@ void smt2_parsert::setup_expressions()
 
   expressions["bvurem"] = [this] { return binary(ID_mod, operands()); };
 
-  expressions["%"] = [this] { return binary(ID_mod, operands()); };
+  expressions["mod"] = [this] {
+    // SMT-LIB2 uses Boute's Euclidean definition for mod,
+    // which is never negative and undefined when the second
+    // argument is zero.
+    return binary(ID_euclidean_mod, operands());
+  };
 
   expressions["concat"] = [this] {
     auto op = operands();

src/util/irep_ids.def

@@ -235,6 +235,7 @@ IREP_ID_ONE(array_equal)
 IREP_ID_ONE(array_set)
 IREP_ID_ONE(array_copy)
 IREP_ID_ONE(array_list)
+IREP_ID_ONE(euclidean_mod)
 IREP_ID_ONE(mod)
 IREP_ID_ONE(rem)
 IREP_ID_ONE(shr)

src/util/std_expr.h

@@ -1088,6 +1088,50 @@ inline mod_exprt &to_mod_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Boute's Euclidean definition of Modulo -- to match SMT-LIB2
+class euclidean_mod_exprt : public binary_exprt
+{
+public:
+  euclidean_mod_exprt(exprt _lhs, exprt _rhs)
+    : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<euclidean_mod_exprt>(const exprt &base)
+{
+  return base.id() == ID_euclidean_mod;
+}
+
+inline void validate_expr(const euclidean_mod_exprt &value)
+{
+  validate_operands(value, 2, "Modulo must have two operands");
+}
+
+/// \brief Cast an exprt to a \ref euclidean_mod_exprt
+///
+/// \a expr must be known to be \ref euclidean_mod_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref euclidean_mod_exprt
+inline const euclidean_mod_exprt &to_euclidean_mod_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_euclidean_mod);
+  const euclidean_mod_exprt &ret =
+    static_cast<const euclidean_mod_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_euclidean_mod_expr(const exprt &)
+inline euclidean_mod_exprt &to_euclidean_mod_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_euclidean_mod);
+  euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
 
 /// \brief Remainder of division
 class rem_exprt:public binary_exprt