Skip to content
Snippets Groups Projects
Commit 29c3acd4 authored by Philippe Suter's avatar Philippe Suter
Browse files

Proper passing of `LeonContext`s in synthesis.

parent deca849d
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
......@@ -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,
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment