From 8f0963fc921841632714156de92d59677b5da848 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 1 Sep 2015 13:16:19 +0200
Subject: [PATCH] This looks like dead code
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 10 ++--------
1 file changed, 2 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f745abec9..fef3dd376 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -517,10 +517,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
excludedPrograms += bvs
}
- def unfold(finalUnfolding: Boolean): Boolean = {
+ def unfold() = {
termSize += 1
updateCTree()
- true
}
/**
@@ -545,7 +544,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
for ((c, alts) <- cTree) {
val activeBs = alts.map(_._1).filter(isBActive)
- val ord = implicitly[Ordering[Identifier]]
val either = for (a1 <- activeBs; a2 <- activeBs if a1 < a2) yield {
Or(Not(a1.toVariable), Not(a2.toVariable))
}
@@ -738,11 +736,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
var skipCESearch = false
// Unfold formula
- val unfoldSuccess = ndProgram.unfold(unfolding == maxUnfoldings)
-
- if (!unfoldSuccess) {
- unfolding = maxUnfoldings
- }
+ ndProgram.unfold()
// Compute all programs that have not been excluded yet
var prunedPrograms: Set[Set[Identifier]] = ndProgram.allPrograms().toSet
--
GitLab