Skip to content

Commit

Permalink
Moving Rational class to utility package
Browse files Browse the repository at this point in the history
  • Loading branch information
marcoeilers committed Aug 27, 2024
1 parent 54bbafb commit a2b79ae
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 48 deletions.
49 changes: 1 addition & 48 deletions src/main/scala/viper/silver/ast/utility/Simplifier.scala
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ package viper.silver.ast.utility
import viper.silver.ast.utility.Statements.EmptyStmt
import viper.silver.ast._
import viper.silver.ast.utility.rewriter._
import viper.silver.utility.Common.Rational

/**
* An implementation for simplifications on the Viper AST.
Expand Down Expand Up @@ -182,52 +183,4 @@ object Simplifier {
case _ => None
}
}

final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
require(d != 0, "Denominator of Rational must not be 0.")

private val g = n.gcd(d)
val numerator: BigInt = n / g * d.signum
val denominator: BigInt = d.abs / g

def +(that: Rational): Rational = {
val newNum = this.numerator * that.denominator + that.numerator * this.denominator
val newDen = this.denominator * that.denominator
Rational(newNum, newDen)
}

def -(that: Rational): Rational = this + (-that)

def unary_- = Rational(-numerator, denominator)

def abs = Rational(numerator.abs, denominator)

def signum = Rational(numerator.signum, 1)

def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)

def /(that: Rational): Rational = this * that.inverse

def inverse = Rational(denominator, numerator)

def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum

override def equals(obj: Any) = obj match {
case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
case _ => false
}

override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)

override lazy val toString = s"$numerator/$denominator"
}

object Rational extends ((BigInt, BigInt) => Rational) {
val zero = Rational(0, 1)
val one = Rational(1, 1)

def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)

def unapply(r: Rational) = Some(r.numerator, r.denominator)
}
}
48 changes: 48 additions & 0 deletions src/main/scala/viper/silver/utility/Common.scala
Original file line number Diff line number Diff line change
Expand Up @@ -76,4 +76,52 @@ object Common {

new JPrintWriter(new JBufferedWriter(new JFileWriter(file, append)), autoFlush)
}

final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
require(d != 0, "Denominator of Rational must not be 0.")

private val g = n.gcd(d)
val numerator: BigInt = n / g * d.signum
val denominator: BigInt = d.abs / g

def +(that: Rational): Rational = {
val newNum = this.numerator * that.denominator + that.numerator * this.denominator
val newDen = this.denominator * that.denominator
Rational(newNum, newDen)
}

def -(that: Rational): Rational = this + (-that)

def unary_- = Rational(-numerator, denominator)

def abs = Rational(numerator.abs, denominator)

def signum = Rational(numerator.signum, 1)

def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)

def /(that: Rational): Rational = this * that.inverse

def inverse = Rational(denominator, numerator)

def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum

override def equals(obj: Any) = obj match {
case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
case _ => false
}

override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)

override lazy val toString = s"$numerator/$denominator"
}

object Rational extends ((BigInt, BigInt) => Rational) {
val zero = Rational(0, 1)
val one = Rational(1, 1)

def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)

def unapply(r: Rational) = Some(r.numerator, r.denominator)
}
}

0 comments on commit a2b79ae

Please sign in to comment.