From c5e4324d979f71f2156127370f88d723918be2f4 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 1 Nov 2016 09:58:25 +0100
Subject: [PATCH] Fix quantification instantiation for same matcher keys
---
.../unrolling/QuantificationTemplates.scala | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 89d522e7f..f0a0a7def 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -457,7 +457,18 @@ trait QuantificationTemplates { self: Templates =>
}
private class MatcherSet extends BlockedSet[Matcher] {
- def contains(m: Matcher): Boolean = get(m).isDefined
+ private val keys = new IncrementalSet[MatcherKey]
+ def contains(m: Matcher): Boolean = keys(matcherKey(m))
+
+ override def +=(p: (Set[Encoded], Matcher)): Unit = {
+ keys += matcherKey(p._2)
+ super.+=(p)
+ }
+
+ override def push(): Unit = { keys.push(); super.push() }
+ override def pop(): Unit = { keys.pop(); super.pop() }
+ override def clear(): Unit = { keys.clear(); super.clear() }
+ override def reset(): Unit = { keys.reset(); super.reset() }
}
private def totalDepth(m: Matcher): Int = 1 + m.args.map {
@@ -565,8 +576,8 @@ trait QuantificationTemplates { self: Templates =>
}
}
- /* @nv: I tried some smarter cost computations here but it turns out that the
- * overhead needed to determine when to optimize exceeds the benefits */
+ /* @nv: I reused the cost heuristic from Leon here, it worked pretty well
+ * on all our pre-existing benchmarks and regressions. */
mappings ++= newMappings.map { case (bs, map, gens, c) =>
val substituter = mkSubstituter(map.mapValues(_.encoded))
val msubst = map.collect { case (q, Right(m)) => q -> m }
--
GitLab