diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala index 6e330c414d5f315c8835fea80c01c89e16a63311..a08ab86d8e03d805f772b545919e8619bf317b08 100644 --- a/src/main/scala/leon/purescala/DefinitionTransformer.scala +++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala @@ -85,32 +85,41 @@ class DefinitionTransformer( val req = deps filter required val allReq = req ++ (deps filter (d => (dependencies(d) & req).nonEmpty)) - val requiredCds = allReq collect { case cd: ClassDef => cd } - val requiredFds = allReq collect { case fd: FunDef => fd } + + val transformedCds = tmpCdMap.filter { case (cd1, cd2) => cd1 ne cd2 }.toMap + val transformedFds = tmpFdMap.filter { case (fd1, fd2) => fd1 ne fd2 }.toMap tmpCdMap.clear() tmpFdMap.clear() - val nonReq = deps filterNot allReq - cdMap ++= nonReq collect { case cd: ClassDef => cd -> cd } - fdMap ++= nonReq collect { case fd: FunDef => fd -> fd } + val requiredCds = allReq.collect { case cd: ClassDef => cd } ++ transformedCds.map(_._1) + val requiredFds = allReq.collect { case fd: FunDef => fd } ++ transformedFds.map(_._1) + + val nonCds = deps collect { case cd: ClassDef if !requiredCds(cd) => cd } + val nonFds = deps collect { case fd: FunDef if !requiredFds(fd) => fd } + + cdMap ++= nonCds.map(cd => cd -> cd) + fdMap ++= nonFds.map(fd => fd -> fd) def trCd(cd: ClassDef): ClassDef = cdMap.cachedB(cd) { val parent = cd.parent.map(act => act.copy(classDef = trCd(act.classDef).asInstanceOf[AbstractClassDef])) - cd match { + transformedCds.getOrElse(cd, cd) match { case acd: AbstractClassDef => acd.duplicate(id = transform(acd.id, true), parent = parent) case ccd: CaseClassDef => ccd.duplicate(id = transform(ccd.id, true), parent = parent) } } - for (cd <- requiredCds) trCd(cd) - for (fd <- requiredFds) { - val newId = transform(fd.id, true) - val newReturn = transform(fd.returnType) - val newParams = fd.params map (vd => ValDef(transform(vd.id))) - fdMap += fd -> fd.duplicate(id = newId, params = newParams, returnType = newReturn) + def trFd(fd: FunDef): FunDef = fdMap.cachedB(fd) { + val ffd = transformedFds.getOrElse(fd, fd) + val newId = transform(ffd.id, true) + val newReturn = transform(ffd.returnType) + val newParams = ffd.params map (vd => ValDef(transform(vd.id))) + ffd.duplicate(id = newId, params = newParams, returnType = newReturn) } + for (cd <- requiredCds) trCd(cd) + for (fd <- requiredFds) trFd(fd) + for (ccd <- requiredCds collect { case ccd: CaseClassDef => ccd }) { val newCcd = cdMap.toB(ccd).asInstanceOf[CaseClassDef] newCcd.setFields(ccd.fields.map(vd => ValDef(transform(vd.id)))) diff --git a/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala index 127c1004eb600c70b240726088c74f72da1d9357..83129798a589d92effac2aa5243237b01621bfbb 100644 --- a/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala +++ b/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala @@ -250,7 +250,7 @@ class TemplateGenerator[T](val theories: TheoryEncoder, def requireDecomposition(e: Expr) = { exists{ - case (_: Choose) | (_: Forall) | (_: Lambda) => true + case (_: Choose) | (_: Forall) | (_: Lambda) | (_: FiniteLambda) => true case (_: Assert) | (_: Ensuring) => true case (_: FunctionInvocation) | (_: Application) => true case _ => false diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala index 9308c54d1895440ea5c7abe760bae23e73c17a38..c7c9989899a61216efeeab61fe6aaa33ed13578d 100644 --- a/src/main/scala/leon/synthesis/ExamplesFinder.scala +++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala @@ -121,7 +121,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) { val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default) val datagen = new GrammarDataGen(evaluator, ValueGrammar) - val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory(() => new FairZ3Solver(ctx, pgm))) + val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory.getFromSettings(ctx, pgm)) val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample) diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala index fe02ce2ef2a8d1eed9e0bbab4d25d695865287f9..e0a1632d279e04ea0848850b3ca5985b8511fe6a 100644 --- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala +++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala @@ -24,6 +24,9 @@ import org.scalatest.Matchers import scala.language.implicitConversions class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures { + + override val leonOpts = List("--solvers=smt-z3") + test("Template Generator simple"){ case (ctx: LeonContext, program: Program) => val TTG = new TypedTemplateGenerator(IntegerType) {} val e = TTG(hole => Plus(hole, hole))