From dd8b19484dd2944628e4183178f41c3d13f9b8a7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 15 Dec 2014 19:12:07 +0100
Subject: [PATCH] Fix forAllTests, improve tests printing
---
src/main/scala/leon/repair/Repairman.scala | 45 +++++++------------
.../scala/leon/synthesis/InOutExample.scala | 23 ++++++++++
src/main/scala/leon/utils/GraphOps.scala | 6 +--
3 files changed, 43 insertions(+), 31 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 10c94e7cc..c88913162 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -141,18 +141,9 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
private def focusRepair(program: Program, fd: FunDef, passingTests: List[Example], failingTests: List[Example]): (Expr, Expr) = {
reporter.ifDebug { printer =>
- printer(title("Tests failing are: "))
- failingTests.foreach { ex =>
- printer(ex.ins.mkString(", "))
- }
- }
- reporter.ifDebug { printer =>
- printer(title("Tests passing are: "))
- passingTests.foreach { ex =>
- printer(ex.ins.mkString(", "))
- }
+ printer(new ExamplesTable("Tests failing:", failingTests).toString)
+ printer(new ExamplesTable("Tests passing:", passingTests).toString)
}
-
val pre = fd.precondition.getOrElse(BooleanLiteral(true))
val args = fd.params.map(_.id)
@@ -168,6 +159,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val evaluator = new DefaultEvaluator(ctx, program)
+ // We exclude redundant failing tests, and only select the minimal tests
val minimalFailingTests = {
// We don't want tests whose invocation will call other failing tests.
// This is because they will appear erroneous,
@@ -179,24 +171,24 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case _ => None
}
}
-
+
val passingTs = for (test <- passingTests) yield InExample(test.ins)
val failingTs = for (test <- failingTests) yield InExample(test.ins)
-
+
val test2Tests : Map[InExample, Set[InExample]] = (failingTs ++ passingTs).map{ ts =>
testEval.eval(body, args.zip(ts.ins).toMap)
(ts, testEval.collected map (InExample(_)))
}.toMap
-
+
val recursiveTests : Set[InExample] = test2Tests.values.toSet.flatten -- (failingTs ++ passingTs)
-
+
val testsTransitive : Map[InExample,Set[InExample]] =
leon.utils.GraphOps.transitiveClosure[InExample](
test2Tests ++ recursiveTests.map ((_,Set[InExample]()))
)
-
+
val knownWithResults : Map[InExample, Boolean] = (failingTs.map((_, false)).toMap) ++ (passingTs.map((_,true)))
-
+
val recWithResults : Map[InExample, Boolean] = recursiveTests.map { ex =>
(ex, evaluator.eval(spec, (args zip ex.ins).toMap + (out -> body)) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => true
@@ -205,19 +197,16 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}.toMap
val allWithResults = knownWithResults ++ recWithResults
-
-
- testsTransitive.collect {
+
+
+ testsTransitive.collect {
case (rest, called) if !allWithResults(rest) && (called forall allWithResults) =>
rest
- }.toSet
+ }.toSeq
}
-
+
reporter.ifDebug { printer =>
- printer(title("MinimalTests are: "))
- minimalFailingTests.foreach { ex =>
- printer(ex.ins.mkString(", "))
- }
+ printer(new ExamplesTable("Minimal failing:", minimalFailingTests).toString)
}
// Check how an expression behaves on tests
@@ -230,9 +219,9 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
evaluator.eval(e, env ++ (args zip ins)) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => Some(true)
case EvaluationResults.Successful(BooleanLiteral(false)) => Some(false)
- case _ => None
+ case e => None
}
- }
+ }.distinct
if (results.size == 1) {
results.head
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index 932801c89..c68590fbd 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -4,8 +4,31 @@ package leon
package synthesis
import purescala.Trees._
+import leon.utils.ASCIIHelpers._
class Example(val ins: Seq[Expr])
case class InOutExample(is: Seq[Expr], val outs: Seq[Expr]) extends Example(is)
case class InExample(is: Seq[Expr]) extends Example(is)
+class ExamplesTable(title: String, ts: Seq[Example]) {
+ override def toString = {
+ var tt = new Table(title)
+
+ for (t <- ts) {
+ val os = t match {
+ case InOutExample(_, outs) =>
+ outs.map(Cell(_))
+ case _ =>
+ Seq(Cell("?"))
+ }
+
+ tt += Row(
+ t.ins.map(Cell(_)) ++ Seq(Cell("->")) ++ os
+ )
+ }
+
+ tt.render
+ }
+
+}
+
diff --git a/src/main/scala/leon/utils/GraphOps.scala b/src/main/scala/leon/utils/GraphOps.scala
index 505829e57..33fcb73f2 100644
--- a/src/main/scala/leon/utils/GraphOps.scala
+++ b/src/main/scala/leon/utils/GraphOps.scala
@@ -22,7 +22,8 @@ object GraphOps {
}
tSort(toPreds, Seq())
}
-
+
+
def transitiveClosure[A](graph: Map[A,Set[A]]) : Map[A,Set[A]] = {
def step(graph : Map[A, Set[A]]) : Map[A,Set[A]] = graph map {
case (k, vs) => (k, vs ++ (vs flatMap { v =>
@@ -39,7 +40,6 @@ object GraphOps {
def sinks[A](graph : Map[A,Set[A]]) =
graph.collect{ case (v, out) if out.isEmpty => v }.toSet
-
/**
* Returns the set of reachable nodes from a given node,
* not including the node itself (unless it is member of a cycle)
@@ -73,4 +73,4 @@ object GraphOps {
rec(source)
}
-}
\ No newline at end of file
+}
--
GitLab