From 13af0f467332c3bbdca611273e87971ad1aaa990 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 24 Oct 2012 18:20:43 +0200
Subject: [PATCH] SynthesisPhase is now an object
---
src/main/scala/leon/plugin/AnalysisComponent.scala | 5 +++--
src/main/scala/leon/plugin/LeonContext.scala | 3 ++-
src/main/scala/leon/synthesis/SynthesisPhase.scala | 9 ++++++---
3 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index d6fbc999a..2d2ea4143 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -52,7 +52,7 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
,
if (Settings.synthesis)
List(
- new SynthesisPhase(leonReporter)
+ SynthesisPhase
)
else
Nil
@@ -71,7 +71,8 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
//global ref to freshName creator
fresh = unit.fresh
- var ac = LeonContext(program = extractCode(unit))
+ var ac = LeonContext(program = extractCode(unit),
+ reporter = leonReporter)
if(Settings.stopAfterExtraction) {
leonReporter.info("Extracted program for " + unit + ": ")
diff --git a/src/main/scala/leon/plugin/LeonContext.scala b/src/main/scala/leon/plugin/LeonContext.scala
index 29274a5fd..0c6ebabdd 100644
--- a/src/main/scala/leon/plugin/LeonContext.scala
+++ b/src/main/scala/leon/plugin/LeonContext.scala
@@ -4,6 +4,7 @@ package plugin
import purescala.Definitions.Program
case class LeonContext(
- val program: Program
+ val program: Program,
+ val reporter: Reporter
)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 84a638905..5666d15c8 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,19 +1,22 @@
package leon
package synthesis
+import plugin.LeonContext
import purescala.Definitions.Program
-class SynthesisPhase(reporter: Reporter) extends plugin.TransformationPhase {
+object SynthesisPhase extends plugin.LeonPhase {
val name = "Synthesis"
val description = "Synthesis"
- def apply(program: Program): Program = {
+ def run(ctx: LeonContext): LeonContext = {
val quietReporter = new QuietReporter
val solvers = List(
new TrivialSolver(quietReporter),
new FairZ3Solver(quietReporter)
)
- new Synthesizer(reporter, solvers).synthesizeAll(program)
+ val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(ctx.program)
+
+ ctx.copy(program = newProgram)
}
}
--
GitLab