From b7b371a2096cf6237fbec7c50abb7dd401da4e85 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 25 Feb 2016 18:02:38 +0100
Subject: [PATCH] Aesthetic fixes
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 4 +---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 2 --
src/main/scala/leon/synthesis/rules/EqualitySplit.scala | 6 +-----
3 files changed, 2 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7ae02d83e..7ad5c222b 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -17,8 +17,6 @@ import xlang.Expressions._
import purescala.ExprOps._
import purescala.Types._
-import scala.collection.mutable.{Map => MutableMap}
-
case class UnsoundExtractionException(ast: Z3AST, msg: String)
extends Exception("Can't extract " + ast + " : " + msg)
@@ -705,7 +703,7 @@ trait AbstractZ3Solver extends Solver {
val elems = r.elems.flatMap {
case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
case (k, _) => None
- }.toMap
+ }
FiniteMap(elems, from, to)
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 0c9adeb86..128d7299d 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -570,8 +570,6 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
// are minimal we make sure we exclude only Bs that are used.
def excludeProgram(bs: Set[Identifier], isMinimal: Boolean): Unit = {
-
-
def filterBTree(c: Identifier): Set[Identifier] = {
val (b, _, subcs) = cTree(c).find(sub => bs(sub._1)).get
subcs.flatMap(filterBTree).toSet + b
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 50a38abc6..afabdad92 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -4,15 +4,11 @@ package leon
package synthesis
package rules
-import leon.purescala.Common.Identifier
+import purescala.Common.Identifier
import purescala.Expressions._
import purescala.Extractors._
import purescala.Constructors._
-import solvers._
-
-import scala.concurrent.duration._
-
/** For every pair of input variables of the same type,
* checks equality and output an If-Then-Else statement with the two new branches. */
case object EqualitySplit extends Rule("Eq. Split") {
--
GitLab