Exercise 7 - Rational.java
Rational.java
—
HTML,
21 kB (22475 bytes)
File contents
/*
* Copyright (C) 2009-2012 University of Freiburg
*
* This file is part of SMTInterpol.
*
* SMTInterpol is free software: you can redistribute it and/or modify
* it under the terms of the GNU Lesser General Public License as published
* by the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* SMTInterpol is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public License
* along with SMTInterpol. If not, see <http://www.gnu.org/licenses/>.
*/
package de.uni_freiburg.informatik.ultimate.logic;
import java.math.BigInteger;
/**
* Class that represents a rational number num/denom,
* where num and denom are BigInteger. This class also handles
* infinity and NAN.
*
* Internally, the numbers are always kept in reduced form; the
* denominator is always kept non-negative. A zero denominator
* with non-zero numerator indicates positive or negative infinity.
* The number 0/0 is used to represent NAN (not a number).
*
* Every operation that involves NAN gives NAN as result.
* The non-obvious rules for ZERO, INFINITY, and NAN are:
* <pre>
* ONE.div(NEGATIVE_INFINITY).isNegative() = false (no negative ZERO)
* ZERO.inverse() = POSITIVE_INFINITY
* POSITIVE_INFINITY.add(finite number) = POSITIVE_INFINITY.
* POSITIVE_INFINITY.add(NEGATIVE_INFINITY) = NAN
* ZERO.mul(POSITIVE_INFINITY) = ZERO.mul(NEGATIVE_INFINITY) = NAN
* number.div(ZERO) = POSITIVE_INFINITY.mul(number.signum())
* NAN.isIntegral = POSITIVE_INFINITY.isIntegral = true
* NAN.floor() = NAN;
* POSITIVE_INFINITY.floor() = POSITIVE_INFINITY;
* NAN.frac() = POSITIVE_INFINITY.frac() = ZERO;
* </pre>
*
* This class only uses bigintegers if either numerator or
* denominator does not fit into an int.
* @author Juergen Christ, Jochen Hoenicke
*/
public class Rational implements Comparable<Rational> {
/**
* The numerator if num and denom are in int range.
*/
int mnum;
/**
* The denominator if num and denom are in int range.
*/
int mdenom;
static class BigRational extends Rational {
/**
* The numerator if num or denom is outside int range.
*/
BigInteger mbignum;
/**
* The denominator if num or denom is outside int range.
*/
BigInteger mbigdenom;
/**
* Construct a rational from two bigints. The constructor
* is private and does not normalize. Use the static
* constructor valueOf instead.
* @param nom Numerator
* @param denom Denominator
*/
private BigRational(BigInteger nom,BigInteger denom) {
super(nom.signum(),1);
mbignum = nom;
mbigdenom = denom;
}
/**
* Return a new rational representing <code>this + other</code>.
* @param other Rational to add.
* @return Sum of <code>this</code> and <code>other</code>.
*/
public Rational add(Rational other) {
/* fast path */
if (other == Rational.ZERO)
return this;
BigInteger tdenom = denominator();
BigInteger odenom = other.denominator();
if (tdenom.equals(odenom)) {
/* another very simple case */
return valueOf(numerator().add(other.numerator()), tdenom);
}
BigInteger gcd = tdenom.gcd(odenom);
BigInteger tdenomgcd = tdenom.divide(gcd);
BigInteger odenomgcd = odenom.divide(gcd);
BigInteger newnum = numerator().multiply(odenomgcd)
.add(other.numerator().multiply(tdenomgcd));
BigInteger newdenom = tdenom.multiply(odenomgcd);
return valueOf(newnum, newdenom);
}
/**
* Returns a new rational equal to <code>-this</code>.
* @return <code>-this</code>
*/
public Rational negate() {
return Rational.valueOf(mbignum.negate(), mbigdenom);
}
/**
* Return a new rational representing <code>this * other</code>.
* @param other Rational to multiply.
* @return Product of <code>this</code> and <code>other</code>.
*/
public Rational mul(Rational other) {
/* fast path */
if (other == Rational.ONE)
return this;
if (other == Rational.ZERO)
return other;
if (other == Rational.MONE)
return this.negate();
BigInteger newnum = numerator().multiply(other.numerator());
BigInteger newdenom = denominator().multiply(other.denominator());
return valueOf(newnum, newdenom);
}
/**
* Return a new rational representing <code>this * other</code>.
* @param other big integer to multiply.
* @return Product of <code>this</code> and <code>other</code>.
*/
public Rational mul(BigInteger other) {
if (other.bitLength() < 2) {
/* fast path */
int oint = other.intValue();
if (oint == 1)
return this;
if (oint == -1)
return this.negate();
if (oint == 0)
return Rational.ZERO;
}
return valueOf(numerator().multiply(other), denominator());
}
/**
* Return a new rational representing <code>this / other</code>.
* @param other Rational to divide.
* @return Quotient of <code>this</code> and <code>other</code>.
*/
public Rational div(Rational other) {
if (other == Rational.ZERO)
throw new ArithmeticException("Division by ZERO");
if (other == Rational.ONE)
return this;
if (other == Rational.MONE)
return this.negate();
BigInteger denom = denominator().multiply(other.numerator());
BigInteger nom = numerator().multiply(other.denominator());
// +-inf : -c = -+inf
if (denom.equals(BigInteger.ZERO) && other.numerator().signum() == -1)
nom = nom.negate();
return valueOf(nom,denom);
}
/**
* Return a new rational representing <code>this / other</code>.
* @param other Rational to divide.
* @return Quotient of <code>this</code> and <code>other</code>.
*/
public Rational idiv(Rational other) {
BigInteger num = denominator().multiply(other.numerator());
BigInteger denom = numerator().multiply(other.denominator());
// +-inf : -c = -+inf
if (denom.equals(BigInteger.ZERO) && numerator().signum() == -1)
num = num.negate();
return valueOf(num,denom);
}
/**
* Returns a new rational representing the inverse of <code>this</code>.
* @return Inverse of <code>this</code>.
*/
public Rational inverse() {
return valueOf(mbigdenom, mbignum);
}
/**
* Compute the gcd of two rationals (this and other). The gcd
* is the rational number, such that dividing this and other with
* the gcd will yield two co-prime integers.
* @param other the second rational argument.
* @return the gcd of this and other.
*/
public Rational gcd(Rational other) {
if (other == Rational.ZERO)
return this;
BigInteger tdenom = this.denominator();
BigInteger odenom = other.denominator();
BigInteger gcddenom = tdenom.gcd(odenom);
BigInteger denom = tdenom.divide(gcddenom).multiply(odenom);
BigInteger num = numerator().gcd(other.numerator());
return Rational.valueOf(num, denom);
}
@Override
public int compareTo(Rational o) {
BigInteger valthis = numerator().multiply(o.denominator());
BigInteger valo = o.numerator().multiply(denominator());
return valthis.compareTo(valo);
}
public boolean equals(Object o) {
if (o instanceof BigRational) {
BigRational r = (BigRational) o;
// Works thanks to normalization!!!
return mbignum.equals(r.mbignum)
&& mbigdenom.equals(r.mbigdenom);
}
if (o instanceof MutableRational)
return ((MutableRational) o).equals(this);
return false;
}
public BigInteger numerator() {
return mbignum;
}
public BigInteger denominator() {
return mbigdenom;
}
public int hashCode() {
return mbignum.hashCode() * 257 + mbigdenom.hashCode();
}
public String toString() {
if (mbigdenom.equals(BigInteger.ONE))
return mbignum.toString();
return mbignum.toString() +"/" + mbigdenom.toString();
}
/**
* Check whether this rational represents an integral value. Both infinity
* values are treated as integral.
* @return <code>true</code> iff value is integral.
*/
public boolean isIntegral() {
return mbigdenom.equals(BigInteger.ONE);
}
/**
* Return a new rational representing the biggest integral rational not
* bigger than <code>this</code>.
* @return Next smaller integer of <code>this</code>.
*/
public Rational floor() {
if( denominator().equals(BigInteger.ONE) )
return this;
BigInteger div = numerator().divide(denominator());
if( numerator().signum() < 0)
div = div.subtract(BigInteger.ONE);
return Rational.valueOf(div,BigInteger.ONE);
}
/**
* Returns the fractional part of the rational, i.e. the
* number this.sub(this.floor()).
* @return Next smaller integer of <code>this</code>.
*/
public Rational frac() {
if( mbigdenom.equals(BigInteger.ONE) )
return Rational.ZERO;
BigInteger newnum = mbignum.mod(mbigdenom);
if( newnum.signum() < 0)
newnum.add(mbigdenom);
return Rational.valueOf(newnum, mbigdenom);
}
/**
* Return a new rational representing the smallest integral rational not
* smaller than <code>this</code>.
* @return Next bigger integer of <code>this</code>.
*/
public Rational ceil() {
if (denominator().equals(BigInteger.ONE))
return this;
BigInteger div = numerator().divide(denominator());
if( numerator().signum() > 0)
div = div.add(BigInteger.ONE);
return Rational.valueOf(div,BigInteger.ONE);
}
public Rational abs() {
return valueOf(mbignum.abs(), mbigdenom);
}
}
/**
* Construct a rational from two ints. The constructor
* is private and does not normalize. Use the static
* constructor valueOf instead.
* @param nom Numerator
* @param denom Denominator
*/
private Rational(int nom, int denom) {
mnum = nom;
mdenom = denom;
}
/**
* Construct a rational from two bigints. Use this method
* to create a rational number if the numerator or denominator
* may be to big to fit in an int. This method normalizes
* the rational number.
*
* @param nom Numerator
* @param denom Denominator
*/
public static Rational valueOf(BigInteger mbignum, BigInteger mbigdenom) {
int cp = mbigdenom.signum();//mbigdenom.compareTo(BigInteger.ZERO);
if( cp < 0 ) {
mbignum = mbignum.negate();
mbigdenom = mbigdenom.negate();
} else if (cp == 0) {
return valueOf(mbignum.signum(), 0);
}
if (!mbigdenom.equals(BigInteger.ONE)) {
BigInteger norm = gcd(mbignum, mbigdenom).abs();
if (!norm.equals(BigInteger.ONE)) {
mbignum = mbignum.divide(norm);
mbigdenom = mbigdenom.divide(norm);
}
}
if( mbigdenom.bitLength() < 32 && mbignum.bitLength() < 32 )
return valueOf(mbignum.intValue(), mbigdenom.intValue());
else
return new BigRational(mbignum, mbigdenom);
}
/**
* Construct a rational from two longs. Use this method
* to create a rational number. This method normalizes
* the rational number and may return a previously created
* one.
* This method does not work if called with value
* Long.MIN_VALUE.
*
* @param nom Numerator.
* @param denom Denominator.
*/
public static Rational valueOf(long newnum, long newdenom) {
if (newdenom != 1) {
long gcd2 = Math.abs(gcd(newnum, newdenom));
if (gcd2 == 0)
return NAN;
if (newdenom < 0)
gcd2 = -gcd2;
newnum /= gcd2;
newdenom /= gcd2;
}
if (newdenom == 1) {
if (newnum == 0)
return ZERO;
if (newnum == 1)
return ONE;
if (newnum == -1)
return MONE;
} else if (newdenom == 0) {
if (newnum == 1)
return POSITIVE_INFINITY;
else
return NEGATIVE_INFINITY;
}
if (Integer.MIN_VALUE <= newnum && newnum <= Integer.MAX_VALUE
&& newdenom <= Integer.MAX_VALUE)
return new Rational((int) newnum, (int) newdenom);
return new BigRational(BigInteger.valueOf(newnum),
BigInteger.valueOf(newdenom));
}
/**
* Calculates the greatest common divisor of two numbers. Expects two
* nonnegative values.
* @param a First number
* @param b Second Number
* @return Greatest common divisor
*/
static int gcd(int a,int b) {
/* This is faster for integer */
//assert(a >= 0 && b >= 0);
while (b != 0) {
int t = a % b;
a = b;
b = t;
}
return a;
}
/**
* Calculates the greatest common divisor of two numbers. Expects two
* nonnegative values.
* @param a First number
* @param b Second Number
* @return Greatest common divisor
*/
static long gcd(long a,long b) {
/* This is faster for longs on 32-bit architectures */
if (a == 0 || b == 1)
return b;
if (b == 0 || a == 1)
return a;
if (a < 0) a = -a;
if (b < 0) b = -b;
int ashift = Long.numberOfTrailingZeros(a);
int bshift = Long.numberOfTrailingZeros(b);
a >>= ashift;
b >>= bshift;
while (a != b) {
long t;
if (a < b) {
t = b - a;
b = a;
} else {
if (b == 1) {a = b;break;}
t = a - b;
}
do {
t >>= 1;
} while (((int) t & 1) == 0);
a = t;
}
return a << Math.min(ashift, bshift);
}
public static BigInteger gcd(BigInteger i1, BigInteger i2) {
if (i1.equals(BigInteger.ONE) || i2.equals(BigInteger.ONE))
return BigInteger.ONE;
int l1 = i1.bitLength();
int l2 = i2.bitLength();
if (l1 < 31 && l2 < 31)
return BigInteger.valueOf(gcd(i1.intValue(), i2.intValue()));
else if (l1 < 63 && l2 < 63)
return BigInteger.valueOf(gcd(i1.longValue(), i2.longValue()));
else
return i1.gcd(i2);
}
/**
* Return a new rational representing <code>this + other</code>.
* @param other Rational to add.
* @return Sum of <code>this</code> and <code>other</code>.
*/
public Rational add(Rational other) {
/* fast path */
if (other == Rational.ZERO)
return this;
if (this == Rational.ZERO)
return other;
if (other instanceof BigRational) {
return other.add(this);
} else {
if (mdenom == other.mdenom) {
/* handle gcd = 0 correctly
* two INFINITYs with same sign give INFINITY,
* otherwise it gives NAN.
*/
if (mdenom == 0)
return mnum == other.mnum ? this : NAN;
/* a common, very simple case, e.g. for integers */
return valueOf((long) mnum + other.mnum, mdenom);
}
/* This also handles infinity/NAN + normal correctly. */
int gcd = gcd(mdenom, other.mdenom);
long denomgcd = (long) (mdenom / gcd);
long otherdenomgcd = (long) (other.mdenom / gcd);
long newdenom = denomgcd * other.mdenom;
long newnum = otherdenomgcd * mnum + denomgcd * other.mnum;
return valueOf(newnum, newdenom);
}
}
/**
* Returns <code>this+(fac1*fac2)</code>
* @param fac1
* @param fac2
* @return
*/
public Rational addmul(Rational fac1,Rational fac2) {
return add(fac1.mul(fac2));
}
/**
* Returns <code>(this-s)/d</code>
* @param s
* @param d
* @return
*/
public Rational subdiv(Rational s,Rational d) {
return sub(s).div(d);
}
/**
* Returns a new rational equal to <code>-this</code>.
* @return <code>-this</code>
*/
public Rational negate() {
return Rational.valueOf(-(long)mnum, mdenom);
}
/**
* Return a new rational representing <code>this - other</code>.
* @param other Rational to subtract.
* @return Difference of <code>this</code> and <code>other</code>.
*/
public Rational sub(Rational other) {
return add(other.negate());
}
/**
* Return a new rational representing <code>this * other</code>.
* @param other Rational to multiply.
* @return Product of <code>this</code> and <code>other</code>.
*/
public Rational mul(Rational other) {
/* fast path */
if (other == Rational.ONE)
return this;
if (this == Rational.ONE)
return other;
if (other == Rational.MONE)
return this.negate();
if (this == Rational.MONE)
return other.negate();
if (other instanceof BigRational)
return other.mul(this);
long newnum = (long)mnum * other.mnum;
long newdenom = (long)mdenom * other.mdenom;
return valueOf(newnum, newdenom);
}
/**
* Return a new rational representing <code>this * other</code>.
* @param other big integer to multiply.
* @return Product of <code>this</code> and <code>other</code>.
*/
public Rational mul(BigInteger other) {
if (other.bitLength() < 32) {
/* fast path */
int oint = other.intValue();
if (oint == 1)
return this;
if (oint == -1)
return this.negate();
long newnum = (long)mnum * oint;
return valueOf(newnum, (long)mdenom);
}
if (this == Rational.ONE)
return valueOf(other, BigInteger.ONE);
if (this == Rational.MONE)
return valueOf(other.negate(), BigInteger.ONE);
return valueOf(numerator().multiply(other), denominator());
}
/**
* Return a new rational representing <code>this / other</code>.
* @param other Rational to divide.
* @return Quotient of <code>this</code> and <code>other</code>.
*/
public Rational div(Rational other) {
if (other == Rational.ZERO)
throw new ArithmeticException("Division by ZERO");
if (other == Rational.ONE)
return this;
if (other == Rational.MONE)
return this.negate();
if (other instanceof BigRational)
return ((BigRational)other).idiv(this);
/* fast path */
long newnum = (long)mnum * other.mdenom;
long newdenom = (long)mdenom * other.mnum;
// +-inf : -c = -+inf
if (newdenom == 0 && other.mnum < 0)
newnum = -newnum;
return valueOf(newnum, newdenom);
}
/**
* Compute the gcd of two rationals (this and other). The gcd
* is the rational number, such that dividing this and other with
* the gcd will yield two co-prime integers.
* @param other the second rational argument.
* @return the gcd of this and other.
*/
public Rational gcd(Rational other) {
if (this == Rational.ZERO)
return other;
if (other == Rational.ZERO)
return this;
if (other instanceof BigRational)
return other.gcd(this);
/* new numerator = gcd(num, other.num) */
/* new denominator = lcm(denom, other.denom) */
int gcddenom = gcd(mdenom, other.mdenom);
long denom = ((long) (mdenom / gcddenom)) * other.mdenom;
long num = gcd(mnum < 0 ? -mnum : mnum,
other.mnum < 0 ? -other.mnum : other.mnum);
return valueOf(num, denom);
}
/**
* Returns a new rational representing the inverse of <code>this</code>.
* @return Inverse of <code>this</code>.
*/
public Rational inverse() {
return valueOf(mdenom, mnum);
}
/**
* Check whether this rational is negative.
* @return <code>true</code> iff this rational is negative.
*/
public boolean isNegative() {
return mnum < 0;
}
public int signum() {
return mnum < 0 ? -1 : mnum == 0 ? 0 : 1;
}
@Override
public int compareTo(Rational o) {
if (o instanceof BigRational)
return -o.compareTo(this);
/* handle infinities and nan */
if (o.mdenom == mdenom)
return mnum < o.mnum ? -1 : mnum == o.mnum ? 0 : 1;
long valt = (long)mnum * o.mdenom;
long valo = (long)o.mnum * mdenom;
return valt < valo ? -1 : valt == valo ? 0 : 1;
}
public boolean equals(Object o) {
if (o instanceof Rational) {
if (o instanceof BigRational)
return false;
Rational r = (Rational) o;
// Works thanks to normalization!!!
return mnum == r.mnum && mdenom == r.mdenom;
}
if (o instanceof MutableRational)
return ((MutableRational) o).equals(this);
return false;
}
public BigInteger numerator() {
return BigInteger.valueOf(mnum);
}
public BigInteger denominator() {
return BigInteger.valueOf(mdenom);
}
public int hashCode() {
return mnum * 257 + mdenom;
}
public String toString() {
if (mdenom == 0)
return mnum > 0 ? "inf" : mnum == 0 ? "nan" : "-inf";
if (mdenom == 1)
return String.valueOf(mnum);
return mnum + "/" + mdenom;
}
/**
* Check whether this rational represents an integral value. Both infinity
* values are treated as integral.
* @return <code>true</code> iff value is integral.
*/
public boolean isIntegral() {
return mdenom <= 1;
}
/**
* Return a new rational representing the biggest integral rational not
* bigger than <code>this</code>.
* @return Next smaller integer of <code>this</code>.
*/
public Rational floor() {
if (mdenom <= 1)
return this;
int div = mnum / mdenom;
// Java rounds the wrong way for negative numbers.
// We know that the division is not exact due to
// normalization and mdenom != 1, so subtracting
// one fixes the result for negative numbers.
if (mnum < 0)
div--;
return valueOf(div, 1);
}
/**
* Returns the fractional part of the rational, i.e. the
* number this.sub(this.floor()).
* @return Next smaller integer of <code>this</code>.
*/
public Rational frac() {
if (mdenom <= 1)
return Rational.ZERO;
int newnum = mnum % mdenom;
// Java rounds the wrong way for negative numbers.
// We know that the division is not exact due to
// normalization and mdenom != 1, so subtracting
// one fixes the result for negative numbers.
if (newnum < 0)
newnum += mdenom;
return valueOf(newnum, mdenom);
}
/**
* Return a new rational representing the smallest integral rational not
* smaller than <code>this</code>.
* @return Next bigger integer of <code>this</code>.
*/
public Rational ceil() {
if (mdenom <= 1)
return this;
int div = mnum / mdenom;
// Java rounds the wrong way for positive numbers.
// We know that the division is not exact due to
// normalization and mdenom != 1, so adding
// one fixes the result for positive numbers.
if (mnum > 0)
div++;
return valueOf(div, 1);
}
public Rational abs() {
return valueOf(Math.abs((long) mnum), mdenom);
}
public final static Rational POSITIVE_INFINITY = new Rational(1,0);
public final static Rational NAN = new Rational(0,0);
public final static Rational NEGATIVE_INFINITY = new Rational(-1,0);
public final static Rational ZERO = new Rational(0,1);
public final static Rational ONE = new Rational(1,1);
public final static Rational MONE = new Rational(-1,1);
public static final Rational TWO = new Rational(2,1);
public Term toTerm(Sort sort) {
return sort.getTheory().constant(this, sort);
}
public Term toSMTLIB(Theory t) {
// Transform this rational to an SMTLIB term.
BigInteger num = numerator();
BigInteger denom = denominator();
assert (!denom.equals(BigInteger.ZERO));
if (denom.equals(BigInteger.ONE))
return t.numeral(num);
return t.term("/", t.numeral(num), t.numeral(denom));
}
}