/* * 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 . */ 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: *
``` * ONE.div(NEGATIVE_INFINITY).isNegative() = false  (no negative ZERO)
* ZERO.inverse() = POSITIVE_INFINITY
* * 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 { /** * 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 `this + other`. * @param other Rational to add. * @return Sum of `this` and `other`. */ 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 `-this`. * @return `-this` */ public Rational negate() { return Rational.valueOf(mbignum.negate(), mbigdenom); } /** * Return a new rational representing `this * other`. * @param other Rational to multiply. * @return Product of `this` and `other`. */ 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 `this * other`. * @param other big integer to multiply. * @return Product of `this` and `other`. */ 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 `this / other`. * @param other Rational to divide. * @return Quotient of `this` and `other`. */ 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 `this / other`. * @param other Rational to divide. * @return Quotient of `this` and `other`. */ 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 `this`. * @return Inverse of `this`. */ 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 `true` iff value is integral. */ public boolean isIntegral() { return mbigdenom.equals(BigInteger.ONE); } /** * Return a new rational representing the biggest integral rational not * bigger than `this`. * @return Next smaller integer of `this`. */ 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 `this`. */ 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 `this`. * @return Next bigger integer of `this`. */ 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 `this + other`. * @param other Rational to add. * @return Sum of `this` and `other`. */ 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 `this+(fac1*fac2)` * @param fac1 * @param fac2 * @return */ public Rational addmul(Rational fac1,Rational fac2) { return add(fac1.mul(fac2)); } /** * Returns `(this-s)/d` * @param s * @param d * @return */ public Rational subdiv(Rational s,Rational d) { return sub(s).div(d); } /** * Returns a new rational equal to `-this`. * @return `-this` */ public Rational negate() { return Rational.valueOf(-(long)mnum, mdenom); } /** * Return a new rational representing `this - other`. * @param other Rational to subtract. * @return Difference of `this` and `other`. */ public Rational sub(Rational other) { return add(other.negate()); } /** * Return a new rational representing `this * other`. * @param other Rational to multiply. * @return Product of `this` and `other`. */ 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 `this * other`. * @param other big integer to multiply. * @return Product of `this` and `other`. */ 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 `this / other`. * @param other Rational to divide. * @return Quotient of `this` and `other`. */ 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 `this`. * @return Inverse of `this`. */ public Rational inverse() { return valueOf(mdenom, mnum); } /** * Check whether this rational is negative. * @return `true` 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 `true` iff value is integral. */ public boolean isIntegral() { return mdenom <= 1; } /** * Return a new rational representing the biggest integral rational not * bigger than `this`. * @return Next smaller integer of `this`. */ 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 `this`. */ 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 `this`. * @return Next bigger integer of `this`. */ 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)); } }