diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-19 21:20:54 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-19 21:20:54 +0000 |
commit | ff70395fd3dcde9f68eda1c6a8bd70e6491f7458 (patch) | |
tree | d0cf52a5e6cb98a0aa6c15ca4c4fe4d258cb626f /src/theory/arith/delta_rational.h | |
parent | 07e1a1668a27e90563f23bcf5abb5cb7fe30da86 (diff) |
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.
Diffstat (limited to 'src/theory/arith/delta_rational.h')
-rw-r--r-- | src/theory/arith/delta_rational.h | 22 |
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 */ |