Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/delta_rational.h	Lines:	81	92	88.0 %
Date:	2021-05-22	Branches:	49	86	57.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Aina Niemetz, Dejan Jovanovic
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#pragma once

#include <ostream>

#include "base/check.h"
#include "base/exception.h"
#include "util/integer.h"
#include "util/rational.h"

namespace cvc5 {

class DeltaRational;

class DeltaRationalException : public Exception {
 public:
  DeltaRationalException(const char* op,
                         const DeltaRational& a,
                         const DeltaRational& b);
  ~DeltaRationalException() override;
};


/**
 * A DeltaRational is a pair of rationals (c,k) that represent the number
 *   c + kd
 * where d is an implicit system wide symbolic infinitesimal.
 */
class DeltaRational {
private:
 cvc5::Rational c;
 cvc5::Rational k;

public:
  DeltaRational() : c(0,1), k(0,1) {}
  DeltaRational(const cvc5::Rational& base) : c(base), k(0, 1) {}
  DeltaRational(const cvc5::Rational& base, const cvc5::Rational& coeff)
      : c(base), k(coeff)
  {
  }

  const cvc5::Rational& getInfinitesimalPart() const { return k; }

  const cvc5::Rational& getNoninfinitesimalPart() const { return c; }

  int sgn() const {
    int s = getNoninfinitesimalPart().sgn();
    if(s == 0){
      return infinitesimalSgn();
    }else{
      return s;
    }
  }

  int infinitesimalSgn() const {
    return getInfinitesimalPart().sgn();
  }

  bool infinitesimalIsZero() const {
    return getInfinitesimalPart().isZero();
  }

  bool noninfinitesimalIsZero() const {
    return getNoninfinitesimalPart().isZero();
  }

  bool isZero() const {
    return noninfinitesimalIsZero() && infinitesimalIsZero();
  }


  int cmp(const DeltaRational& other) const{
    int cmp = c.cmp(other.c);
    if(cmp == 0){
      return k.cmp(other.k);
    }else{
      return cmp;
    }
  }

  DeltaRational operator+(const DeltaRational& other) const{
    cvc5::Rational tmpC = c + other.c;
    cvc5::Rational tmpK = k + other.k;
    return DeltaRational(tmpC, tmpK);
  }

  DeltaRational operator*(const Rational& a) const{
    cvc5::Rational tmpC = a * c;
    cvc5::Rational tmpK = a * k;
    return DeltaRational(tmpC, tmpK);
  }


  /**
   * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
   * This can be done whenever this->k or a.k is 0.
   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
   */
  DeltaRational operator*(const DeltaRational& a) const
  /* throw(DeltaRationalException) */ {
    if(infinitesimalIsZero()){
      return a * (this->getNoninfinitesimalPart());
    }else if(a.infinitesimalIsZero()){
      return (*this) * a.getNoninfinitesimalPart();
    }else{
      throw DeltaRationalException("operator*", *this, a);
    }
  }


  DeltaRational operator-(const DeltaRational& a) const{
    cvc5::Rational negOne(cvc5::Integer(-1));
    return *(this) + (a * negOne);
  }

  DeltaRational operator-() const{
    return DeltaRational(-c, -k);
  }

  DeltaRational operator/(const Rational& a) const{
    cvc5::Rational tmpC = c / a;
    cvc5::Rational tmpK = k / a;
    return DeltaRational(tmpC, tmpK);
  }

  DeltaRational operator/(const Integer& a) const{
    cvc5::Rational tmpC = c / a;
    cvc5::Rational tmpK = k / a;
    return DeltaRational(tmpC, tmpK);
  }

  /**
   * Divides (*this) / (a.c + a.k * delta)
   * This can be done when a.k is 0 and a.c is non-zero.
   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
   */
  DeltaRational operator/(const DeltaRational& a) const
  /* throw(DeltaRationalException) */ {
    if(a.infinitesimalIsZero()){
      return (*this) / a.getNoninfinitesimalPart();
    }else{
      throw DeltaRationalException("operator/", *this, a);
    }
  }


  DeltaRational abs() const {
    if(sgn() >= 0){
      return *this;
    }else{
      return (*this) * Rational(-1);
    }
  }

