GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/delta_rational.cpp Lines: 26 52 50.0 %
Date: 2021-03-22 Branches: 37 210 17.6 %

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