From aae7c8b165e4360f3b1de2a9da445c0b5f5b8828 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 23 Mar 2016 10:08:54 +0100
Subject: [PATCH] Better directed unrolling in the presence of quantifiers
---
.../solvers/unrolling/TemplateManager.scala | 1 +
.../solvers/unrolling/UnrollingBank.scala | 35 +++++++++++++------
.../solvers/unrolling/UnrollingSolver.scala | 2 +-
3 files changed, 27 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
index 36bad0b58..e55c46f2f 100644
--- a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
@@ -497,6 +497,7 @@ class TemplateManager[T](protected[unrolling] val encoder: TemplateEncoder[T]) e
def blocker(b: T): Unit = condImplies += (b -> Set.empty)
def isBlocker(b: T): Boolean = condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b)
def blockerParents(b: T): Set[T] = condImplied(b)
+ def blockerChildren(b: T): Set[T] = condImplies(b)
def implies(b1: T, b2: T): Unit = implies(b1, Set(b2))
def implies(b1: T, b2s: Set[T]): Unit = {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala b/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
index feb618827..7ba55bd37 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
@@ -196,7 +196,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
clauses
}
- def nextGeneration(gen: Int) = gen + 3
+ def nextGeneration(gen: Int) = gen + 5
def decreaseAllGenerations() = {
for ((block, (gen, origGen, ast, infos)) <- callInfos) {
@@ -209,19 +209,34 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
}
}
- def promoteBlocker(b: T) = {
- if (callInfos contains b) {
- val (_, origGen, notB, fis) = callInfos(b)
+ def promoteBlocker(b: T, force: Boolean = false): Boolean = {
+ var seen: Set[T] = Set.empty
+ var promoted: Boolean = false
- callInfos += b -> (1, origGen, notB, fis)
- }
+ def rec(b: T): Unit = if (!seen(b)) {
+ seen += b
+ if (callInfos contains b) {
+ val (_, origGen, notB, fis) = callInfos(b)
+
+ callInfos += b -> (1, origGen, notB, fis)
+ promoted = true
+ }
- if (blockerToApps contains b) {
- val app = blockerToApps(b)
- val (_, origGen, _, notB, infos) = appInfos(app)
+ if (blockerToApps contains b) {
+ val app = blockerToApps(b)
+ val (_, origGen, _, notB, infos) = appInfos(app)
- appInfos += app -> (1, origGen, b, notB, infos)
+ appInfos += app -> (1, origGen, b, notB, infos)
+ promoted = true
+ }
+
+ if (!promoted && force) {
+ for (cb <- templateGenerator.manager.blockerChildren(b)) rec(cb)
+ }
}
+
+ rec(b)
+ promoted
}
def instantiateQuantifiers(force: Boolean = false): Seq[T] = {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 99fdbd048..76f18864b 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -397,7 +397,7 @@ trait AbstractUnrollingSolver[T]
unrollingBank.decreaseAllGenerations()
for (b <- templateGenerator.manager.getBlockersToPromote(model.eval)) {
- unrollingBank.promoteBlocker(b)
+ unrollingBank.promoteBlocker(b, force = true)
}
}
}
--
GitLab