blob: 39b99d62550c8125de2514bc0f3caec7b0bb0710 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
/********************* */
/*! \file delta_rational.cpp
** \verbatim
** Original author: taking
** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "theory/arith/delta_rational.h"
using namespace std;
namespace CVC4 {
std::ostream& operator<<(std::ostream& os, const DeltaRational& dq){
return os << "(" << dq.getNoninfinitesimalPart()
<< "," << dq.getInfinitesimalPart() << ")";
}
std::string DeltaRational::toString() const {
return "(" + getNoninfinitesimalPart().toString() + "," +
getInfinitesimalPart().toString() + ")";
}
void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b){
Assert(res.sgn() > 0);
int cmp = a.cmp(b);
if(cmp != 0){
bool aLeqB = cmp < 0;
const DeltaRational& min = aLeqB ? a : b;
const DeltaRational& max = aLeqB ? b : a;
const Rational& pinf = min.getInfinitesimalPart();
const Rational& cinf = max.getInfinitesimalPart();
const Rational& pmaj = min.getNoninfinitesimalPart();
const Rational& cmaj = max.getNoninfinitesimalPart();
if(pmaj == cmaj){
Assert(pinf < cinf);
// any value of delta preserves the order
}else if(pinf == cinf){
Assert(pmaj < cmaj);
// any value of delta preserves the order
}else{
Assert(pinf != cinf && pmaj != cmaj);
Rational denDiffAbs = (cinf - pinf).abs();
Rational numDiff = (cmaj - pmaj);
Assert(numDiff.sgn() >= 0);
Assert(denDiffAbs.sgn() > 0);
Rational ratio = numDiff / denDiffAbs;
Assert(ratio.sgn() > 0);
if(ratio < res){
res = ratio;
}
}
}
}
DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){
std::stringstream ss;
ss << "Operation [" << op << "] between DeltaRational values ";
ss << a << " and " << b << " is not a DeltaRational.";
setMessage(ss.str());
}
DeltaRationalException::~DeltaRationalException() throw () { }
Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
if(isIntegral() && y.isIntegral()){
Integer ti = floor();
Integer yi = y.floor();
return ti.euclidianDivideQuotient(yi);
}else{
throw DeltaRationalException("euclidianDivideQuotient", *this, y);
}
}
Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
if(isIntegral() && y.isIntegral()){
Integer ti = floor();
Integer yi = y.floor();
return ti.euclidianDivideRemainder(yi);
}else{
throw DeltaRationalException("euclidianDivideRemainder", *this, y);
}
}
}/* CVC4 namespace */
|
