From 5a367480a5d8cc543c1cc199ea7bf9eb851a6e01 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Mar 2016 17:19:18 +0100
Subject: [PATCH] Take precondition of function into account when simplifying
Solution
---
src/main/scala/leon/repair/Repairman.scala | 4 ++--
src/main/scala/leon/synthesis/Solution.scala | 4 ++--
src/main/scala/leon/synthesis/SynthesisPhase.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 4 ++--
.../scala/leon/regression/synthesis/StablePrintingSuite.scala | 3 +--
5 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 07bdeb6ca..d941f1c0e 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -132,7 +132,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val (solSize, proof) = solutions.headOption match {
case Some((sol, trusted)) =>
- val solExpr = sol.toSimplifiedExpr(ctx, program)
+ val solExpr = sol.toSimplifiedExpr(ctx, program, fd)
val totalSolSize = formulaSize(solExpr)
(locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
case _ =>
@@ -162,7 +162,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
reporter.info(ASCIIHelpers.title("Repair successful:"))
for ( ((sol, isTrusted), i) <- solutions.zipWithIndex) {
reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+ (if(isTrusted) "" else " (untrusted)" ) + ":"))
- val expr = sol.toSimplifiedExpr(ctx, synth.program)
+ val expr = sol.toSimplifiedExpr(ctx, synth.program, fd)
reporter.info(expr.asString(program)(ctx))
}
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index d57045254..fd7d3fb6a 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -54,8 +54,8 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
}
- def toSimplifiedExpr(ctx: LeonContext, p: Program): Expr = {
- Simplifiers.bestEffort(ctx, p)(toExpr)
+ def toSimplifiedExpr(ctx: LeonContext, p: Program, within: FunDef): Expr = {
+ withoutSpec(Simplifiers.bestEffort(ctx, p)(req(within.precOrTrue, toExpr))).get
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ad309905e..f40117cf1 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -89,7 +89,7 @@ object SynthesisPhase extends UnitPhase[Program] {
}
solutions.headOption foreach { case (sol, _) =>
- val expr = sol.toSimplifiedExpr(ctx, program)
+ val expr = sol.toSimplifiedExpr(ctx, program, ci.fd)
fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
functions += fd
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 624ec5eaa..c81b045d0 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -97,7 +97,7 @@ class Synthesizer(val context : LeonContext,
val (size, calls, proof) = result.headOption match {
case Some((sol, trusted)) =>
- val expr = sol.toSimplifiedExpr(context, program)
+ val expr = sol.toSimplifiedExpr(context, program, ci.fd)
val pr = trusted match {
case Some(true) => "✓"
case Some(false) => "✗"
@@ -165,7 +165,7 @@ class Synthesizer(val context : LeonContext,
def solutionToProgram(sol: Solution): (Program, List[FunDef]) = {
// We replace the choose with the body of the synthesized solution
- val solutionExpr = sol.toSimplifiedExpr(context, program)
+ val solutionExpr = sol.toSimplifiedExpr(context, program, ci.fd)
val (npr, fdMap) = replaceFunDefs(program)({
case fd if fd eq ci.fd =>
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index cedfa529f..da7f51f4f 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -40,7 +40,6 @@ class StablePrintingSuite extends LeonRegressionSuite {
EquivalentInputs,
UnconstrainedOutput,
OptimisticGround,
- EqualitySplit,
InequalitySplit,
rules.Assert,
DetupleOutput,
@@ -115,7 +114,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
case RuleExpanded(sub) =>
a.onSuccess(sub.map(Solution.choose)) match {
case Some(sol) =>
- val result = sol.toSimplifiedExpr(ctx, pgm)
+ val result = sol.toSimplifiedExpr(ctx, pgm, ci.fd)
val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.source, (indent: Int) => {
val p = new ScalaPrinter(PrinterOptions(), Some(pgm))
--
GitLab