From f54da2c2d4c76ef2773c75fc497f8056d76881fe Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Jun 2015 18:03:47 +0200
Subject: [PATCH] Replace solution within choose, since now it can do direct
recursive calls
---
.../scala/leon/synthesis/Synthesizer.scala | 30 +++++++------------
1 file changed, 11 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index de108afa9..b5b908394 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -6,6 +6,7 @@ package synthesis
import purescala.Common._
import purescala.Definitions._
import purescala.ExprOps._
+import purescala.DefOps._
import purescala.Expressions._
import purescala.Constructors._
import purescala.ScalaPrinter
@@ -97,28 +98,19 @@ class Synthesizer(val context : LeonContext,
// Returns the new program and the new functions generated for this
def solutionToProgram(sol: Solution): (Program, List[FunDef]) = {
+ // We replace the choose with the body of the synthesized solution
- // Create new fundef for the body
- val ret = tupleTypeWrap(problem.xs.map(_.getType))
- val res = Variable(FreshIdentifier("res", ret))
+ val solutionExpr = sol.toSimplifiedExpr(context, program)
- val mapPost: Map[Expr, Expr] = problem.xs.zipWithIndex.map{ case (id, i) =>
- Variable(id) -> tupleSelect(res, i+1, problem.xs.size)
- }.toMap
-
- val fd = new FunDef(FreshIdentifier(ci.fd.id.name+"_final", alwaysShowUniqueID = true), Nil, ret, problem.as.map(ValDef(_)), DefType.MethodDef)
- fd.precondition = Some(and(problem.pc, sol.pre))
- fd.postcondition = Some(Lambda(Seq(ValDef(res.id)), replace(mapPost, problem.phi)))
- fd.body = Some(sol.term)
-
- val newDefs = fd +: sol.defs.toList
-
- val newModule = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq, false)
- val newUnit = UnitDef(FreshIdentifier("synthesis"), Seq(newModule), Nil, Seq(), true)
-
- val npr = program.copy(units = newUnit :: program.units)
+ val (npr, fdMap) = replaceFunDefs(program)({
+ case fd if fd eq ci.fd =>
+ val nfd = fd.duplicate
+ nfd.fullBody = replace(Map(ci.source -> solutionExpr), nfd.fullBody)
+ Some(nfd)
+ case _ => None
+ })
- (npr, newDefs)
+ (npr, fdMap.get(ci.fd).toList)
}
def shutdown(): Unit = {
--
GitLab