From c43e316fe58f1207df8cccffe80f4d4e1a201e3e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 2 Dec 2014 16:42:58 +0100
Subject: [PATCH] Implement what is necessary to do repair from the web
interface
---
library/annotation/package.scala | 2 ++
src/main/scala/leon/refactor/Repairman.scala | 14 +++++++++++---
src/main/scala/leon/synthesis/Solution.scala | 5 +++++
3 files changed, 18 insertions(+), 3 deletions(-)
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index ca65c78bd..f6e084cda 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -9,6 +9,8 @@ package object annotation {
class library extends StaticAnnotation
@ignore
class verified extends StaticAnnotation
+ @ignore
+ class repair extends StaticAnnotation
@ignore
class induct extends StaticAnnotation
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index c9bd7e9fc..bbaec332e 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -32,7 +32,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
var solutions: List[(Solution, Expr, List[FunDef])] = Nil
- def repair(): Unit = {
+ def getChooseInfo(): ChooseInfo = {
// Gather in/out tests
val pre = fd.precondition.getOrElse(BooleanLiteral(true))
val args = fd.params.map(_.id)
@@ -78,6 +78,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
// Synthesis from the ground up
val p = Problem(fd.params.map(_.id).toList, pc, spec, List(out))
val ch = Choose(List(out), spec)
+ // do we really want to do that?
fd.body = Some(ch)
val soptions0 = SynthesisPhase.processOptions(ctx);
@@ -91,7 +92,14 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
)) diff Seq(ADTInduction)
);
- val synthesizer = new Synthesizer(ctx, fd, program, p, soptions)
+ ChooseInfo(ctx, program, fd, pc, gexpr, ch, soptions)
+ }
+
+ def repair(): Unit = {
+ val ci = getChooseInfo()
+ val p = ci.problem
+
+ val synthesizer = ci.synthesizer
synthesizer.synthesize() match {
case (search, sols) =>
@@ -115,7 +123,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
}
}
- if (soptions.generateDerivationTrees) {
+ if (ci.options.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index a6a6b2989..4da0c9dc7 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -9,6 +9,7 @@ import purescala.TypeTrees.{TypeTree,TupleType}
import purescala.Definitions._
import purescala.TreeOps._
import purescala.ScopeSimplifier
+import purescala.Constructors._
import solvers.z3._
import solvers._
@@ -70,6 +71,10 @@ object Solution {
new Solution(BooleanLiteral(true), Set(), Choose(p.xs, p.phi))
}
+ def chooseComplete(p: Problem): Solution = {
+ new Solution(BooleanLiteral(true), Set(), Choose(p.xs, and(p.pc, p.phi)))
+ }
+
// Generate the simplest, wrongest solution, used for complexity lowerbound
def basic(p: Problem): Solution = {
new Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(id => simplestValue(id.getType))))
--
GitLab