FCSimplex branch merge

1 files changed, 27 insertions, 1 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index e97bde555..7945b44c3 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -160,6 +160,14 @@ public:
   }
 
 
+  DeltaRational abs() const {
+    if(sgn() >= 0){
+      return *this;
+    }else{
+      return (*this) * Rational(-1);
+    }
+  }
+
   bool operator==(const DeltaRational& other) const{
     return (k == other.k) && (c == other.c);
   }
@@ -196,13 +204,20 @@ public:
     return *(this);
   }
 
-  DeltaRational& operator+=(DeltaRational& other){
+  DeltaRational& operator+=(const DeltaRational& other){
     c += other.c;
     k += other.k;
 
     return *(this);
   }
 
+  DeltaRational& operator/=(const Rational& a){
+    Assert(!a.isZero());
+    c /= a;
+    k /= a;
+    return *(this);
+  }
+
   bool isIntegral() const {
     if(infinitesimalIsZero()){
       return getNoninfinitesimalPart().isIntegral();
@@ -260,6 +275,17 @@ public:
    */
   static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b);
 
+  uint32_t complexity() const {
+    return c.complexity() + k.complexity();
+  }
+
+  double approx(double deltaSub) const {
+    double maj = getNoninfinitesimalPart().getDouble();
+    double min = deltaSub * (getInfinitesimalPart().getDouble());
+    return maj + min;
+  }
+
+
 };
 
 std::ostream& operator<<(std::ostream& os, const DeltaRational& n);