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

4 files changed, 11 insertions, 11 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);