Merge pull request #8441 from diffblue/zero_expr

introduce `zero_expr()` and `one_expr()` for number types

Author: kroening

src/util/mathematical_types.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "mathematical_types.h"
 
+#include "std_expr.h"
+
 /// Returns true if the type is a rational, real, integer, natural, complex,
 /// unsignedbv, signedbv, floatbv or fixedbv.
 bool is_number(const typet &type)
@@ -21,3 +23,43 @@ bool is_number(const typet &type)
          id == ID_natural || id == ID_complex || id == ID_unsignedbv ||
          id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv;
 }
+
+constant_exprt integer_typet::zero_expr() const
+{
+  return constant_exprt{ID_0, *this};
+}
+
+constant_exprt integer_typet::one_expr() const
+{
+  return constant_exprt{ID_1, *this};
+}
+
+constant_exprt natural_typet::zero_expr() const
+{
+  return constant_exprt{ID_0, *this};
+}
+
+constant_exprt natural_typet::one_expr() const
+{
+  return constant_exprt{ID_1, *this};
+}
+
+constant_exprt rational_typet::zero_expr() const
+{
+  return constant_exprt{ID_0, *this};
+}
+
+constant_exprt rational_typet::one_expr() const
+{
+  return constant_exprt{ID_1, *this};
+}
+
+constant_exprt real_typet::zero_expr() const
+{
+  return constant_exprt{ID_0, *this};
+}
+
+constant_exprt real_typet::one_expr() const
+{
+  return constant_exprt{ID_1, *this};
+}

src/util/mathematical_types.h

@@ -17,13 +17,18 @@ Author: Daniel Kroening, [email protected]
 #include "invariant.h"
 #include "type.h"
 
+class constant_exprt;
+
 /// Unbounded, signed integers (mathematical integers, not bitvectors)
 class integer_typet : public typet
 {
 public:
   integer_typet() : typet(ID_integer)
   {
   }
+
+  constant_exprt zero_expr() const;
+  constant_exprt one_expr() const;
 };
 
 /// Natural numbers including zero (mathematical integers, not bitvectors)
@@ -33,6 +38,9 @@ class natural_typet : public typet
   natural_typet() : typet(ID_natural)
   {
   }
+
+  constant_exprt zero_expr() const;
+  constant_exprt one_expr() const;
 };
 
 /// Unbounded, signed rational numbers
@@ -42,6 +50,9 @@ class rational_typet : public typet
   rational_typet() : typet(ID_rational)
   {
   }
+
+  constant_exprt zero_expr() const;
+  constant_exprt one_expr() const;
 };
 
 /// Unbounded, signed real numbers
@@ -51,6 +62,9 @@ class real_typet : public typet
   real_typet() : typet(ID_real)
   {
   }
+
+  constant_exprt zero_expr() const;
+  constant_exprt one_expr() const;
 };
 
 /// A type for mathematical functions (do not confuse with functions/methods