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