Fix forAllTests, improve tests printing

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

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
+  }
+
+}
+

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