diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 7b06e97c391d3309dc5fc7258db15134a1efb2c7..95a0c0195ecc96bd8e1204228fe2442f7be6bfe4 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -398,6 +398,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (RealLiteral(r1), RealLiteral(r2)) => BooleanLiteral(r1 < r2)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -406,6 +407,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (RealLiteral(r1), RealLiteral(r2)) => BooleanLiteral(r1 > r2)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -414,6 +416,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (RealLiteral(r1), RealLiteral(r2)) => BooleanLiteral(r1 <= r2)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -422,6 +425,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (RealLiteral(r1), RealLiteral(r2)) => BooleanLiteral(r1 >= r2)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 7765eacd0c9658ed0421a0f0e4930cdca281006b..ec3c9738a9cacab212d8cab6054bcad88c84afe5 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -106,6 +106,8 @@ trait ASTExtractors {
}
def hasBigIntType(t : Tree) = isBigIntSym(t.tpe.typeSymbol)
+
+ def hasRealType(t : Tree) = isRealSym(t.tpe.typeSymbol)
object ExtractorHelpers {
@@ -849,6 +851,13 @@ trait ASTExtractors {
}
}
+ object ExRealUMinus {
+ def unapply(tree: Select): Option[Tree] = tree match {
+ case Select(t, n) if n == nme.UNARY_- && hasRealType(t) => Some(t)
+ case _ => None
+ }
+ }
+
object ExBVUMinus {
def unapply(tree: Select): Option[Tree] = tree match {
case Select(t, n) if n == nme.UNARY_- && hasIntType(t) => Some(t)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 8ede9e830080e8faf167f93a26dd90b287800749..a95b760ca1384d3815fd567b999ed1750ffdd4fc 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1330,6 +1330,7 @@ trait CodeExtraction extends ASTExtractors {
case ExNot(e) => Not(extractTree(e))
case ExUMinus(e) => UMinus(extractTree(e))
+ case ExRealUMinus(e) => RealUMinus(extractTree(e))
case ExBVUMinus(e) => BVUMinus(extractTree(e))
case ExBVNot(e) => BVNot(extractTree(e))
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
index ae9bba6367b0f5bb44bab6e82ddcf09e8baaa17d..86113df87beb774acd56f6c10b01eef48210560c 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorSuite.scala
@@ -124,6 +124,49 @@ class DefaultEvaluatorSuite extends leon.test.LeonTestSuite {
InfiniteIntegerLiteral(1))
}
+ test("eval of simple arithmetic comparisons over integers") {
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(InfiniteIntegerLiteral(4), InfiniteIntegerLiteral(7))), BooleanLiteral(true)
+ )
+ }
+
+
test("Eval of division and remainder semantics for bit vectors") {
expectSuccessful(
defaultEvaluator.eval(BVDivision(IntLiteral(10), IntLiteral(3))),
@@ -206,6 +249,47 @@ class DefaultEvaluatorSuite extends leon.test.LeonTestSuite {
RealLiteral(6))
}
+ test("eval of simple arithmetic comparisons over real") {
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(7), RealLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(7), RealLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterEquals(RealLiteral(4), RealLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(7), RealLiteral(4))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(7), RealLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(GreaterThan(RealLiteral(4), RealLiteral(7))), BooleanLiteral(false)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(7), RealLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(7), RealLiteral(7))), BooleanLiteral(true)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessEquals(RealLiteral(4), RealLiteral(7))), BooleanLiteral(true)
+ )
+
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(7), RealLiteral(4))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(7), RealLiteral(7))), BooleanLiteral(false)
+ )
+ expectSuccessful(
+ defaultEvaluator.eval(LessThan(RealLiteral(4), RealLiteral(7))), BooleanLiteral(true)
+ )
+ }
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 0c149333ecac69f2c322dcd63452761e4dda64ae..10722f1b026bc9c11527f1e5f55c7c99d76a00d2 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
@@ -272,10 +272,10 @@ class EvaluatorSuite extends leon.test.LeonTestSuite {
for(e <- evaluators) {
// Some simple math.
- checkComp(e, mkCall("plus", RL(60), UMinus(RL(18))), RL(42))
+ checkComp(e, mkCall("plus", RL(60), RealUMinus(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("max", RL(42), RealUMinus(RL(42))), RL(42))
+ checkComp(e, mkCall("intSqrt", RealUMinus(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))