From 76cd5058c75c84d0f875c400ae11cdcecdcd3bf4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 26 Oct 2015 14:53:03 +0100
Subject: [PATCH] Refactor ChooseInfo to account for all types of synthesis
problems
- Rename fromChoose to fromSpec
- Handle source/spec correctly
- Fix FileInterface to substitute any synth. problem
---
src/main/scala/leon/codegen/CodeGeneration.scala | 2 +-
.../scala/leon/evaluators/RecursiveEvaluator.scala | 2 +-
src/main/scala/leon/repair/Repairman.scala | 14 +++++---------
src/main/scala/leon/synthesis/ChooseInfo.scala | 4 ++--
src/main/scala/leon/synthesis/FileInterface.scala | 3 +--
src/main/scala/leon/synthesis/Problem.scala | 10 +++++-----
src/main/scala/leon/synthesis/SynthesisPhase.scala | 3 +--
.../regression/synthesis/StablePrintingSuite.scala | 4 ++--
8 files changed, 18 insertions(+), 24 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 33975a011..6543da029 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1098,7 +1098,7 @@ trait CodeGeneration {
ch << ATHROW
case choose: Choose =>
- val prob = synthesis.Problem.fromChoose(choose)
+ val prob = synthesis.Problem.fromSpec(choose.pred)
val id = runtime.ChooseEntryPoint.register(prob, this)
ch << Ldc(id)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 80f71fd87..216f51c5d 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -641,7 +641,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
implicit val debugSection = utils.DebugSectionSynthesis
- val p = synthesis.Problem.fromChoose(choose)
+ val p = synthesis.Problem.fromSpec(choose.pred)
ctx.reporter.debug("Executing choose!")
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index d4a935303..e62ee6658 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -129,20 +129,16 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val origBody = fd.body.get
- val spec = fd.postOrTrue
-
- val choose = Choose(spec)
-
val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
val guide = Guide(origBody)
val pre = fd.precOrTrue
val ci = ChooseInfo(
- fd,
- andJoin(Seq(pre, guide, term)),
- origBody,
- choose,
- eb
+ fd = fd,
+ pc = andJoin(Seq(pre, guide, term)),
+ source = origBody,
+ spec = fd.postOrTrue,
+ eb = eb
)
// Return synthesizer for this choose
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 5e36c593b..43e351086 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -12,7 +12,7 @@ import Witnesses._
case class ChooseInfo(fd: FunDef,
pc: Expr,
source: Expr,
- ch: Choose,
+ spec: Expr,
eb: ExamplesBank) {
val problem = Problem.fromChooseInfo(this)
@@ -57,7 +57,7 @@ object ChooseInfo {
ExamplesBank.empty
}
- val ci = ChooseInfo(fd, and(path, term), ch, ch, outerEb)
+ val ci = ChooseInfo(fd, and(path, term), ch, ch.pred, outerEb)
val pcEb = eFinder.generateForPC(ci.problem.as, path, 20)
val chooseEb = eFinder.extractFromProblem(ci.problem)
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 251c6af0e..94bb363c4 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -5,7 +5,6 @@ package synthesis
import purescala.Expressions._
import purescala.Common.Tree
-import purescala.Definitions.Definition
import purescala.ScalaPrinter
import purescala.PrinterOptions
import purescala.PrinterContext
@@ -35,7 +34,7 @@ class FileInterface(reporter: Reporter) {
var newCode = origCode
for ( (ci, e) <- solutions) {
- newCode = substitute(newCode, ci.ch, e)
+ newCode = substitute(newCode, ci.source, e)
}
val out = new BufferedWriter(new FileWriter(newFile))
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index f0d266df7..a48e3111d 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -38,13 +38,13 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
}
object Problem {
- def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true), eb: ExamplesBank = ExamplesBank.empty): Problem = {
+ def fromSpec(spec: Expr, pc: Expr = BooleanLiteral(true), eb: ExamplesBank = ExamplesBank.empty): Problem = {
val xs = {
- val tps = ch.pred.getType.asInstanceOf[FunctionType].from
- tps map (FreshIdentifier("x", _, true))
+ val tps = spec.getType.asInstanceOf[FunctionType].from
+ tps map (FreshIdentifier("x", _, alwaysShowUniqueID = true))
}.toList
- val phi = application(simplifyLets(ch.pred), xs map { _.toVariable})
+ val phi = application(simplifyLets(spec), xs map { _.toVariable})
val as = (variablesOf(And(pc, phi)) -- xs).toList.sortBy(_.name)
val TopLevelAnds(clauses) = pc
@@ -60,7 +60,7 @@ object Problem {
def fromChooseInfo(ci: ChooseInfo): Problem = {
// Same as fromChoose, but we order the input variables by the arguments of
// the functions, so that tests are compatible
- val p = fromChoose(ci.ch, ci.pc, ci.eb)
+ val p = fromSpec(ci.spec, ci.pc, ci.eb)
val argsIndex = ci.fd.params.map(_.id).zipWithIndex.toMap.withDefaultValue(100)
p.copy( as = p.as.sortBy(a => argsIndex(a)))
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ef2bb41e7..dabd354e0 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -65,7 +65,6 @@ object SynthesisPhase extends TransformationPhase {
def apply(ctx: LeonContext, program: Program): Program = {
val options = processOptions(ctx)
-
val chooses = ChooseInfo.extractFromProgram(ctx, program)
var functions = Set[FunDef]()
@@ -75,7 +74,7 @@ object SynthesisPhase extends TransformationPhase {
val synthesizer = new Synthesizer(ctx, program, ci, options)
- val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), true)
+ val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
try {
if (options.generateDerivationTrees) {
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index 8ed9ed14e..2daccc24d 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -93,8 +93,8 @@ class StablePrintingSuite extends LeonRegressionSuite {
for (e <- reporter.lastErrors) {
info(e)
}
- println(e)
info(e.getMessage)
+ e.printStackTrace()
fail("Compilation failed")
}
@@ -117,7 +117,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
case Some(sol) =>
val result = sol.toSimplifiedExpr(ctx, pgm)
- val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.ch, (indent: Int) => {
+ val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.source, (indent: Int) => {
val p = new ScalaPrinter(PrinterOptions(), Some(pgm))
p.pp(result)(PrinterContext(result, List(ci.fd), indent, p))
p.toString
--
GitLab