Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/delta_rational.h	Lines:	78	92	84.8 %
Date:	2021-08-14	Branches:	46	86	53.5 %


/******************************************************************************
 * 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	56039460	class DeltaRational {
49		private:
50		cvc5::Rational c;
51		cvc5::Rational k;
52
53		public:
54	3925867	DeltaRational() : c(0,1), k(0,1) {}
55	7487268	DeltaRational(const cvc5::Rational& base) : c(base), k(0, 1) {}
56	28742309	DeltaRational(const cvc5::Rational& base, const cvc5::Rational& coeff)
57	28742309	: c(base), k(coeff)
58		{
59	28742309	}
60
61	192365840	const cvc5::Rational& getInfinitesimalPart() const { return k; }
62
63	193392190	const cvc5::Rational& getNoninfinitesimalPart() const { return c; }
64
65	6243835	int sgn() const {
66	6243835	int s = getNoninfinitesimalPart().sgn();
67	6243835	if(s == 0){
68	4117578	return infinitesimalSgn();
69		}else{
70	2126257	return s;
71		}
72		}
73
74	6793910	int infinitesimalSgn() const {
75	6793910	return getInfinitesimalPart().sgn();
76		}
77
78	182383654	bool infinitesimalIsZero() const {
79	182383654	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	12961313	int cmp(const DeltaRational& other) const{
92	12961313	int cmp = c.cmp(other.c);
93	12961313	if(cmp == 0){
94	6136478	return k.cmp(other.k);
95		}else{
96	6824835	return cmp;
97		}
98		}
99
100	12784593	DeltaRational operator+(const DeltaRational& other) const{
101	25569186	cvc5::Rational tmpC = c + other.c;
102	25569186	cvc5::Rational tmpK = k + other.k;
103	25569186	return DeltaRational(tmpC, tmpK);
104		}
105
106	13720981	DeltaRational operator*(const Rational& a) const{
107	27441962	cvc5::Rational tmpC = a * c;
108	27441962	cvc5::Rational tmpK = a * k;
109	27441962	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	999972	DeltaRational operator*(const DeltaRational& a) const
119		/* throw(DeltaRationalException) */ {
120	999972	if(infinitesimalIsZero()){
121	999972	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	1378574	DeltaRational operator-(const DeltaRational& a) const{
131	2757148	cvc5::Rational negOne(cvc5::Integer(-1));
132	2757148	return (this) + (a negOne);
133		}
134
135	548	DeltaRational operator-() const{
136	548	return DeltaRational(-c, -k);
137		}
138
139	662631	DeltaRational operator/(const Rational& a) const{
140	1325262	cvc5::Rational tmpC = c / a;
141	1325262	cvc5::Rational tmpK = k / a;
142	1325262	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	3384403	bool operator==(const DeltaRational& other) const{
175	3384403	return (k == other.k) && (c == other.c);
176		}
177
178	285477	bool operator!=(const DeltaRational& other) const{
179	285477	return !(*this == other);
180		}
181
182
183	47594893	bool operator<=(const DeltaRational& other) const{
184	47594893	int cmp = c.cmp(other.c);
185	47594893	return (cmp < 0) \|\| ((cmp==0)&&(k <= other.k));
186		}
187	31367708	bool operator<(const DeltaRational& other) const{
188	31367708	return (other > *this);
189		}
190	3847643	bool operator>=(const DeltaRational& other) const{
191	3847643	return (other <= *this);
192		}
193	34670188	bool operator>(const DeltaRational& other) const{
194	34670188	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	20677516	DeltaRational& operator=(const DeltaRational& other){
203	20677516	c = other.c;
204	20677516	k = other.k;
205	20677516	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	2746001	DeltaRational& operator+=(const DeltaRational& other){
217	2746001	c += other.c;
218	2746001	k += other.k;
219
220	2746001	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	180710556	bool isIntegral() const {
231	180710556	if(infinitesimalIsZero()){
232	180705925	return getNoninfinitesimalPart().isIntegral();
233		}else{
234	4631	return false;
235		}
236		}
237
238	1285692	Integer floor() const {
239	1285692	if(getNoninfinitesimalPart().isIntegral()){
240	1285692	if(getInfinitesimalPart().sgn() >= 0){
241	37619	return getNoninfinitesimalPart().getNumerator();
242		}else{
243	1248073	return getNoninfinitesimalPart().getNumerator() - Integer(1);
244		}
245		}else{
246		return getNoninfinitesimalPart().floor();
247		}
248		}
249
250	69672	Integer ceiling() const {
251	69672	if(getNoninfinitesimalPart().isIntegral()){
252	69672	if(getInfinitesimalPart().sgn() <= 0){
253		return getNoninfinitesimalPart().getNumerator();
254		}else{
255	69672	return getNoninfinitesimalPart().getNumerator() + Integer(1);
256		}
257		}else{
258		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	244288	Rational substituteDelta(const Rational& d) const{
273	244288	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