diff --git a/src/main/java/leon/codegen/runtime/Real.java b/src/main/java/leon/codegen/runtime/Real.java
new file mode 100644
index 0000000000000000000000000000000000000000..9d80935eb2f189bac1464d7d134a314b04d2ae0a
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/Real.java
@@ -0,0 +1,81 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.codegen.runtime;
+
+import java.math.BigInteger;
+import java.math.BigDecimal;
+
+public final class Real {
+
+ private final BigDecimal _underlying;
+
+ public final BigDecimal underlying() {
+ return _underlying;
+ }
+
+ private Real(BigDecimal value) {
+ _underlying = value;
+ }
+
+ public Real(String value) {
+ _underlying = new BigDecimal(value);
+ }
+
+ public Real add(Real that) {
+ return new Real(_underlying.add(that.underlying()));
+ }
+
+ public Real sub(Real that) {
+ return new Real(_underlying.subtract(that.underlying()));
+ }
+
+ public Real mult(Real that) {
+ return new Real(_underlying.multiply(that.underlying()));
+ }
+
+ public Real div(Real that) {
+ return new Real(_underlying.divide(that.underlying()));
+ }
+
+ public Real neg() {
+ return new Real(_underlying.negate());
+ }
+
+
+ public boolean lessThan(Real that) {
+ return _underlying.compareTo(that.underlying()) < 0;
+ }
+
+ public boolean lessEquals(Real that) {
+ return _underlying.compareTo(that.underlying()) <= 0;
+ }
+
+ public boolean greaterThan(Real that) {
+ return _underlying.compareTo(that.underlying()) > 0;
+ }
+
+ public boolean greaterEquals(Real that) {
+ return _underlying.compareTo(that.underlying()) >= 0;
+ }
+
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof Real)) return false;
+
+ Real other = (Real)that;
+ return this.underlying().equals(other.underlying());
+ }
+
+ @Override
+ public String toString() {
+ return _underlying.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ return _underlying.hashCode();
+ }
+
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index bfe23c143f4fcac4f1ccdf67e27a8099d1bb546e..bac144ad6ceb83f1e439d31a7d6528c26c44aeba 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -67,6 +67,7 @@ trait CodeGeneration {
private[codegen] val SetClass = "leon/codegen/runtime/Set"
private[codegen] val MapClass = "leon/codegen/runtime/Map"
private[codegen] val BigIntClass = "leon/codegen/runtime/BigInt"
+ private[codegen] val RealClass = "leon/codegen/runtime/Real"
private[codegen] val CaseClassClass = "leon/codegen/runtime/CaseClass"
private[codegen] val LambdaClass = "leon/codegen/runtime/Lambda"
private[codegen] val ErrorClass = "leon/codegen/runtime/LeonCodeGenRuntimeException"
@@ -109,6 +110,9 @@ trait CodeGeneration {
case IntegerType =>
"L" + BigIntClass + ";"
+ case RealType =>
+ "L" + RealClass + ";"
+
case _ : FunctionType =>
"L" + LambdaClass + ";"
@@ -197,7 +201,7 @@ trait CodeGeneration {
case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case IntegerType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _ : FunctionType | _ : TypeParameter =>
+ case IntegerType | RealType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _ : FunctionType | _ : TypeParameter =>
ch << ARETURN
case other =>
@@ -245,6 +249,11 @@ trait CodeGeneration {
ch << Ldc(v.toString)
ch << InvokeSpecial(BigIntClass, constructorName, "(Ljava/lang/String;)V")
+ case RealLiteral(v) =>
+ ch << New(RealClass) << DUP
+ ch << Ldc(v.toString)
+ ch << InvokeSpecial(RealClass, constructorName, "(Ljava/lang/String;)V")
+
// Case classes
case CaseClass(cct, as) =>
val (ccName, ccApplySig) = leonClassToJVMInfo(cct.classDef).getOrElse {
@@ -656,6 +665,31 @@ trait CodeGeneration {
mkExpr(e, ch)
ch << InvokeVirtual(BigIntClass, "neg", s"()L$BigIntClass;")
+ case RealPlus(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeVirtual(RealClass, "add", s"(L$RealClass;)L$RealClass;")
+
+ case RealMinus(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeVirtual(RealClass, "sub", s"(L$RealClass;)L$RealClass;")
+
+ case RealTimes(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeVirtual(RealClass, "mult", s"(L$RealClass;)L$RealClass;")
+
+ case RealDivision(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeVirtual(RealClass, "div", s"(L$RealClass;)L$RealClass;")
+
+ case RealUMinus(e) =>
+ mkExpr(e, ch)
+ ch << InvokeVirtual(RealClass, "neg", s"()L$RealClass;")
+
+
//BV arithmetic
case BVPlus(l, r) =>
mkExpr(l, ch)
@@ -905,6 +939,9 @@ trait CodeGeneration {
case IntegerType =>
ch << CheckCast(BigIntClass)
+ case RealType =>
+ ch << CheckCast(RealClass)
+
case tt : TupleType =>
ch << CheckCast(TupleClass)
@@ -979,6 +1016,9 @@ trait CodeGeneration {
case IntegerType =>
ch << InvokeVirtual(BigIntClass, "lessThan", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
+ case RealType =>
+ ch << InvokeVirtual(RealClass, "lessThan", s"(L$RealClass;)Z")
+ ch << IfEq(elze) << Goto(thenn)
}
case GreaterThan(l,r) =>
@@ -990,6 +1030,9 @@ trait CodeGeneration {
case IntegerType =>
ch << InvokeVirtual(BigIntClass, "greaterThan", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
+ case RealType =>
+ ch << InvokeVirtual(RealClass, "greaterThan", s"(L$RealClass;)Z")
+ ch << IfEq(elze) << Goto(thenn)
}
case LessEquals(l,r) =>
@@ -1001,6 +1044,9 @@ trait CodeGeneration {
case IntegerType =>
ch << InvokeVirtual(BigIntClass, "lessEquals", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
+ case RealType =>
+ ch << InvokeVirtual(RealClass, "lessEquals", s"(L$RealClass;)Z")
+ ch << IfEq(elze) << Goto(thenn)
}
case GreaterEquals(l,r) =>
@@ -1012,6 +1058,9 @@ trait CodeGeneration {
case IntegerType =>
ch << InvokeVirtual(BigIntClass, "greaterEquals", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
+ case RealType =>
+ ch << InvokeVirtual(RealClass, "greaterEquals", s"(L$RealClass;)Z")
+ ch << IfEq(elze) << Goto(thenn)
}
case IfExpr(c, t, e) =>
@@ -1141,7 +1190,7 @@ trait CodeGeneration {
// Since the underlying field only has boxed types, we have to unbox them to return them
mkUnbox(lzy.returnType, ch)(NoLocals(isStatic))
ch << IRETURN
- case IntegerType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _: TypeParameter =>
+ case IntegerType | RealType | _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _: TypeParameter =>
ch << ARETURN
case other => throw CompilationException("Unsupported return type : " + other.getClass)
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index ef820f287f478863119ae1b2df38843f7a9f4a29..6f02907c5df52127a2b65ef8956fd10693a0bf12 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -191,6 +191,10 @@ class CompilationUnit(val ctx: LeonContext,
case (c: runtime.BigInt, IntegerType) =>
InfiniteIntegerLiteral(BigInt(c.underlying))
+ case (c: runtime.Real, RealType) =>
+ RealLiteral(BigDecimal(c.underlying))
+
+
case (b: java.lang.Boolean, BooleanType) =>
BooleanLiteral(b.booleanValue)
@@ -312,7 +316,7 @@ class CompilationUnit(val ctx: LeonContext,
case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case IntegerType | _: TupleType | _: SetType | _: MapType | _: AbstractClassType | _: CaseClassType | _: ArrayType | _: FunctionType | _: TypeParameter =>
+ case IntegerType | RealType | _: TupleType | _: SetType | _: MapType | _: AbstractClassType | _: CaseClassType | _: ArrayType | _: FunctionType | _: TypeParameter =>
ch << ARETURN
case other =>
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 2b2cd3df44a2707c446fd64108dbc759a1bc94d5..7b06e97c391d3309dc5fc7258db15134a1efb2c7 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -244,6 +244,18 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
}
+ case RealPlus(l,r) =>
+ (e(l), e(r)) match {
+ case (RealLiteral(i1), RealLiteral(i2)) => RealLiteral(i1 + i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
+ }
+
+ case RealMinus(l,r) =>
+ (e(l), e(r)) match {
+ case (RealLiteral(i1), RealLiteral(i2)) => RealLiteral(i1 - i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
+ }
+
case BVPlus(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
@@ -268,6 +280,13 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case re => throw EvalError(typeErrorMsg(re, Int32Type))
}
+ case RealUMinus(ex) =>
+ e(ex) match {
+ case RealLiteral(i) => RealLiteral(-i)
+ case re => throw EvalError(typeErrorMsg(re, RealType))
+ }
+
+
case BVNot(ex) =>
e(ex) match {
case IntLiteral(i) => IntLiteral(~i)
@@ -325,6 +344,20 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
+ case RealTimes(l,r) =>
+ (e(l), e(r)) match {
+ case (RealLiteral(i1), RealLiteral(i2)) => RealLiteral(i1 * i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
+ }
+
+ case RealDivision(l,r) =>
+ (e(l), e(r)) match {
+ case (RealLiteral(i1), RealLiteral(i2)) =>
+ if(i2 != 0) RealLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
+ case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
+ }
+
+
case BVAnd(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 & i2)
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
index 7286ef382207a01c049976d0706d1691c9ce6f3d..ae9bba6367b0f5bb44bab6e82ddcf09e8baaa17d 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
@@ -31,6 +31,9 @@ class DefaultEvaluatorSuite extends leon.test.LeonTestSuite {
expectSuccessful(defaultEvaluator.eval(UnitLiteral()), UnitLiteral())
expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(0)), InfiniteIntegerLiteral(0))
expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(42)), InfiniteIntegerLiteral(42))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(0)), RealLiteral(0))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(42)), RealLiteral(42))
+ expectSuccessful(defaultEvaluator.eval(RealLiteral(13.255)), RealLiteral(13.255))
}
test("eval of simple bit vector arithmetic expressions") {
@@ -184,6 +187,25 @@ class DefaultEvaluatorSuite extends leon.test.LeonTestSuite {
BooleanLiteral(false))
}
+ test("eval of simple arithmetic expressions over real") {
+ expectSuccessful(
+ defaultEvaluator.eval(RealPlus(RealLiteral(3), RealLiteral(5))),
+ RealLiteral(8))
+ expectSuccessful(
+ defaultEvaluator.eval(RealMinus(RealLiteral(7), RealLiteral(2))),
+ RealLiteral(5))
+ expectSuccessful(
+ defaultEvaluator.eval(RealUMinus(RealLiteral(7))),
+ RealLiteral(-7))
+ expectSuccessful(
+ defaultEvaluator.eval(RealTimes(RealLiteral(2), RealLiteral(3))),
+ RealLiteral(6))
+
+ expectSuccessful(
+ defaultEvaluator.eval(RealPlus(RealLiteral(2.5), RealLiteral(3.5))),
+ RealLiteral(6))
+ }
+
test("eval simple variable") {
val id = FreshIdentifier("id", Int32Type)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
index b5c623ab62252b2515de76f44c45054c8f4a4838..0c149333ecac69f2c322dcd63452761e4dda64ae 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
@@ -160,7 +160,7 @@ class EvaluatorSuite extends leon.test.LeonTestSuite {
private val T = BooleanLiteral(true)
private val F = BooleanLiteral(false)
- import purescala.Expressions.{IntLiteral => IL, InfiniteIntegerLiteral => BIL}
+ import purescala.Expressions.{IntLiteral => IL, InfiniteIntegerLiteral => BIL, RealLiteral => RL}
test("Arithmetic") {
val p = """|object Program {
@@ -251,6 +251,39 @@ class EvaluatorSuite extends leon.test.LeonTestSuite {
}
}
+ test("Real Arithmetic") {
+ val p = """|import leon.lang._
+ |object Program {
+ | def plus(x : Real, y : Real) : Real = x + y
+ | def max(x : Real, y : Real) : Real = if(x >= y) x else y
+ | def square(i : Real) : Real = { val j = i; j * i }
+ | def abs(i : Real) : Real = if(i < Real(0)) -i else i
+ | def intSqrt(n : Real) : Real = intSqrt0(abs(n), Real(0))
+ | def intSqrt0(n : Real, c : Real) : Real = {
+ | val s = square(c+Real(1))
+ | if(s > n) c else intSqrt0(n, c+Real(1))
+ | }
+ | def div(x : Real, y : Real) : Real = (x / y)
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+ val evaluators = prepareEvaluators
+
+ for(e <- evaluators) {
+ // Some simple math.
+ checkComp(e, mkCall("plus", RL(60), UMinus(RL(18))), RL(42))
+ checkComp(e, mkCall("max", RL(4), RL(42)), RL(42))
+ checkComp(e, mkCall("max", RL(42), UMinus(RL(42))), RL(42))
+ checkComp(e, mkCall("intSqrt", UMinus(RL(1800))), RL(42))
+ checkComp(e, mkCall("div", RL(7), RL(7)), RL(1))
+ checkComp(e, mkCall("div", RL(5), RL(2)), RL(2.5))
+
+ // Things that should crash.
+ checkError(e, mkCall("div", RL(42), RL(0)))
+ }
+ }
+
test("Booleans") {
val p = """|object Program {
|def and1(x : Boolean, y : Boolean) : Boolean = x && y