Changing the rewriter to use Boute's Euclidean definition of division.

6 files changed, 150 insertions, 23 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a367b8599..823b61df5 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -338,7 +338,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
 
     bool isDiv = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
 
-    Integer result = isDiv ? ni.floorDivideQuotient(di) : ni.floorDivideRemainder(di);
+    Integer result = isDiv ? ni.euclidianDivideQuotient(di) : ni.euclidianDivideRemainder(di);
 
     Node resultNode = mkRationalNode(Rational(result));
     return RewriteResponse(REWRITE_DONE, resultNode);
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index a334e2c3d..39b99d625 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -83,23 +83,23 @@ DeltaRationalException::DeltaRationalException(const char* op, const DeltaRation
 DeltaRationalException::~DeltaRationalException() throw () { }
 
 
-Integer DeltaRational::floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
-    return ti.floorDivideQuotient(yi);
+    return ti.euclidianDivideQuotient(yi);
   }else{
-    throw DeltaRationalException("floorDivideQuotient", *this, y);
+    throw DeltaRationalException("euclidianDivideQuotient", *this, y);
   }
 }
 
-Integer DeltaRational::floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
-    return ti.floorDivideRemainder(yi);
+    return ti.euclidianDivideRemainder(yi);
   }else{
-    throw DeltaRationalException("floorDivideRemainder", *this, y);
+    throw DeltaRationalException("euclidianDivideRemainder", *this, y);
   }
 }
 
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index dc4202f36..19a16d558 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -236,10 +236,10 @@ public:
   }
 
   /** Only well defined if both this and y are integral. */
-  Integer floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
+  Integer euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
 
   /** Only well defined if both this and y are integral. */
-  Integer floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
+  Integer euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
 
 
   std::string toString() const;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ec6c7090..c2c005767 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2009,10 +2009,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalExce
       if(n.getKind() == kind::DIVISION_TOTAL){
         res = numer / denom;
       }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){
-        res = Rational(numer.floorDivideQuotient(denom));
+        res = Rational(numer.euclidianDivideQuotient(denom));
       }else{
         Assert(n.getKind() == kind::INTS_MODULUS_TOTAL);
-        res = Rational(numer.floorDivideRemainder(denom));
+        res = Rational(numer.euclidianDivideRemainder(denom));
       }
       if(isSetup(n)){
         ArithVar var = d_arithvarNodeMap.asArithVar(n);
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 211c40741..b5452ae00 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -275,6 +275,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 {
@@ -371,15 +426,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 bebd0e1e2..176604268 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -180,16 +180,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
@@ -246,6 +246,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 {
@@ -259,7 +314,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);
   }
@@ -273,12 +328,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;
   }