From 5b5765c1eae3f1fbd9267b0e1783104bc49ad720 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 Apr 2016 11:39:30 +0200
Subject: [PATCH] Pass correct solver to SolverDataGen, synthesis improvements
---
src/main/scala/leon/datagen/SolverDataGen.scala | 4 +---
src/main/scala/leon/purescala/PrettyPrinter.scala | 2 ++
src/main/scala/leon/synthesis/ExamplesFinder.scala | 5 +++--
src/main/scala/leon/synthesis/SourceInfo.scala | 2 +-
src/main/scala/leon/synthesis/rules/DetupleInput.scala | 9 ++++-----
.../scala/leon/synthesis/rules/OptimisticGround.scala | 2 +-
6 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 3a222bd6b..34d94c1a9 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -11,8 +11,7 @@ import purescala.Constructors._
import solvers._
import utils._
-
-class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program) => SolverFactory[Solver])) extends DataGenerator {
+class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) extends DataGenerator {
implicit val ctx0 = ctx
def generate(tpe: TypeTree): FreeableIterator[Expr] = {
@@ -73,7 +72,6 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
ModuleDef(FreshIdentifier("new"), fds.values.toSeq, false)
)))
- val sf = sff(ctx, pgm1)
val modelEnum = new ModelEnumerator(ctx, pgm1, sf)
val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 38644fc4a..0dbf1aba9 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -634,6 +634,7 @@ class PrettyPrinter(opts: PrinterOptions,
case Assert(_, _, bd) => Seq(bd)
case Let(_, _, bd) => Seq(bd)
case LetDef(_, bd) => Seq(bd)
+ case LetPattern(_, _, bd) => Seq(bd)
case Require(_, bd) => Seq(bd)
case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
case Ensuring(bd, pred) => Seq(bd, pred)
@@ -669,6 +670,7 @@ class PrettyPrinter(opts: PrinterOptions,
_: Ensuring | _: Assert | _: Require | _: Definition | _: MatchExpr | _: MatchCase |
_: Let | _: LetDef | _: IfExpr | _ : CaseClass | _ : Lambda | _ : Choose | _ : Tuple
)) => false
+ case (_:Pattern, _) => false
case (ex: StringConcat, Some(_: StringConcat)) => false
case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index c7c998989..628a9201a 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -116,12 +116,13 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
ExamplesBank(examples.filter(isValidExample), Seq())
}
- def generateForPC(ids: List[Identifier], pc: Expr, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
+ def generateForPC(ids: List[Identifier], pc: Expr, ctx: LeonContext, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
//println(program.definedClasses)
val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
val datagen = new GrammarDataGen(evaluator, ValueGrammar)
- val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory.getFromSettings(ctx, pgm))
+ val solverF = SolverFactory.getFromSettings(ctx, program)
+ val solverDataGen = new SolverDataGen(ctx, program, solverF)
val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample)
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index cf6063da0..0e9a22fd3 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -63,7 +63,7 @@ object SourceInfo {
val p = Problem.fromSpec(ch.pred, and(path, term), outerEb, Some(fd))
- val pcEb = eFinder.generateForPC(p.as, path, 20)
+ val pcEb = eFinder.generateForPC(p.as, path, ctx, 20)
val chooseEb = eFinder.extractFromProblem(p)
val eb = (outerEb union chooseEb) union pcEb
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 28d567e1b..771899a7c 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -112,11 +112,10 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb).withWs(hints)
val s = { (e: Expr) =>
- LetPattern(
- tuplePatternWrap(patts),
- tupleWrap(as map Variable),
- simplePostTransform(revMap)(e)
- )
+ val body = simplePostTransform(revMap)(e)
+ (patts zip as).foldRight(body) { case ((patt, a), bd) =>
+ LetPattern(patt, a.toVariable, bd)
+ }
}
Some(decomp(List(sub), forwardMap(s), s"Detuple ${as.mkString(", ")}"))
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 775b496be..6a688b120 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -45,7 +45,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- // Model apprears valid, but it might be a fake expression (generic values)
+ // Model appears valid, but it might be a fake expression (generic values)
val outExpr = tupleWrap(p.xs.map(valuateWithModel(satModel)))
if (!isRealExpr(outExpr)) {
--
GitLab