From 22406c41f54d26580e2d472b08dbfd81431b1efb Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 10 Jul 2015 16:09:43 +0200
Subject: [PATCH] rational available in lang

---
 library/lang/Rational.scala                   | 97 +++++++++++++++++++
 .../verification/math/RationalProps.scala     | 47 +++++++++
 2 files changed, 144 insertions(+)
 create mode 100644 library/lang/Rational.scala
 create mode 100644 testcases/verification/math/RationalProps.scala

diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
new file mode 100644
index 000000000..2d609980d
--- /dev/null
+++ b/library/lang/Rational.scala
@@ -0,0 +1,97 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+@library
+case class Rational(numerator: BigInt, denominator: BigInt) {
+
+  def +(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
+  }
+
+  def -(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
+  }
+
+  def *(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.numerator, this.denominator*that.denominator)
+  }
+
+  def /(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.denominator, this.denominator*that.numerator)
+  }
+
+
+  def ~(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    this.numerator*that.denominator == that.numerator*this.denominator
+  }
+
+  def <(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else
+      this.numerator*that.denominator < that.numerator*this.denominator
+  }
+
+  def <=(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else
+      this.numerator*that.denominator <= that.numerator*this.denominator
+  }
+
+  def >(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else
+      this.numerator*that.denominator > that.numerator*this.denominator
+  }
+
+  def >=(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else
+      this.numerator*that.denominator >= that.numerator*this.denominator
+  }
+
+  def nonZero: Boolean = {
+    require(this.isRational)
+    numerator != 0
+  }
+
+  def isRational: Boolean = denominator != 0
+}
+
+object Rational {
+
+  implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)
+
+  def apply(n: BigInt): Rational = Rational(n, 1)
+}
diff --git a/testcases/verification/math/RationalProps.scala b/testcases/verification/math/RationalProps.scala
new file mode 100644
index 000000000..ed42a2318
--- /dev/null
+++ b/testcases/verification/math/RationalProps.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RationalProps {
+
+  def squarePos(r: Rational): Rational = {
+    require(r.isRational)
+    r * r
+  } ensuring(_ >= Rational(0))
+
+  def additionIsCommutative(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational)
+    p + q == q + p
+  } holds
+
+  def multiplicationIsCommutative(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational)
+    p * q == q * p
+  } holds
+
+  def lessThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p < q && q < r)
+    p < r
+  } holds
+
+  def lessEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p <= q && q <= r)
+    p <= r
+  } holds
+
+  def greaterThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p > q && q > r)
+    p > r
+  } holds
+
+  def greaterEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p >= q && q >= r)
+    p >= r
+  } holds
+
+  def distributionMult(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational)
+    (p*(q + r)) ~ (p*q + p*r)
+  } holds
+
+}
-- 
GitLab