LCOV - code coverage report
Current view: top level - buildbot/coverage/build/src/util - finite_field_value.h (source / functions) Hit Total Coverage
Test: coverage.info Lines: 18 19 94.7 %
Date: 2024-12-28 12:36:19 Functions: 9 9 100.0 %
Branches: 3 8 37.5 %

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

Generated by: LCOV version 1.14