From 5992df3610e3b4f38d2f175bcd4263631553468b Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Wed, 29 Apr 2015 17:36:23 +0200
Subject: [PATCH] implement body of abs function --> Termination2 works
---
.../leon/termination/RelationProcessor.scala | 3 ++-
.../leon/termination/StructuralSize.scala | 20 +++++++++++++------
2 files changed, 16 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index d4d1aad73..df39e0ad7 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -24,7 +24,8 @@ class RelationProcessor(
reporter.debug("- Strengthening applications")
checker.strengthenApplications(problem.funSet)(this)
- val formulas = problem.funDefs.map({ funDef =>
+ val formulas: Set[(FunDef, Set[(FunDef, (Expr, Expr))])] =
+ problem.funDefs.map({ funDef =>
funDef -> checker.getRelations(funDef).collect({
case Relation(_, path, FunctionInvocation(tfd, args), _) if problem.funSet(tfd.fd) =>
val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 6afe9d72a..693f336a5 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -16,16 +16,25 @@ trait StructuralSize {
private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
- private val absFun = new FunDef(
+ // function abs(x: BigInt): BigInt = if (x >= 0) x else -x
+ val typedAbsFun = makeAbsFun
+
+ def makeAbsFun: TypedFunDef = {
+ val x = FreshIdentifier("x", IntegerType, alwaysShowUniqueID = true)
+ val absFun = new FunDef(
FreshIdentifier("abs", alwaysShowUniqueID = true),
Seq(), // no type params
IntegerType, // returns BigInt
- Seq(ValDef(FreshIdentifier("x", IntegerType, alwaysShowUniqueID = true))),
+ Seq(ValDef(x)),
DefType.MethodDef
- )
+ )
+ absFun.body = Some(IfExpr(
+ GreaterEquals(Variable(x), InfiniteIntegerLiteral(0)),
+ Variable(x),
+ Minus(InfiniteIntegerLiteral(0), Variable(x))))
+ TypedFunDef(absFun, Seq()) // Seq() because no generic type params
+ }
- private val typedAbsFun = TypedFunDef(absFun, Seq(IntegerType))
-
def size(expr: Expr) : Expr = {
def funDef(ct: ClassType, cases: ClassType => Seq[MatchCase]): FunDef = {
// we want to reuse generic size functions for sub-types
@@ -77,7 +86,6 @@ trait StructuralSize {
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