1 /********************* */
4 ** Original author: taking
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A multiprecision rational constant.
16 ** A multiprecision rational constant.
17 ** This stores the rational as a pair of multiprecision integers,
18 ** one for the numerator and one for the denominator.
19 ** The number is always stored so that the gcd of the numerator and denominator
20 ** is 1. (This is referred to as referred to as canonical form in GMP's
21 ** literature.) A consquence is that that the numerator and denominator may be
22 ** different than the values used to construct the Rational.
24 #ifdef __CVC4__USE_CLN_IMP
26 #include "util/integer.h"
30 std::ostream
& CVC4::operator<<(std::ostream
& os
, const Integer
& n
) {
31 return os
<< n
.toString();
34 #endif /* __CVC4__USE_CLN_IMP */