From ab7e0b6518621db1535c84a7ca101c9698ebea4f Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 1 Nov 2016 10:25:31 +0100
Subject: [PATCH] More optimizations in quantifier instantiation
---
.../unrolling/QuantificationTemplates.scala | 6 +++---
src/main/scala/inox/utils/IncrementalSet.scala | 17 +++++++++++------
2 files changed, 14 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index f0a0a7def..32016af41 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -457,11 +457,11 @@ trait QuantificationTemplates { self: Templates =>
}
private class MatcherSet extends BlockedSet[Matcher] {
- private val keys = new IncrementalSet[MatcherKey]
- def contains(m: Matcher): Boolean = keys(matcherKey(m))
+ private val keys = new IncrementalSet[(MatcherKey, Seq[Arg])]
+ def contains(m: Matcher): Boolean = keys(matcherKey(m) -> m.args)
override def +=(p: (Set[Encoded], Matcher)): Unit = {
- keys += matcherKey(p._2)
+ keys += matcherKey(p._2) -> p._2.args
super.+=(p)
}
diff --git a/src/main/scala/inox/utils/IncrementalSet.scala b/src/main/scala/inox/utils/IncrementalSet.scala
index ae329af5d..8bbdf40f2 100644
--- a/src/main/scala/inox/utils/IncrementalSet.scala
+++ b/src/main/scala/inox/utils/IncrementalSet.scala
@@ -13,11 +13,12 @@ class IncrementalSet[A] extends IncrementalState
with Builder[A, IncrementalSet[A]] {
private[this] val stack = new Stack[MSet[A]]()
- override def repr = stack.flatten.toSet
+ override def repr = stack.head.toSet
/** Removes all the elements */
override def clear(): Unit = {
stack.clear()
+ push()
}
/** Removes all the elements and creates a new set */
@@ -28,7 +29,11 @@ class IncrementalSet[A] extends IncrementalState
/** Creates one more set level */
def push(): Unit = {
- stack.push(MSet())
+ if (stack.isEmpty) {
+ stack.push(MSet())
+ } else {
+ stack.push(stack.head.clone)
+ }
}
/** Removes one set level */
@@ -37,16 +42,16 @@ class IncrementalSet[A] extends IncrementalState
}
/** Returns true if the set contains elem */
- def apply(elem: A) = repr.contains(elem)
+ def apply(elem: A) = stack.head.contains(elem)
/** Returns true if the set contains elem */
- def contains(elem: A) = repr.contains(elem)
+ def contains(elem: A) = stack.head.contains(elem)
/** Returns an iterator over all the elements */
- def iterator = stack.flatten.iterator
+ def iterator = stack.head.iterator
/** Add an element to the head set */
def += (elem: A) = { stack.head += elem; this }
/** Removes an element from all stacked sets */
- def -= (elem: A) = { stack.foreach(_ -= elem); this }
+ def -= (elem: A) = { stack.head -= elem; this }
override def newBuilder = new scala.collection.mutable.SetBuilder(Set.empty[A])
def result = this
--
GitLab