diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index e231e6ee323ae80bcd7dc8d28205e938fd84a5b4..1f584efa4a2392bfb02947c6c99c388fe5aadafa 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -78,7 +78,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
options)
val sol = synth.synthesize()
- solutions += ch -> (f, sol)
+ solutions += ch -> (f, sol._1)
a
case _ =>
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index fe8f2ef8fedb453d950011581c7d5e208f5ce922..ccf4be6d12f19de9e5abe39ddf00a3a5e6c638d6 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -28,7 +28,7 @@ class Synthesizer(val context : LeonContext,
var continue = true
- def synthesize(): Solution = {
+ def synthesize(): (Solution, Boolean) = {
val search = if (options.parallel) {
new ParallelSearch(this, problem, rules, options.costModel)
@@ -64,9 +64,9 @@ class Synthesizer(val context : LeonContext,
res match {
case Some(solution) =>
- solution
+ (solution, true)
case None =>
- new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem)).getSolution
+ (new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem)).getSolution, false)
}
}
diff --git a/src/test/resources/synthesis/Cegis1.scala b/src/test/resources/synthesis/Cegis1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0c5c44d8555c4e50c463df5f921762fe9242b8f
--- /dev/null
+++ b/src/test/resources/synthesis/Cegis1.scala
@@ -0,0 +1,17 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Injection {
+ sealed abstract class List
+ case class Cons(tail: List) extends List
+ case class Nil() extends List
+
+ // proved with unrolling=0
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def simple(in: List) = choose{out: List => size(out) == size(in) }
+}
diff --git a/src/test/scala/leon/test/PureScalaPrograms.scala b/src/test/scala/leon/test/PureScalaPrograms.scala
index f6241e682fb536c00b56b9af78d26e566e002a32..ff95fa366d9c93b9ccbf691cfb097af5a375f115 100644
--- a/src/test/scala/leon/test/PureScalaPrograms.scala
+++ b/src/test/scala/leon/test/PureScalaPrograms.scala
@@ -21,14 +21,12 @@ class PureScalaPrograms extends FunSuite {
private def mkTest(file : File)(block: Output=>Unit) = {
val fullName = file.getPath()
val start = fullName.indexOf("regression")
- val displayName = file.getAbsolutePath()
-/*
+
val displayName = if(start != -1) {
fullName.substring(start, fullName.length)
} else {
fullName
}
- */
test("PureScala program %3d: [%s]".format(nextInt(), displayName)) {
assert(file.exists && file.isFile && file.canRead,
diff --git a/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala b/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..827accc66a500dd487aaa740c3d9de8dfb005fef
--- /dev/null
+++ b/src/test/scala/leon/test/synthesis/RuleApplicationSuite.scala
@@ -0,0 +1,205 @@
+package leon.test.synthesis
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.solvers.z3._
+import leon.synthesis._
+
+import org.scalatest.FunSuite
+
+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"
+
+ def run(ctx: LeonContext)(p: Program): Map[Choose, (Solution, Boolean)] = {
+ val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
+
+ val mainSolver = new FairZ3Solver(silentContext)
+ mainSolver.setProgram(p)
+
+ val uninterpretedZ3 = new UninterpretedZ3Solver(silentContext)
+ uninterpretedZ3.setProgram(p)
+
+ 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)
+ val synth = new Synthesizer(ctx,
+ mainSolver,
+ p,
+ problem,
+ rules,
+ options)
+ val (sol, isComplete) = synth.synthesize()
+
+ 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
+ }
+
+ 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
+ }
+
+ synthesizeAll(p)
+ }
+}
+
+class SynthesisSuite extends FunSuite {
+ private var counter : Int = 0
+ private def nextInt() : Int = {
+ counter += 1
+ 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)
+
+ block(pipeline.run(ctx)("--synthesize" :: file.getPath :: Nil))
+ }
+ }
+
+ def synthesisStep(file: File, rule: Rule)(block: Map[Choose, RuleResult] => 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 SynthesisRuleTestPhase(opts, rule)
+
+ block(pipeline.run(ctx)("--synthesize" :: file.getPath :: Nil))
+ }
+ }
+
+ def assertInnaplicable(rr: RuleResult) {
+ assert(rr.alternatives.forall(alt => alt.apply() == RuleApplicationImpossible) === true, "Rule was applicable")
+ }
+
+ def assertSuccess(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).")
+ }
+
+ new File(res.toURI)
+ }
+
+ synthesisStep(fileFor("synthesis/Cegis1.scala"), rules.CEGIS) { res =>
+ for ((ch, rr) <- res) {
+ assertSuccess(rr)
+ }
+ }
+}