From 1cedfcf7d263a989702f049c606aaab40aafcbcf Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Mar 2016 10:47:22 +0100
Subject: [PATCH] Synthesis should be a UnitPhase
---
src/main/scala/leon/LeonPhase.scala | 2 +-
src/main/scala/leon/synthesis/SynthesisPhase.scala | 5 ++---
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 92ab88473..db04f677e 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -28,7 +28,7 @@ abstract class UnitPhase[T] extends LeonPhase[T, T] {
def apply(ctx: LeonContext, p: T): Unit
override def run(ctx: LeonContext, p: T) = {
- ctx.reporter.debug("Running unit phase phase: " + name)(utils.DebugSectionLeon)
+ ctx.reporter.debug("Running unit phase: " + name)(utils.DebugSectionLeon)
apply(ctx, p)
(ctx, p)
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 422d90be2..ad309905e 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -10,7 +10,7 @@ import purescala.Definitions.{Program, FunDef}
import leon.utils._
import graph._
-object SynthesisPhase extends TransformationPhase {
+object SynthesisPhase extends UnitPhase[Program] {
val name = "Synthesis"
val description = "Partial synthesis of \"choose\" constructs. Also used by repair during the synthesis stage."
@@ -65,7 +65,7 @@ object SynthesisPhase extends TransformationPhase {
)
}
- def apply(ctx: LeonContext, program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program): Unit = {
val options = processOptions(ctx)
val chooses = SourceInfo.extractFromProgram(ctx, program)
@@ -106,7 +106,6 @@ object SynthesisPhase extends TransformationPhase {
ctx.reporter.info("")
}
- program
}
}
--
GitLab