GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/delta_rational.h Lines: 82 96 85.4 %
Date: 2021-03-22 Branches: 49 88 55.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file delta_rational.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Dejan Jovanovic, Morgan Deters
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include <ostream>
23
24
#include "base/check.h"
25
#include "base/exception.h"
26
#include "util/integer.h"
27
#include "util/rational.h"
28
29
namespace CVC4 {
30
31
class DeltaRational;
32
33
class DeltaRationalException : public Exception {
34
 public:
35
  DeltaRationalException(const char* op,
36
                         const DeltaRational& a,
37
                         const DeltaRational& b);
38
  ~DeltaRationalException() override;
39
};
40
41
42
/**
43
 * A DeltaRational is a pair of rationals (c,k) that represent the number
44
 *   c + kd
45
 * where d is an implicit system wide symbolic infinitesimal.
46
 */
47
55622338
class DeltaRational {
48
private:
49
  CVC4::Rational c;
50
  CVC4::Rational k;
51
52
public:
53
3792056
  DeltaRational() : c(0,1), k(0,1) {}
54
7644461
  DeltaRational(const CVC4::Rational& base) : c(base), k(0,1) {}
55
26715862
  DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) :
56
26715862
    c(base), k(coeff) {}
57
58
226376139
  const CVC4::Rational& getInfinitesimalPart() const {
59
226376139
    return k;
60
  }
61
62
226375861
  const CVC4::Rational& getNoninfinitesimalPart() const {
63
226375861
    return c;
64
  }
65
66
4915929
  int sgn() const {
67
4915929
    int s = getNoninfinitesimalPart().sgn();
68
4915929
    if(s == 0){
69
3629251
      return infinitesimalSgn();
70
    }else{
71
1286678
      return s;
72
    }
73
  }
74
75
6376089
  int infinitesimalSgn() const {
76
6376089
    return getInfinitesimalPart().sgn();
77
  }
78
79
216424092
  bool infinitesimalIsZero() const {
80
216424092
    return getInfinitesimalPart().isZero();
81
  }
82
83
  bool noninfinitesimalIsZero() const {
84
    return getNoninfinitesimalPart().isZero();
85
  }
86
87
  bool isZero() const {
88
    return noninfinitesimalIsZero() && infinitesimalIsZero();
89
  }
90
91
92
13101276
  int cmp(const DeltaRational& other) const{
93
13101276
    int cmp = c.cmp(other.c);
94
13101276
    if(cmp == 0){
95
6096535
      return k.cmp(other.k);
96
    }else{
97
7004741
      return cmp;
98
    }
99
  }
100
101
13107728
  DeltaRational operator+(const DeltaRational& other) const{
102
26215456
    CVC4::Rational tmpC = c+other.c;
103
26215456
    CVC4::Rational tmpK = k+other.k;
104
26215456
    return DeltaRational(tmpC, tmpK);
105
  }
106
107
11570299
  DeltaRational operator*(const Rational& a) const{
108
23140598
    CVC4::Rational tmpC = a*c;
109
23140598
    CVC4::Rational tmpK = a*k;
110
23140598
    return DeltaRational(tmpC, tmpK);
111
  }
112
113
114
  /**
115
   * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
116
   * This can be done whenever this->k or a.k is 0.
117
   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
118
   */
119
1177164
  DeltaRational operator*(const DeltaRational& a) const
120
  /* throw(DeltaRationalException) */ {
121
1177164
    if(infinitesimalIsZero()){
122
1177164
      return a * (this->getNoninfinitesimalPart());
123
    }else if(a.infinitesimalIsZero()){
124
      return (*this) * a.getNoninfinitesimalPart();
125
    }else{
126
      throw DeltaRationalException("operator*", *this, a);
127
    }
128
  }
129
130
131
1388196
  DeltaRational operator-(const DeltaRational& a) const{
132
2776392
    CVC4::Rational negOne(CVC4::Integer(-1));
133
2776392
    return *(this) + (a * negOne);
134
  }
135
136
384
  DeltaRational operator-() const{
137
384
    return DeltaRational(-c, -k);
138
  }
139
140
606906
  DeltaRational operator/(const Rational& a) const{
141
1213812
    CVC4::Rational tmpC = c/a;
142
1213812
    CVC4::Rational tmpK = k/a;
143
1213812
    return DeltaRational(tmpC, tmpK);
144
  }
145
146
  DeltaRational operator/(const Integer& a) const{
147
    CVC4::Rational tmpC = c/a;
148
    CVC4::Rational tmpK = k/a;
149
    return DeltaRational(tmpC, tmpK);
150
  }
151
152
  /**
153
   * Divides (*this) / (a.c + a.k * delta)
154
   * This can be done when a.k is 0 and a.c is non-zero.
155
   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
156
   */
157
  DeltaRational operator/(const DeltaRational& a) const
158
  /* throw(DeltaRationalException) */ {
159
    if(a.infinitesimalIsZero()){
160
      return (*this) / a.getNoninfinitesimalPart();
161
    }else{
162
      throw DeltaRationalException("operator/", *this, a);
163
    }
164
  }
165
166
167
  DeltaRational abs() const {
168
    if(sgn() >= 0){
169
      return *this;
170
    }else{
171
      return (*this) * Rational(-1);
172
    }
173
  }
174
175
3304386
  bool operator==(const DeltaRational& other) const{
176
3304386
    return (k == other.k) && (c == other.c);
177
  }
178
179
102925
  bool operator!=(const DeltaRational& other) const{
180
102925
    return !(*this == other);
181
  }
182
183
184
48383852
  bool operator<=(const DeltaRational& other) const{
185
48383852
    int cmp = c.cmp(other.c);
186
48383852
    return (cmp < 0) || ((cmp==0)&&(k <= other.k));
187
  }
188
32908695
  bool operator<(const DeltaRational& other) const{
189
32908695
    return (other  > *this);
190
  }
191
3676139
  bool operator>=(const DeltaRational& other) const{
192
3676139
    return (other <= *this);
193
  }
194
35970750
  bool operator>(const DeltaRational& other) const{
195
35970750
    return !(*this <= other);
196
  }
197
198
  int compare(const DeltaRational& other) const{
199
    int cmpRes = c.cmp(other.c);
200
    return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
201
  }
202
203
20963155
  DeltaRational& operator=(const DeltaRational& other){
204
20963155
    c = other.c;
205
20963155
    k = other.k;
206
20963155
    return *(this);
207
  }
208
209
  DeltaRational& operator*=(const CVC4::Rational& a){
210
    c *=  a;
211
    k *=  a;
212
213
    return *(this);
214
  }
215
216
747352
  DeltaRational& operator+=(const DeltaRational& other){
217
747352
    c += other.c;
218
747352
    k += other.k;
219
220
747352
    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
214622709
  bool isIntegral() const {
231
214622709
    if(infinitesimalIsZero()){
232
214618695
      return getNoninfinitesimalPart().isIntegral();
233
    }else{
234
4014
      return false;
235
    }
236
  }
237
238
1401712
  Integer floor() const {
239
1401712
    if(getNoninfinitesimalPart().isIntegral()){
240
1400839
      if(getInfinitesimalPart().sgn() >= 0){
241
33662
        return getNoninfinitesimalPart().getNumerator();
242
      }else{
243
1367177
        return getNoninfinitesimalPart().getNumerator() - Integer(1);
244
      }
245
    }else{
246
873
      return getNoninfinitesimalPart().floor();
247
    }
248
  }
249
250
81891
  Integer ceiling() const {
251
81891
    if(getNoninfinitesimalPart().isIntegral()){
252
81020
      if(getInfinitesimalPart().sgn() <= 0){
253
5
        return getNoninfinitesimalPart().getNumerator();
254
      }else{
255
81015
        return getNoninfinitesimalPart().getNumerator() + Integer(1);
256
      }
257
    }else{
258
871
      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
311706
  Rational substituteDelta(const Rational& d) const{
273
311706
    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
}/* CVC4 namespace */