merged master into branch

6 files changed, 165 insertions, 25 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5df632ff4..c9661c0c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -190,22 +190,27 @@ public:
     return d_value.isBitSet(i); 
   }
   
-  BitVector unsignedDiv (const BitVector& y) const {
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedDivTotal (const BitVector& y) const {
+
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, Integer(0));
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
-
-  BitVector unsignedRem(const BitVector& y) const {
+  
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedRemTotal(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, d_value);
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index e2a8f4a62..81c0428cb 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -285,6 +285,61 @@ public:
   }
 
   /**
+   * Computes a quoitent and remainder according to Boute's Euclidean definition.
+   * euclidianDivideQuotient, euclidianDivideRemainder.
+   *
+   * Boute, Raymond T. (April 1992).
+   * The Euclidean definition of the functions div and mod.
+   * ACM Transactions on Programming Languages and Systems (TOPLAS)
+   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
+   */
+  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
+    // compute the floor and then fix the value up if needed.
+    floorQR(q,r,x,y);
+
+    if(r.strictlyNegative()){
+      // if r < 0
+      // abs(r) < abs(y)
+      // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
+      // n = y * q + r
+      // n = y * q - abs(y) + r + abs(y)
+      if(r.sgn() >= 0){
+        // y = abs(y)
+        // n = y * q - y + r + y
+        // n = y * (q-1) + (r+y)
+        q -= 1;
+        r += y;
+      }else{
+        // y = -abs(y)
+        // n = y * q + y + r - y
+        // n = y * (q+1) + (r-y)
+        q += 1;
+        r -= y;
+      }
+    }
+  }
+
+  /**
+   * Returns the quoitent according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideQuotient(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return q;
+  }
+
+  /**
+   * Returns the remainfing according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideRemainder(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return r;
+  }
+
+  /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
@@ -381,15 +436,24 @@ public:
     return cln::cl_I_to_int(sgn);
   }
 
-  bool isZero() const {
-    return cln::zerop(d_value);
+
+  inline bool strictlyPositive() const {
+    return sgn() > 0;
+  }
+
+  inline bool strictlyNegative() const {
+    return sgn() < 0;
+  }
+
+  inline bool isZero() const {
+    return sgn() == 0;
   }
 
-  bool isOne() const {
+  inline bool isOne() const {
     return d_value == 1;
   }
 
-  bool isNegativeOne() const {
+  inline bool isNegativeOne() const {
     return d_value == -1;
   }
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index d6882b6ac..85d49f921 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -199,16 +199,16 @@ public:
     mpz_class res = d_value;
 
     for (unsigned i = size; i < size + amount; ++i) {
-      mpz_setbit(res.get_mpz_t(), i); 
+      mpz_setbit(res.get_mpz_t(), i);
     }
-    
-    return Integer(res); 
+
+    return Integer(res);
   }
-  
+
   uint32_t toUnsignedInt() const {
     return  mpz_get_ui(d_value.get_mpz_t());
   }
-  
+
   /** See GMP Documentation. */
   Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
     // bitCount = high-low+1
@@ -265,6 +265,61 @@ public:
   }
 
   /**
+   * Computes a quoitent and remainder according to Boute's Euclidean definition.
+   * euclidianDivideQuotient, euclidianDivideRemainder.
+   *
+   * Boute, Raymond T. (April 1992).
+   * The Euclidean definition of the functions div and mod.
+   * ACM Transactions on Programming Languages and Systems (TOPLAS)
+   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
+   */
+  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
+    // compute the floor and then fix the value up if needed.
+    floorQR(q,r,x,y);
+
+    if(r.strictlyNegative()){
+      // if r < 0
+      // abs(r) < abs(y)
+      // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
+      // n = y * q + r
+      // n = y * q - abs(y) + r + abs(y)
+      if(r.sgn() >= 0){
+        // y = abs(y)
+        // n = y * q - y + r + y
+        // n = y * (q-1) + (r+y)
+        q -= 1;
+        r += y;
+      }else{
+        // y = -abs(y)
+        // n = y * q + y + r - y
+        // n = y * (q+1) + (r-y)
+        q += 1;
+        r -= y;
+      }
+    }
+  }
+  /**
+   * Returns the quoitent according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideQuotient(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return q;
+  }
+
+  /**
+   * Returns the remainfing according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideRemainder(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return r;
+  }
+
+
+  /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
@@ -278,7 +333,7 @@ public:
    * Returns y mod 2^exp
    */
   Integer modByPow2(uint32_t exp) const {
-    mpz_class res; 
+    mpz_class res;
     mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
     return Integer(res);
   }
@@ -292,12 +347,20 @@ public:
     return Integer(res);
   }
 
-  
+
   int sgn() const {
     return mpz_sgn(d_value.get_mpz_t());
   }
 
-  bool isZero() const {
+  inline bool strictlyPositive() const {
+    return sgn() > 0;
+  }
+
+  inline bool strictlyNegative() const {
+    return sgn() < 0;
+  }
+
+  inline bool isZero() const {
     return sgn() == 0;
   }
 
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index e444ba6e2..4c8e646bd 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -36,10 +36,11 @@ class NodeVisitor {
   /**
    * Guard against NodeVisitor<> being re-entrant.
    */
+  template <class T>
   class GuardReentry {
-    bool& d_guard;
+    T& d_guard;
   public:
-    GuardReentry(bool& guard)
+    GuardReentry(T& guard)
     : d_guard(guard) {
       Assert(!d_guard);
       d_guard = true;
@@ -71,7 +72,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(s_inRun));
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);
diff --git a/src/util/record.h b/src/util/record.h
index 2c15d30e0..27b090e1d 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -29,7 +29,7 @@
 
 namespace CVC4 {
 
-class Record;
+class CVC4_PUBLIC Record;
 
 // operators for record select and update
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3bf990dbb..af9088663 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -23,6 +23,7 @@
 
 #include "util/statistics.h"
 #include "util/exception.h"
+#include "lib/clock_gettime.h"
 
 #include <sstream>
 #include <iomanip>
@@ -612,12 +613,17 @@ public:
 
 };/* class StatisticsRegistry */
 
+}/* CVC4 namespace */
+
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /** Compute the sum of two timespecs. */
 inline timespec& operator+=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -640,6 +646,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
 
 /** Compute the difference of two timespecs. */
 inline timespec& operator-=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -716,6 +723,8 @@ inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 }
 
+namespace CVC4 {
+
 class CodeTimer;
 
 /**
@@ -765,7 +774,6 @@ public:
 
 };/* class TimerStat */
 
-
 /**
  * Utility class to make it easier to call stop() at the end of a
  * code block.  When constructed, it starts the timer.  When
@@ -788,7 +796,6 @@ public:
   }
 };/* class CodeTimer */
 
-
 /**
  * To use a statistic, you need to declare it, initialize it in your
  * constructor, register it in your constructor, and deregister it in