Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/real_algebraic_number_poly_imp.h	Lines:	4	5	80.0 %
Date:	2021-09-17	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Algebraic number constants; wraps a libpoly algebraic number.
 */

#include "cvc5_private.h"

#ifndef CVC5__REAL_ALGEBRAIC_NUMBER_H
#define CVC5__REAL_ALGEBRAIC_NUMBER_H

#include <vector>

#include <poly/polyxx.h>

#include "util/integer.h"
#include "util/rational.h"

namespace cvc5 {

/**
 * Represents a real algebraic number based on poly::AlgebraicNumber.
 * This real algebraic number is represented by a (univariate) polynomial and an
 * isolating interval. The interval contains exactly one real root of the
 * polynomial, which is the number the real algebraic number as a whole
 * represents.
 * This representation can hold rationals (where the interval can be a point
 * interval and the polynomial is omitted), an irrational algebraic number (like
 * square roots), but no trancendentals (like pi).
 * Note that the interval representation uses dyadic rationals (denominators are
 * only powers of two).
 */
class RealAlgebraicNumber
{
 public:
  /** Construct as zero. */
  RealAlgebraicNumber() = default;
  /** Move from a poly::AlgebraicNumber type. */
  RealAlgebraicNumber(poly::AlgebraicNumber&& an);
  /** Copy from an Integer. */
  RealAlgebraicNumber(const Integer& i);
  /** Copy from a Rational. */
  RealAlgebraicNumber(const Rational& r);
  /**
   * Construct from a polynomial with the given coefficients and an open
   * interval with the given bounds.
   */
  RealAlgebraicNumber(const std::vector<long>& coefficients,
                      long lower,
                      long upper);
  /**
   * Construct from a polynomial with the given coefficients and an open
   * interval with the given bounds. If the bounds are not dyadic, we need to
   * perform refinement to find a suitable dyadic interval.
   * See poly_utils::toRanWithRefinement for more details.
   */
  RealAlgebraicNumber(const std::vector<Integer>& coefficients,
                      const Rational& lower,
                      const Rational& upper);
  /**
   * Construct from a polynomial with the given coefficients and an open
   * interval with the given bounds. If the bounds are not dyadic, we need to
   * perform refinement to find a suitable dyadic interval.
   * See poly_utils::toRanWithRefinement for more details.
   */
  RealAlgebraicNumber(const std::vector<Rational>& coefficients,
                      const Rational& lower,
                      const Rational& upper);

  /** Copy constructor. */
  RealAlgebraicNumber(const RealAlgebraicNumber& ran) = default;
  /** Move constructor. */
  RealAlgebraicNumber(RealAlgebraicNumber&& ran) = default;

  /** Default destructor. */
  ~RealAlgebraicNumber() = default;

  /** Copy assignment. */
  RealAlgebraicNumber& operator=(const RealAlgebraicNumber& ran) = default;
  /** Move assignment. */
  RealAlgebraicNumber& operator=(RealAlgebraicNumber&& ran) = default;

  /** Get the internal value as a const reference. */
  const poly::AlgebraicNumber& getValue() const { return d_value; }
  /** Get the internal value as a non-const reference. */
  poly::AlgebraicNumber& getValue() { return d_value; }

 private:
  /**
   * Stores the actual real algebraic number.
   */
  poly::AlgebraicNumber d_value;
}; /* class RealAlgebraicNumber */

/** Stream a real algebraic number to an output stream. */
std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran);

/** Compare two real algebraic numbers. */
bool operator==(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
/** Compare two real algebraic numbers. */
bool operator!=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
/** Compare two real algebraic numbers. */
bool operator<(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
/** Compare two real algebraic numbers. */
bool operator<=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
/** Compare two real algebraic numbers. */
bool operator>(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
/** Compare two real algebraic numbers. */
bool operator>=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);

/** Add two real algebraic numbers. */
RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
                              const RealAlgebraicNumber& rhs);
/** Subtract two real algebraic numbers. */
RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
                              const RealAlgebraicNumber& rhs);
/** Negate a real algebraic number. */
RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
/** Multiply two real algebraic numbers. */
RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
                              const RealAlgebraicNumber& rhs);

/** Add and assign two real algebraic numbers. */
RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
                                const RealAlgebraicNumber& rhs);
/** Subtract and assign two real algebraic numbers. */
RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
                                const RealAlgebraicNumber& rhs);
/** Multiply and assign two real algebraic numbers. */
RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
                                const RealAlgebraicNumber& rhs);

/** Compute the sign of a real algebraic number. */
int sgn(const RealAlgebraicNumber& ran);

/** Check whether a real algebraic number is zero. */
bool isZero(const RealAlgebraicNumber& ran);
/** Check whether a real algebraic number is one. */
bool isOne(const RealAlgebraicNumber& ran);

}  // namespace cvc5