  bool operator==(const DeltaRational& other) const{
    return (k == other.k) && (c == other.c);
  }

  bool operator!=(const DeltaRational& other) const{
    return !(*this == other);
  }


  bool operator<=(const DeltaRational& other) const{
    int cmp = c.cmp(other.c);
    return (cmp < 0) || ((cmp==0)&&(k <= other.k));
  }
  bool operator<(const DeltaRational& other) const{
    return (other  > *this);
  }
  bool operator>=(const DeltaRational& other) const{
    return (other <= *this);
  }
  bool operator>(const DeltaRational& other) const{
    return !(*this <= other);
  }

  int compare(const DeltaRational& other) const{
    int cmpRes = c.cmp(other.c);
    return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
  }

  DeltaRational& operator=(const DeltaRational& other){
    c = other.c;
    k = other.k;
    return *(this);
  }

  DeltaRational& operator*=(const cvc5::Rational& a)
  {
    c *=  a;
    k *=  a;

    return *(this);
  }

  DeltaRational& operator+=(const DeltaRational& other){
    c += other.c;
    k += other.k;

    return *(this);
  }

  DeltaRational& operator/=(const Rational& a){
    Assert(!a.isZero());
    c /= a;
    k /= a;
    return *(this);
  }

  bool isIntegral() const {
    if(infinitesimalIsZero()){
      return getNoninfinitesimalPart().isIntegral();
    }else{
      return false;
    }
  }

  Integer floor() const {
    if(getNoninfinitesimalPart().isIntegral()){
      if(getInfinitesimalPart().sgn() >= 0){
        return getNoninfinitesimalPart().getNumerator();
      }else{
        return getNoninfinitesimalPart().getNumerator() - Integer(1);
      }
    }else{
      return getNoninfinitesimalPart().floor();
    }
  }

  Integer ceiling() const {
    if(getNoninfinitesimalPart().isIntegral()){
      if(getInfinitesimalPart().sgn() <= 0){
        return getNoninfinitesimalPart().getNumerator();
      }else{
        return getNoninfinitesimalPart().getNumerator() + Integer(1);
      }
    }else{
      return getNoninfinitesimalPart().ceiling();
    }
  }

  /** Only well defined if both this and y are integral. */
  Integer euclidianDivideQuotient(const DeltaRational& y) const
      /* throw(DeltaRationalException) */;

  /** Only well defined if both this and y are integral. */
  Integer euclidianDivideRemainder(const DeltaRational& y) const
      /* throw(DeltaRationalException) */;

  std::string toString() const;

  Rational substituteDelta(const Rational& d) const{
    return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
  }

  /**
   * Computes a sufficient upperbound to separate two DeltaRationals.
   * This value is stored in res.
   * For any rational d such that
   *   0 < d < res
   * then
   *   a < b if and only if substituteDelta(a, d) < substituteDelta(b,d).
   * (Similar relationships hold for for a == b and a > b.)
   * Precondition: res > 0
   */
  static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b);

  uint32_t complexity() const {
    return c.complexity() + k.complexity();
  }

  double approx(double deltaSub) const {
    double maj = getNoninfinitesimalPart().getDouble();
    double min = deltaSub * (getInfinitesimalPart().getDouble());
    return maj + min;
  }


};

