FCSimplex branch merge

9 files changed, 213 insertions, 11 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index f95382cb1..4f93f5a61 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -39,6 +39,7 @@ libutil_la_SOURCES = \
 	datatype.h \
 	datatype.cpp \
 	tuple.h \
+	maybe.h \
 	record.h \
 	record.cpp \
 	matcher.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index ba141cc58..f03c5e959 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -121,6 +121,10 @@ bool Configuration::isBuiltWithCln() {
   return IS_CLN_BUILD;
 }
 
+bool Configuration::isBuiltWithGlpk() {
+  return IS_GLPK_BUILD;
+}
+
 bool Configuration::isBuiltWithCudd() {
   return false;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index a63a0d6f3..7e543c54e 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -87,6 +87,8 @@ public:
 
   static bool isBuiltWithCln();
 
+  static bool isBuiltWithGlpk();
+
   static bool isBuiltWithCudd();
 
   static bool isBuiltWithTlsSupport();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 272766ff4..3b3115887 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -101,6 +101,12 @@ namespace CVC4 {
 #  define IS_CLN_BUILD false
 #endif /* CVC4_CLN_IMP */
 
+#if CVC4_USE_GLPK
+#  define IS_GLPK_BUILD true
+#else /* CVC4_USE_GLPK */
+#  define IS_GLPK_BUILD false
+#endif /* CVC4_USE_GLPK */
+
 #ifdef TLS
 #  define USING_TLS true
 #else /* TLS */
@@ -124,13 +130,20 @@ Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
 This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\
 However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well\n\
+and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well.\n\
 Please consult the CVC4 documentation for instructions about building\n\
 without CLN if you want to license CVC4 under the (modified) BSD license.\n\n\
+" : ( IS_GLPK_BUILD ? "\
+This CVC4 library uses GLPK in its arithmetic solver.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n\
+However, GLPK, the GNU Linear Programming Kit, is covered by the GPLv3,\n\
+and so this \"combined\" work, CVC4+GLPK, is covered by the GPLv3 as well.\n\
+Please consult the CVC4 documentation for instructions about building\n\
+without GLPK if you want to license CVC4 under the (modified) BSD license.\n\n\
 " : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\n\
-" ) + "\
+" ) ) + "\
 THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\
 See the file COPYING (distributed with the source code, and with all binaries)\n\
 for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" )
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index b8acf1556..8f8b63668 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -29,6 +29,7 @@
 #include <vector>
 #include <boost/integer_traits.hpp>
 #include "util/index.h"
+#include "util/cvc4_assert.h"
 
 namespace CVC4 {
 
@@ -287,15 +288,36 @@ public:
 
   bool isMember(Element x) const{ return d_map.isKey(x); }
 
-  void add(Element x){
+  void add(Element x, CountType c = 1u){
+    Assert(c > 0);
     if(d_map.isKey(x)){
-      d_map.set(x, d_map.get(x)+1);
+      d_map.set(x, d_map.get(x)+c);
     }else{
-      d_map.set(x,1);
+      d_map.set(x,c);
     }
   }
 
-  void remove(Element x){ return d_map.remove(x); }
+  void setCount(Element x, CountType c){
+    d_map.set(x, c);
+  }
+
+  void removeAll(Element x){ return d_map.remove(x); }
+
+  void removeOne(Element x){
+    CountType c = count(x);
+    switch(c){
+    case 0: break; // do nothing
+    case 1: removeAll(x); break; // remove
+    default: d_map.set(x, c-1); break; // decrease
+    }
+  }
+
+  void removeOneOfEverything(){
+    BackingMap::KeyList keys(d_map.begin(), d_map.end());
+    for(BackingMap::const_iterator i=keys.begin(), i_end = keys.end(); i != i_end; ++i){
+      removeOne(*i);
+    }
+  }
 
   CountType count(Element x) const {
     if(d_map.isKey(x)){
diff --git a/src/util/maybe.h b/src/util/maybe.h
new file mode 100644
index 000000000..795eac759
--- /dev/null
+++ b/src/util/maybe.h
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file maybe.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This provides a templated Maybe construct.
+ **
+ ** This class provides a templated Maybe<T> construct.
+ ** This follows the rough pattern of the Maybe monad in haskell.
+ ** A Maybe is an algebraic type that is either Nothing | Just T
+ **
+ ** T must support T() and operator=.
+ **
+ ** This has a couple of uses:
+ ** - There is no reasonable value or particularly clean way to represent
+ **   Nothing using a value of T
+ ** - High level of assurance that a value is not used before it is set.
+ **/
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <ostream>
+#include "util/exception.h"
+
+namespace CVC4 {
+
+template <class T>
+class Maybe {
+private:
+  bool d_just;
+  T d_value;
+
+public:
+  Maybe() : d_just(false), d_value(){}
+  Maybe(const T& val): d_just(true), d_value(val){}
+
+  Maybe& operator=(const T& v){
+    d_just = true;
+    d_value = v;
+    return *this;
+  }
+
+  inline bool nothing() const { return !d_just; }
+  inline bool just() const { return d_just; }
+
+  void clear() {
+    if(just()){
+      d_just = false;
+      d_value = T();
+    }
+  }
+
+  T& value() {
+    Assert(just(), "Maybe::value() requires the maybe to be set.");
+    return d_value;
+  }
+  const T& constValue() const {
+    Assert(just(), "Maybe::constValue() requires the maybe to be set.");
+    return d_value;
+  }
+
+  operator const T&() const { return constValue(); }
+};
+
+template <class T>
+inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
+  out << "{";
+  if(m.nothing()){
+    out << "Nothing";
+  }else{
+    out << m.constValue();
+  }
+  out << "}";
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 476ddd544..1e27fa859 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -30,6 +30,8 @@
 #include <cln/output.h>
 #include <cln/rational_io.h>
 #include <cln/number_io.h>
+#include <cln/dfloat.h>
+#include <cln/real.h>
 
 #include "util/exception.h"
 #include "util/integer.h"
@@ -139,16 +141,16 @@ public:
    * Constructs a canonical Rational from a numerator and denominator.
    */
   Rational(signed int n, signed int d) : d_value((signed long int)n) {
-    d_value /= d;
+    d_value /= cln::cl_I(d);
   }
   Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) {
-    d_value /= d;
+    d_value /= cln::cl_I(d);
   }
   Rational(signed long int n, signed long int d) : d_value(n) {
-    d_value /= d;
+    d_value /= cln::cl_I(d);
   }
   Rational(unsigned long int n, unsigned long int d) : d_value(n) {
-    d_value /= d;
+    d_value /= cln::cl_I(d);
   }
 
 #ifdef CVC4_NEED_INT64_T_OVERLOADS
@@ -186,6 +188,14 @@ public:
     return Integer(cln::denominator(d_value));
   }
 
+  /** Return an exact rational for a double d. */
+  static Rational fromDouble(double d){
+    cln::cl_DF fromD = d;
+    Rational q;
+    q.d_value = cln::rationalize(fromD);
+    return q;
+  }
+
   /**
    * Get a double representation of this Rational, which is
    * approximate: truncation may occur, overflow may result in
@@ -302,6 +312,11 @@ public:
     return (*this);
   }
 
+  Rational& operator-=(const Rational& y){
+    d_value -= y.d_value;
+    return (*this);
+  }
+
   Rational& operator*=(const Rational& y){
     d_value *= y.d_value;
     return (*this);
@@ -330,6 +345,10 @@ public:
     return equal_hashcode(d_value);
   }
 
+  uint32_t complexity() const {
+    return getNumerator().length() + getDenominator().length();
+  }
+
 };/* class Rational */
 
 struct RationalHashFunction {
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 0916b523a..02ccc273c 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -156,7 +156,6 @@ public:
   }
   ~Rational() {}
 
-
   /**
    * Returns the value of numerator of the Rational.
    * Note that this makes a deep copy of the numerator.
@@ -173,6 +172,13 @@ public:
     return Integer(d_value.get_den());
   }
 
+  /** Return an exact rational for a double d. */
+  static Rational fromDouble(double d){
+    Rational q;
+    mpq_set_d(q.d_value.get_mpq_t(), d);
+    return q;
+  }
+
   /**
    * Get a double representation of this Rational, which is
    * approximate: truncation may occur, overflow may result in
@@ -280,6 +286,10 @@ public:
     d_value += y.d_value;
     return (*this);
   }
+  Rational& operator-=(const Rational& y){
+    d_value -= y.d_value;
+    return (*this);
+  }
 
   Rational& operator*=(const Rational& y){
     d_value *= y.d_value;
@@ -311,6 +321,11 @@ public:
     return numeratorHash xor denominatorHash;
   }
 
+  uint32_t complexity() const {
+    uint32_t numLen = getNumerator().length();
+    uint32_t denLen = getDenominator().length();
+    return  numLen + denLen;
+  }
 };/* class Rational */
 
 struct RationalHashFunction {
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index e0bc81d91..3bec559d5 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -29,6 +29,7 @@
 #include <iomanip>
 #include <ctime>
 #include <vector>
+#include <map>
 #include <stdint.h>
 #include <cassert>
 
@@ -537,6 +538,47 @@ public:
 
 };/* class ListStat */
 
+template <class T>
+class HistogramStat : public Stat {
+private:
+  typedef std::map<T, unsigned int> Histogram;
+  Histogram d_hist;
+public:
+
+  /** Construct a histogram of a stream of entries. */
+  HistogramStat(const std::string& name) : Stat(name) {}
+  ~HistogramStat() {}
+
+  void flushInformation(std::ostream& out) const{
+    if(__CVC4_USE_STATISTICS) {
+      typename Histogram::const_iterator i = d_hist.begin();
+      typename Histogram::const_iterator end =  d_hist.end();
+      out << "[";
+      while(i != end){
+        const T& key = (*i).first;
+        unsigned int count = (*i).second;
+        out << "("<<key<<" : "<<count<< ")";
+        ++i;
+        if(i != end){
+          out << ", ";
+        }
+      }
+      out << "]";
+    }
+  }
+
+  HistogramStat& operator<<(const T& val){
+    if(__CVC4_USE_STATISTICS) {
+      if(d_hist.find(val) == d_hist.end()){
+        d_hist.insert(std::make_pair(val,0));
+      }
+      d_hist[val]++;
+    }
+    return (*this);
+  }
+
+};/* class HistogramStat */
+
 /****************************************************************************/
 /* Statistics Registry                                                      */
 /****************************************************************************/