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

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
new file mode 100644
index 000000000..7217d0c5a
--- /dev/null
+++ b/src/util/integer_gmp_imp.h
@@ -0,0 +1,168 @@
+/*********************                                                        */
+/*! \file integer.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan, cconway
+ ** 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 integer constant.
+ **
+ ** A multiprecision integer constant.
+ **/
+
+#ifdef __CVC4__USE_GMP_IMP
+#include "cvc4_public.h"
+
+#ifndef __CVC4__INTEGER_H
+#define __CVC4__INTEGER_H
+
+#include <string>
+#include <iostream>
+#include "util/gmp_util.h"
+
+namespace CVC4 {
+
+class Rational;
+
+class Integer {
+private:
+  /**
+   * Stores the value of the rational is stored in a C++ GMP integer class.
+   * Using this instead of mpz_t allows for easier destruction.
+   */
+  mpz_class d_value;
+
+  /**
+   * Gets a reference to the gmp data that backs up the integer.
+   * Only accessible to friend classes.
+   */
+  const mpz_class& get_mpz() const { return d_value; }
+
+  /**
+   * Constructs an Integer by copying a GMP C++ primitive.
+   */
+  Integer(const mpz_class& val) : d_value(val) {}
+
+public:
+
+  /** Constructs a rational with the value 0. */
+  Integer() : d_value(0){}
+
+  /**
+   * Constructs a Integer from a C 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().
+   */
+  explicit Integer(const char * s, int base = 10): d_value(s,base) {}
+  Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
+
+  Integer(const Integer& q) : d_value(q.d_value) {}
+
+  Integer(  signed int z) : d_value(z) {}
+  Integer(unsigned int z) : d_value(z) {}
+  Integer(  signed long int z) : d_value(z) {}
+  Integer(unsigned long int z) : d_value(z) {}
+
+  ~Integer() {}
+
+
+  Integer& operator=(const Integer& x){
+    if(this == &x) return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  bool operator==(const Integer& y) const {
+    return d_value == y.d_value;
+  }
+
+  Integer operator-() const{
+    return Integer(-(d_value));
+  }
+
+
+  bool operator!=(const Integer& y) const {
+    return d_value != y.d_value;
+  }
+
+  bool operator< (const Integer& y) const {
+    return d_value < y.d_value;
+  }
+
+  bool operator<=(const Integer& y) const {
+    return d_value <= y.d_value;
+  }
+
+  bool operator> (const Integer& y) const {
+    return d_value > y.d_value;
+  }
+
+  bool operator>=(const Integer& y) const {
+    return d_value >= y.d_value;
+  }
+
+
+  Integer operator+(const Integer& y) const{
+    return Integer( d_value + y.d_value );
+  }
+
+  Integer operator-(const Integer& y) const {
+    return Integer( d_value - y.d_value );
+  }
+
+  Integer operator*(const Integer& y) const {
+    return Integer( d_value * y.d_value );
+  }
+  Integer operator/(const Integer& y) const {
+    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);
+  }
+
+  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+  long getLong() const { return d_value.get_si(); }
+  unsigned long getUnsignedLong() const {return d_value.get_ui(); }
+
+  /**
+   * Computes the hash of the node from the first word of the
+   * numerator, the denominator.
+   */
+  size_t hash() const {
+    return gmpz_hash(d_value.get_mpz_t());
+  }
+
+  friend class CVC4::Rational;
+};/* class Integer */
+
+struct IntegerHashStrategy {
+  static inline size_t hash(const CVC4::Integer& i) {
+    return i.hash();
+  }
+};/* struct IntegerHashStrategy */
+
+std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__INTEGER_H */
+#endif /* __CVC4__USE_GMP_IMP */