1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King, Morgan Deters |
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 "theory/arith/delta_rational.h" |
20 |
|
|
21 |
|
#include <sstream> |
22 |
|
|
23 |
|
using namespace std; |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
|
27 |
|
std::ostream& operator<<(std::ostream& os, const DeltaRational& dq){ |
28 |
|
return os << "(" << dq.getNoninfinitesimalPart() |
29 |
|
<< "," << dq.getInfinitesimalPart() << ")"; |
30 |
|
} |
31 |
|
|
32 |
|
|
33 |
|
std::string DeltaRational::toString() const { |
34 |
|
return "(" + getNoninfinitesimalPart().toString() + "," + |
35 |
|
getInfinitesimalPart().toString() + ")"; |
36 |
|
} |
37 |
|
|
38 |
136185 |
void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b){ |
39 |
136185 |
Assert(res.sgn() > 0); |
40 |
|
|
41 |
136185 |
int cmp = a.cmp(b); |
42 |
136185 |
if(cmp != 0){ |
43 |
136185 |
bool aLeqB = cmp < 0; |
44 |
|
|
45 |
136185 |
const DeltaRational& min = aLeqB ? a : b; |
46 |
136185 |
const DeltaRational& max = aLeqB ? b : a; |
47 |
|
|
48 |
136185 |
const Rational& pinf = min.getInfinitesimalPart(); |
49 |
136185 |
const Rational& cinf = max.getInfinitesimalPart(); |
50 |
|
|
51 |
136185 |
const Rational& pmaj = min.getNoninfinitesimalPart(); |
52 |
136185 |
const Rational& cmaj = max.getNoninfinitesimalPart(); |
53 |
|
|
54 |
136185 |
if(pmaj == cmaj){ |
55 |
14250 |
Assert(pinf < cinf); |
56 |
|
// any value of delta preserves the order |
57 |
121935 |
}else if(pinf == cinf){ |
58 |
101477 |
Assert(pmaj < cmaj); |
59 |
|
// any value of delta preserves the order |
60 |
|
}else{ |
61 |
20458 |
Assert(pinf != cinf && pmaj != cmaj); |
62 |
40916 |
Rational denDiffAbs = (cinf - pinf).abs(); |
63 |
|
|
64 |
40916 |
Rational numDiff = (cmaj - pmaj); |
65 |
20458 |
Assert(numDiff.sgn() >= 0); |
66 |
20458 |
Assert(denDiffAbs.sgn() > 0); |
67 |
40916 |
Rational ratio = numDiff / denDiffAbs; |
68 |
20458 |
Assert(ratio.sgn() > 0); |
69 |
|
|
70 |
20458 |
if(ratio < res){ |
71 |
3946 |
res = ratio; |
72 |
|
} |
73 |
|
} |
74 |
|
} |
75 |
136185 |
} |
76 |
|
|
77 |
|
DeltaRationalException::DeltaRationalException(const char* op, |
78 |
|
const DeltaRational& a, |
79 |
|
const DeltaRational& b) |
80 |
|
{ |
81 |
|
std::stringstream ss; |
82 |
|
ss << "Operation [" << op << "] between DeltaRational values "; |
83 |
|
ss << a << " and " << b << " is not a DeltaRational."; |
84 |
|
setMessage(ss.str()); |
85 |
|
} |
86 |
|
|
87 |
|
DeltaRationalException::~DeltaRationalException() {} |
88 |
|
Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const |
89 |
|
{ |
90 |
|
if(isIntegral() && y.isIntegral()){ |
91 |
|
Integer ti = floor(); |
92 |
|
Integer yi = y.floor(); |
93 |
|
return ti.euclidianDivideQuotient(yi); |
94 |
|
}else{ |
95 |
|
throw DeltaRationalException("euclidianDivideQuotient", *this, y); |
96 |
|
} |
97 |
|
} |
98 |
|
|
99 |
|
Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const |
100 |
|
{ |
101 |
|
if(isIntegral() && y.isIntegral()){ |
102 |
|
Integer ti = floor(); |
103 |
|
Integer yi = y.floor(); |
104 |
|
return ti.euclidianDivideRemainder(yi); |
105 |
|
}else{ |
106 |
|
throw DeltaRationalException("euclidianDivideRemainder", *this, y); |
107 |
|
} |
108 |
|
} |
109 |
|
|
110 |
28191 |
} // namespace cvc5 |