Adds a number of new capabilities to DeltaRational. This adds DeltaRationalException which can be called when an operation on a DeltaRational does not have well formed semantics. This allows for things like multiplying two DeltaRationals, which may or may not result in a DeltaRational.

2 files changed, 156 insertions, 8 deletions

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index 9305b1efd..a334e2c3d 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -19,9 +19,10 @@
 #include "theory/arith/delta_rational.h"
 
 using namespace std;
-using namespace CVC4;
 
-std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os, const DeltaRational& dq){
   return os << "(" << dq.getNoninfinitesimalPart()
             << "," << dq.getInfinitesimalPart() << ")";
 }
@@ -31,3 +32,75 @@ std::string DeltaRational::toString() const {
   return "(" + getNoninfinitesimalPart().toString() + "," +
     getInfinitesimalPart().toString() + ")";
 }
+
+void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b){
+  Assert(res.sgn() > 0);
+
+  int cmp = a.cmp(b);
+  if(cmp != 0){
+    bool aLeqB = cmp < 0;
+
+    const DeltaRational& min = aLeqB ? a : b;
+    const DeltaRational& max = aLeqB ? b : a;
+
+    const Rational& pinf = min.getInfinitesimalPart();
+    const Rational& cinf = max.getInfinitesimalPart();
+
+    const Rational& pmaj = min.getNoninfinitesimalPart();
+    const Rational& cmaj = max.getNoninfinitesimalPart();
+
+    if(pmaj == cmaj){
+      Assert(pinf < cinf);
+      // any value of delta preserves the order
+    }else if(pinf == cinf){
+      Assert(pmaj < cmaj);
+      // any value of delta preserves the order
+    }else{
+      Assert(pinf != cinf && pmaj != cmaj);
+      Rational denDiffAbs = (cinf - pinf).abs();
+
+      Rational numDiff = (cmaj - pmaj);
+      Assert(numDiff.sgn() >= 0);
+      Assert(denDiffAbs.sgn() > 0);
+      Rational ratio = numDiff / denDiffAbs;
+      Assert(ratio.sgn() > 0);
+
+      if(ratio < res){
+        res = ratio;
+      }
+    }
+  }
+}
+
+
+DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){
+    std::stringstream ss;
+    ss << "Operation [" << op << "] between DeltaRational values ";
+    ss << a << " and " << b << " is not a DeltaRational.";
+    setMessage(ss.str());
+}
+
+DeltaRationalException::~DeltaRationalException() throw () { }
+
+
+Integer DeltaRational::floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
+  if(isIntegral() && y.isIntegral()){
+    Integer ti = floor();
+    Integer yi = y.floor();
+    return ti.floorDivideQuotient(yi);
+  }else{
+    throw DeltaRationalException("floorDivideQuotient", *this, y);
+  }
+}
+
+Integer DeltaRational::floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
+  if(isIntegral() && y.isIntegral()){
+    Integer ti = floor();
+    Integer yi = y.floor();
+    return ti.floorDivideRemainder(yi);
+  }else{
+    throw DeltaRationalException("floorDivideRemainder", *this, y);
+  }
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 1723b8680..dc4202f36 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -19,15 +19,24 @@
 
 #include "util/integer.h"
 #include "util/rational.h"
+#include "util/exception.h"
 
-#include <ostream>
 
+#include <ostream>
+#pragma once
 
-#ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
-#define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
 
 namespace CVC4 {
 
+class DeltaRational;
+
+class DeltaRationalException : public Exception {
+public:
+  DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw ();
+  virtual ~DeltaRationalException() throw ();
+};
+
+
 /**
  * A DeltaRational is a pair of rationals (c,k) that represent the number
  *   c + kd
@@ -65,6 +74,19 @@ public:
     return getInfinitesimalPart().sgn();
   }
 
+  bool infinitesimalIsZero() const {
+    return getInfinitesimalPart().isZero();
+  }
+
+  bool noninfinitesimalIsZero() const {
+    return getNoninfinitesimalPart().isZero();
+  }
+
+  bool isZero() const {
+    return noninfinitesimalIsZero() && infinitesimalIsZero();
+  }
+
+
   int cmp(const DeltaRational& other) const{
     int cmp = c.cmp(other.c);
     if(cmp == 0){
@@ -86,6 +108,23 @@ public:
     return DeltaRational(tmpC, tmpK);
   }
 
+
+  /**
+   * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
+   * This can be done whenever this->k or a.k is 0.
+   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
+   */
+  DeltaRational operator*(const DeltaRational& a) const throw(DeltaRationalException){
+    if(infinitesimalIsZero()){
+      return a * (this->getNoninfinitesimalPart());
+    }else if(a.infinitesimalIsZero()){
+      return (*this) * a.getNoninfinitesimalPart();
+    }else{
+      throw DeltaRationalException("operator*", *this, a);
+    }
+  }
+
+
   DeltaRational operator-(const DeltaRational& a) const{
     CVC4::Rational negOne(CVC4::Integer(-1));
     return *(this) + (a * negOne);
@@ -107,10 +146,29 @@ public:
     return DeltaRational(tmpC, tmpK);
   }
 
+  /**
+   * Divides (*this) / (a.c + a.k * delta)
+   * This can be done when a.k is 0 and a.c is non-zero.
+   * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
+   */
+  DeltaRational operator/(const DeltaRational& a) const throw(DeltaRationalException){
+    if(a.infinitesimalIsZero()){
+      return (*this) / a.getNoninfinitesimalPart();
+    }else{
+      throw DeltaRationalException("operator/", *this, a);
+    }
+  }
+
+
   bool operator==(const DeltaRational& other) const{
     return (k == other.k) && (c == other.c);
   }
 
+  bool operator!=(const DeltaRational& other) const{
+    return !(*this == other);
+  }
+
+
   bool operator<=(const DeltaRational& other) const{
     int cmp = c.cmp(other.c);
     return (cmp < 0) || ((cmp==0)&&(k <= other.k));
@@ -146,7 +204,7 @@ public:
   }
 
   bool isIntegral() const {
-    if(getInfinitesimalPart().sgn() == 0){
+    if(infinitesimalIsZero()){
       return getNoninfinitesimalPart().isIntegral();
     }else{
       return false;
@@ -177,16 +235,33 @@ public:
     }
   }
 
+  /** Only well defined if both this and y are integral. */
+  Integer floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
+
+  /** Only well defined if both this and y are integral. */
+  Integer floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
+
+
   std::string toString() const;
 
   Rational substituteDelta(const Rational& d) const{
     return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
   }
 
+  /**
+   * Computes a sufficient upperbound to seperate two DeltaRationals.
+   * This value is stored in res.
+   * For any rational d such that
+   *   0 < d < res
+   * then
+   *   a < b if and only if substituteDelta(a, d) < substituteDelta(b,d).
+   * (Similar relationships hold for for a == b and a > b.)
+   * Precondition: res > 0
+   */
+  static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b);
+
 };
 
 std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
 
 }/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */