Improve FF utility class (cvc5#10129)

* FfSize wraps field sizes that have been tested to be prime * add in-place operators * a few random helpers: isZero, isOne
ajreynol · Nov 14, 2023 · 4c9b37b · 4c9b37b
1 parent 53486ac
commit 4c9b37b
Show file tree

Hide file tree

Showing 3 changed files with 114 additions and 34 deletions.
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
@@ -229,7 +229,7 @@ bool Smt2Printer::toStreamBase(std::ostream& out,
       out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
       break;
     case Kind::FINITE_FIELD_TYPE:
-      out << "(_ FiniteField " << n.getConst<FfSize>().d_size << ")";
+      out << "(_ FiniteField " << n.getConst<FfSize>().d_val << ")";
       break;
     case Kind::FLOATINGPOINT_TYPE:
       out << "(_ FloatingPoint "

diff --git a/src/util/finite_field_value.cpp b/src/util/finite_field_value.cpp
@@ -21,13 +21,17 @@ namespace cvc5::internal {
 
 const Integer& FiniteFieldValue::getValue() const { return d_value; }
 
+bool FiniteFieldValue::isZero() const { return d_value.isZero(); }
+
+bool FiniteFieldValue::isOne() const { return d_value.isOne(); }
+
 const Integer& FiniteFieldValue::getFieldSize() const { return d_size; }
 
 Integer FiniteFieldValue::toInteger() const { return d_value; }
 
 Integer FiniteFieldValue::toSignedInteger() const
 {
-  Integer half_size = d_size.divByPow2(1) + 1;
+  Integer half_size = d_size.d_val.divByPow2(1) + 1;
   return (d_value < half_size) ? d_value : d_value - d_size;
 }
 
@@ -39,7 +43,12 @@ std::string FiniteFieldValue::toString() const
 size_t FiniteFieldValue::hash() const
 {
   PairHashFunction<size_t, size_t> h;
-  return h(std::make_pair(d_value.hash(), d_size.hash()));
+  return h(std::make_pair(d_value.hash(), d_size.d_val.hash()));
+}
+
+void FiniteFieldValue::normalize()
+{
+  d_value = d_value.floorDivideRemainder(d_size.d_val);
 }
 
 /* -----------------------------------------------------------------------
@@ -101,7 +110,7 @@ FiniteFieldValue operator-(const FiniteFieldValue& x, const FiniteFieldValue& y)
 
 FiniteFieldValue operator-(const FiniteFieldValue& x)
 {
-  return {x.d_size - x.d_value, x.d_size};
+  return {x.d_size.d_val - x.d_value, x.d_size};
 }
 
 FiniteFieldValue operator*(const FiniteFieldValue& x, const FiniteFieldValue& y)
@@ -123,6 +132,45 @@ FiniteFieldValue FiniteFieldValue::recip() const
   return {d_value.modInverse(d_size), d_size};
 }
 
+/* In-Place Arithmetic --------------------------------------------------- */
+
+FiniteFieldValue& FiniteFieldValue::operator+=(const FiniteFieldValue& y)
+{
+  Assert(d_size == y.d_size)
+      << "Size mismatch: " << d_size << " != " << y.d_size;
+  d_value += y.d_value;
+  normalize();
+  return *this;
+}
+
+FiniteFieldValue& FiniteFieldValue::operator-=(const FiniteFieldValue& y)
+{
+  Assert(d_size == y.d_size)
+      << "Size mismatch: " << d_size << " != " << y.d_size;
+  d_value -= y.d_value;
+  normalize();
+  return *this;
+}
+
+FiniteFieldValue& FiniteFieldValue::operator*=(const FiniteFieldValue& y)
+{
+  Assert(d_size == y.d_size)
+      << "Size mismatch: " << d_size << " != " << y.d_size;
+  d_value *= y.d_value;
+  normalize();
+  return *this;
+}
+
+FiniteFieldValue& FiniteFieldValue::operator/=(const FiniteFieldValue& y)
+{
+  Assert(d_size == y.d_size)
+      << "Size mismatch: " << d_size << " != " << y.d_size;
+  d_value *= y.d_value.modInverse(d_size);
+  normalize();
+  return *this;
+}
+
+
 /* -----------------------------------------------------------------------
  * Output stream
  * ----------------------------------------------------------------------- */
@@ -132,12 +180,23 @@ std::ostream& operator<<(std::ostream& os, const FiniteFieldValue& ff)
   return os << ff.toString();
 }
 
+std::ostream& operator<<(std::ostream& os, const FfSize& ff)
+{
+  return os << ff.d_val;
+}
+
 /* -----------------------------------------------------------------------
  * Static helpers.
  * ----------------------------------------------------------------------- */
 
-FiniteFieldValue FiniteFieldValue::mkZero(const Integer& size) { return {0, size}; }
+FiniteFieldValue FiniteFieldValue::mkZero(const Integer& size)
+{
+  return {0, size};
+}
 
-FiniteFieldValue FiniteFieldValue::mkOne(const Integer& size) { return {1, size}; }
+FiniteFieldValue FiniteFieldValue::mkOne(const Integer& size)
+{
+  return {1, size};
+}
 
 }  // namespace cvc5::internal
diff --git a/src/util/finite_field_value.h b/src/util/finite_field_value.h
@@ -31,26 +31,45 @@
 
 namespace cvc5::internal {
 
+/** Stores a field size that have been validated to be prime */
+struct FfSize
+{
+  FfSize(Integer size) : d_val(size)
+  {
+    // we only support prime fields right now
+    Assert(size.isProbablePrime()) << "not prime: " << size;
+  }
+  FfSize(int size) : d_val(size)
+  {
+    // we only support prime fields right now
+    Assert(d_val.isProbablePrime()) << "not prime: " << size;
+  }
+  FfSize(size_t size) : d_val(size)
+  {
+    // we only support prime fields right now
+    Assert(d_val.isProbablePrime()) << "not prime: " << size;
+  }
+  operator const Integer&() const { return d_val; }
+  bool operator==(const FfSize& y) const { return d_val == y.d_val; }
+  bool operator!=(const FfSize& y) const { return d_val != y.d_val; }
+
+  Integer d_val;
+}; /* struct FfSize */
+
 class FiniteFieldValue
 {
  public:
-  FiniteFieldValue(const Integer& val, const Integer& size)
+  FiniteFieldValue(const Integer& val, const FfSize& size)
       : d_size(size),
         // normalize value into [0, size)
         d_value(val.floorDivideRemainder(size))
   {
-    // we only support prime fields right now
-    Assert(size.isProbablePrime());
   }
 
   /**
    * Construct the zero in this field
    */
-  FiniteFieldValue(const Integer& size) : d_size(size), d_value(0)
-  {
-    // we only support prime fields right now
-    Assert(size.isProbablePrime());
-  }
+  FiniteFieldValue(const FfSize& size) : d_size(size), d_value(0) {}
 
   ~FiniteFieldValue() {}
 
@@ -68,6 +87,12 @@ class FiniteFieldValue
   /* Get value. */
   const Integer& getValue() const;
 
+  /* Is zero? */
+  bool isZero() const;
+
+  /* Is one? */
+  bool isOne() const;
+
   /* Get field size. */
   const Integer& getFieldSize() const;
 
@@ -103,6 +128,11 @@ class FiniteFieldValue
   friend FiniteFieldValue operator/(const FiniteFieldValue&,
                                     const FiniteFieldValue&);
 
+  FiniteFieldValue& operator+=(const FiniteFieldValue&);
+  FiniteFieldValue& operator-=(const FiniteFieldValue&);
+  FiniteFieldValue& operator*=(const FiniteFieldValue&);
+  FiniteFieldValue& operator/=(const FiniteFieldValue&);
+
   /* Reciprocal. Crashes on 0. */
   FiniteFieldValue recip() const;
 
@@ -117,29 +147,27 @@ class FiniteFieldValue
   static FiniteFieldValue mkOne(const Integer& modulus);
 
  private:
+  /** bring d_value back into the range below */
+  void normalize();
+
   /**
    * Class invariants:
    *  - no overflows: d_value < d_modulus
    *  - no negative numbers: d_value >= 0
    */
 
-  Integer d_size;
+  FfSize d_size;
   Integer d_value;
 
 }; /* class FiniteFieldValue */
 
-struct FfSize
+/*
+ * Hash function for the FfSize constants.
+ */
+struct FfSizeHashFunction
 {
-  FfSize(Integer size) : d_size(size)
-  {
-    // we only support prime fields right now
-    Assert(size.isProbablePrime());
-  }
-  operator const Integer&() const { return d_size; }
-  bool operator==(const FfSize& y) const { return d_size == y.d_size; }
-
-  Integer d_size;
-}; /* struct FfSize */
+  size_t operator()(const FfSize& to) const { return to.d_val.hash(); }
+}; /* struct FfSizeHashFunction */
 
 /*
  * Hash function for the FiniteFieldValue.
@@ -149,14 +177,6 @@ struct FiniteFieldValueHashFunction
   size_t operator()(const FiniteFieldValue& ff) const { return ff.hash(); }
 }; /* struct FiniteFieldValueHashFunction */
 
-/*
- * Hash function for the FfSize constants.
- */
-struct FfSizeHashFunction
-{
-  size_t operator()(const FfSize& size) const { return size.d_size.hash(); }
-}; /* struct FiniteFieldValueHashFunction */
-
 /* -----------------------------------------------------------------------
  ** Operators
  * ----------------------------------------------------------------------- */
@@ -209,6 +229,7 @@ FiniteFieldValue operator/(const FiniteFieldValue& x,
  * ----------------------------------------------------------------------- */
 
 std::ostream& operator<<(std::ostream& os, const FiniteFieldValue& ff);
+std::ostream& operator<<(std::ostream& os, const FfSize& ff);
 
 }  // namespace cvc5::internal