From 8f737a51f0479ad9c6c6114a7aab530c2c01ec6d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Mar 2016 11:03:55 +0100
Subject: [PATCH] SearchContext should not hold duplicate information
---
src/main/scala/leon/repair/rules/Focus.scala | 2 +-
src/main/scala/leon/synthesis/Search.scala | 4 ++--
src/main/scala/leon/synthesis/SearchContext.scala | 3 ++-
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 6 +++---
.../scala/leon/integration/solvers/StringRenderSuite.scala | 4 ++--
.../leon/regression/synthesis/StablePrintingSuite.scala | 2 +-
6 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index f62a7bdcd..943a5a67f 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -30,7 +30,7 @@ case object Focus extends PreprocessingRule("Focus") {
}
- val fd = hctx.ci.fd
+ val fd = hctx.functionContext
val program = hctx.program
val evaluator = new DefaultEvaluator(hctx, program)
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index 225495cac..564c630fc 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -24,11 +24,11 @@ class Search(val ctx: LeonContext, ci: SourceInfo, p: Problem, val strat: Strate
n match {
case an: AndNode =>
ctx.timers.synthesis.applications.get(an.ri.asString(sctx)).timed {
- an.expand(new SearchContext(sctx, ci, an, this))
+ an.expand(new SearchContext(sctx, ci.source, an, this))
}
case on: OrNode =>
- on.expand(new SearchContext(sctx, ci, on, this))
+ on.expand(new SearchContext(sctx, ci.source, on, this))
}
}
}
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 201dcaf21..63683d927 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -4,6 +4,7 @@ package leon
package synthesis
import graph._
+import purescala.Expressions.Expr
/**
* This is context passed down rules, and include search-wise context, as well
@@ -11,7 +12,7 @@ import graph._
*/
class SearchContext (
sctx: SynthesisContext,
- val ci: SourceInfo,
+ val source: Expr,
val currentNode: Node,
val search: Search
) extends SynthesisContext(
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 913e54a49..32bf63486 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -284,7 +284,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
.getOrElse(hctx.reporter.fatalError("Unable to get outer solution"))
}
- val program0 = addFunDefs(hctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
+ val program0 = addFunDefs(hctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.functionContext)
cTreeFd.body = None
@@ -295,11 +295,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
)
replaceFunDefs(program0){
- case fd if fd == hctx.ci.fd =>
+ case fd if fd == hctx.functionContext =>
val nfd = fd.duplicate()
nfd.fullBody = postMap {
- case src if src eq hctx.ci.source =>
+ case src if src eq hctx.source =>
Some(outerSolution.term)
case _ => None
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
index fb3f1ecae..c0c724c81 100644
--- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
@@ -86,7 +86,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender)))
val orNode = search.g.root
if (!orNode.isExpanded) {
- val hctx = new SearchContext(synth.sctx, synth.ci, orNode, search)
+ val hctx = new SearchContext(synth.sctx, synth.ci.source, orNode, search)
orNode.expand(hctx)
}
val andNodes = orNode.descendants.collect {
@@ -104,7 +104,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
val solutions = (search.traversePath(path) match {
case Some(an: AndNode) =>
- val hctx = new SearchContext(synth.sctx, synth.ci, an, search)
+ val hctx = new SearchContext(synth.sctx, synth.ci.source, an, search)
an.ri.apply(hctx)
case _ => throw new Exception("Was not an and node")
}) match {
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index c2f818a78..cedfa529f 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -104,7 +104,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
val sctx = synthesizer.sctx
try {
val search = synthesizer.getSearch
- val hctx = new SearchContext(sctx, ci, search.g.root, search)
+ val hctx = new SearchContext(sctx, ci.source, search.g.root, search)
val problem = ci.problem
info(j.info("synthesis "+problem.asString(sctx)))
val apps = decompRules flatMap { _.instantiateOn(hctx, problem)}
--
GitLab