Rational (SMTInterpol 2.1 Public API)

java.lang.Object
- de.uni_freiburg.informatik.ultimate.logic.Rational

All Implemented Interfaces:

java.lang.Comparable<Rational>
```
public class Rational
extends java.lang.Object
implements java.lang.Comparable<Rational>
```
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
 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;
 
```
This class only uses bigintegers if either numerator or denominator does not fit into an int.
Author:

Juergen Christ, Jochen Hoenicke

Field Summary

Fields
Modifier and Type	Field and Description
`static Rational`	`MONE` The number -1.
`static Rational`	`NAN` Not a number.
`static Rational`	`NEGATIVE_INFINITY` Negative infinity.
`static Rational`	`ONE` The number 1.
`static Rational`	`POSITIVE_INFINITY` Positive infinity.
`static Rational`	`TWO` The number 2.
`static Rational`	`ZERO` The number 0.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`Rational`	`abs()` Compute the absolute of this rational.
`Rational`	`add(Rational other)` Return a new rational representing `this + other`.
`Rational`	`addmul(Rational fac1, Rational fac2)` Computes `this + (fac1*fac2)`.
`Rational`	`ceil()` Return a new rational representing the smallest integral rational not smaller than `this`.
`int`	`compareTo(Rational o)`
`java.math.BigInteger`	`denominator()` Get the denominator of this rational.
`Rational`	`div(Rational other)` Return a new rational representing `this / other`.
`boolean`	`equals(java.lang.Object o)`
`Rational`	`floor()` Return a new rational representing the biggest integral rational not bigger than `this`.
`Rational`	`frac()` Returns the fractional part of the rational, i.e. the number this.sub(this.floor()).
`static java.math.BigInteger`	`gcd(java.math.BigInteger i1, java.math.BigInteger i2)` Compute the gcd of two BigInteger.
`Rational`	`gcd(Rational other)` Compute the gcd of two rationals (this and other).
`int`	`hashCode()` Computes a hashcode.
`Rational`	`inverse()` Returns a new rational representing the inverse of `this`.
`boolean`	`isIntegral()` Check whether this rational represents an integral value.
`boolean`	`isNegative()` Check whether this rational is negative.
`boolean`	`isRational()` Check whether this rational corresponds to a (finite) rational value.
`Rational`	`mul(java.math.BigInteger other)` Return a new rational representing `this * other`.
`Rational`	`mul(Rational other)` Return a new rational representing `this * other`.
`Rational`	`negate()` Returns a new rational equal to `-this`.
`java.math.BigInteger`	`numerator()` Get the numerator of this rational.
`int`	`signum()` Return the sign of this rational.
`Rational`	`sub(Rational other)` Return a new rational representing `this - other`.
`Rational`	`subdiv(Rational s, Rational d)` Computes `(this - s) / d`.
`Term`	`toSMTLIB(de.uni_freiburg.informatik.ultimate.logic.Theory t)` Deprecated. Use `toTerm(Sort)` since this is the type-safe version
`java.lang.String`	`toString()` Get a string representation of this number.
`Term`	`toTerm(Sort sort)` Creates a constant term containing this rational.
`static Rational`	`valueOf(java.math.BigInteger bignum, java.math.BigInteger bigdenom)` Construct a rational from two bigints.
`static Rational`	`valueOf(long newnum, long newdenom)` Construct a rational from two longs.

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - POSITIVE_INFINITY
```
public static final Rational POSITIVE_INFINITY
```
    Positive infinity. Used to represent the result of 1/0.
  - NAN
```
public static final Rational NAN
```
    Not a number. Used to represent the result of 0/0.
  - NEGATIVE_INFINITY
```
public static final Rational NEGATIVE_INFINITY
```
    Negative infinity. Used to represent the result of -1/0.
  - ZERO
```
public static final Rational ZERO
```
    The number 0.
  - ONE
```
public static final Rational ONE
```
    The number 1.
  - MONE
```
public static final Rational MONE
```
    The number -1.
  - TWO
```
public static final Rational TWO
```
    The number 2.
- Method Detail
  - valueOf
```
public static Rational valueOf(java.math.BigInteger bignum,
                               java.math.BigInteger bigdenom)
```
    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 and does partial unification.
    
    Parameters:
    
    bignum - The numerator.
    
    bigdenom - The denominator.
    
    Returns:
    
    a rational representing numerator/denominator.
  - valueOf
```
public static Rational valueOf(long newnum,
                               long newdenom)
```
    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.
    
    Parameters:
    
    newnum - The numerator.
    
    newdenom - The denominator.
    
    Returns:
    
    a rational representing numerator/denominator.
  - gcd
```
public static java.math.BigInteger gcd(java.math.BigInteger i1,
                                       java.math.BigInteger i2)
```
    Compute the gcd of two BigInteger. This is the same as i1.gcd(i2), but it is more efficient for small numbers.
    
    Parameters:
    
    i1 - the first big integer.
    
    i2 - the second big integer.
    
    Returns:
    
    the gcd of i1 and i2.
  - add
```
public Rational add(Rational other)
```
    Return a new rational representing this + other.
    
    Parameters:
    
    other - Rational to add.
    
    Returns:
    
    Sum of this and other.
  - addmul
```
public Rational addmul(Rational fac1,
                       Rational fac2)
