From ab0fb4f5006e161ec676e72e839dc8601bd9d7e0 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 25 Apr 2016 22:10:18 +0200
Subject: [PATCH] Moved termination regression back to fairz3
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
src/main/scala/leon/termination/StructuralSize.scala | 11 ++++++-----
.../regression/termination/TerminationSuite.scala | 2 +-
3 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9907f0394..1036643df 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -160,7 +160,7 @@ trait AbstractZ3Solver extends Solver {
val defs = for ((_, DataType(sym, cases)) <- adts) yield {(
sym.uniqueName,
cases.map(c => c.sym.uniqueName),
- cases.map(c => c.fields.map{ case(id, tpe) => (id.uniqueName, typeToSortRef(tpe))})
+ cases.map(c => c.fields.map { case(id, tpe) => (id.uniqueName, typeToSortRef(tpe))})
)}
val resultingZ3Info = z3.mkADTSorts(defs)
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index f7554e7aa..6d6bf6894 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -205,20 +205,21 @@ trait StructuralSize {
case ct: ClassType =>
val root = ct.root
val fd = outerCache.getOrElse(root.classDef.typed, {
- val id = FreshIdentifier("x", root.classDef.typed, true)
+ val tcd = root.classDef.typed
+ val id = FreshIdentifier("x", tcd, true)
val fd = new FunDef(FreshIdentifier("outerSize", alwaysShowUniqueID = true),
root.classDef.tparams,
Seq(ValDef(id)),
IntegerType)
- outerCache(root.classDef.typed) = fd
+ outerCache(tcd) = fd
- fd.body = Some(MatchExpr(Variable(id), root.knownCCDescendants map { cct =>
+ fd.body = Some(MatchExpr(Variable(id), tcd.knownCCDescendants map { cct =>
val args = cct.fields.map(_.id.freshen)
purescala.Extractors.SimpleCase(
CaseClassPattern(None, cct, args.map(id => WildcardPattern(Some(id)))),
args.foldLeft[Expr](InfiniteIntegerLiteral(1)) { case (e, id) =>
plus(e, id.getType match {
- case ct: ClassType if dependencies(root)(ct.root) => outerSize(Variable(id))
+ case ct: ClassType if dependencies(tcd)(ct.root) => outerSize(Variable(id))
case _ => InfiniteIntegerLiteral(0)
})
})
@@ -229,7 +230,7 @@ trait StructuralSize {
fd
})
- FunctionInvocation(fd.typed(ct.tps), Seq(e))
+ FunctionInvocation(fd.typed(root.tps), Seq(e))
case _ => InfiniteIntegerLiteral(0)
})
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 876ad77bd..5aa1d7891 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
for(f <- files) {
- mkTest(f, Seq("--solvers=smt-z3"), forError)(block)
+ mkTest(f, Seq(), forError)(block)
}
}
--
GitLab