From 896008d8acb3d7e989897ba5692bce51bd98a647 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Jan 2015 16:28:03 +0100
Subject: [PATCH] Fix PartialSolution to apply onSuccess on the correct
solution
---
.../leon/repair/rules/GuidedCloser.scala | 5 ++---
.../leon/synthesis/PartialSolution.scala | 21 +++----------------
.../leon/synthesis/rules/CegisLike.scala | 8 ++++---
3 files changed, 10 insertions(+), 24 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
index e5b3dfce0..50b255755 100644
--- a/src/main/scala/leon/repair/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -37,18 +37,17 @@ case object GuidedCloser extends NormalizingRule("Guided Closer") {
val alts = guides.filter(isDeterministic).flatMap { e =>
// Tentative solution using e
- val wrappedE = if (p.xs.size == 1) Tuple(Seq(e)) else e
val simp = Simplifiers.bestEffort(hctx.context, hctx.program) _
- val vc = simp(and(p.pc, letTuple(p.xs, wrappedE, not(p.phi))))
+ val vc = simp(and(p.pc, letTuple(p.xs, e, not(p.phi))))
val solver = hctx.sctx.newSolver.setTimeout(2000L)
solver.assertCnstr(vc)
val osol = solver.check match {
case Some(false) =>
- Some(Solution(BooleanLiteral(true), Set(), wrappedE, true))
+ Some(Solution(BooleanLiteral(true), Set(), e, true))
case None =>
hctx.reporter.ifDebug { printer =>
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index 13c9fc99d..f76355b78 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -20,7 +20,7 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
Solution.choose(p)
}
- def solutionAround(n: Node): Option[Expr => Solution] = {
+ def solutionAround(n: Node): Expr => Option[Solution] = {
def solveWith(optn: Option[Node], sol: Solution): Option[Solution] = optn match {
case None =>
Some(sol)
@@ -47,23 +47,8 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
}
}
- val anchor = FreshIdentifier("anchor").setType(n.p.outType)
- val s = Solution(BooleanLiteral(true), Set(), anchor.toVariable)
-
- solveWith(Some(n), s) map {
- case s @ Solution(pre, defs, term) =>
- (e: Expr) =>
- Solution(replaceFromIDs(Map(anchor -> e), pre),
- defs.map { d =>
- d.fullBody = preMap({
- case Variable(`anchor`) => Some(e)
- case _ => None
- })(d.fullBody)
- d
- },
- replaceFromIDs(Map(anchor -> e), term),
- s.isTrusted)
- }
+ e : Expr => solveWith(Some(n), Solution(BooleanLiteral(true), Set(), e))
+
}
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 372845ce4..dcc7cad3f 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -202,13 +202,15 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
-
/**
* Information about the final Program representing CEGIS solutions at
* the current unfolding level
*/
- private val outerSolution = new PartialSolution(hctx.search.g).solutionAround(hctx.currentNode).getOrElse {
- sctx.reporter.fatalError("Unable to create outer solution")
+ private val outerSolution = {
+ val part = new PartialSolution(hctx.search.g)
+ e : Expr => part.solutionAround(hctx.currentNode)(e).getOrElse {
+ sctx.reporter.fatalError("Unable to create outer solution")
+ }
}
private val bArrayId = FreshIdentifier("bArray", true).setType(ArrayType(BooleanType))
--
GitLab