Significant revision to theory/arith. The new draft has a lot of small bug fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

1 files changed, 19 insertions, 3 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 5fd4d4e07..c84a28e3d 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -3,10 +3,14 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
+#include <ostream>
+
 
 #ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
 #define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H
 
+namespace CVC4 {
+
 /**
  * A DeltaRational is a pair of rationals (c,k) that represent the number
  *   c + kd
@@ -18,11 +22,19 @@ private:
   CVC4::Rational k;
 
 public:
-  DeltaRational() : c(0), k(0) {}
-  DeltaRational(const CVC4::Rational& base) : c(base), k(0) {}
+  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& getInfintestimalPart() const {
+    return k;
+  }
+
+  const CVC4::Rational& getNoninfintestimalPart() const {
+    return c;
+  }
+
   DeltaRational operator+(const DeltaRational& other) const{
     CVC4::Rational tmpC = c+other.c;
     CVC4::Rational tmpK = k+other.k;
@@ -58,7 +70,7 @@ public:
     return !(*this <= other);
   }
 
-  DeltaRational& operator=(DeltaRational& other){
+  DeltaRational& operator=(const DeltaRational& other){
     c = other.c;
     k = other.k;
     return *(this);
@@ -79,4 +91,8 @@ public:
   }
 };
 
+std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
+
+}/* CVC4 namespace */
+
 #endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */