diff --git a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala b/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
index 827accc66a500dd487aaa740c3d9de8dfb005fef..fa1305579b78742c870cdf41f4fd3a773f1c4633 100644
--- a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
+++ b/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
@@ -5,105 +5,47 @@ import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.solvers.z3._
+import leon.solvers.Solver
import leon.synthesis._
import org.scalatest.FunSuite
+import org.scalatest.matchers.ShouldMatchers._
import java.io.{BufferedWriter, FileWriter, File}
-class SynthesisTestPhase(val options: SynthesizerOptions,
- val rules: Set[Rule]) extends LeonPhase[Program, Map[Choose, (Solution, Boolean)]] {
- val name = "Synthesis-test"
- val description = "Synthesis-test"
+object ExtractProblemsPhase extends LeonPhase[Program, (Map[FunDef, Seq[Problem]], Solver)] {
+ val name = "Synthesis Problem Extraction"
+ val description = "Synthesis Problem Extraction"
- def run(ctx: LeonContext)(p: Program): Map[Choose, (Solution, Boolean)] = {
- val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
+ def run(ctx: LeonContext)(p: Program): (Map[FunDef, Seq[Problem]], Solver) = {
- val mainSolver = new FairZ3Solver(silentContext)
- mainSolver.setProgram(p)
+ val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
+ val mainSolver = new FairZ3Solver(silentContext)
+ mainSolver.setProgram(p)
- val uninterpretedZ3 = new UninterpretedZ3Solver(silentContext)
- uninterpretedZ3.setProgram(p)
+ var results = Map[FunDef, Seq[Problem]]()
+ def noop(u:Expr, u2: Expr) = u
- def synthesizeAll(program: Program): Map[Choose, (Solution, Boolean)] = {
- def noop(u:Expr, u2: Expr) = u
- var solutions = Map[Choose, (Solution, Boolean)]()
+ def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
+ case ch @ Choose(vars, pred) =>
+ val problem = Problem.fromChoose(ch)
- def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
- case ch @ Choose(vars, pred) =>
- val problem = Problem.fromChoose(ch)
- val synth = new Synthesizer(ctx,
- mainSolver,
- p,
- problem,
- rules,
- options)
- val (sol, isComplete) = synth.synthesize()
+ results += f -> (results.getOrElse(f, Seq()) :+ problem)
- solutions += ch -> (sol, isComplete)
-
- a
- case _ =>
- a
- }
-
- // Look for choose()
- for (f <- program.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- if (options.filterFuns.isEmpty || options.filterFuns.get.contains(f.id.toString)) {
- treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
- }
- }
-
- solutions
+ a
+ case _ =>
+ a
}
- synthesizeAll(p)
- }
-}
-
-class SynthesisRuleTestPhase(val options: SynthesizerOptions,
- val rule: Rule) extends LeonPhase[Program, Map[Choose, RuleResult]] {
- val name = "Synthesis-test"
- val description = "Synthesis-test"
-
- def run(ctx: LeonContext)(p: Program): Map[Choose, RuleResult] = {
-
- val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
- val mainSolver = new FairZ3Solver(silentContext)
- mainSolver.setProgram(p)
-
- def synthesizeAll(program: Program): Map[Choose, RuleResult] = {
- def noop(u:Expr, u2: Expr) = u
-
- var results = Map[Choose, RuleResult]()
-
-
- def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
- case ch @ Choose(vars, pred) =>
- val problem = Problem.fromChoose(ch)
-
- val sctx = SynthesisContext(mainSolver, silentContext.reporter)
-
- results += ch -> rule.attemptToApplyOn(sctx, problem)
-
- a
- case _ =>
- a
- }
-
- // Look for choose()
- for (f <- program.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- if (options.filterFuns.isEmpty || options.filterFuns.get.contains(f.id.toString)) {
- treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
- }
- }
-
- results
+ // Look for choose()
+ for (f <- p.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
+ treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
}
- synthesizeAll(p)
+ (results, mainSolver)
}
+
}
class SynthesisSuite extends FunSuite {
@@ -113,39 +55,19 @@ class SynthesisSuite extends FunSuite {
counter
}
- def synthesisSearch(file: File, rules: Set[Rule])(block: Map[Choose, (Solution, Boolean)] => Unit) {
- val fullName = file.getPath()
- val start = fullName.indexOf("synthesis")
-
- val displayName = if(start != -1) {
- fullName.substring(start, fullName.length)
- } else {
- fullName
- }
-
- test("Synthesizing %3d: [%s]".format(nextInt(), displayName)) {
- assert(file.exists && file.isFile && file.canRead,
- "Benchmark [%s] is not a readable file".format(displayName))
-
- val ctx = LeonContext(
- settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ),
- files = List(file),
- reporter = new SilentReporter
- )
-
- val opts = SynthesizerOptions()
- val pipeline = leon.plugin.ExtractionPhase andThen new SynthesisTestPhase(opts, rules)
+ def testFile(file: String): (((Solver, FunDef, Problem) => Unit) => Unit) = testFile{
+ val res = this.getClass.getClassLoader.getResource(file)
- block(pipeline.run(ctx)("--synthesize" :: file.getPath :: Nil))
+ if(res == null || res.getProtocol != "file") {
+ assert(false, "Tests have to be run from within `sbt`, for otherwise " +
+ "the test files will be harder to access (and we dislike that).")
}
+
+ new File(res.toURI)
}
- def synthesisStep(file: File, rule: Rule)(block: Map[Choose, RuleResult] => Unit) {
+ def testFile(file: File)(block: (Solver, FunDef, Problem) => Unit) {
val fullName = file.getPath()
val start = fullName.indexOf("synthesis")
@@ -159,6 +81,7 @@ class SynthesisSuite extends FunSuite {
assert(file.exists && file.isFile && file.canRead,
"Benchmark [%s] is not a readable file".format(displayName))
+
val ctx = LeonContext(
settings = Settings(
synthesis = true,
@@ -171,35 +94,43 @@ class SynthesisSuite extends FunSuite {
val opts = SynthesizerOptions()
- val pipeline = leon.plugin.ExtractionPhase andThen new SynthesisRuleTestPhase(opts, rule)
+ val pipeline = leon.plugin.ExtractionPhase andThen ExtractProblemsPhase
- block(pipeline.run(ctx)("--synthesize" :: file.getPath :: Nil))
+ val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil)
+
+ for ((f, ps) <- results; p <- ps) {
+ block(solver, f, p)
+ }
}
}
- def assertInnaplicable(rr: RuleResult) {
- assert(rr.alternatives.forall(alt => alt.apply() == RuleApplicationImpossible) === true, "Rule was applicable")
+ def synthesisStep(s: Solver, r: Rule, p: Problem): RuleResult = {
+ val sctx = SynthesisContext(s, new SilentReporter)
+ r.attemptToApplyOn(sctx, p)
}
- def assertSuccess(rr: RuleResult) {
+ def assertRuleSuccess(rr: RuleResult) {
assert(rr.alternatives.isEmpty === false, "No rule alternative while the rule should have succeeded")
assert(rr.alternatives.exists(alt => alt.apply().isInstanceOf[RuleSuccess]) === true, "Rule did not succeed")
}
- def fileFor(name: String): File = {
- val res = this.getClass.getClassLoader.getResource(name)
- if(res == null || res.getProtocol != "file") {
- assert(false, "Tests have to be run from within `sbt`, for otherwise " +
- "the test files will be harder to access (and we dislike that).")
- }
+ def assertFastEnough(rr: RuleResult, timeoutMs: Long) {
+ for (alt <- rr.alternatives) {
+ val ts = System.currentTimeMillis
- new File(res.toURI)
- }
+ val res = alt.apply()
- synthesisStep(fileFor("synthesis/Cegis1.scala"), rules.CEGIS) { res =>
- for ((ch, rr) <- res) {
- assertSuccess(rr)
+ val t = System.currentTimeMillis - ts
+
+ t should be <= timeoutMs
}
}
+
+
+ testFile("synthesis/Cegis1.scala") {
+ case (solver, fd, p) =>
+ assertRuleSuccess(synthesisStep(solver, rules.CEGIS, p))
+ assertFastEnough(synthesisStep(solver, rules.CEGIS, p), 100)
+ }
}