Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Andrew Reynolds, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :            :  * Algebraic number constants; wraps a libpoly algebraic number.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__REAL_ALGEBRAIC_NUMBER_H
      19                 :            : #define CVC5__REAL_ALGEBRAIC_NUMBER_H
      20                 :            : 
      21                 :            : #include <vector>
      22                 :            : 
      23                 :            : #ifdef CVC5_POLY_IMP
      24                 :            : #include <poly/polyxx.h>
      25                 :            : #endif
      26                 :            : 
      27                 :            : #include "util/integer.h"
      28                 :            : #include "util/rational.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : 
      32                 :            : class PolyConverter;
      33                 :            : 
      34                 :            : /**
      35                 :            :  * Represents a real algebraic number based on poly::AlgebraicNumber.
      36                 :            :  * This real algebraic number is represented by a (univariate) polynomial and an
      37                 :            :  * isolating interval. The interval contains exactly one real root of the
      38                 :            :  * polynomial, which is the number the real algebraic number as a whole
      39                 :            :  * represents.
      40                 :            :  * This representation can hold rationals (where the interval can be a point
      41                 :            :  * interval and the polynomial is omitted), an irrational algebraic number (like
      42                 :            :  * square roots), but no trancendentals (like pi).
      43                 :            :  * Note that the interval representation uses dyadic rationals (denominators are
      44                 :            :  * only powers of two).
      45                 :            :  *
      46                 :            :  * If libpoly is not available, this class serves as a wrapper around Rational
      47                 :            :  * to allow using RealAlgebraicNumber, even if libpoly is not enabled.
      48                 :            :  */
      49                 :    9450570 : class RealAlgebraicNumber
      50                 :            : {
      51                 :            :   friend class PolyConverter;
      52                 :            : 
      53                 :            :  public:
      54                 :            :   /** Construct as zero. */
      55                 :            :   RealAlgebraicNumber();
      56                 :            : #ifdef CVC5_POLY_IMP
      57                 :            :   /** Move from a poly::AlgebraicNumber type. */
      58                 :            :   RealAlgebraicNumber(poly::AlgebraicNumber&& an);
      59                 :            : #endif
      60                 :            :   /** Copy from an Integer. */
      61                 :            :   RealAlgebraicNumber(const Integer& i);
      62                 :            :   /** Copy from a Rational. */
      63                 :            :   RealAlgebraicNumber(const Rational& r);
      64                 :            :   /**
      65                 :            :    * Construct from a polynomial with the given coefficients and an open
      66                 :            :    * interval with the given bounds.
      67                 :            :    */
      68                 :            :   RealAlgebraicNumber(const std::vector<long>& coefficients,
      69                 :            :                       long lower,
      70                 :            :                       long upper);
      71                 :            :   /**
      72                 :            :    * Construct from a polynomial with the given coefficients and an open
      73                 :            :    * interval with the given bounds. If the bounds are not dyadic, we need to
      74                 :            :    * perform refinement to find a suitable dyadic interval.
      75                 :            :    * See poly_utils::toRanWithRefinement for more details.
      76                 :            :    */
      77                 :            :   RealAlgebraicNumber(const std::vector<Integer>& coefficients,
      78                 :            :                       const Rational& lower,
      79                 :            :                       const Rational& upper);
      80                 :            :   /**
      81                 :            :    * Construct from a polynomial with the given coefficients and an open
      82                 :            :    * interval with the given bounds. If the bounds are not dyadic, we need to
      83                 :            :    * perform refinement to find a suitable dyadic interval.
      84                 :            :    * See poly_utils::toRanWithRefinement for more details.
      85                 :            :    */
      86                 :            :   RealAlgebraicNumber(const std::vector<Rational>& coefficients,
      87                 :            :                       const Rational& lower,
      88                 :            :                       const Rational& upper);
      89                 :            : 
      90                 :            :   /** Copy constructor. */
      91                 :   17463500 :   RealAlgebraicNumber(const RealAlgebraicNumber& ran) = default;
      92                 :            :   /** Move constructor. */
      93                 :    2168770 :   RealAlgebraicNumber(RealAlgebraicNumber&& ran) = default;
      94                 :            : 
      95                 :            :   /** Default destructor. */
      96                 :   73716977 :   ~RealAlgebraicNumber() = default;
      97                 :            : 
      98                 :            :   /** Copy assignment. */
      99                 :            :   RealAlgebraicNumber& operator=(const RealAlgebraicNumber& ran) = default;
     100                 :            :   /** Move assignment. */
     101                 :            :   RealAlgebraicNumber& operator=(RealAlgebraicNumber&& ran) = default;
     102                 :            : 
     103                 :            :   /**
     104                 :            :    * Check if this real algebraic number is actually rational.
     105                 :            :    * If true, the value is rational and toRational() can safely be called.
     106                 :            :    * If false, the value may still be rational, but was not recognized as
     107                 :            :    * such yet.
     108                 :            :    */
     109                 :            :   bool isRational() const;
     110                 :            :   /**
     111                 :            :    * Returns the stored value as a rational.
     112                 :            :    * The value is exact if isRational() returns true, otherwise it may only be a
     113                 :            :    * rational approximation (of unknown precision).
     114                 :            :    */
     115                 :            :   Rational toRational() const;
     116                 :            : 
     117                 :            :   std::string toString() const;
     118                 :            : 
     119                 :            :   /** Compare two real algebraic numbers. */
     120                 :            :   bool operator==(const RealAlgebraicNumber& rhs) const;
     121                 :            :   /** Compare two real algebraic numbers. */
     122                 :            :   bool operator!=(const RealAlgebraicNumber& rhs) const;
     123                 :            :   /** Compare two real algebraic numbers. */
     124                 :            :   bool operator<(const RealAlgebraicNumber& rhs) const;
     125                 :            :   /** Compare two real algebraic numbers. */
     126                 :            :   bool operator<=(const RealAlgebraicNumber& rhs) const;
     127                 :            :   /** Compare two real algebraic numbers. */
     128                 :            :   bool operator>(const RealAlgebraicNumber& rhs) const;
     129                 :            :   /** Compare two real algebraic numbers. */
     130                 :            :   bool operator>=(const RealAlgebraicNumber& rhs) const;
     131                 :            : 
     132                 :            :   /** Add two real algebraic numbers. */
     133                 :            :   RealAlgebraicNumber operator+(const RealAlgebraicNumber& rhs) const;
     134                 :            :   /** Subtract two real algebraic numbers. */
     135                 :            :   RealAlgebraicNumber operator-(const RealAlgebraicNumber& rhs) const;
     136                 :            :   /** Negate a real algebraic number. */
     137                 :            :   RealAlgebraicNumber operator-() const;
     138                 :            :   /** Multiply two real algebraic numbers. */
     139                 :            :   RealAlgebraicNumber operator*(const RealAlgebraicNumber& rhs) const;
     140                 :            :   /** Divide two real algebraic numbers. */
     141                 :            :   RealAlgebraicNumber operator/(const RealAlgebraicNumber& rhs) const;
     142                 :            : 
     143                 :            :   /** Add and assign two real algebraic numbers. */
     144                 :            :   RealAlgebraicNumber& operator+=(const RealAlgebraicNumber& rhs);
     145                 :            :   /** Subtract and assign two real algebraic numbers. */
     146                 :            :   RealAlgebraicNumber& operator-=(const RealAlgebraicNumber& rhs);
     147                 :            :   /** Multiply and assign two real algebraic numbers. */
     148                 :            :   RealAlgebraicNumber& operator*=(const RealAlgebraicNumber& rhs);
     149                 :            : 
     150                 :            :   /** Compute the sign of a real algebraic number. */
     151                 :            :   int sgn() const;
     152                 :            : 
     153                 :            :   /** Check whether a real algebraic number is zero. */
     154                 :            :   bool isZero() const;
     155                 :            :   /** Check whether a real algebraic number is one. */
     156                 :            :   bool isOne() const;
     157                 :            :   /** Compute the inverse of a real algebraic number. */
     158                 :            :   RealAlgebraicNumber inverse() const;
     159                 :            :   /** Hash function */
     160                 :            :   size_t hash() const;
     161                 :            : 
     162                 :            :  private:
     163                 :            : #ifdef CVC5_POLY_IMP
     164                 :            :   /** Get the internal value as a const reference. */
     165                 :       2738 :   const poly::AlgebraicNumber& getValue() const { return d_value; }
     166                 :            :   /** Get the internal value as a non-const reference. */
     167                 :        379 :   poly::AlgebraicNumber& getValue() { return d_value; }
     168                 :            :   /**
     169                 :            :    * Convert rational to poly, which returns d_value if it stores the
     170                 :            :    * value of r, otherwise it converts and returns the rational value of r.
     171                 :            :    */
     172                 :            :   static poly::AlgebraicNumber convertToPoly(const RealAlgebraicNumber& r);
     173                 :            : #endif
     174                 :            :   /** Get the internal rational value as a const reference. */
     175                 :   81370100 :   const Rational& getRationalValue() const { return d_rat; }
     176                 :            :   /** Get the internal rational value as a non-const reference. */
     177                 :   36249100 :   Rational& getRationalValue() { return d_rat; }
     178                 :            : #ifdef CVC5_POLY_IMP
     179                 :            :   /**
     180                 :            :    * Whether the value of this real algebraic number is stored in d_rat.
     181                 :            :    * Otherwise, it is stored in d_value.
     182                 :            :    */
     183                 :            :   bool d_isRational;
     184                 :            :   /** Stores the actual real algebraic number, if applicable. */
     185                 :            :   poly::AlgebraicNumber d_value;
     186                 :            : #endif
     187                 :            :   /** Stores the rational, if applicable. */
     188                 :            :   Rational d_rat;
     189                 :            : }; /* class RealAlgebraicNumber */
     190                 :            : 
     191                 :            : /** Stream a real algebraic number to an output stream. */
     192                 :            : std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran);
     193                 :            : 
     194                 :            : using RealAlgebraicNumberHashFunction = std::hash<RealAlgebraicNumber>;
     195                 :            : 
     196                 :            : }  // namespace cvc5::internal
     197                 :            : 
     198                 :            : namespace std {
     199                 :            : template <>
     200                 :            : struct hash<cvc5::internal::RealAlgebraicNumber>
     201                 :            : {
     202                 :            :   /**
     203                 :            :    * Computes a hash of the given real algebraic number. Given that the internal
     204                 :            :    * representation of real algebraic numbers are inherently mutable (th
     205                 :            :    * interval may be refined for comparisons) we hash a well-defined rational
     206                 :            :    * approximation.
     207                 :            :    */
     208                 :            :   size_t operator()(const cvc5::internal::RealAlgebraicNumber& ran) const;
     209                 :            : };
     210                 :            : }  // namespace std
     211                 :            : 
     212                 :            : #endif /* CVC5__REAL_ALGEBRAIC_NUMBER_H */