```
    Computes this + (fac1*fac2).
    
    Parameters:
    
    fac1 - one of the factors.
    
    fac2 - the other factor.
    
    Returns:
    
    the result of the computation.
  - subdiv
```
public Rational subdiv(Rational s,
                       Rational d)
```
    Computes (this - s) / d.
    
    Parameters:
    
    s - the rational to subtract.
    
    d - the divisor.
    
    Returns:
    
    the result of the computation.
  - negate
```
public Rational negate()
```
    Returns a new rational equal to -this.
    
    Returns:
    
    -this.
  - sub
```
public Rational sub(Rational other)
```
    Return a new rational representing this - other.
    
    Parameters:
    
    other - Rational to subtract.
    
    Returns:
    
    Difference of this and other.
  - mul
```
public Rational mul(Rational other)
```
    Return a new rational representing this * other.
    
    Parameters:
    
    other - Rational to multiply.
    
    Returns:
    
    Product of this and other.
  - mul
```
public Rational mul(java.math.BigInteger other)
```
    Return a new rational representing this * other.
    
    Parameters:
    
    other - big integer to multiply.
    
    Returns:
    
    Product of this and other.
  - div
```
public Rational div(Rational other)
```
    Return a new rational representing this / other.
    
    Parameters:
    
    other - Rational to divide.
    
    Returns:
    
    Quotient of this and other.
  - gcd
```
public Rational gcd(Rational other)
```
    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.
    
    Parameters:
    
    other - the second rational argument.
    
    Returns:
    
    the gcd of this and other.
  - inverse
```
public Rational inverse()
```
    Returns a new rational representing the inverse of this.
    
    Returns:
    
    Inverse of this.
  - isNegative
```
public boolean isNegative()
```
    Check whether this rational is negative.
    
    Returns:
    
    true iff this rational is negative.
  - signum
```
public int signum()
```
    Return the sign of this rational. The sign will be -1, 0, or 1 if this rational is negative, zero, or positive.
    
    Returns:
    
    The sign of this rational.
  - compareTo
```
public int compareTo(Rational o)
```
    Specified by:
    
    compareTo in interface java.lang.Comparable<Rational>
  - equals
```
public boolean equals(java.lang.Object o)
```
    Overrides:
    
    equals in class java.lang.Object
  - numerator
```
public java.math.BigInteger numerator()
```
    Get the numerator of this rational.
    
    Returns:
    
    the numerator.
  - denominator
```
public java.math.BigInteger denominator()
```
    Get the denominator of this rational.
    
    Returns:
    
    the denominator.
  - hashCode
```
public int hashCode()
```
    Computes a hashcode. The hashcode is computed as 257 * numerator + denominator if both fit into an integer and 257 * numerator().hashCode() + denominator().hashCode() if big integers are necessary.
    
    Overrides:
    
    hashCode in class java.lang.Object
    
    Returns:
    
    the hashcode.
  - toString
```
public java.lang.String toString()
```
    Get a string representation of this number. This is numerator()+ "/" + denominator() except for infinity ("inf"), nan ("nan"), or minus infinity ("-inf").
    
    Overrides:
    
    toString in class java.lang.Object
    
    Returns:
    
    the string representation.
  - isIntegral
```
public boolean isIntegral()
```
    Check whether this rational represents an integral value. Both infinity values are treated as integral.
    
    Returns:
    
    true iff value is integral.
  - floor
```
public Rational floor()
```
    Return a new rational representing the biggest integral rational not bigger than this.
    
    Returns:
    
    Next smaller integer of this.
  - frac
```
public Rational frac()
```
    Returns the fractional part of the rational, i.e. the number this.sub(this.floor()).
    
    Returns:
    
    Next smaller integer of this.
  - ceil
```
public Rational ceil()
```
    Return a new rational representing the smallest integral rational not smaller than this.
    
    Returns:
    
    Next bigger integer of this.
  - abs
```
public Rational abs()
```
    Compute the absolute of this rational.
    
    Returns:
    
    Rational that is equal to the absolute value of this rational.
  - toTerm
```
public Term toTerm(Sort sort)
```
    Creates a constant term containing this rational.
    
    Parameters:
    
    sort - the sort of the constant term that should be created.
    
    Returns:
    
    a constant term with this rational value.
    
    Throws:
    
    SMTLIBException - if term is infinite or NaN, if the sort is not numeric, or if the term is not integral and the sort is Int.
  - toSMTLIB
```
@Deprecated
public Term toSMTLIB(de.uni_freiburg.informatik.ultimate.logic.Theory t)
```
    Deprecated. Use toTerm(Sort) since this is the type-safe version
    
    Convert this rational into an SMTLIB term.
    
    Parameters:
    
    t - Theory to use during conversion.
    
    Returns:
    
    SMTLIB term corresponding to this rational.
  - isRational
```
public boolean isRational()
```
    Check whether this rational corresponds to a (finite) rational value. This function can be used to test for infinites and NaNs.
    
    Returns:
    
    true if and only if this rational is not infinite or NaN.

Class Rational

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

POSITIVE_INFINITY

NAN

NEGATIVE_INFINITY

ZERO

ONE

MONE

TWO

Method Detail

valueOf

valueOf

gcd

add

addmul

subdiv

negate

sub

mul

mul

div

gcd

inverse

isNegative

signum

compareTo

equals

numerator

denominator

hashCode

toString

isIntegral

floor

frac

ceil

abs

toTerm

toSMTLIB

isRational