#endif /* CVC5__REAL_ALGEBRAIC_NUMBER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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		#include <poly/polyxx.h>
24
25		#include "util/integer.h"
26		#include "util/rational.h"
27
28		namespace cvc5 {
29
30		/**
31		* Represents a real algebraic number based on poly::AlgebraicNumber.
32		* This real algebraic number is represented by a (univariate) polynomial and an
33		* isolating interval. The interval contains exactly one real root of the
34		* polynomial, which is the number the real algebraic number as a whole
35		* represents.
36		* This representation can hold rationals (where the interval can be a point
37		* interval and the polynomial is omitted), an irrational algebraic number (like
38		* square roots), but no trancendentals (like pi).
39		* Note that the interval representation uses dyadic rationals (denominators are
40		* only powers of two).
41		*/
42	2	class RealAlgebraicNumber
43		{
44		public:
45		/** Construct as zero. */
46	8	RealAlgebraicNumber() = default;
47		/** Move from a poly::AlgebraicNumber type. */
48		RealAlgebraicNumber(poly::AlgebraicNumber&& an);
49		/** Copy from an Integer. */
50		RealAlgebraicNumber(const Integer& i);
51		/** Copy from a Rational. */
52		RealAlgebraicNumber(const Rational& r);
53		/**
54		* Construct from a polynomial with the given coefficients and an open
55		* interval with the given bounds.
56		*/
57		RealAlgebraicNumber(const std::vector<long>& coefficients,
58		long lower,
59		long upper);
60		/**
61		* Construct from a polynomial with the given coefficients and an open
62		* interval with the given bounds. If the bounds are not dyadic, we need to
63		* perform refinement to find a suitable dyadic interval.
64		* See poly_utils::toRanWithRefinement for more details.
65		*/
66		RealAlgebraicNumber(const std::vector<Integer>& coefficients,
67		const Rational& lower,
68		const Rational& upper);
69		/**
70		* Construct from a polynomial with the given coefficients and an open
71		* interval with the given bounds. If the bounds are not dyadic, we need to
72		* perform refinement to find a suitable dyadic interval.
73		* See poly_utils::toRanWithRefinement for more details.
74		*/
75		RealAlgebraicNumber(const std::vector<Rational>& coefficients,
76		const Rational& lower,
77		const Rational& upper);
78
79		/** Copy constructor. */
80		RealAlgebraicNumber(const RealAlgebraicNumber& ran) = default;
81		/** Move constructor. */
82		RealAlgebraicNumber(RealAlgebraicNumber&& ran) = default;
83
84		/** Default destructor. */
85	54	~RealAlgebraicNumber() = default;
86
87		/** Copy assignment. */
88		RealAlgebraicNumber& operator=(const RealAlgebraicNumber& ran) = default;
89		/** Move assignment. */
90		RealAlgebraicNumber& operator=(RealAlgebraicNumber&& ran) = default;
91
92		/** Get the internal value as a const reference. */
93	102	const poly::AlgebraicNumber& getValue() const { return d_value; }
94		/** Get the internal value as a non-const reference. */
95		poly::AlgebraicNumber& getValue() { return d_value; }
96
97		private:
98		/**
99		* Stores the actual real algebraic number.
100		*/
101		poly::AlgebraicNumber d_value;
102		}; /* class RealAlgebraicNumber */
103
104		/** Stream a real algebraic number to an output stream. */
105		std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran);
106
107		/** Compare two real algebraic numbers. */
108		bool operator==(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
109		/** Compare two real algebraic numbers. */
110		bool operator!=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
111		/** Compare two real algebraic numbers. */
112		bool operator<(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
113		/** Compare two real algebraic numbers. */
114		bool operator<=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
115		/** Compare two real algebraic numbers. */
116		bool operator>(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
117		/** Compare two real algebraic numbers. */
118		bool operator>=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
119
120		/** Add two real algebraic numbers. */
121		RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
122		const RealAlgebraicNumber& rhs);
123		/** Subtract two real algebraic numbers. */
124		RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
125		const RealAlgebraicNumber& rhs);
126		/** Negate a real algebraic number. */
127		RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
128		/** Multiply two real algebraic numbers. */
129		RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
130		const RealAlgebraicNumber& rhs);
131
132		/** Add and assign two real algebraic numbers. */
133		RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
134		const RealAlgebraicNumber& rhs);
135		/** Subtract and assign two real algebraic numbers. */
136		RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
137		const RealAlgebraicNumber& rhs);
138		/** Multiply and assign two real algebraic numbers. */
139		RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
140		const RealAlgebraicNumber& rhs);
141
142		/** Compute the sign of a real algebraic number. */
143		int sgn(const RealAlgebraicNumber& ran);
144
145		/** Check whether a real algebraic number is zero. */
146		bool isZero(const RealAlgebraicNumber& ran);
147		/** Check whether a real algebraic number is one. */
148		bool isOne(const RealAlgebraicNumber& ran);
149
150		} // namespace cvc5
151
152		#endif /* CVC5__REAL_ALGEBRAIC_NUMBER_H */