From 506231656ff51865234b15540e3057e72f51ff51 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 9 Apr 2016 18:55:42 +0200
Subject: [PATCH] Moved StringRenderSuite to smt-z3 because of libc crash
---
.../purescala/DefinitionTransformer.scala | 33 ++++++++++++-------
.../solvers/unrolling/TemplateGenerator.scala | 2 +-
.../scala/leon/synthesis/ExamplesFinder.scala | 2 +-
.../solvers/StringRenderSuite.scala | 3 ++
4 files changed, 26 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 6e330c414..a08ab86d8 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 127c1004e..83129798a 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 9308c54d1..c7c998989 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 fe02ce2ef..e0a1632d2 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))
--
GitLab