Implementing Rational::fromDecimal and adding support for real constants in SMT parsers

5 files changed, 53 insertions, 9 deletions

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 18317e4d8..f52467ad9 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -29,6 +29,8 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/Assert.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 
@@ -146,6 +148,8 @@ public:
   static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
+  /** Retrive a Bitvector from the text of a token */
+//  static Bitvector tokenToBitvector(pANTLR3_COMMON_TOKEN token, int base);
 
 protected:
   /** Create an input. This input takes ownership of the given input stream,
@@ -202,8 +206,7 @@ inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
 }
 
 inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
-  Rational r( tokenText(token) );
-  return r;
+  return Rational::fromDecimal( tokenText(token) );
 }
 
 }/* CVC4::parser namespace */
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) {
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index b8060086f..da636353e 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -173,8 +173,8 @@ const string goodSmt2Exprs[] = {
     "(= (xor a b) (and (or a b) (not (and a b))))",
     "(ite a (f x) y)",
     "1",
-    "0"// ,
-//    "1.5"
+    "0",
+    "1.5"
 };
 
 const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string);