diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dfbf50aa68fee0beba9437dc16a2909aeb0c0c9f
--- /dev/null
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -0,0 +1,99 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Definitions._
+import purescala.Common._
+import purescala.Constructors._
+import purescala.Extractors._
+import evaluators._
+import solvers._
+import solvers.combinators._
+import solvers.smtlib._
+import solvers.z3._
+import utils._
+
+
+class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program) => SolverFactory[Solver])) extends DataGenerator {
+ implicit val ctx0 = ctx
+
+ def generate(tpe: TypeTree): Iterator[Expr] = {
+ generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head)
+ }
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
+ if (ins.isEmpty) {
+ Iterator.empty
+ } else {
+
+ var fds = Map[ClassDef, FunDef]()
+
+ def sizeFor(of: Expr): Expr = of.getType match {
+ case AbstractClassType(acd, tps) =>
+ val fd = fds.getOrElse(acd, {
+ val actDef = AbstractClassType(acd, acd.tparams.map(_.tp))
+
+ val e = FreshIdentifier("e", actDef)
+
+ val fd: FunDef = new FunDef(FreshIdentifier("sizeOf", Untyped),
+ acd.tparams,
+ IntegerType,
+ Seq(ValDef(e)))
+
+ fds += acd -> fd
+
+
+ fd.body = Some(MatchExpr(e.toVariable,
+ actDef.knownCCDescendants.map { cct =>
+ val fields = cct.fieldsTypes.map ( t => FreshIdentifier("field", t))
+
+ val rhs = fields.foldLeft(InfiniteIntegerLiteral(1): Expr) { (i, f) =>
+ plus(i, sizeFor(f.toVariable))
+ }
+
+ MatchCase(CaseClassPattern(None, cct, fields.map(f => WildcardPattern(Some(f)))), None, rhs)
+ }
+ ))
+
+ fd
+ })
+
+ FunctionInvocation(fd.typed(tps), Seq(of))
+
+ case tt @ TupleType(tps) =>
+ val exprs = for ((t,i) <- tps.zipWithIndex) yield {
+ sizeFor(tupleSelect(of, i+1, tps.size))
+ }
+
+ exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus _)
+
+ case _ =>
+ InfiniteIntegerLiteral(1)
+ }
+
+ val sizeOf = sizeFor(tupleWrap(ins.map(_.toVariable)))
+
+ // We need to synthesize a size function for ins' types.
+ val pgm1 = Program(pgm.units :+ UnitDef(FreshIdentifier("new"), List(
+ ModuleDef(FreshIdentifier("new"), fds.values.toSeq, false)
+ )))
+
+ val sf = sff(ctx, pgm1)
+ val modelEnum = new ModelEnumerator(ctx, pgm1, sf)
+
+ println("Generating for "+ins.map(_.getType.asString)+", satisfying "+satisfying.asString)
+
+ val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
+
+ try {
+ enum.take(maxValid).map(model => ins.map(model)).toList.iterator
+ } finally {
+ enum.free()
+ }
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index f4bd40885d1b11d4d3924ad8c724874368b0dd8a..494f4b9b6fbe4b652455891d08986634d9d5ec91 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -17,7 +17,6 @@ import utils.Interruptible
import evaluators._
class UnrollingSolver(val context: LeonContext, program: Program, underlying: Solver) extends Solver with NaiveAssumptionSolver {
-
val feelingLucky = context.findOptionOrDefault(optFeelingLucky)
val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
val assumePreHolds = context.findOptionOrDefault(optAssumePre)
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 90556b035df96c47cb1a4b9f3d277389e7010cf5..1f34fe87d8f48e9de1ff39e018bdcb0c63eaad59 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -88,14 +88,14 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
}
}
- def asString(title: String): String = {
+ def asString(title: String)(implicit ctx: LeonContext): String = {
var tt = new Table(title)
if (examples.nonEmpty) {
val ow = examples.map {
case InOutExample(_, out) => out.size
- case _ => 0
+ case _ => 1
}.max
val iw = examples.map(_.ins.size).max
@@ -115,13 +115,13 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
for (t <- ts) {
val os = t match {
case InOutExample(_, outs) =>
- outs.map(Cell(_))
+ outs.map(o => Cell(o.asString))
case _ =>
Seq(Cell("?", ow))
}
tt += Row(
- t.ins.map(Cell(_)) ++ Seq(Cell("->")) ++ os
+ t.ins.map(i => Cell(i.asString)) ++ Seq(Cell("->")) ++ os
)
}
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 7877e9a34dbcee152f2a439665fa3d3697e64cff..9ef46ec5ac3b3aa3c97e315d9a6b755eba21b3bf 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -14,6 +14,9 @@ import evaluators._
import grammars._
import bonsai.enumerators._
import codegen._
+import datagen._
+import solvers._
+import solvers.z3._
class ExamplesFinder(ctx0: LeonContext, program: Program) {
@@ -104,30 +107,14 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
def generateForPC(ids: List[Identifier], pc: Expr, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
+ val datagen = new GrammarDataGen(evaluator, ValueGrammar)
+ val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory(() => new FairZ3Solver(ctx, pgm)))
- val inputs = enum.iterator(tupleTypeWrap(ids map { _.getType})).map(unwrapTuple(_, ids.size))
+ val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample(_))
- val filtering: Seq[Expr] => Boolean = pc match {
- case BooleanLiteral(true) =>
- _ => true
- case pc =>
- evaluator.compile(pc, ids) match {
- case Some(evalFun) =>
- { (e: Seq[Expr]) => evalFun(e).result == Some(BooleanLiteral(true)) }
- case None =>
- { _ => false }
- }
- }
-
- val generatedTests = inputs
- .take(maxEnumerated)
- .filter(filtering)
- .take(maxValid)
- .map(InExample(_))
- .toList
+ val solverExamples = solverDataGen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample(_))
- ExamplesBank(generatedTests, Nil)
+ ExamplesBank(generatedExamples.toSeq ++ solverExamples.toSeq, Nil)
}
private def extractTestsOf(e: Expr): Set[Map[Identifier, Expr]] = {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 2b770e0c5aeee2f8eeffaf49183d1374bf0538bb..ff822ac420879bf2808084d0672691d40f38608f 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -65,27 +65,25 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def run(ctx: LeonContext)(program: Program): Program = {
val options = processOptions(ctx)
- def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
+ def excludeByDefault(fd: FunDef): Boolean = { fd.annotations contains "library" }
val fdFilter = {
import OptionsHelpers._
- val ciTofd = { (ci: ChooseInfo) => ci.fd }
-
- filterInclusive(options.functions.map(fdMatcher(program)), Some(excludeByDefault _)) compose ciTofd
+ filterInclusive(options.functions.map(fdMatcher(program)), Some(excludeByDefault _))
}
- val chooses = ChooseInfo.extractFromProgram(ctx, program).filter(fdFilter)
+ val chooses = program.definedFunctions.filter(fdFilter).flatMap(ChooseInfo.extractFromFunction(ctx, program, _))
var functions = Set[FunDef]()
- chooses.foreach { ci =>
+ chooses.toSeq.sortBy(_.fd.id).foreach { ci =>
val fd = ci.fd
val synthesizer = new Synthesizer(ctx, program, ci, options)
+
val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), true)
try {
-
if (options.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 9659f2b7704520ef871211aa969d24d01fa0ece3..891ff435c98594c02a075e3a751fc2185213785a 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -24,6 +24,8 @@ class Synthesizer(val context : LeonContext,
lazy val sctx = SynthesisContext.fromSynthesizer(this)
+ implicit val debugSection = leon.utils.DebugSectionSynthesis
+
def getSearch: Search = {
if (settings.manualSearch.isDefined) {
new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
@@ -33,6 +35,11 @@ class Synthesizer(val context : LeonContext,
}
def synthesize(): (Search, Stream[Solution]) = {
+
+ reporter.ifDebug { printer =>
+ printer(problem.eb.asString("Tests available for synthesis")(context))
+ }
+
val s = getSearch
val t = context.timers.synthesis.search.start()
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a15922640077052f8164780df49d51866ac5fa4f
--- /dev/null
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -0,0 +1,19 @@
+package leon
+package utils
+
+abstract class FreeableIterator[T] extends Iterator[T] {
+ private[this] var nextElem: Option[T] = None
+
+ def hasNext() = {
+ nextElem = computeNext()
+ nextElem.nonEmpty
+ }
+
+ def next() = {
+ nextElem.get
+ }
+
+ def computeNext(): Option[T]
+
+ def free()
+}
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index 2467a902137a37929580e33a04debbf78411069c..81bacf1623c37a83ed484004b9e84b4cbcbbb339 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -29,9 +29,8 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
enumVarying0(ids, satisfying, Some(measure), nPerMeasure)
}
- private[this] def enumVarying0(ids: Seq[Identifier], satisfying: Expr, measure: Option[Expr], nPerMeasure: Int = 1): Iterator[Map[Identifier, Expr]] = {
+ private[this] def enumVarying0(ids: Seq[Identifier], satisfying: Expr, measure: Option[Expr], nPerMeasure: Int = 1): FreeableIterator[Map[Identifier, Expr]] = {
val s = sf.getNewSolver
- reclaimPool ::= s
s.assertCnstr(satisfying)
@@ -46,35 +45,40 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
var perMeasureRem = Map[Expr, Int]().withDefaultValue(nPerMeasure)
- new Iterator[Map[Identifier, Expr]] {
- def hasNext = {
- s.check == Some(true)
- }
-
- def next() = {
- val sm = s.getModel
- val model = ids.map { id =>
- id -> sm.getOrElse(id, simplestValue(id.getType))
- }.toMap
+ new FreeableIterator[Map[Identifier, Expr]] {
+ def computeNext() = {
+ s.check match {
+ case Some(true) =>
+ val model = s.getModel
+ val idsModel = (ids.map { id =>
+ id -> model.getOrElse(id, simplestValue(id.getType))
+ }).toMap
+ // Vary the model
+ s.assertCnstr(not(andJoin(idsModel.toSeq.sortBy(_._1).map { case (k, v) => equality(k.toVariable, v) })))
- // Vary the model
- s.assertCnstr(not(andJoin(model.toSeq.sortBy(_._1).map { case (k,v) => equality(k.toVariable, v) })))
+ measure match {
+ case Some(ms) =>
+ val mValue = evaluator.eval(ms, idsModel).result.get
- measure match {
- case Some(ms) =>
- val mValue = evaluator.eval(ms, model).result.get
+ perMeasureRem += (mValue -> (perMeasureRem(mValue) - 1))
- perMeasureRem += (mValue -> (perMeasureRem(mValue) - 1))
+ if (perMeasureRem(mValue) <= 0) {
+ s.assertCnstr(not(equality(m.toVariable, mValue)))
+ }
- if (perMeasureRem(mValue) <= 0) {
- s.assertCnstr(not(equality(m.toVariable, mValue)))
+ case None =>
}
- case None =>
+ Some(idsModel)
+
+ case _ =>
+ None
}
+ }
- model
+ def free() {
+ sf.reclaim(s)
}
}
}
@@ -91,7 +95,7 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
case object Up extends SearchDirection
case object Down extends SearchDirection
- private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): Iterator[Map[Identifier, Expr]] = {
+ private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): FreeableIterator[Map[Identifier, Expr]] = {
assert(measure.getType == IntegerType)
val s = sf.getNewSolver
@@ -126,73 +130,77 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
case _ => None
}
- def getNext(): Stream[Map[Identifier, Expr]] = {
- if (rangeEmpty()) {
- Stream.empty
- } else {
- // Assert a new pivot point
- val thisTry = getPivot()
- thisTry.foreach { t =>
- s.push()
- dir match {
- case Up =>
- s.assertCnstr(GreaterThan(mId.toVariable, InfiniteIntegerLiteral(t)))
- case Down =>
- s.assertCnstr(LessThan(mId.toVariable, InfiniteIntegerLiteral(t)))
- }
- t
- }
-
- s.check match {
- case Some(true) =>
- val sm = s.getModel
- val m = ids.map { id =>
- id -> sm.getOrElse(id, simplestValue(id.getType))
- }.toMap
-
- evaluator.eval(measure, m).result match {
- case Some(InfiniteIntegerLiteral(measureVal)) =>
- // Positive result
- dir match {
- case Up => lb = Some(measureVal)
- case Down => ub = Some(measureVal)
- }
-
- Stream.cons(m, getNext())
-
- case _ =>
- ctx.reporter.warning("Evaluator failed to evaluate measure!")
- Stream.empty
- }
-
-
- case Some(false) =>
- // Negative result
- thisTry match {
- case Some(t) =>
- s.pop()
-
- dir match {
- case Up => ub = Some(t)
- case Down => lb = Some(t)
- }
- getNext()
-
- case None =>
- Stream.empty
+ new FreeableIterator[Map[Identifier, Expr]] {
+ def computeNext(): Option[Map[Identifier, Expr]] = {
+ if (rangeEmpty()) {
+ None
+ } else {
+ // Assert a new pivot point
+ val thisTry = getPivot().map { t =>
+ s.push()
+ dir match {
+ case Up =>
+ s.assertCnstr(GreaterThan(mId.toVariable, InfiniteIntegerLiteral(t)))
+ case Down =>
+ s.assertCnstr(LessThan(mId.toVariable, InfiniteIntegerLiteral(t)))
}
+ t
+ }
- case None =>
- Stream.empty
+ s.check match {
+ case Some(true) =>
+ val sm = s.getModel
+ val m = (ids.map { id =>
+ id -> sm.getOrElse(id, simplestValue(id.getType))
+ }).toMap
+
+ evaluator.eval(measure, m).result match {
+ case Some(InfiniteIntegerLiteral(measureVal)) =>
+ // Positive result
+ dir match {
+ case Up => lb = Some(measureVal)
+ case Down => ub = Some(measureVal)
+ }
+
+ Some(m)
+
+ case _ =>
+ ctx.reporter.warning("Evaluator failed to evaluate measure!")
+ None
+ }
+
+
+ case Some(false) =>
+ // Negative result
+ thisTry match {
+ case Some(t) =>
+ s.pop()
+
+ dir match {
+ case Up => ub = Some(t)
+ case Down => lb = Some(t)
+ }
+ computeNext()
+
+ case None =>
+ None
+ }
+
+ case None =>
+ None
+ }
}
}
- }
- getNext().iterator
+ def free() {
+ sf.reclaim(s)
+ }
+ }
}
def shutdown() = {
+ println("Terminating!")
reclaimPool.foreach(sf.reclaim)
}