diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:51 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:51 +0000 |
commit | e909abcaf122e7c426d2b078728679f43a8ca442 (patch) | |
tree | 76b30fe96fe097770e7ab90518d945fd41555b76 /src/util | |
parent | 4e365ace4baa9eb519268c621ac69843a0599208 (diff) |
Implementing Rational::fromDecimal and adding support for real constants in SMT parsers
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/integer.h | 14 | ||||
-rw-r--r-- | src/util/rational.cpp | 26 | ||||
-rw-r--r-- | src/util/rational.h | 11 |
3 files changed, 46 insertions, 5 deletions
diff --git a/src/util/integer.h b/src/util/integer.h index 2aa8b711a..c019144a9 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -52,8 +52,8 @@ public: /** * Constructs a Integer from a C string. - * Throws std::invalid_argument if the stribng is not a valid rational. - * For more information about what is a vaid rational string, + * Throws std::invalid_argument if the string is not a valid rational. + * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ Integer(const char * s, int base = 10): d_value(s,base) {} @@ -120,6 +120,16 @@ public: return Integer( d_value / y.d_value ); } + /** Raise this Integer to the power <code>exp</code>. + * + * @param exp the exponent + */ + Integer pow(unsigned long int exp) const { + mpz_class result; + mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp); + return Integer( result ); + } + std::string toString(int base = 10) const{ return d_value.get_str(base); } diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 3ed357de7..5e9141758 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -10,13 +10,37 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** A multiprecision rational constant. + ** A multi-precision rational constant. **/ +#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(); } diff --git a/src/util/rational.h b/src/util/rational.h index 90ac388b2..f50b4e63e 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -48,6 +48,13 @@ private: public: + /** Creates a rational from a decimal string (e.g., <code>"1.5"</code>). + * + * @param dec a string encoding a decimal number in the format + * <code>[0-9]*\.[0-9]*</code> + */ + static Rational fromDecimal(const std::string& dec); + /** Constructs a rational with the value 0/1. */ Rational() : d_value(0){ d_value.canonicalize(); @@ -55,8 +62,8 @@ public: /** * Constructs a Rational from a C string in a given base (defaults to 10). - * Throws std::invalid_argument if the stribng is not a valid rational. - * For more information about what is a vaid rational string, + * Throws std::invalid_argument if the string is not a valid rational. + * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ Rational(const char * s, int base = 10): d_value(s,base) { |