/********************* */ /*! \file rational_cln_imp.cpp ** \verbatim ** Original author: taking ** Major contributors: mdeters ** 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. **/ #include "cvc4autoconfig.h" #include "util/rational.h" #include #ifndef CVC4_CLN_IMP # error "This source should only ever be built if CVC4_CLN_IMP is on !" #endif /* CVC4_CLN_IMP */ using namespace std; using namespace CVC4; /* Computes a rational given a decimal string. The rational * version of xxx.yyy is xxxyyy/(10^3). */ Rational Rational::fromDecimal(const std::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(); }