From eda946cc6795e64f6ed850b21a16e935dcc2e500 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Fri, 24 Apr 2015 17:43:06 +0200
Subject: [PATCH] replace case IntegerType in size func by abs(expr), does not
work on mytests/Termination2.scala
---
mytests/Termination2.scala | 14 ++++++++++++++
.../scala/leon/termination/StructuralSize.scala | 13 +++++++++++++
2 files changed, 27 insertions(+)
create mode 100644 mytests/Termination2.scala
diff --git a/mytests/Termination2.scala b/mytests/Termination2.scala
new file mode 100644
index 000000000..4ef5ba8b0
--- /dev/null
+++ b/mytests/Termination2.scala
@@ -0,0 +1,14 @@
+
+object Test {
+ def f(x: BigInt): BigInt = {
+ if (x == 0) {
+ 0
+ } else if (x > 0) {
+ f(x-1)+2
+ } else if (x < 0) {
+ f(x+1)-2
+ } else {
+ 33
+ }
+ } ensuring (_ == x*2)
+}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 32b35b18f..6afe9d72a 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -15,6 +15,16 @@ import scala.collection.mutable.{Map => MutableMap}
trait StructuralSize {
private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
+
+ private val absFun = new FunDef(
+ FreshIdentifier("abs", alwaysShowUniqueID = true),
+ Seq(), // no type params
+ IntegerType, // returns BigInt
+ Seq(ValDef(FreshIdentifier("x", IntegerType, alwaysShowUniqueID = true))),
+ DefType.MethodDef
+ )
+
+ private val typedAbsFun = TypedFunDef(absFun, Seq(IntegerType))
def size(expr: Expr) : Expr = {
def funDef(ct: ClassType, cases: ClassType => Seq[MatchCase]): FunDef = {
@@ -66,6 +76,9 @@ trait StructuralSize {
case TupleType(argTypes) => argTypes.zipWithIndex.map({
case (_, index) => size(tupleSelect(expr, index + 1, true))
}).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
+ case IntegerType =>
+ println("here")
+ FunctionInvocation(typedAbsFun, Seq(expr))
case _ => InfiniteIntegerLiteral(0)
}
}
--
GitLab