Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A finite-field element, implemented as a wrapper around Integer.
      11                 :            :  *
      12                 :            :  * TODOs:
      13                 :            :  * * extend to non-prime fields
      14                 :            :  * (https://github.com/cvc5/cvc5-wishues/issues/139)
      15                 :            :  * * consider montgomery form (https://github.com/cvc5/cvc5-wishues/issues/140)
      16                 :            :  */
      17                 :            : 
      18                 :            : #include "cvc5_public.h"
      19                 :            : 
      20                 :            : #ifndef CVC5__FINITE_FIELDVALUE_H
      21                 :            : #define CVC5__FINITE_FIELDVALUE_H
      22                 :            : 
      23                 :            : #include <iosfwd>
      24                 :            : 
      25                 :            : #include "base/check.h"
      26                 :            : #include "base/exception.h"
      27                 :            : #include "util/integer.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :            : /** Stores a field size that have been validated to be prime */
      32                 :            : struct FfSize
      33                 :            : {
      34                 :      70046 :   FfSize(Integer size) : d_val(size)
      35                 :            :   {
      36                 :            :     // we only support prime fields right now
      37 [ -  + ][ -  + ]:      70046 :     Assert(size.isProbablePrime()) << "not prime: " << size;
                 [ -  - ]
      38                 :      70046 :   }
      39                 :            :   FfSize(int size) : d_val(size)
      40                 :            :   {
      41                 :            :     // we only support prime fields right now
      42                 :            :     Assert(d_val.isProbablePrime()) << "not prime: " << size;
      43                 :            :   }
      44                 :            :   FfSize(size_t size) : d_val(size)
      45                 :            :   {
      46                 :            :     // we only support prime fields right now
      47                 :            :     Assert(d_val.isProbablePrime()) << "not prime: " << size;
      48                 :            :   }
      49                 :     740756 :   operator const Integer&() const { return d_val; }
      50                 :      32588 :   bool operator==(const FfSize& y) const { return d_val == y.d_val; }
      51                 :      27567 :   bool operator!=(const FfSize& y) const { return d_val != y.d_val; }
      52                 :            : 
      53                 :            :   Integer d_val;
      54                 :            : }; /* struct FfSize */
      55                 :            : 
      56                 :            : class FiniteFieldValue
      57                 :            : {
      58                 :            :  public:
      59                 :      93095 :   FiniteFieldValue(const Integer& val, const FfSize& size)
      60                 :      93095 :       : d_size(size),
      61                 :            :         // normalize value into [0, size)
      62                 :      93095 :         d_value(val.floorDivideRemainder(size))
      63                 :            :   {
      64                 :      93095 :   }
      65                 :            : 
      66                 :            :   /**
      67                 :            :    * Construct the zero in this field
      68                 :            :    */
      69                 :            :   FiniteFieldValue(const FfSize& size) : d_size(size), d_value(0) {}
      70                 :            : 
      71                 :            :   /* Get value. */
      72                 :            :   const Integer& getValue() const;
      73                 :            : 
      74                 :            :   /* Is zero? */
      75                 :            :   bool isZero() const;
      76                 :            : 
      77                 :            :   /* Is one? */
      78                 :            :   bool isOne() const;
      79                 :            : 
      80                 :            :   /* Get field size. */
      81                 :            :   const Integer& getFieldSize() const;
      82                 :            : 
      83                 :            :   /* Return value. */
      84                 :            :   Integer toInteger() const;
      85                 :            :   /* Return Integer of smallest absolute value that represents this.
      86                 :            :    *
      87                 :            :    * For fields of odd size, there is always a unique representative of
      88                 :            :    * smallest absolute value.
      89                 :            :    *
      90                 :            :    * For GF(2), the multiplicative identity is represented as "1", not "-1".
      91                 :            :    * */
      92                 :            :   Integer toSignedInteger() const;
      93                 :            :   /* Return string representation (of the value as a signed integer). */
      94                 :            :   std::string toString() const;
      95                 :            : 
      96                 :            :   /* Return hash value. */
      97                 :            :   size_t hash() const;
      98                 :            : 
      99                 :            :   friend bool operator==(const FiniteFieldValue&, const FiniteFieldValue&);
     100                 :            :   friend bool operator!=(const FiniteFieldValue&, const FiniteFieldValue&);
     101                 :            :   friend bool operator<(const FiniteFieldValue&, const FiniteFieldValue&);
     102                 :            :   friend bool operator>(const FiniteFieldValue&, const FiniteFieldValue&);
     103                 :            :   friend bool operator>=(const FiniteFieldValue&, const FiniteFieldValue&);
     104                 :            :   friend bool operator<=(const FiniteFieldValue&, const FiniteFieldValue&);
     105                 :            :   friend FiniteFieldValue operator+(const FiniteFieldValue&,
     106                 :            :                                     const FiniteFieldValue&);
     107                 :            :   friend FiniteFieldValue operator-(const FiniteFieldValue&,
     108                 :            :                                     const FiniteFieldValue&);
     109                 :            :   friend FiniteFieldValue operator-(const FiniteFieldValue&);
     110                 :            :   friend FiniteFieldValue operator*(const FiniteFieldValue&,
     111                 :            :                                     const FiniteFieldValue&);
     112                 :            :   friend FiniteFieldValue operator/(const FiniteFieldValue&,
     113                 :            :                                     const FiniteFieldValue&);
     114                 :            : 
     115                 :            :   FiniteFieldValue& operator+=(const FiniteFieldValue&);
     116                 :            :   FiniteFieldValue& operator-=(const FiniteFieldValue&);
     117                 :            :   FiniteFieldValue& operator*=(const FiniteFieldValue&);
     118                 :            :   FiniteFieldValue& operator/=(const FiniteFieldValue&);
     119                 :            : 
     120                 :            :   /* Reciprocal. Crashes on 0. */
     121                 :            :   FiniteFieldValue recip() const;
     122                 :            : 
     123                 :            :   /* -----------------------------------------------------------------------
     124                 :            :    ** Static helpers.
     125                 :            :    * ----------------------------------------------------------------------- */
     126                 :            : 
     127                 :            :   /* Create zero bit-vector of given size. */
     128                 :            :   static FiniteFieldValue mkZero(const Integer& modulus);
     129                 :            : 
     130                 :            :   /* Create bit-vector representing value 1 of given size. */
     131                 :            :   static FiniteFieldValue mkOne(const Integer& modulus);
     132                 :            : 
     133                 :            :  private:
     134                 :            :   /** bring d_value back into the range below */
     135                 :            :   void normalize();
     136                 :            : 
     137                 :            :   /**
     138                 :            :    * Class invariants:
     139                 :            :    *  - no overflows: d_value < d_modulus
     140                 :            :    *  - no negative numbers: d_value >= 0
     141                 :            :    */
     142                 :            : 
     143                 :            :   FfSize d_size;
     144                 :            :   Integer d_value;
     145                 :            : 
     146                 :            : }; /* class FiniteFieldValue */
     147                 :            : 
     148                 :            : /*
     149                 :            :  * Hash function for the FfSize constants.
     150                 :            :  */
     151                 :            : struct FfSizeHashFunction
     152                 :            : {
     153                 :      15239 :   size_t operator()(const FfSize& to) const { return to.d_val.hash(); }
     154                 :            : }; /* struct FfSizeHashFunction */
     155                 :            : 
     156                 :            : /*
     157                 :            :  * Hash function for the FiniteFieldValue.
     158                 :            :  */
     159                 :            : struct FiniteFieldValueHashFunction
     160                 :            : {
     161                 :      33100 :   size_t operator()(const FiniteFieldValue& ff) const { return ff.hash(); }
     162                 :            : }; /* struct FiniteFieldValueHashFunction */
     163                 :            : 
     164                 :            : /* -----------------------------------------------------------------------
     165                 :            :  ** Operators
     166                 :            :  * ----------------------------------------------------------------------- */
     167                 :            : 
     168                 :            : /* (Dis)Equality --------------------------------------------------------- */
     169                 :            : 
     170                 :            : /* Return true if x is equal to 'y'. */
     171                 :            : bool operator==(const FiniteFieldValue& x, const FiniteFieldValue& y);
     172                 :            : 
     173                 :            : /* Return true if x is not equal to 'y'. */
     174                 :            : bool operator!=(const FiniteFieldValue& x, const FiniteFieldValue& y);
     175                 :            : 
     176                 :            : /* Unsigned Inequality --------------------------------------------------- */
     177                 :            : 
     178                 :            : /* Return true if x is unsigned less than finite field 'y'. */
     179                 :            : bool operator<(const FiniteFieldValue& x, const FiniteFieldValue& y);
     180                 :            : 
     181                 :            : /* Return true if x is unsigned less than or equal to finite field 'y'. */
     182                 :            : bool operator<=(const FiniteFieldValue& x, const FiniteFieldValue& y);
     183                 :            : 
     184                 :            : /* Return true if x is unsigned greater than finite field 'y'. */
     185                 :            : bool operator>(const FiniteFieldValue& x, const FiniteFieldValue& y);
     186                 :            : 
     187                 :            : /* Return true if x is unsigned greater than or equal to finite field 'y'. */
     188                 :            : bool operator>=(const FiniteFieldValue& x, const FiniteFieldValue& y);
     189                 :            : 
     190                 :            : /* Arithmetic operations ------------------------------------------------- */
     191                 :            : 
     192                 :            : /* Return a finite field representing the addition (x + y). */
     193                 :            : FiniteFieldValue operator+(const FiniteFieldValue& x,
     194                 :            :                            const FiniteFieldValue& y);
     195                 :            : 
     196                 :            : /* Return a finite field representing the subtraction (x - y). */
     197                 :            : FiniteFieldValue operator-(const FiniteFieldValue& x,
     198                 :            :                            const FiniteFieldValue& y);
     199                 :            : 
     200                 :            : /* Return a finite field representing the negation of x. */
     201                 :            : FiniteFieldValue operator-(const FiniteFieldValue& x);
     202                 :            : 
     203                 :            : /* Return a finite field representing the multiplication (x * y). */
     204                 :            : FiniteFieldValue operator*(const FiniteFieldValue& x,
     205                 :            :                            const FiniteFieldValue& y);
     206                 :            : 
     207                 :            : /* Return a finite field representing the division (x / y). */
     208                 :            : FiniteFieldValue operator/(const FiniteFieldValue& x,
     209                 :            :                            const FiniteFieldValue& y);
     210                 :            : 
     211                 :            : /* -----------------------------------------------------------------------
     212                 :            :  * Output stream
     213                 :            :  * ----------------------------------------------------------------------- */
     214                 :            : 
     215                 :            : std::ostream& operator<<(std::ostream& os, const FiniteFieldValue& ff);
     216                 :            : std::ostream& operator<<(std::ostream& os, const FfSize& ff);
     217                 :            : 
     218                 :            : }  // namespace cvc5::internal
     219                 :            : 
     220                 :            : #endif /* CVC5__FINITE_FIELDVALUE_H */