From 29c3acd4b7d43c56bdfb10d7052d91cfeebe7a10 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 26 Nov 2012 13:15:31 +0100
Subject: [PATCH] Proper passing of `LeonContext`s in synthesis.
---
src/main/scala/leon/synthesis/ParallelSearch.scala | 3 +--
src/main/scala/leon/synthesis/SynthesisPhase.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 4 +++-
3 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index f11526f3c..184714e7b 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -14,8 +14,7 @@ class ParallelSearch(synth: Synthesizer,
def initWorkerContext(wr: ActorRef) = {
val reporter = new SilentReporter
- // TODO FIXME : the proper LeonContext should make its way here.
- val solver = new FairZ3Solver(LeonContext(reporter = reporter))
+ val solver = new FairZ3Solver(synth.context)
solver.setProgram(synth.program)
SynthesisContext(solver = solver, reporter = synth.reporter)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 2901bb382..7f9a8b054 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -66,7 +66,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
case ch @ Choose(vars, pred) =>
val problem = Problem.fromChoose(ch)
- val synth = new Synthesizer(ctx.reporter,
+ val synth = new Synthesizer(ctx,
mainSolver,
p,
problem,
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 51444a16b..b669335b9 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -15,7 +15,7 @@ import collection.mutable.PriorityQueue
import synthesis.search._
-class Synthesizer(val reporter: Reporter,
+class Synthesizer(val context : LeonContext,
val solver: Solver,
val program: Program,
val problem: Problem,
@@ -25,6 +25,8 @@ class Synthesizer(val reporter: Reporter,
parallel: Boolean = false,
firstOnly: Boolean = false,
timeoutMs: Option[Long] = None) {
+ protected[synthesis] val reporter = context.reporter
+
import reporter.{error,warning,info,fatalError}
var continue = true
--
GitLab