From 369440efdcf26321f588b6b485e40f7c609f12da Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 21 Nov 2012 18:36:29 +0000 Subject: [PATCH] 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. --- src/theory/arith/delta_rational.cpp | 77 ++++++++++++++++++++++++- src/theory/arith/delta_rational.h | 87 +++++++++++++++++++++++++++-- 2 files changed, 156 insertions(+), 8 deletions(-) diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 9305b1efd..a334e2c3d 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -19,9 +19,10 @@ #include "theory/arith/delta_rational.h" using namespace std; -using namespace CVC4; -std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){ +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const DeltaRational& dq){ return os << "(" << dq.getNoninfinitesimalPart() << "," << dq.getInfinitesimalPart() << ")"; } @@ -31,3 +32,75 @@ std::string DeltaRational::toString() const { return "(" + getNoninfinitesimalPart().toString() + "," + getInfinitesimalPart().toString() + ")"; } + +void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b){ + Assert(res.sgn() > 0); + + int cmp = a.cmp(b); + if(cmp != 0){ + bool aLeqB = cmp < 0; + + const DeltaRational& min = aLeqB ? a : b; + const DeltaRational& max = aLeqB ? b : a; + + const Rational& pinf = min.getInfinitesimalPart(); + const Rational& cinf = max.getInfinitesimalPart(); + + const Rational& pmaj = min.getNoninfinitesimalPart(); + const Rational& cmaj = max.getNoninfinitesimalPart(); + + if(pmaj == cmaj){ + Assert(pinf < cinf); + // any value of delta preserves the order + }else if(pinf == cinf){ + Assert(pmaj < cmaj); + // any value of delta preserves the order + }else{ + Assert(pinf != cinf && pmaj != cmaj); + Rational denDiffAbs = (cinf - pinf).abs(); + + Rational numDiff = (cmaj - pmaj); + Assert(numDiff.sgn() >= 0); + Assert(denDiffAbs.sgn() > 0); + Rational ratio = numDiff / denDiffAbs; + Assert(ratio.sgn() > 0); + + if(ratio < res){ + res = ratio; + } + } + } +} + + +DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){ + std::stringstream ss; + ss << "Operation [" << op << "] between DeltaRational values "; + ss << a << " and " << b << " is not a DeltaRational."; + setMessage(ss.str()); +} + +DeltaRationalException::~DeltaRationalException() throw () { } + + +Integer DeltaRational::floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){ + if(isIntegral() && y.isIntegral()){ + Integer ti = floor(); + Integer yi = y.floor(); + return ti.floorDivideQuotient(yi); + }else{ + throw DeltaRationalException("floorDivideQuotient", *this, y); + } +} + +Integer DeltaRational::floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){ + if(isIntegral() && y.isIntegral()){ + Integer ti = floor(); + Integer yi = y.floor(); + return ti.floorDivideRemainder(yi); + }else{ + throw DeltaRationalException("floorDivideRemainder", *this, y); + } +} + +}/* CVC4 namespace */ 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 +#include +#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 */ -- 2.30.2