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 */