diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala index e5b3dfce0c4797d05bed467d5e334104f9e5f7d1..50b2557554cfa623bf64d753d38c0052bc7e132b 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 13c9fc99d080bc1662e64dd22b92f2dc8edc7629..f76355b7851f59d4515fbfbb0feaa3e6504d4f22 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 372845ce470b8cb1e563672d5d3d9522b3f88017..dcc7cad3fee9a039533cf94aea017fd14744545d 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))