From cc60855a5c3bea9f71cae1c18bb0b2022202916d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 18 Nov 2013 14:36:13 +0100
Subject: [PATCH] Duplicate programs to limit side-effects
---
src/main/scala/leon/purescala/Definitions.scala | 17 +++++++++++++++++
.../termination/ComplexTerminationChecker.scala | 3 ++-
2 files changed, 19 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 62f9ecbd1..0c65ed814 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -65,6 +65,13 @@ object Definitions {
out.write(ScalaPrinter(this))
out.close
}
+
+ def duplicate = {
+ copy(mainObject = mainObject.copy(defs = mainObject.defs.collect {
+ case fd: FunDef => fd.duplicate
+ case d => d
+ }))
+ }
}
object Program {
@@ -278,6 +285,16 @@ object Definitions {
var parent: Option[FunDef] = None
var orig: Option[FunDef] = None
+ def duplicate: FunDef = {
+ val fd = new FunDef(id, returnType, args)
+ fd.body = body
+ fd.precondition = precondition
+ fd.postcondition = postcondition
+ fd.parent = parent
+ fd.orig = orig
+ fd
+ }
+
def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index de9d00cc2..8dcd43fb2 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,8 @@ package termination
import purescala.Definitions._
import purescala.Trees._
-class ComplexTerminationChecker(context: LeonContext, program: Program) extends TerminationChecker(context, program) {
+class ComplexTerminationChecker(context: LeonContext, _program: Program) extends TerminationChecker(context, _program.duplicate) {
+
import scala.collection.mutable.{Map => MutableMap}
val name = "Complex Termination Checker"
--
GitLab