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.

1 files changed, 52 insertions, 0 deletions

diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
new file mode 100644
index 000000000..e5ff11c07
--- /dev/null
+++ b/src/util/rational_gmp_imp.cpp
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file rational.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_GMP_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_GMP_IMP */