From 205c01ae45b73677076ba847299ff1734a0e4124 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Mon, 19 Apr 2021 22:37:23 +0200 Subject: [PATCH] Reactor: optimize and cleanup ClassicTermTrie Also drop obsolete implementation of TermTrie. --- .../mps/logic/reactor/util/ClassicTermTrie.kt | 69 ++-- .../logic/reactor/util/PersistentTermTrie.kt | 322 ------------------ 2 files changed, 44 insertions(+), 347 deletions(-) delete mode 100644 reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/ClassicTermTrie.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/ClassicTermTrie.kt index db27e3b7..db01f500 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/util/ClassicTermTrie.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/util/ClassicTermTrie.kt @@ -27,6 +27,19 @@ import kotlin.collections.HashMap */ /** + * A map-like structure to keep multiple values associated with a single term. + * + * Term variables are supported: a variable matches any term, including other variable. All variables are treated + * as "wildcards", so the subsequent unification of the query term and the key does not necessarily succeeds. + * + * To access the stored values, the method `lookupValues` returns all values associated with terms. + * The method `allValues` returns all stored values. Neither method makes any guarantees about the cardinality or + * the order of the values returned. + * + * The implementation is based on the structure called "discrimination tree" as described in the chapter 26 of [1]. + * + * [1] Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. + * Elsevier Sci. Pub. B. V., Amsterdam, The Netherlands, The Netherlands. * An implementation of TermTrie not relying on persistent data structures. */ @@ -159,39 +172,43 @@ class ClassicTermTrie : TermTrie { */ private fun visitMatching(pattern: Term, visitor: (T) -> Unit) { val seenNonLeaf = IdentityHashMap() + val canonicTerms = IdentityHashMap>() val visitStack = arrayListOf, List>>(root to arrayListOf(pattern)) while (!visitStack.isEmpty()) { - val (node, terms) = visitStack.pop() - if (!terms.isEmpty()) { - val head = terms.first() - val tail = terms.subList(1, terms.size) + val (base, ptnTerms) = visitStack.pop() + if (!ptnTerms.isEmpty()) { + val ptnHead = ptnTerms.first() + val ptnTail = ptnTerms.subList(1, ptnTerms.size) - // dereferece the term only if it hasn't been dereferenced before - val term = deref(head).let { dt -> seenNonLeaf[dt]?.run { head } ?: dt } + if (!canonicTerms.containsKey(ptnHead)) { + // dereferece the term only if it hasn't been dereferenced before + val derefPtnHead = deref(ptnHead).let { dt -> seenNonLeaf[dt]?.run { ptnHead } ?: dt } + canonicTerms[ptnHead] = derefPtnHead to symbolOrWildcard(derefPtnHead) + } + val (term, sym) = canonicTerms[ptnHead] !! - val sym = symbolOrWildcard(term) if (sym == WILDCARD) { - if (!tail.isEmpty()) { + if (!ptnTail.isEmpty()) { // skip the current node // match the patterns tail with the current node's direct successors - val (allTerms, allEdge) = node.allTerms2edge() - allTerms.forEach { it.values().forEach (visitor) } - allEdge.forEach { visitStack.push(it to tail) } + val (terms, bases) = base.terms2bases() + terms.forEach { it.values().forEach (visitor) } + bases.forEach { visitStack.push(it to ptnTail) } } else { // wildcard consumes the rest of the trie - node.allNext().forEach { visitAll(it, visitor) } + base.allNext().forEach { visitAll(it, visitor) } } } else { - node.next(WILDCARD)?.let { nn -> + base.next(WILDCARD)?.let { nn -> nn.values().forEach(visitor) - if (!tail.isEmpty()) { - visitStack.push(nn to tail) + if (!ptnTail.isEmpty()) { + visitStack.push(nn to ptnTail) } } - node.next(sym)?.let { nn -> + base.next(sym)?.let { nn -> nn.values().forEach(visitor) // prepend this patternTerm's arguments to the tail pattern terms @@ -199,7 +216,7 @@ class ClassicTermTrie : TermTrie { if (newTail.size > 0) { seenNonLeaf[term] = term } - newTail.addAll(tail) + newTail.addAll(ptnTail) if (!newTail.isEmpty()) { visitStack.push(nn to newTail) } @@ -229,9 +246,11 @@ class ClassicTermTrie : TermTrie { fun allNext(): Iterable> = next.values /** + * Helper method for processing a wildcard in pattern. + * * Returns a pair of iterables: - * - first component contains all the nodes that make up the next *term*; - * - second component contains the nodes on the edge before the *term* after that one. + * - first component contains all nodes that make up the next *term*; + * - second component contains base nodes that precede terms following that *term*. * * The trie keeps the terms _flattened_, and the following proposition holds. * @@ -243,15 +262,15 @@ class ClassicTermTrie : TermTrie { * The size of a list representing a flattened term is equal to * the sum of arities of all symbols in this list plus 1. */ - fun allTerms2edge(): Pair>, Iterable>> { + fun terms2bases(): Pair>, Iterable>> { // for every current node there is a number // initially 0 // counting down with every call to allNext() // increased by current node's arity - val term = ArrayList>() - val edge = ArrayList>() + val terms = ArrayList>() + val bases = ArrayList>() val stack = arrayListOf, Int>>() for (n in allNext()) { @@ -262,15 +281,15 @@ class ClassicTermTrie : TermTrie { val (n, count) = stack.pop() val newCount = count + n.arity if (newCount == 0) { - edge.add(n) + bases.add(n) } else { - term.add(n) + terms.add(n) n.allNext().forEach { stack.push(it to (newCount - 1)) } } } - return term to edge + return terms to bases } fun putNext(node: PathNode): PathNode { diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt deleted file mode 100644 index fa1cd948..00000000 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/util/PersistentTermTrie.kt +++ /dev/null @@ -1,322 +0,0 @@ -/* - * Copyright 2014-2018 JetBrains s.r.o. - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package jetbrains.mps.logic.reactor.util - -import jetbrains.mps.unification.Term -import java.util.* -import kotlin.collections.ArrayList - -/** - * @author Fedor Isakov - */ - -/** - * A persistent map-like structure to keep multiple values associated with a single term. - * - * The method `put` returns a new instance updated to contain the new association. Likewise, the method - * `remove` returns the new instance updated to remove the association. - * - * Term variables are supported: a variable matches any term, including other variable. All variables are treated - * as "wildcards", so the subsequent unification of the query term and the key does not necessarily succeeds. - * - * To access the stored values, the method `lookupValues` returns all values associated with terms. - * The method `allValues` returns all stored values. Neither method makes any guarantees about the cardinality or - * the order of the values returned. - * - * The implementation is based on the structure called "discrimination tree" as described in the chapter 26 of [1]. - * - * [1] Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. - * Elsevier Sci. Pub. B. V., Amsterdam, The Netherlands, The Netherlands. - * - */ -class PersistentTermTrie() : TermTrie { - - private companion object { - - private val WILDCARD = object : Any() { - override fun toString() = "WILDCARD" - } - - } - - private var root: PathNode - - init { - root = PathNode(WILDCARD, 1) - } - - private constructor(setRoot: PathNode) : this() { - this.root = setRoot - } - - override fun put(term: Term, value: T): PersistentTermTrie = PersistentTermTrie(putValue(term, value)) - - override fun remove(term: Term, value: T): PersistentTermTrie = PersistentTermTrie(removeValue(term, value)) - - override fun lookupValues(term: Term): Iterable { - val result = ArrayList() - visitMatching(term) { value -> result.add(value) } - return result - } - - override fun allValues(): Iterable { - val result = ArrayList() - visitAll(root, { value -> result.add(value) }) - return result - } - - private fun putValue(matchTerm: Term, value: T): PathNode { - val seen = IdentityHashMap() - var nodeStack: PersList> = Lists.of(root) - val termList = arrayListOf(matchTerm) - - while (!termList.isEmpty()) { - val node = nodeStack.first() !! - val term = termList.removeAt(termList.size - 1) - - // dereferece the term only if it hasn't been dereferenced before - val deref = deref(term).let { dt -> seen[dt]?.run { term } ?: dt.apply { seen[dt] = term } } - val arguments = deref.arguments().toList() - for(i in 1..arguments.size) { - termList.add(arguments[arguments.size - i]) - } - - val nextNode = node.nextOrDefault(symbolOrWildcard(deref)) { sym -> PathNode(sym, arguments.size) } - nodeStack = nodeStack.prepend(nextNode) - } - - val head = nodeStack.first() !! - return nodeStack.tail().fold(head.addValue(value)) { nextNode, node -> node.putNext(nextNode) } - } - - private fun removeValue(matchTerm: Term, value: T): PathNode { - val seen = IdentityHashMap() - var nodeStack: PersList> = Lists.of(root) - val termStack = arrayListOf(matchTerm) - - while (!termStack.isEmpty()) { - val node = nodeStack.first() !! - val term = termStack.pop() - - // dereferece the term only if it hasn't been dereferenced before - val deref = deref(term).let { dt -> seen[dt]?.run { term } ?: dt.apply { seen[dt] = term } } - val arguments = deref.arguments().toList() - for(i in 1..arguments.size) { - termStack.push(arguments[arguments.size - i]) - } - - val nextNode = node.next(symbolOrWildcard(deref)) - if (nextNode == null) { - // term not found - return root - } - nodeStack = nodeStack.prepend(nextNode) - } - - val head = nodeStack.first() !! - val newHead = head.removeValue(value) - return if (head !== newHead) { - nodeStack.tail().fold(newHead) { nextNode, node -> node.putNext(nextNode) } - } else { - // value not found - root - } - } - - /** - * Given a pattern term, which may contain variables that are treated as wildcards, - * call the passed visitor function with values of all matching nodes and all the nodes that precede them. - */ - private fun visitMatching(pattern: Term, visitor: (T) -> Unit) { - val seen = IdentityHashMap() - val visitStack = arrayListOf(root to Lists.of(pattern)) - - while (!visitStack.isEmpty()) { - val (node, patternTerms) = visitStack.pop() - if (!patternTerms.isEmpty) { - val patternTermsHead = patternTerms.first() !! - val patternTermsTail = patternTerms.tail() - - // dereferece the term only if it hasn't been dereferenced before - val patternTerm = deref(patternTermsHead).let { dt -> - seen[dt]?.run { patternTermsHead } ?: dt.apply { seen[dt] = patternTermsHead } - } - - val sym = symbolOrWildcard(patternTerm) - if (sym == WILDCARD) { - if (!patternTermsTail.isEmpty) { - // skip the current node - // match the patterns tail with the current node's direct successors - val (allTerms, allEdge) = node.allTerms2edge() - allTerms.forEach { it.values.forEach(visitor) } - allEdge.forEach { n -> visitStack.push(n to patternTermsTail) } - - } else { - // wildcard consumes the rest of the trie - node.forEachNext { visitAll(it, visitor) } - } - - } else { - node.next(WILDCARD)?.let { nn -> - nn.values().forEach(visitor) - if (!patternTermsTail.isEmpty) { - visitStack.push(nn to patternTermsTail) - } - } - node.next(sym)?.let { nn -> - nn.values().forEach(visitor) - - var newTail = patternTermsTail - val arguments = patternTerm.arguments().toList() - // prepend patternTerm's arguments in reverse order - // this results in newTail being ordered normally - for(i in 1..arguments.size) { - newTail = newTail.prepend(arguments[arguments.size - i]) - } - - if (!newTail.isEmpty) { - visitStack.push(nn to newTail) - } - } - } - } - } - } - - /** - * Call the visitor function with values of the given node and all its direct and indirect successors. - */ - private fun visitAll(node: PathNode, visitor: (T) -> Unit) { - node.values().forEach(visitor) - node.forEachNext { visitAll(it, visitor) } - } - - private fun deref(term: Term): Term { - var deref = term - while (deref.`is`(Term.Kind.REF)) { - deref = deref.get() - } - return deref - } - - private fun symbolOrWildcard(term: Term): Any { - return if (term.`is`(Term.Kind.VAR)) { - WILDCARD - - } else { - term.symbol() - } - } - - /** - * A trie node. Corresponds to a particular subterm. - */ - private class PathNode(val symbol: Any, - val arity: Int, - val next: PersMap>, - val values: IdHashSet) - { - - constructor(symbol: Any, arity: Int) : - this(symbol, arity, Maps.of(), emptyIdSet()) - - constructor(copyFrom: PathNode, setValues: IdHashSet) : - this(copyFrom.symbol, copyFrom.arity, copyFrom.next, setValues) - - constructor(copyFrom: PathNode, setNext: PersMap>) : - this(copyFrom.symbol, copyFrom.arity, setNext, copyFrom.values) - - fun values(): Iterable = values - - fun next(symbol: Any): PathNode? = next[symbol] - - /** - * Returns all trie nodes that are direct successors of this one. - */ -// fun allNext(): Iterable> = next.values() - - inline fun forEachNext(code: (PathNode) -> Unit) { - val it = next.iterator() - while (it.hasNext()) { - code(it.next().getValue()) - } - } - - /** - * Returns a pair of iterables: - * - first component contains all the nodes that make up the next *term*; - * - second component contains the nodes on the edge before the *term* after that one. - * - * The trie keeps the terms _flattened_, and the following proposition holds. - * - * Let t = f(...) be a term. Let flt: Term->List be a function that transforms terms to lists of symbols. - * Let ar: Symbol->int be a function that returns arity for a given symbol. - * - * Then size(flt t) = 1 + sum . (map ar) (flt t), where '.' stands for function composition. - * - * The size of a list representing a flattened term is equal to - * the sum of arities of all symbols in this list plus 1. - */ - fun allTerms2edge(): Pair>, Iterable>> { - - // for every current node there is a number - // initially 0 - // counting down with every call to allNext() - // increased by current node's arity - - val term = ArrayList>() - val edge = ArrayList>() - - val stack = ArrayList, Int>>() - forEachNext { - stack.push(it to 0) - } - - while (stack.isNotEmpty()) { - val (n, count) = stack.pop() - val newCount = count + n.arity - if (newCount == 0) { - edge.add(n) - - } else { - term.add(n) - n.forEachNext { stack.push(it to (newCount - 1)) } - } - } - - return term to edge - } - - fun putNext(node: PathNode): PathNode = PathNode(this, next.assoc(node.symbol, node)) - - fun removeNext(node: PathNode): PathNode = PathNode(this, next.without(node.symbol)) - - fun addValue(value: T): PathNode = PathNode(this, values.add(value)) - - fun removeValue(value: T): PathNode = - if (values.contains(value)) PathNode(this, values.remove(value)) else this - - inline fun nextOrDefault(symbol: Any, - default: (sym: Any) -> PathNode): PathNode - { - return next[symbol] ?: default(symbol) - } - - } - - -} \ No newline at end of file