diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-14 21:07:00 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-14 21:07:00 -0500 |
commit | cb3c0621a7d54325c8863d315ea7569fa70bdc10 (patch) | |
tree | 610813d2c679d3dac3085c13817978e8c6dc533e /src | |
parent | 282f757fd1c9a5277e9d7053e9a20d792c8b81b0 (diff) | |
parent | 7d0625db683e06cc55b8ffa2f56a8b26e6bb7427 (diff) |
Merging in patch from branch '1.0.x'.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 72 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 79 |
6 files changed, 150 insertions, 23 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a367b8599..823b61df5 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -338,7 +338,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ bool isDiv = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); - Integer result = isDiv ? ni.floorDivideQuotient(di) : ni.floorDivideRemainder(di); + Integer result = isDiv ? ni.euclidianDivideQuotient(di) : ni.euclidianDivideRemainder(di); Node resultNode = mkRationalNode(Rational(result)); return RewriteResponse(REWRITE_DONE, resultNode); diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index a334e2c3d..39b99d625 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -83,23 +83,23 @@ DeltaRationalException::DeltaRationalException(const char* op, const DeltaRation DeltaRationalException::~DeltaRationalException() throw () { } -Integer DeltaRational::floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){ +Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){ if(isIntegral() && y.isIntegral()){ Integer ti = floor(); Integer yi = y.floor(); - return ti.floorDivideQuotient(yi); + return ti.euclidianDivideQuotient(yi); }else{ - throw DeltaRationalException("floorDivideQuotient", *this, y); + throw DeltaRationalException("euclidianDivideQuotient", *this, y); } } -Integer DeltaRational::floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){ +Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){ if(isIntegral() && y.isIntegral()){ Integer ti = floor(); Integer yi = y.floor(); - return ti.floorDivideRemainder(yi); + return ti.euclidianDivideRemainder(yi); }else{ - throw DeltaRationalException("floorDivideRemainder", *this, y); + throw DeltaRationalException("euclidianDivideRemainder", *this, y); } } diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index dc4202f36..19a16d558 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -236,10 +236,10 @@ public: } /** Only well defined if both this and y are integral. */ - Integer floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException); + Integer euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException); /** Only well defined if both this and y are integral. */ - Integer floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException); + Integer euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException); std::string toString() const; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f036e20fd..7f7ee3bb1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2060,10 +2060,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalExce if(n.getKind() == kind::DIVISION_TOTAL){ res = numer / denom; }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){ - res = Rational(numer.floorDivideQuotient(denom)); + res = Rational(numer.euclidianDivideQuotient(denom)); }else{ Assert(n.getKind() == kind::INTS_MODULUS_TOTAL); - res = Rational(numer.floorDivideRemainder(denom)); + res = Rational(numer.euclidianDivideRemainder(denom)); } if(isSetup(n)){ ArithVar var = d_arithvarNodeMap.asArithVar(n); diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 211c40741..b5452ae00 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -275,6 +275,61 @@ public: } /** + * Computes a quoitent and remainder according to Boute's Euclidean definition. + * euclidianDivideQuotient, euclidianDivideRemainder. + * + * Boute, Raymond T. (April 1992). + * The Euclidean definition of the functions div and mod. + * ACM Transactions on Programming Languages and Systems (TOPLAS) + * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862. + */ + static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + // compute the floor and then fix the value up if needed. + floorQR(q,r,x,y); + + if(r.strictlyNegative()){ + // if r < 0 + // abs(r) < abs(y) + // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y) + // n = y * q + r + // n = y * q - abs(y) + r + abs(y) + if(r.sgn() >= 0){ + // y = abs(y) + // n = y * q - y + r + y + // n = y * (q-1) + (r+y) + q -= 1; + r += y; + }else{ + // y = -abs(y) + // n = y * q + y + r - y + // n = y * (q+1) + (r-y) + q += 1; + r -= y; + } + } + } + + /** + * Returns the quoitent according to Boute's Euclidean definition. + * See the documentation for euclidianQR. + */ + Integer euclidianDivideQuotient(const Integer& y) const { + Integer q,r; + euclidianQR(q,r, *this, y); + return q; + } + + /** + * Returns the remainfing according to Boute's Euclidean definition. + * See the documentation for euclidianQR. + */ + Integer euclidianDivideRemainder(const Integer& y) const { + Integer q,r; + euclidianQR(q,r, *this, y); + return r; + } + + /** * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { @@ -371,15 +426,24 @@ public: return cln::cl_I_to_int(sgn); } - bool isZero() const { - return cln::zerop(d_value); + + inline bool strictlyPositive() const { + return sgn() > 0; + } + + inline bool strictlyNegative() const { + return sgn() < 0; + } + + inline bool isZero() const { + return sgn() == 0; } - bool isOne() const { + inline bool isOne() const { return d_value == 1; } - bool isNegativeOne() const { + inline bool isNegativeOne() const { return d_value == -1; } diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index bebd0e1e2..176604268 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -180,16 +180,16 @@ public: mpz_class res = d_value; for (unsigned i = size; i < size + amount; ++i) { - mpz_setbit(res.get_mpz_t(), i); + mpz_setbit(res.get_mpz_t(), i); } - - return Integer(res); + + return Integer(res); } - + uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); } - + /** See GMP Documentation. */ Integer extractBitRange(uint32_t bitCount, uint32_t low) const { // bitCount = high-low+1 @@ -246,6 +246,61 @@ public: } /** + * Computes a quoitent and remainder according to Boute's Euclidean definition. + * euclidianDivideQuotient, euclidianDivideRemainder. + * + * Boute, Raymond T. (April 1992). + * The Euclidean definition of the functions div and mod. + * ACM Transactions on Programming Languages and Systems (TOPLAS) + * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862. + */ + static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + // compute the floor and then fix the value up if needed. + floorQR(q,r,x,y); + + if(r.strictlyNegative()){ + // if r < 0 + // abs(r) < abs(y) + // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y) + // n = y * q + r + // n = y * q - abs(y) + r + abs(y) + if(r.sgn() >= 0){ + // y = abs(y) + // n = y * q - y + r + y + // n = y * (q-1) + (r+y) + q -= 1; + r += y; + }else{ + // y = -abs(y) + // n = y * q + y + r - y + // n = y * (q+1) + (r-y) + q += 1; + r -= y; + } + } + } + /** + * Returns the quoitent according to Boute's Euclidean definition. + * See the documentation for euclidianQR. + */ + Integer euclidianDivideQuotient(const Integer& y) const { + Integer q,r; + euclidianQR(q,r, *this, y); + return q; + } + + /** + * Returns the remainfing according to Boute's Euclidean definition. + * See the documentation for euclidianQR. + */ + Integer euclidianDivideRemainder(const Integer& y) const { + Integer q,r; + euclidianQR(q,r, *this, y); + return r; + } + + + /** * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { @@ -259,7 +314,7 @@ public: * Returns y mod 2^exp */ Integer modByPow2(uint32_t exp) const { - mpz_class res; + mpz_class res; mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(res); } @@ -273,12 +328,20 @@ public: return Integer(res); } - + int sgn() const { return mpz_sgn(d_value.get_mpz_t()); } - bool isZero() const { + inline bool strictlyPositive() const { + return sgn() > 0; + } + + inline bool strictlyNegative() const { + return sgn() < 0; + } + + inline bool isZero() const { return sgn() == 0; } |