From 04f248daf266a130712aceb0d915c2b12f72b7b8 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 18 May 2016 16:04:04 +0200
Subject: [PATCH] Search can be passed problem once - make it public
---
src/main/scala/leon/synthesis/Search.scala | 4 +++-
src/main/scala/leon/synthesis/Synthesizer.scala | 6 ++----
.../scala/leon/integration/solvers/StringRenderSuite.scala | 2 +-
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index e9501009d..15efbc18f 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -11,7 +11,9 @@ import scala.annotation.tailrec
import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
-class Search(val ctx: LeonContext, ci: SourceInfo, p: Problem, val strat: Strategy) extends Interruptible {
+class Search(val ctx: LeonContext, ci: SourceInfo, val strat: Strategy) extends Interruptible {
+
+ val p: Problem = ci.problem
val g = new Graph(p)
val interrupted = new AtomicBoolean(false)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 8baabbe25..c9be0bf70 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -20,8 +20,6 @@ class Synthesizer(val context : LeonContext,
val ci: SourceInfo,
val settings: SynthesisSettings) {
- val problem = ci.problem
-
val reporter = context.reporter
lazy val sctx = new SynthesisContext(context, settings, ci.fd, program)
@@ -44,14 +42,14 @@ class Synthesizer(val context : LeonContext,
strat1
}
- new Search(context, ci, problem, strat2)
+ new Search(context, ci, strat2)
}
private var lastTime: Long = 0
def synthesize(): (Search, Stream[Solution]) = {
reporter.ifDebug { printer =>
- printer(problem.eb.asString("Tests available for synthesis")(context))
+ printer(ci.problem.eb.asString("Tests available for synthesis")(context))
}
val s = getSearch
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
index 72bc14f65..681ac6287 100644
--- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
@@ -85,7 +85,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
def applyStringRenderOn(functionName: String): (FunDef, Program) = {
val ci = synthesisInfos(functionName)
- val search = new Search(ctx, ci, ci.problem, new CostBasedStrategy(ctx, CostModels.default))
+ val search = new Search(ctx, ci, new CostBasedStrategy(ctx, CostModels.default))
val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender)))
val orNode = search.g.root
if (!orNode.isExpanded) {
--
GitLab