From 65a5c24eb9672404df1ab87f3c84a77bb50142bb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 13:16:27 +0200
Subject: [PATCH] Fix SynthesisSuite and a test
---
.../regression/synthesis/Holes/Hole1.scala | 2 +-
.../synthesis/SynthesisRegressionSuite.scala | 35 +++++++++----------
2 files changed, 17 insertions(+), 20 deletions(-)
diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala
index ce983abae..37990792d 100644
--- a/src/test/resources/regression/synthesis/Holes/Hole1.scala
+++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala
@@ -5,7 +5,7 @@ import leon.collection._
import leon.lang.synthesis._
object Holes {
- def abs3(a: Int) = {
+ def abs3(a: BigInt) = {
if (?(a > 0, a < 0)) {
a
} else {
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index b676a3633..723c8319d 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -20,33 +20,30 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
}
private def testSynthesis(cat: String, f: File, bound: Int) {
+ val ctx = createLeonContext("--synthesis")
- var chooses = List[SourceInfo]()
- var program: Program = null
- var ctx: LeonContext = null
- var opts: SynthesisSettings = null
+ val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase
- test(cat+": "+f.getName+" Compilation") {
- ctx = createLeonContext("--synthesis")
-
- opts = SynthesisSettings(searchBound = Some(bound))
-
- val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase
-
- val (ctx2, pgm2) = pipeline.run(ctx, f.getAbsolutePath :: Nil)
-
- program = pgm2
-
- chooses = SourceInfo.extractFromProgram(ctx2, program)
+ val (ctx2, program) = try {
+ pipeline.run(ctx, f.getAbsolutePath :: Nil)
+ } catch {
+ case LeonFatalError(msg) =>
+ test(s"$cat: ${f.getName}") {
+ fail(s"Compilation failed: ${msg.getOrElse("")}")
+ }
+ return
}
+ val chooses = SourceInfo.extractFromProgram(ctx2, program)
+ val settings = SynthesisSettings(searchBound = Some(bound))
+
for (ci <- chooses) {
- test(cat+": "+f.getName+" - "+ci.fd.id.name) {
- val synthesizer = new Synthesizer(ctx, program, ci, opts)
+ test(s"$cat: ${f.getName} - ${ci.fd.id.name}") {
+ val synthesizer = new Synthesizer(ctx, program, ci, settings)
try {
val (_, sols) = synthesizer.synthesize()
if (sols.isEmpty) {
- fail("Solution was not found. (Search bound: "+bound+")")
+ fail(s"Solution was not found. (Search bound: $bound)")
}
} finally {
synthesizer.shutdown()
--
GitLab