From f8ba2df6215b04b385044d0e269f7e03c5ce86e4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 8 Dec 2014 13:45:28 +0100
Subject: [PATCH] Fixes here and there
---
src/main/scala/leon/refactor/Repairman.scala | 15 +++++++--------
src/main/scala/leon/synthesis/Problem.scala | 6 +++++-
src/main/scala/leon/synthesis/Rules.scala | 2 +-
3 files changed, 13 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index de119dbc2..9edbe56b3 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 getChooseInfo(): ChooseInfo = {
+ def getSynthesizer(): Synthesizer = {
// Gather in/out tests
val pre = fd.precondition.getOrElse(BooleanLiteral(true))
val args = fd.params.map(_.id)
@@ -95,21 +95,20 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
)) diff Seq(ADTInduction)
);
- ChooseInfo(ctx, program, fd, pre, gexpr, ch, soptions)
+ new Synthesizer(ctx, fd, program, p, soptions)
}
def repair(): Unit = {
- val ci = getChooseInfo()
- val p = ci.problem
+ val synth = getSynthesizer()
+ val p = synth.problem
- val synthesizer = ci.synthesizer
- synthesizer.synthesize() match {
+ synth.synthesize() match {
case (search, sols) =>
for (sol <- sols) {
val expr = sol.toSimplifiedExpr(ctx, program)
- val (npr, fds) = synthesizer.solutionToProgram(sol)
+ val (npr, fds) = synth.solutionToProgram(sol)
if (!sol.isTrusted) {
getVerificationCounterExamples(fds.head, npr) match {
@@ -126,7 +125,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
}
}
- if (ci.options.generateDerivationTrees) {
+ if (synth.options.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
}
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b3959f35c..19f54d171 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -12,7 +12,11 @@ import leon.purescala.Constructors._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier]) {
- override def toString = "⟦ "+as.mkString(";")+", "+(if (ws != BooleanLiteral(true)) ws+" - " else "")+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+
+ override def toString = {
+ val pcws = and(ws, pc)
+ "⟦ "+as.mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+ }
def getTests(sctx: SynthesisContext): Seq[Example] = {
import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 7e5e20ea9..b36573bc7 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -26,7 +26,7 @@ object Rules {
InequalitySplit,
CEGIS,
TEGIS,
- //BottomUpTEGIS,
+ BottomUpTEGIS,
rules.Assert,
DetupleOutput,
DetupleInput,
--
GitLab