1 files changed, 22 insertions, 23 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index ce0a2cffd..e2b769b18 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -26,7 +26,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class DeltaRational;
 
@@ -46,22 +46,20 @@ class DeltaRationalException : public Exception {
  */
 class DeltaRational {
 private:
-  CVC4::Rational c;
-  CVC4::Rational k;
+ CVC5::Rational c;
+ CVC5::Rational k;
 
 public:
   DeltaRational() : c(0,1), k(0,1) {}
-  DeltaRational(const CVC4::Rational& base) : c(base), k(0,1) {}
-  DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) :
-    c(base), k(coeff) {}
-
-  const CVC4::Rational& getInfinitesimalPart() const {
-    return k;
+  DeltaRational(const CVC5::Rational& base) : c(base), k(0, 1) {}
+  DeltaRational(const CVC5::Rational& base, const CVC5::Rational& coeff)
+      : c(base), k(coeff)
+  {
   }
 
-  const CVC4::Rational& getNoninfinitesimalPart() const {
-    return c;
-  }
+  const CVC5::Rational& getInfinitesimalPart() const { return k; }
+
+  const CVC5::Rational& getNoninfinitesimalPart() const { return c; }
 
   int sgn() const {
     int s = getNoninfinitesimalPart().sgn();
@@ -99,14 +97,14 @@ public:
   }
 
   DeltaRational operator+(const DeltaRational& other) const{
-    CVC4::Rational tmpC = c+other.c;
-    CVC4::Rational tmpK = k+other.k;
+    CVC5::Rational tmpC = c + other.c;
+    CVC5::Rational tmpK = k + other.k;
     return DeltaRational(tmpC, tmpK);
   }
 
   DeltaRational operator*(const Rational& a) const{
-    CVC4::Rational tmpC = a*c;
-    CVC4::Rational tmpK = a*k;
+    CVC5::Rational tmpC = a * c;
+    CVC5::Rational tmpK = a * k;
     return DeltaRational(tmpC, tmpK);
   }
 
@@ -129,7 +127,7 @@ public:
 
 
   DeltaRational operator-(const DeltaRational& a) const{
-    CVC4::Rational negOne(CVC4::Integer(-1));
+    CVC5::Rational negOne(CVC5::Integer(-1));
     return *(this) + (a * negOne);
   }
 
@@ -138,14 +136,14 @@ public:
   }
 
   DeltaRational operator/(const Rational& a) const{
-    CVC4::Rational tmpC = c/a;
-    CVC4::Rational tmpK = k/a;
+    CVC5::Rational tmpC = c / a;
+    CVC5::Rational tmpK = k / a;
     return DeltaRational(tmpC, tmpK);
   }
 
   DeltaRational operator/(const Integer& a) const{
-    CVC4::Rational tmpC = c/a;
-    CVC4::Rational tmpK = k/a;
+    CVC5::Rational tmpC = c / a;
+    CVC5::Rational tmpK = k / a;
     return DeltaRational(tmpC, tmpK);
   }
 
@@ -206,7 +204,8 @@ public:
     return *(this);
   }
 
-  DeltaRational& operator*=(const CVC4::Rational& a){
+  DeltaRational& operator*=(const CVC5::Rational& a)
+  {
     c *=  a;
     k *=  a;
 
@@ -300,4 +299,4 @@ public:
 
 std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
 
-}/* CVC4 namespace */
+}  // namespace CVC5