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, 34 insertions, 0 deletions

diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
new file mode 100644
index 000000000..35293bb84
--- /dev/null
+++ b/src/util/integer_cln_imp.cpp
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file integer.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** 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 multiprecision rational constant.
+ **
+ ** A multiprecision rational constant.
+ ** This stores the rational as a pair of multiprecision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1.  (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consquence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **/
+#ifdef __CVC4__USE_CLN_IMP
+
+#include "util/integer.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
+
+#endif /* __CVC4__USE_CLN_IMP */