From 41a774f7c98aa0fb0a03a2580f1a2b811c9c7124 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 29 Jun 2015 17:22:04 +0200
Subject: [PATCH] Recursive focusing now relies on correct tests
---
src/main/scala/leon/repair/rules/Focus.scala | 6 +++---
src/main/scala/leon/synthesis/TestBank.scala | 1 -
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index d1ddf7037..102ab004c 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -42,10 +42,10 @@ case object Focus extends Rule("Focus") {
// - returns Some(true) if for all tests e evaluates to true
// - returns Some(false) if for all tests e evaluates to false
// - returns None otherwise
- def forAllTests(tests: Seq[Example])(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
+ def forAllTestsOf(p: Problem)(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Option[Boolean] = {
var soFar: Option[Boolean] = None
- tests.foreach { ex =>
+ p.tb.invalids.foreach { ex =>
evaluator.eval(e, (p.as zip ex.ins).toMap ++ env) match {
case EvaluationResults.Successful(BooleanLiteral(b)) =>
soFar match {
@@ -74,7 +74,7 @@ case object Focus extends Rule("Focus") {
}
def focus(p: Problem): Traversable[RuleInstantiation] = {
- val faTests = forAllTests(p.tb.invalids) _
+ val faTests = forAllTestsOf(p) _
val TopLevelAnds(clauses) = p.ws
diff --git a/src/main/scala/leon/synthesis/TestBank.scala b/src/main/scala/leon/synthesis/TestBank.scala
index 94dc664b1..b4067cb2e 100644
--- a/src/main/scala/leon/synthesis/TestBank.scala
+++ b/src/main/scala/leon/synthesis/TestBank.scala
@@ -136,7 +136,6 @@ case class TestBank(valids: Seq[Example], invalids: Seq[Example]) {
"No tests."
}
}
-
}
object TestBank {
--
GitLab