diff options
author | Tim King <taking@cs.nyu.edu> | 2010-07-02 18:49:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-07-02 18:49:47 +0000 |
commit | fdf952bba734d63fe52b18bba1ef7a8f9c935455 (patch) | |
tree | 5f8eea581731091bb61fb150d28a394b0df2bda2 /src/util/rational_cln_imp.cpp | |
parent | 5f2d818b1a2801f647fe1f3ce2a61d7d4806e251 (diff) |
Merges the cln-test branch into the main branch.
The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac. A configure time flag has not yet been added for deciding between the two.
To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev). You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure.
Diffstat (limited to 'src/util/rational_cln_imp.cpp')
-rw-r--r-- | src/util/rational_cln_imp.cpp | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp new file mode 100644 index 000000000..0960b79b9 --- /dev/null +++ b/src/util/rational_cln_imp.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file rational_cln_imp.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters, cconway + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A multi-precision rational constant. + ** + ** A multi-precision rational constant. + **/ + +#ifdef __CVC4__USE_CLN_IMP + + +#include "util/integer.h" +#include "util/rational.h" +#include <string> + +using namespace std; +using namespace CVC4; + +/* Computes a rational given a decimal string. The rational + * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. + */ +Rational Rational::fromDecimal(const string& dec) { + // Find the decimal point, if there is one + string::size_type i( dec.find(".") ); + if( i != string::npos ) { + /* Erase the decimal point, so we have just the numerator. */ + Integer numerator( string(dec).erase(i,1) ); + + /* Compute the denominator: 10 raise to the number of decimal places */ + int decPlaces = dec.size() - (i + 1); + Integer denominator( Integer(10).pow(decPlaces) ); + + return Rational( numerator, denominator ); + } else { + /* No decimal point, assume it's just an integer. */ + return Rational( dec ); + } +} + +std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ + return os << q.toString(); +} + +#endif /* __CVC4__USE_CLN_IMP */ |