From 62c0a0a3e76cd29fc9546dec399543262b48490d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 May 2016 14:23:42 +0200
Subject: [PATCH] CEGIS should find replaced functions in program
---
.../leon/synthesis/rules/CEGISLike.scala | 26 +++++++++----------
1 file changed, 12 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index e572ab185..5a34ee60f 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -268,28 +268,26 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
}
- // The function which calls the synthesized expression within programCTree
- private val cTreeFd = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), p.outType)
- // The spec of the problem
- private val phiFd = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), BooleanType)
+ private val cTreeFd0 = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), p.outType)
+ private val phiFd0 = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), BooleanType)
// The program with the body of the current function replaced by the current partial solution
private val (innerProgram, origIdMap, origFdMap, origCdMap) = {
val outerSolution = {
new PartialSolution(hctx.search.strat, true)
- .solutionAround(hctx.currentNode)(FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)))
+ .solutionAround(hctx.currentNode)(FunctionInvocation(cTreeFd0.typed, p.as.map(_.toVariable)))
.getOrElse(fatalError("Unable to get outer solution"))
}
- val program0 = addFunDefs(hctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.functionContext)
+ val program0 = addFunDefs(hctx.program, Seq(cTreeFd0, phiFd0) ++ outerSolution.defs, hctx.functionContext)
- cTreeFd.body = None
+ cTreeFd0.body = None
- phiFd.body = Some(
+ phiFd0.body = Some(
letTuple(p.xs,
- FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)),
+ FunctionInvocation(cTreeFd0.typed, p.as.map(_.toVariable)),
p.phi)
)
@@ -306,16 +304,16 @@ abstract class CEGISLike(name: String) extends Rule(name) {
Some(nfd)
- // We freshen/duplicate every functions, except these two as they are
- // fresh anyway and we refer to them directly.
- case `cTreeFd` | `phiFd` =>
- None
-
case fd =>
Some(fd.duplicate())
}
}
+ // The function which calls the synthesized expression within programCTree
+ private val cTreeFd = origFdMap.getOrElse(cTreeFd0, cTreeFd0)
+ // The spec of the problem
+ private val phiFd = origFdMap.getOrElse(phiFd0, phiFd0)
+
private val outerToInner = new purescala.TreeTransformer {
override def transform(id: Identifier): Identifier = origIdMap.getOrElse(id, id)
override def transform(cd: ClassDef): ClassDef = origCdMap.getOrElse(cd, cd)
--
GitLab