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

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
new file mode 100644
index 000000000..347c1d195
--- /dev/null
+++ b/src/util/rational_cln_imp.h
@@ -0,0 +1,286 @@
+/*********************                                                        */
+/*! \file rational.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters, 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 Multi-precision rational constants.
+ **
+ ** Multi-precision rational constants.
+ **/
+
+#ifdef __CVC4__USE_CLN_IMP
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
+#include <gmp.h>
+#include <string>
+#include <sstream>
+#include <cln/rational.h>
+#include <cln/input.h>
+#include <cln/rational_io.h>
+#include <cln/number_io.h>
+#include "util/Assert.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+/**
+ ** A multi-precision rational constant.
+ ** This stores the rational as a pair of multi-precision 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 consequence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **
+ ** NOTE: The correct way to create a Rational from an int is to use one of the
+ ** int numerator/int denominator constructors with the denominator 1.  Trying
+ ** to construct a Rational with a single int, e.g., Rational(0), will put you
+ ** in danger of invoking the char* constructor, from whence you will segfault.
+ **/
+
+class CVC4_PUBLIC Rational {
+private:
+  /**
+   * Stores the value of the rational is stored in a C++ GMP rational class.
+   * Using this instead of mpq_t allows for easier destruction.
+   */
+  cln::cl_RA d_value;
+
+  /**
+   * Constructs a Rational from a mpq_class object.
+   * Does a deep copy.
+   * Assumes that the value is in canonical form, and thus does not
+   * have to call canonicalize() on the value.
+   */
+  //Rational(const mpq_class& val) : d_value(val) {  }
+  Rational(const cln::cl_RA& val) : d_value(val) {  }
+
+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){
+  }
+
+  /**
+   * Constructs a Rational from a C string in a given base (defaults to 10).
+   * 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 Rational(const char * s, int base = 10) throw (std::invalid_argument){
+    cln::cl_read_flags flags;
+
+    flags.syntax = cln::syntax_rational;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_rational(flags, s, NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+      throw std::invalid_argument(ss.str());
+    }
+  }
+  Rational(const std::string& s, int base = 10) throw (std::invalid_argument){
+    cln::cl_read_flags flags;
+
+    flags.syntax = cln::syntax_rational;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_rational(flags, s.c_str(), NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+      throw std::invalid_argument(ss.str());
+    }
+  }
+
+  /**
+   * Creates a Rational from another Rational, q, by performing a deep copy.
+   */
+  Rational(const Rational& q) : d_value(q.d_value) { }
+
+  /**
+   * Constructs a canonical Rational from a numerator.
+   */
+  Rational(signed int n) : d_value(n) { }
+  Rational(unsigned int n) : d_value(n) { }
+  Rational(signed long int n) : d_value(n) { }
+  Rational(unsigned long int n) : d_value(n) { }
+
+  /**
+   * Constructs a canonical Rational from a numerator and denominator.
+   */
+  Rational(signed int n, signed int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(unsigned int n, unsigned int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(signed long int n, signed long int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(unsigned long int n, unsigned long int d) : d_value(n) {
+    d_value /= d;
+  }
+
+  Rational(const Integer& n, const Integer& d) :
+    d_value(n.get_cl_I())
+  {
+    d_value /= d.get_cl_I();
+  }
+  Rational(const Integer& n) : d_value(n.get_cl_I()){  }
+
+  ~Rational() {}
+
+
+  /**
+   * Returns the value of numerator of the Rational.
+   * Note that this makes a deep copy of the numerator.
+   */
+  Integer getNumerator() const {
+    return Integer(cln::numerator(d_value));
+  }
+
+  /**
+   * Returns the value of denominator of the Rational.
+   * Note that this makes a deep copy of the denominator.
+   */
+  Integer getDenominator() const{
+    return Integer(cln::denominator(d_value));
+  }
+
+  Rational inverse() const {
+    return Rational(cln::recip(d_value));
+  }
+
+  int cmp(const Rational& x) const {
+    //Don't use mpq_class's cmp() function.
+    //The name ends up conflicting with this function.
+    return cln::compare(d_value, x.d_value);
+  }
+
+
+  int sgn() {
+    cln::cl_RA sign = cln::signum(d_value);
+    if(sign == 0)
+      return 0;
+    else if(sign == -1)
+      return -1;
+    else if(sign == 1)
+      return 1;
+    else
+      Unreachable();
+  }
+
+  Rational& operator=(const Rational& x){
+    if(this == &x) return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  Rational operator-() const{
+    return Rational(-(d_value));
+  }
+
+  bool operator==(const Rational& y) const {
+    return d_value == y.d_value;
+  }
+
+  bool operator!=(const Rational& y) const {
+    return d_value != y.d_value;
+  }
+
+  bool operator< (const Rational& y) const {
+    return d_value < y.d_value;
+  }
+
+  bool operator<=(const Rational& y) const {
+    return d_value <= y.d_value;
+  }
+
+  bool operator> (const Rational& y) const {
+    return d_value > y.d_value;
+  }
+
+  bool operator>=(const Rational& y) const {
+    return d_value >= y.d_value;
+  }
+
+
+  
+
+  Rational operator+(const Rational& y) const{
+    return Rational( d_value + y.d_value );
+  }
+  Rational operator-(const Rational& y) const {
+    return Rational( d_value - y.d_value );
+  }
+
+  Rational operator*(const Rational& y) const {
+    return Rational( d_value * y.d_value );
+  }
+  Rational operator/(const Rational& y) const {
+    return Rational( d_value / y.d_value );
+  }
+
+  Rational& operator+=(const Rational& y){
+    d_value += y.d_value;
+    return (*this);
+  }
+
+  Rational& operator*=(const Rational& y){
+    d_value *= y.d_value;
+    return (*this);
+  }
+
+  /** Returns a string representing the rational in the given base. */
+  std::string toString(int base = 10) const {
+    std::stringstream ss;
+    fprint(ss, d_value);
+    return ss.str();
+  }
+
+  /**
+   * Computes the hash of the rational from hashes of the numerator and the
+   * denominator.
+   */
+  size_t hash() const {
+    return equal_hashcode(d_value);
+  }
+
+};/* class Rational */
+
+struct RationalHashStrategy {
+  static inline size_t hash(const CVC4::Rational& r) {
+    return r.hash();
+  }
+};/* struct RationalHashStrategy */
+
+std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+
+#endif /* __CVC4__USE_CLN_IMP */