diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 3f89f71b06f..82b678949df 100644 --- 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().d_size << ")"; break; case Kind::FINITE_FIELD_TYPE: - out << "(_ FiniteField " << n.getConst().d_size << ")"; + out << "(_ FiniteField " << n.getConst().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 index 41612a069ff..25961446472 100644 --- 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 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 index efa1d276bd6..1406cc2719e 100644 --- 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