* improving arithmetic getEqualityStatus

* some sharing improvements based on model

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index c004a681f..a46dde1cf 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -89,6 +89,18 @@ public:
     return *(this) + (a * negOne);
   }
 
+  DeltaRational operator/(const Rational& a) const{
+    CVC4::Rational tmpC = c/a;
+    CVC4::Rational tmpK = k/a;
+    return DeltaRational(tmpC, tmpK);
+  }
+
+  DeltaRational operator/(const Integer& a) const{
+    CVC4::Rational tmpC = c/a;
+    CVC4::Rational tmpK = k/a;
+    return DeltaRational(tmpC, tmpK);
+  }
+
   bool operator==(const DeltaRational& other) const{
     return (k == other.k) && (c == other.c);
   }