From 396625e0f9d89b05453f3015daa54fd86dfc26e5 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 17 Jul 2015 15:41:23 +0200
Subject: [PATCH] extensive testing of real evaluators
---
.../leon/evaluators/RecursiveEvaluator.scala | 4 +
.../leon/frontends/scalac/ASTExtractors.scala | 9 ++
.../frontends/scalac/CodeExtraction.scala | 1 +
.../evaluators/DefaultEvaluatorSuite.scala | 84 +++++++++++++++++++
.../leon/test/evaluators/EvaluatorSuite.scala | 6 +-
5 files changed, 101 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 7b06e97c3..95a0c0195 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 7765eacd0..ec3c9738a 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 8ede9e830..a95b760ca 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 ae9bba636..86113df87 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 0c149333e..10722f1b0 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))
--
GitLab