GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/rational_cln_imp.cpp Lines: 34 48 70.8 %
Date: 2021-03-22 Branches: 38 120 31.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rational_cln_imp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Christopher L. Conway, 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 A multi-precision rational constant.
13
 **
14
 ** A multi-precision rational constant.
15
 **/
16
#include "util/rational.h"
17
18
#include <sstream>
19
#include <string>
20
21
#include "cvc4autoconfig.h"
22
23
#ifndef CVC4_CLN_IMP
24
#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
25
#endif /* CVC4_CLN_IMP */
26
27
#include "base/check.h"
28
29
using namespace std;
30
31
namespace CVC4 {
32
33
/* Computes a rational given a decimal string. The rational
34
 * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
35
 */
36
379922
Rational Rational::fromDecimal(const std::string& dec) {
37
  // Find the decimal point, if there is one
38
379922
  string::size_type i( dec.find(".") );
39
379922
  if( i != string::npos ) {
40
    /* Erase the decimal point, so we have just the numerator. */
41
44584
    Integer numerator( string(dec).erase(i,1) );
42
43
    /* Compute the denominator: 10 raise to the number of decimal places */
44
22288
    int decPlaces = dec.size() - (i + 1);
45
44576
    Integer denominator( Integer(10).pow(decPlaces) );
46
47
22288
    return Rational( numerator, denominator );
48
  } else {
49
    /* No decimal point, assume it's just an integer. */
50
357630
    return Rational( dec );
51
  }
52
}
53
54
401388354
int Rational::sgn() const
55
{
56
401388354
  if (cln::zerop(d_value))
57
  {
58
40176370
    return 0;
59
  }
60
361211984
  else if (cln::minusp(d_value))
61
  {
62
234736653
    return -1;
63
  }
64
  else
65
  {
66
126475331
    Assert(cln::plusp(d_value));
67
126475331
    return 1;
68
  }
69
}
70
71
729956
std::ostream& operator<<(std::ostream& os, const Rational& q){
72
729956
  return os << q.toString();
73
}
74
75
76
77
/** Equivalent to calling (this->abs()).cmp(b.abs()) */
78
7864641
int Rational::absCmp(const Rational& q) const{
79
7864641
  const Rational& r = *this;
80
7864641
  int rsgn = r.sgn();
81
7864641
  int qsgn = q.sgn();
82
7864641
  if(rsgn == 0){
83
    return (qsgn == 0) ? 0 : -1;
84
7864641
  }else if(qsgn == 0){
85
    Assert(rsgn != 0);
86
    return 1;
87
7864641
  }else if((rsgn > 0) && (qsgn > 0)){
88
6210926
    return r.cmp(q);
89
1653715
  }else if((rsgn < 0) && (qsgn < 0)){
90
    // if r < q < 0, q.cmp(r) = +1, (r.abs()).cmp(q.abs()) = +1
91
    // if q < r < 0, q.cmp(r) = -1, (r.abs()).cmp(q.abs()) = -1
92
    // if q = r < 0, q.cmp(r) =  0, (r.abs()).cmp(q.abs()) =  0
93
194947
    return q.cmp(r);
94
1458768
  }else if((rsgn < 0) && (qsgn > 0)){
95
1653260
    Rational rpos = -r;
96
826630
    return rpos.cmp(q);
97
  }else {
98
632138
    Assert(rsgn > 0 && (qsgn < 0));
99
1264276
    Rational qpos = -q;
100
632138
    return r.cmp(qpos);
101
  }
102
}
103
104
Maybe<Rational> Rational::fromDouble(double d)
105
{
106
  try{
107
    cln::cl_DF fromD = d;
108
    Rational q;
109
    q.d_value = cln::rationalize(fromD);
110
    return q;
111
  }catch(cln::floating_point_underflow_exception& fpue){
112
    return Maybe<Rational>();
113
  }catch(cln::floating_point_nan_exception& fpne){
114
    return Maybe<Rational>();
115
  }catch(cln::floating_point_overflow_exception& fpoe){
116
    return Maybe<Rational>();
117
  }
118
}
119
120
26676
} /* namespace CVC4 */