From 8fe43dd4df23d5b9d2c72745188935f3461f6974 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 14 Apr 2015 15:47:32 +0200
Subject: [PATCH] Allow test-only to find tests, limit functions to visible
ones
---
build.sbt | 3 +-
.../SynthesisProblemExtractionPhase.scala | 3 +-
.../leon/test/synthesis/SynthesisSuite.scala | 62 -------------------
3 files changed, 4 insertions(+), 64 deletions(-)
diff --git a/build.sbt b/build.sbt
index 75b810dd1..14d73203e 100644
--- a/build.sbt
+++ b/build.sbt
@@ -39,6 +39,7 @@ javaOptions in Test ++= Seq("-Xss32M", "-Xmx4G", "-XX:MaxPermSize=128M")
parallelExecution in Test := false
-testOptions in Test := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument("-oDF"))
+testOptions in (Test, run) := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument("-oDF"))
+testOptions in (Test, testOnly) := Seq(Tests.Argument("-oDF"))
sourcesInBase in Compile := false
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 658a4b532..f2fb6f47b 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -4,6 +4,7 @@ package leon
package synthesis
package utils
+import purescala.DefOps.funDefsFromMain
import purescala.Definitions._
object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
@@ -12,7 +13,7 @@ object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[
def run(ctx: LeonContext)(p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
// Look for choose()
- val results = for (f <- p.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) yield {
+ val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id.toString) if f.body.isDefined) yield {
f -> ChooseInfo.extractFromFunction(p, f)
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 6978a3fa8..a5cf9ef81 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -118,68 +118,6 @@ class SynthesisSuite extends LeonTestSuite {
}
}
-// def synthesizeWith(search: SearchContext, p: Problem, ss: Apply): Solution = {
-// val apps = hctx.sctx.rules flatMap { _.instantiateOn(hctx, p)}
-//
-// def matchingDesc(app: RuleInstantiation, ss: Apply): Boolean = {
-// import java.util.regex.Pattern;
-// val pattern = Pattern.quote(ss.desc).replace("*", "\\E.*\\Q")
-// app.toString.matches(pattern)
-// }
-//
-// apps.filter(matchingDesc(_, ss)) match {
-// case app :: Nil =>
-// app.apply(hctx) match {
-// case RuleClosed(sols) =>
-// assert(sols.nonEmpty)
-// assert(ss.andThen.isEmpty)
-// sols.head
-//
-// case RuleExpanded(sub) =>
-// val subSols = (sub zip ss.andThen) map { case (p, ss) => synthesizeWith(hctx, p, ss) }
-// app.onSuccess(subSols).get
-// }
-//
-// case Nil =>
-// throw new AssertionError("Failed to find "+ss.desc+". Available: "+apps.mkString(", "))
-//
-// case xs =>
-// throw new AssertionError("Ambiguous "+ss.desc+". Found: "+xs.mkString(", "))
-// }
-// }
-//
-// def synthesize(title: String)(program: String)(strategies: PartialFunction[String, Apply]) {
-// forProgram(title)(program) {
-// case (hctx, fd, p) =>
-// strategies.lift.apply(fd.id.toString) match {
-// case Some(ss) =>
-// synthesizeWith(hctx, p, ss)
-//
-// case None =>
-// assert(false, "Function "+fd.id.toString+" not found")
-// }
-// }
-// }
-//
-//
-// def assertAllAlternativesSucceed(hctx: SearchContext, rr: Traversable[RuleInstantiation]) {
-// assert(!rr.isEmpty)
-//
-// for (r <- rr) {
-// assertRuleSuccess(hctx, r)
-// }
-// }
-//
-// def assertRuleSuccess(hctx: SearchContext, rr: RuleInstantiation): Option[Solution] = {
-// rr.apply(hctx) match {
-// case RuleClosed(sols) if sols.nonEmpty =>
-// sols.headOption
-// case _ =>
-// assert(false, "Rule did not succeed")
-// None
-// }
-// }
-
forProgram("Ground Enum", SynthesisSettings(selectedSolvers = Set("enum")))(
"""
import leon.annotation._
--
GitLab