From 11d63cc2665fa6dd0429a8c8e08dad7a57e5d5c4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 27 Oct 2014 17:40:55 +0100
Subject: [PATCH] Fix tests with new synthesis refactoring
---
.../test/synthesis/StablePrintingSuite.scala | 6 ++----
.../synthesis/SynthesisRegressionSuite.scala | 4 ++--
.../leon/test/synthesis/SynthesisSuite.scala | 20 +++++++++----------
3 files changed, 13 insertions(+), 17 deletions(-)
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index bf0279bea..625f1fa94 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -91,8 +91,8 @@ class StablePrintingSuite extends LeonTestSuite {
for (a <- apps) {
a.apply(sctx) match {
- case RuleSuccess(sol, isTrusted) =>
- case RuleDecomposed(sub) =>
+ case RuleClosed(sols) =>
+ case RuleExpanded(sub) =>
a.onSuccess(sub.map(Solution.choose(_))) match {
case Some(sol) =>
val result = sol.toSimplifiedExpr(ctx, pgm)
@@ -106,8 +106,6 @@ class StablePrintingSuite extends LeonTestSuite {
workList push Job(newContent, (i to i+sub.size).toSet, a.toString :: j.rules)
case None =>
}
-
- case RuleApplicationImpossible =>
}
}
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index e79a022db..eeeadde94 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -41,8 +41,8 @@ class SynthesisRegressionSuite extends LeonTestSuite {
for (ci <- chooses) {
test(cat+": "+f.getName()+" - "+ci.fd.id.name) {
- val (sol, isComplete) = ci.synthesizer.synthesize()
- if (!isComplete) {
+ val (search, sols) = ci.synthesizer.synthesize()
+ if (sols.isEmpty) {
fail("Solution was not found. (Search bound: "+bound+")")
}
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 3d5efd0bb..a21d3e7c1 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -64,16 +64,14 @@ class SynthesisSuite extends LeonTestSuite {
apps.filter(matchingDesc(_, ss)) match {
case app :: Nil =>
app.apply(sctx) match {
- case RuleSuccess(sol, trusted) =>
+ case RuleClosed(sols) =>
+ assert(sols.nonEmpty)
assert(ss.andThen.isEmpty)
- sol
+ sols.head
- case RuleDecomposed(sub) =>
+ case RuleExpanded(sub) =>
val subSols = (sub zip ss.andThen) map { case (p, ss) => synthesizeWith(sctx, p, ss) }
app.onSuccess(subSols).get
-
- case _ =>
- throw new AssertionError("Failed to apply "+app+" on "+p)
}
case Nil =>
@@ -108,8 +106,8 @@ class SynthesisSuite extends LeonTestSuite {
def assertRuleSuccess(sctx: SynthesisContext, rr: RuleInstantiation): Option[Solution] = {
rr.apply(sctx) match {
- case RuleSuccess(sol, trusted) =>
- Some(sol)
+ case RuleClosed(sols) if sols.nonEmpty =>
+ sols.headOption
case _ =>
assert(false, "Rule did not succeed")
None
@@ -189,13 +187,13 @@ object Injection {
) {
case (sctx, fd, p) =>
rules.CEGIS.instantiateOn(sctx, p).head.apply(sctx) match {
- case RuleSuccess(sol, trusted) =>
- assert(false, "CEGIS should have failed, but found : %s".format(sol))
+ case RuleClosed(sols) if sols.nonEmpty =>
+ assert(false, "CEGIS should have failed, but found : %s".format(sols.head))
case _ =>
}
rules.ADTSplit.instantiateOn(sctx, p).head.apply(sctx) match {
- case RuleDecomposed(subs) =>
+ case RuleExpanded(subs) =>
for (sub <- subs; alt <- rules.CEGIS.instantiateOn(sctx, sub)) {
assertRuleSuccess(sctx, alt)
}
--
GitLab