diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-21 18:36:29 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-21 18:36:29 +0000 |
commit | 369440efdcf26321f588b6b485e40f7c609f12da (patch) | |
tree | 94932d687496f055d2da18698d8bf34de9fafd56 /src/theory/arith/delta_rational.h | |
parent | 130de2a67cb3c9d4e009d921e3a60a669aedfaff (diff) |
Adds a number of new capabilities to DeltaRational. This adds DeltaRationalException which can be called when an operation on a DeltaRational does not have well formed semantics. This allows for things like multiplying two DeltaRationals, which may or may not result in a DeltaRational.
Diffstat (limited to 'src/theory/arith/delta_rational.h')
-rw-r--r-- | src/theory/arith/delta_rational.h | 87 |
1 files changed, 81 insertions, 6 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 1723b8680..dc4202f36 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -19,15 +19,24 @@ #include "util/integer.h" #include "util/rational.h" +#include "util/exception.h" -#include <ostream> +#include <ostream> +#pragma once -#ifndef __CVC4__THEORY__ARITH__DELTA_RATIONAL_H -#define __CVC4__THEORY__ARITH__DELTA_RATIONAL_H namespace CVC4 { +class DeltaRational; + +class DeltaRationalException : public Exception { +public: + DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (); + virtual ~DeltaRationalException() throw (); +}; + + /** * A DeltaRational is a pair of rationals (c,k) that represent the number * c + kd @@ -65,6 +74,19 @@ public: return getInfinitesimalPart().sgn(); } + bool infinitesimalIsZero() const { + return getInfinitesimalPart().isZero(); + } + + bool noninfinitesimalIsZero() const { + return getNoninfinitesimalPart().isZero(); + } + + bool isZero() const { + return noninfinitesimalIsZero() && infinitesimalIsZero(); + } + + int cmp(const DeltaRational& other) const{ int cmp = c.cmp(other.c); if(cmp == 0){ @@ -86,6 +108,23 @@ public: return DeltaRational(tmpC, tmpK); } + + /** + * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta) + * This can be done whenever this->k or a.k is 0. + * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown. + */ + DeltaRational operator*(const DeltaRational& a) const throw(DeltaRationalException){ + if(infinitesimalIsZero()){ + return a * (this->getNoninfinitesimalPart()); + }else if(a.infinitesimalIsZero()){ + return (*this) * a.getNoninfinitesimalPart(); + }else{ + throw DeltaRationalException("operator*", *this, a); + } + } + + DeltaRational operator-(const DeltaRational& a) const{ CVC4::Rational negOne(CVC4::Integer(-1)); return *(this) + (a * negOne); @@ -107,10 +146,29 @@ public: return DeltaRational(tmpC, tmpK); } + /** + * Divides (*this) / (a.c + a.k * delta) + * This can be done when a.k is 0 and a.c is non-zero. + * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown. + */ + DeltaRational operator/(const DeltaRational& a) const throw(DeltaRationalException){ + if(a.infinitesimalIsZero()){ + return (*this) / a.getNoninfinitesimalPart(); + }else{ + throw DeltaRationalException("operator/", *this, a); + } + } + + bool operator==(const DeltaRational& other) const{ return (k == other.k) && (c == other.c); } + bool operator!=(const DeltaRational& other) const{ + return !(*this == other); + } + + bool operator<=(const DeltaRational& other) const{ int cmp = c.cmp(other.c); return (cmp < 0) || ((cmp==0)&&(k <= other.k)); @@ -146,7 +204,7 @@ public: } bool isIntegral() const { - if(getInfinitesimalPart().sgn() == 0){ + if(infinitesimalIsZero()){ return getNoninfinitesimalPart().isIntegral(); }else{ return false; @@ -177,16 +235,33 @@ public: } } + /** Only well defined if both this and y are integral. */ + Integer floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException); + + /** Only well defined if both this and y are integral. */ + Integer floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException); + + std::string toString() const; Rational substituteDelta(const Rational& d) const{ return getNoninfinitesimalPart() + (d * getInfinitesimalPart()); } + /** + * Computes a sufficient upperbound to seperate two DeltaRationals. + * This value is stored in res. + * For any rational d such that + * 0 < d < res + * then + * a < b if and only if substituteDelta(a, d) < substituteDelta(b,d). + * (Similar relationships hold for for a == b and a > b.) + * Precondition: res > 0 + */ + static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b); + }; std::ostream& operator<<(std::ostream& os, const DeltaRational& n); }/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__DELTA_RATIONAL_H */ |