std::ostream& operator<<(std::ostream& os, const DeltaRational& n);

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Aina Niemetz, Dejan Jovanovic
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "cvc5_private.h"
20
21		#pragma once
22
23		#include <ostream>
24
25		#include "base/check.h"
26		#include "base/exception.h"
27		#include "util/integer.h"
28		#include "util/rational.h"
29
30		namespace cvc5 {
31
32		class DeltaRational;
33
34		class DeltaRationalException : public Exception {
35		public:
36		DeltaRationalException(const char* op,
37		const DeltaRational& a,
38		const DeltaRational& b);
39		~DeltaRationalException() override;
40		};
41
42
43		/**
44		* A DeltaRational is a pair of rationals (c,k) that represent the number
45		* c + kd
46		* where d is an implicit system wide symbolic infinitesimal.
47		*/
48	50650395	class DeltaRational {
49		private:
50		cvc5::Rational c;
51		cvc5::Rational k;
52
53		public:
54	3690284	DeltaRational() : c(0,1), k(0,1) {}
55	6289158	DeltaRational(const cvc5::Rational& base) : c(base), k(0, 1) {}
56	26438213	DeltaRational(const cvc5::Rational& base, const cvc5::Rational& coeff)
57	26438213	: c(base), k(coeff)
58		{
59	26438213	}
60
61	125211701	const cvc5::Rational& getInfinitesimalPart() const { return k; }
62
63	125891290	const cvc5::Rational& getNoninfinitesimalPart() const { return c; }
64
65	5310354	int sgn() const {
66	5310354	int s = getNoninfinitesimalPart().sgn();
67	5310354	if(s == 0){
68	3633411	return infinitesimalSgn();
69		}else{
70	1676943	return s;
71		}
72		}
73
74	5859940	int infinitesimalSgn() const {
75	5859940	return getInfinitesimalPart().sgn();
76		}
77
78	116667398	bool infinitesimalIsZero() const {
79	116667398	return getInfinitesimalPart().isZero();
80		}
81
82		bool noninfinitesimalIsZero() const {
83		return getNoninfinitesimalPart().isZero();
84		}
85
86		bool isZero() const {
87		return noninfinitesimalIsZero() && infinitesimalIsZero();
88		}
89
90
91	11407691	int cmp(const DeltaRational& other) const{
92	11407691	int cmp = c.cmp(other.c);
93	11407691	if(cmp == 0){
94	5127749	return k.cmp(other.k);
95		}else{
96	6279942	return cmp;
97		}
98		}
99
100	11961880	DeltaRational operator+(const DeltaRational& other) const{
101	23923760	cvc5::Rational tmpC = c + other.c;
102	23923760	cvc5::Rational tmpK = k + other.k;
103	23923760	return DeltaRational(tmpC, tmpK);
104		}
105
106	12408517	DeltaRational operator*(const Rational& a) const{
107	24817034	cvc5::Rational tmpC = a * c;
108	24817034	cvc5::Rational tmpK = a * k;
109	24817034	return DeltaRational(tmpC, tmpK);
110		}
111
112
113		/**
114		* Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
115		* This can be done whenever this->k or a.k is 0.
116		* Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
117		*/
118	934490	DeltaRational operator*(const DeltaRational& a) const
119		/* throw(DeltaRationalException) */ {
120	934490	if(infinitesimalIsZero()){
121	934490	return a * (this->getNoninfinitesimalPart());
122		}else if(a.infinitesimalIsZero()){
123		return (this) a.getNoninfinitesimalPart();
124		}else{
125		throw DeltaRationalException("operator", this, a);
126		}
127		}
128
129
130	1315322	DeltaRational operator-(const DeltaRational& a) const{
131	2630644	cvc5::Rational negOne(cvc5::Integer(-1));
132	2630644	return (this) + (a negOne);
133		}
134
135	472	DeltaRational operator-() const{
136	472	return DeltaRational(-c, -k);
137		}
138
139	625909	DeltaRational operator/(const Rational& a) const{
140	1251818	cvc5::Rational tmpC = c / a;
141	1251818	cvc5::Rational tmpK = k / a;
142	1251818	return DeltaRational(tmpC, tmpK);
143		}
144
145		DeltaRational operator/(const Integer& a) const{
146		cvc5::Rational tmpC = c / a;
147		cvc5::Rational tmpK = k / a;
148		return DeltaRational(tmpC, tmpK);
149		}
150
151		/**
152		* Divides (this) / (a.c + a.k delta)
153		* This can be done when a.k is 0 and a.c is non-zero.
154		* Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
155		*/
156		DeltaRational operator/(const DeltaRational& a) const
157		/* throw(DeltaRationalException) */ {
158		if(a.infinitesimalIsZero()){
159		return (*this) / a.getNoninfinitesimalPart();
160		}else{
161		throw DeltaRationalException("operator/", *this, a);
162		}
163		}
164
165
166		DeltaRational abs() const {
167		if(sgn() >= 0){
168		return *this;
169		}else{
170		return (this) Rational(-1);
171		}
172		}
173
174	2721814	bool operator==(const DeltaRational& other) const{
175	2721814	return (k == other.k) && (c == other.c);
176		}
177
178	162735	bool operator!=(const DeltaRational& other) const{
179	162735	return !(*this == other);
180		}
181
182
183	38626695	bool operator<=(const DeltaRational& other) const{
184	38626695	int cmp = c.cmp(other.c);
185	38626695	return (cmp < 0) \|\| ((cmp==0)&&(k <= other.k));
186		}
187	26539209	bool operator<(const DeltaRational& other) const{
188	26539209	return (other > *this);
189		}
190	2777473	bool operator>=(const DeltaRational& other) const{
191	2777473	return (other <= *this);
192		}
193	29086482	bool operator>(const DeltaRational& other) const{
194	29086482	return !(*this <= other);
195		}
196
197		int compare(const DeltaRational& other) const{
198		int cmpRes = c.cmp(other.c);
199		return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
200		}
201
202	19384985	DeltaRational& operator=(const DeltaRational& other){
203	19384985	c = other.c;
204	19384985	k = other.k;
205	19384985	return *(this);
206		}
207
208		DeltaRational& operator*=(const cvc5::Rational& a)
209		{
210		c *= a;
211		k *= a;
212
213		return *(this);
214		}
215
216	1981371	DeltaRational& operator+=(const DeltaRational& other){
217	1981371	c += other.c;
218	1981371	k += other.k;
219
220	1981371	return *(this);
221		}
222
223		DeltaRational& operator/=(const Rational& a){
224		Assert(!a.isZero());
225		c /= a;
226		k /= a;
227		return *(this);
228		}
229
230	115096138	bool isIntegral() const {
231	115096138	if(infinitesimalIsZero()){
232	115090748	return getNoninfinitesimalPart().isIntegral();
233		}else{
234	5390	return false;
235		}
236		}
237
238	1056978	Integer floor() const {
239	1056978	if(getNoninfinitesimalPart().isIntegral()){
240	1055917	if(getInfinitesimalPart().sgn() >= 0){
241	39012	return getNoninfinitesimalPart().getNumerator();
242		}else{
243	1016905	return getNoninfinitesimalPart().getNumerator() - Integer(1);
244		}
245		}else{
246	1061	return getNoninfinitesimalPart().floor();
247		}
248		}
249
250	55467	Integer ceiling() const {
251	55467	if(getNoninfinitesimalPart().isIntegral()){
252	54408	if(getInfinitesimalPart().sgn() <= 0){
253	21	return getNoninfinitesimalPart().getNumerator();
254		}else{
255	54387	return getNoninfinitesimalPart().getNumerator() + Integer(1);
256		}
257		}else{
258	1059	return getNoninfinitesimalPart().ceiling();
259		}
260		}
261
262		/** Only well defined if both this and y are integral. */
263		Integer euclidianDivideQuotient(const DeltaRational& y) const
264		/* throw(DeltaRationalException) */;
265
266		/** Only well defined if both this and y are integral. */
267		Integer euclidianDivideRemainder(const DeltaRational& y) const
268		/* throw(DeltaRationalException) */;
269
270		std::string toString() const;
271
272	226139	Rational substituteDelta(const Rational& d) const{
273	226139	return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
274		}
275
276		/**
277		* Computes a sufficient upperbound to separate two DeltaRationals.
278		* This value is stored in res.
279		* For any rational d such that
280		* 0 < d < res
281		* then
282		* a < b if and only if substituteDelta(a, d) < substituteDelta(b,d).
283		* (Similar relationships hold for for a == b and a > b.)
284		* Precondition: res > 0
285		*/
286		static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b);
287
288		uint32_t complexity() const {
289		return c.complexity() + k.complexity();
290		}
291
292		double approx(double deltaSub) const {
293		double maj = getNoninfinitesimalPart().getDouble();
294		double min = deltaSub * (getInfinitesimalPart().getDouble());
295		return maj + min;
296		}
297
298
299		};
300
301		std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
302
303		} // namespace cvc5